Compute with a recursive function defined by well-defined induction

Link:: https://stackoverflow.com/q/32354286

Display all goals and responses

Question

When I use Function to define a non-structurally recursive function in Coq, the resulting object behaves strangely when a specific computation is asked. Indeed, instead of giving directly the result, the Eval compute in ... directive return a rather long (typically 170 000 lines) expression. It seems that Coq cannot evaluate everything, and therefore returns a simplified (but long) expression instead of just a value.

The problem seems to come from the way I prove the obligations generated by Function. First, I thought the problem came from the opaque terms I used, and I converted all the lemmas to transparent constants. By the way, is there a way to list the opaque terms appearing in a term? Or any other way to turn opaque lemmas into transparent ones?

I then remarked that the problem came more precisely from the proof that the order used is well-founded. But I got strange results.

For example, I define log2 on the natural numbers by repeatedly applying div2. Here is the definition:

Function log2 n {wf lt n} :=
  match n with
  | 0 => 0
  | 1 => 0
  | n => S (log2 (Nat.div2 n))
  end.forall n n0 n1 : nat,
n0 = S n1 ->
n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1)
well_founded lt

I get two proof obligations. The first one checks that n respects the relation lt in the recursive calls and can be proved easily.

-forall n n0 n1 : nat,
n0 = S n1 ->
n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1) 1 subgoal

  ============================
  forall n n0 n1 : nat,
  n0 = S n1 ->
  n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1)  intros.n, n0, n1: nat
teq0: n0 = S n1
teq: n = S (S n1)
Nat.div2 (S (S n1)) < S (S n1) apply Nat.lt_div2, le_n_S, le_0_n.

The second one checks that lt is a well-founded order. This is already proved in the standard library. The corresponding lemma is Coq.Arith.Wf_nat.lt_wf.

-well_founded lt apply Wf_nat.lt_wf.
Defined.

If I use this proof, the resulting function behaves normally.

Eval compute in log2 10.= 3
: nat

But if I want to do the proof myself, I do not always get this behaviour. First, if I end the proof with Qed instead of Defined, the result of the computation (even on small numbers) is a complex expression and not a single number. So I use Defined and try to use only transparent lemmas.

Lemma lt_wf2 : well_founded lt.well_founded lt
Proof.well_founded lt
  unfold well_founded.forall a : nat, Acc lt a intros n.n: nat
Acc lt n
  apply (lemma1 n).n: nat
forall n : nat,
(forall p : nat, p < n -> Acc lt p) -> Acc lt n clear n.forall n : nat,
(forall p : nat, p < n -> Acc lt p) -> Acc lt n
  intros.n: nat
H: forall p : nat, p < n -> Acc lt p
Acc lt n constructor.n: nat
H: forall p : nat, p < n -> Acc lt p
forall y : nat, y < n -> Acc lt y apply H.
Defined.

Here, lemma1 is a proof of the well-founded induction on the natural numbers. Here again, I can use already existing lemmas, such as lt_wf_ind, lt_wf_rec, lt_wf_rec1 located in Coq.Arith.Wf_nat, or even well_founded_ind lt_wf. The first one does not work, it seems this is because it is opaque. The three others work.

I tried to prove it directly using the standard induction on the natural numbers, nat_ind. This gives:

Lemma lemma1 : forall n (P : nat -> Prop),
    (forall n, (forall p, p < n -> P p) -> P n) -> P n.forall (n : nat) (P : nat -> Prop),
(forall n0 : nat,
 (forall p : nat, p < n0 -> P p) -> P n0) -> P n
Proof.forall (n : nat) (P : nat -> Prop),
(forall n0 : nat,
 (forall p : nat, p < n0 -> P p) -> P n0) -> P n
  intros n P H.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
P n pose proof (nat_ind (fun n => forall p, p < n -> P p)).n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (fun n : nat => forall p : nat, p < n -> P p) 0 ->
(forall n : nat,
 (fun n0 : nat => forall p : nat, p < n0 -> P p)
   n ->
 (fun n0 : nat => forall p : nat, p < n0 -> P p)
   (S n)) ->
forall n : nat,
(fun n0 : nat => forall p : nat, p < n0 -> P p) n
P n
  simpl in H0.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
P n apply H0 with (n:=S n).n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
forall p : nat, p < 0 -> P p
n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
forall n : nat,
(forall p : nat, p < n -> P p) ->
forall p : nat, p < S n -> P p
n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n < S n
  -n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
forall p : nat, p < 0 -> P p intros.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
p: nat
H1: p < 0
P p inversion H1.
  -n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
forall n : nat,
(forall p : nat, p < n -> P p) ->
forall p : nat, p < S n -> P p intros.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < S n0
P p inversion H2.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < S n0
H4: p = n0
P n0
n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < S n0
m: nat
H4: S p <= n0
H3: m = n0
P p
    +n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < S n0
H4: p = n0
P n0 apply H.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < S n0
H4: p = n0
forall p : nat, p < n0 -> P p exact H1.
    +n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < S n0
m: nat
H4: S p <= n0
H3: m = n0
P p apply H1.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < S n0
m: nat
H4: S p <= n0
H3: m = n0
p < n0 assumption.
  -n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n < S n apply le_n.
Defined.

With this proof (and some variants of it), log2 has the same strange behaviour. And this proof seems to use only transparent objects, so maybe the problem is not there.

How can I define a Function that returns understandable results on specific values?

A: Print Opaque Dependencies log2 can be used to list the opaque terms used in log2.

Answer (Anton Trunov)

I've managed to pin-point the place that causes troubles: it's inversion H2. in lemma1. It turns out we don't need that case-analysis and intuition can finish the proof (it doesn't pattern-match on H2):

Lemma lemma1 : forall n (P : nat -> Prop),
    (forall n, (forall p, p < n -> P p) -> P n) -> P n.forall (n : nat) (P : nat -> Prop),
(forall n0 : nat,
 (forall p : nat, p < n0 -> P p) -> P n0) -> P n
Proof.forall (n : nat) (P : nat -> Prop),
(forall n0 : nat,
 (forall p : nat, p < n0 -> P p) -> P n0) -> P n
  intros n P H.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
P n pose proof (nat_ind (fun n => forall p, p < n -> P p)).n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (fun n : nat => forall p : nat, p < n -> P p) 0 ->
(forall n : nat,
 (fun n0 : nat => forall p : nat, p < n0 -> P p)
   n ->
 (fun n0 : nat => forall p : nat, p < n0 -> P p)
   (S n)) ->
forall n : nat,
(fun n0 : nat => forall p : nat, p < n0 -> P p) n
P n
  simpl in H0.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
P n apply H0 with (n:=S n).n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
forall p : nat, p < 0 -> P p
n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
forall n : nat,
(forall p : nat, p < n -> P p) ->
forall p : nat, p < S n -> P p
n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n < S n
  -n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
forall p : nat, p < 0 -> P p intros.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
p: nat
H1: p < 0
P p inversion H1.
  -n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
forall n : nat,
(forall p : nat, p < n -> P p) ->
forall p : nat, p < S n -> P p intros.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < S n0
P p apply Lt.lt_n_Sm_le, Nat.lt_eq_cases in H2.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < n0 \/ p = n0
P p destruct H2.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < n0
P p
n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p = n0
P p
    +n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p < n0
P p now apply H1.
    +n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
p: nat
H2: p = n0
P p subst p.n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n0: nat
H1: forall p : nat, p < n0 -> P p
P n0 now apply H.
  -n: nat
P: nat -> Prop
H: forall n : nat,
(forall p : nat, p < n -> P p) -> P n
H0: (forall p : nat, p < 0 -> P p) ->
(forall n : nat,
 (forall p : nat, p < n -> P p) ->
 forall p : nat, p < S n -> P p) ->
forall n p : nat, p < n -> P p
n < S n apply le_n.
Defined.

If we use lemma1 with this proof, the computation of log2 10 results in 3.

By the way, here is my version of lt_wf2 (it lets us compute as well):

Lemma lt_wf2 : well_founded lt.well_founded lt
Proof.well_founded lt
  unfold well_founded.forall a : nat, Acc lt a intros n.n: nat
Acc lt n
  induction n; constructor; intros k Hk.k: nat
Hk: k < 0
Acc lt k
n: nat
IHn: Acc lt n
k: nat
Hk: k < S n
Acc lt k
  -k: nat
Hk: k < 0
Acc lt k inversion Hk.
  -n: nat
IHn: Acc lt n
k: nat
Hk: k < S n
Acc lt k constructor.n: nat
IHn: Acc lt n
k: nat
Hk: k < S n
forall y : nat, y < k -> Acc lt y intros m Hm.n: nat
IHn: Acc lt n
k: nat
Hk: k < S n
m: nat
Hm: m < k
Acc lt m
    apply IHn.n: nat
IHn: Acc lt n
k: nat
Hk: k < S n
m: nat
Hm: m < k
m < n lia.
    (* OR: apply IHn, Nat.lt_le_trans with (m := k); auto with arith. *)
Defined.

I believe the Using Coq's evaluation mechanisms in anger blog post by Xavier Leroy explains this kind of behavior.

it eliminates the proof of equality between the heads before recursing over the tails and finally deciding whether to produce a left or a right. This makes the left/right data part of the final result dependent on a proof term, which in general does not reduce!

In our case we eliminate the proof of inequality (inversion H2.) in the proof of lemma1 and the Function mechanism makes our computations depend on a proof term. Hence, the evaluator can't proceed when n > 1.

And the reason inversion H1. in the body of the lemma doesn't influence computations is that for n = 0 and n = 1, log2 n is defined within the match expression as base cases.

To illustrate this point, let me show an example when we can prevent evaluation of log2 n on any values n and n + 1 of our choice, where n > 1 and nowhere else!

Lemma lt_wf2' : well_founded lt.well_founded lt
Proof.well_founded lt
  unfold well_founded.forall a : nat, Acc lt a intros n.n: nat
Acc lt n
  induction n; constructor; intros k Hk.k: nat
Hk: k < 0
Acc lt k
n: nat
IHn: Acc lt n
k: nat
Hk: k < S n
Acc lt k
  -k: nat
Hk: k < 0
Acc lt k inversion Hk.          (* n = 0 *)
  -n: nat
IHn: Acc lt n
k: nat
Hk: k < S n
Acc lt k destruct n.IHn: Acc lt 0
k: nat
Hk: k < 1
Acc lt k
n: nat
IHn: Acc lt (S n)
k: nat
Hk: k < S (S n)
Acc lt k intuition. (* n = 1 *)n: nat
IHn: Acc lt (S n)
k: nat
Hk: k < S (S n)
Acc lt k
    destruct n.IHn: Acc lt 1
k: nat
Hk: k < 2
Acc lt k
n: nat
IHn: Acc lt (S (S n))
k: nat
Hk: k < S (S (S n))
Acc lt k intuition. (* n = 2 *)n: nat
IHn: Acc lt (S (S n))
k: nat
Hk: k < S (S (S n))
Acc lt k
    destruct n.IHn: Acc lt 2
k: nat
Hk: k < 3
Acc lt k
n: nat
IHn: Acc lt (S (S (S n)))
k: nat
Hk: k < S (S (S (S n)))
Acc lt k intuition. (* n = 3 *)n: nat
IHn: Acc lt (S (S (S n)))
k: nat
Hk: k < S (S (S (S n)))
Acc lt k
    destruct n.IHn: Acc lt 3
k: nat
Hk: k < 4
Acc lt k
n: nat
IHn: Acc lt (S (S (S (S n))))
k: nat
Hk: k < S (S (S (S (S n))))
Acc lt k inversion Hk; intuition. (* n = 4 and n = 5 - won't evaluate *)n: nat
IHn: Acc lt (S (S (S (S n))))
k: nat
Hk: k < S (S (S (S (S n))))
Acc lt k
    (* n > 5 *)
    constructor; intros m Hm; apply IHn; lia.
Defined.

If you use this modified lemma in the definition of log2 you'll see that it computes everywhere except n = 4 and n = 5. Well, almost everywhere -- computations with large nats can result in stack overflow or segmentation fault, as Coq warns us:

Warning: Stack overflow or segmentation fault happens when working with large numbers in nat (observed threshold may vary from 5000 to 70000 depending on your system limits and on the command executed).

And to make log2 work for n = 4 and n = 5 even for the above "flawed" proof, we could amend log2 like this

Function log2 n {wf lt n} :=
  match n with
  | 0 => 0
  | 1 => 0
  | 4 => 2
  | 5 => 2
  | n => S (log2 (Nat.div2 n))
  end.forall n n0 n1 : nat,
n1 = 0 -> n0 = 1 -> n = 2 -> Nat.div2 2 < 2
forall n n0 n1 n2 : nat,
n2 = 0 -> n1 = 1 -> n0 = 2 -> n = 3 -> Nat.div2 3 < 3
forall n n0 n1 n2 n3 n4 n5 : nat,
n4 = S n5 ->
n3 = S (S n5) ->
n2 = S (S (S n5)) ->
n1 = S (S (S (S n5))) ->
n0 = S (S (S (S (S n5)))) ->
n = S (S (S (S (S (S n5))))) ->
Nat.div2 (S (S (S (S (S (S n5)))))) <
S (S (S (S (S (S n5)))))
well_founded lt

adding the necessary proofs at the end.

The "well-founded" proof must be transparent and can't rely on pattern-matching on proof objects because the Function mechanism actually uses the lt_wf lemma to compute the decreasing termination guard. If we look at the term produced by Eval (in a case where evaluation fails to produce a nat), we'll see something along these lines:

fix Ffix (x : nat) (x0 : Acc (fun x0 x1 : nat => S x0 <= x1) x) {struct x0}

It's easy to see that x0 : Prop, so it gets erased when extracting the functional program log2 into, say OCaml, but Coq's internal evaluation mechanism have to use it to ensure termination.

Q: Is this behaviour due to the way Function is implemented or will it be present in every implementation?

A: I think it's a major design decision for Function to make extraction eligible. Basically, Function adds one dummy argument and turns (under the hood) your unary function into a binary one. But this dummy argument doesn't necessarily have to live in Prop. Here is an example how we could've achieved almost the same thing with Fixpoint, except for the fact that the extracted function does some excessive amount of work. Sorry, if I headed the wrong way -- it's a bit unclear to me what you meant.

A: Notice that not all opaque terms prevent evaluation. I've made an explicit version of what Function does (I've tried to preserve the spirit, not to provide the real implementation). The opaque terms created with Nat.lt_div2 and Nat.lt_0_succ do not prevent evaluation. If our usage of opaque terms prevents evaluation to the weak head normal form for the termination guard, then we'll get stuck. And that would happen if we destructed some proof term like (y < n).

Answer (Arthur Azevedo De Amorim)

The reduction behavior of functions defined by well-founded recursion in Coq is generally not very good, even when you declare your proofs to be transparent. The reason for this is that arguments of well-foundedness usually need to be done with complicated proof terms. Since these proofs terms end up appearing in well-founded recursive definitions, "simplifying" your function will make all of those proof terms appear, as you noticed.

It is easier to rely on custom tactics and lemmas to reduce functions defined this way. First, I would recommend favoring Program Fixpoint over Function, because the latter is much older and (I think) less well maintained. Thus, you would end up with a definition like this:

Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Coq.Program.Wf.
Require Import Coq.Program.Tactics.

Program Fixpoint log2 n {wf lt n} :=
  match n with
  | 0 => 0
  | 1 => 0
  | n => S (log2 (Nat.div2 n))
  end.

Next Obligation.n0: nat
log2: forall n : nat, n < n0 -> nat
H0: 0 <> n0
H: 1 <> n0
Nat.div2 n0 < n0
Admitted.

Now, you just need to use the program_simpl tactic to simplify calls to log2. Here's an example:

Lemma foo : log2 4 = 2.Nat.log2 4 = 2
Proof.Nat.log2 4 = 2
  program_simpl.
Qed.

Q: Ok, this is an alternative. But I would have liked to understand what is going on with this Function stuff. Moreover, I do not know how to reason with Program Fixpoint. How can I get the functional recursion and equation lemmas that I can get with Function using Functional Scheme?

A: I think it should be possible to prove them directly using well-founded induction and the program_simpl tactic.

Q: I managed to prove both log25_equation and log25_ind using fix_sub_eq and Fix_sub_rect respectively (in Coq.Program.Wf). I do not know if it is the best solution. And one error in my previous comment: Function automatically generates the equation and functional induction lemmas. Functional Scheme is useful for classic Fixpoint.