I'm writing (for myself) an explanation of how to do well-founded recursion in Coq. (see i.e. the Coq'Art book, chapter 15.2). First I made an example function based on nat and that worked fine, but then I did it again for Z, and when I use Compute to evaluate it, it doesn't reduce all the way down to a Z value. Why?
Here is my example (I put the text inside comments so one can copy-paste the whole thing into your editor):
(* Test of well-founded recursion *)
(* TL;DR: To do well-founded recursion, first create 'functional' and then create the recursive function using Acc_iter, the iterator for accessible relations *)
(* As an example, compute the sum of the series from 1 to n, something like this sketch:
fix f n := (if n = 0 then 0 else n + f (n-1))
Now, let's not use structural recursion on n.
Instead, we use well-founded recursion on n, using that the relation less-than ('lt') is wellfounded. The function f terminates because the recursive call is made on a structurally smaller term (in the decreasing Acc-chain). *)
(* First we do it for nat *)
Require Import Arith.Arith.
Require Import Program.Utils. (* for 'dec' *)
Require Import Wellfounded.
(* From a proof that a relation is wellfounded, we can get a proof that a particular element in its domain is accessible.
The Check commands here are not necessary, just for documentation, dear reader. *)
Check well_founded : forall A : Type, (A -> A -> Prop) -> Prop.
Check lt_wf : well_founded lt.
Check (lt_wf 4711 : Acc lt 4711).
(* First define a 'functional' F for f. It is a function that takes a function F_rec for the 'recursive call' as an argument. Because we need to know n <> 0 in the second branch we use 'dec' to turn the boolean if-condition into a sumbool. This we get info about it into the branches.
We write most of it with refine, and leave some holes to be filled in with tactics later. *)
Definition F (n:nat) (F_rec : (forall y : nat, y < n -> nat)): nat.
refine ( if dec (n =? 0) then 0 else n + (F_rec (n-1) _ ) ).
(* now we need to show that n-1 < n, which is true for nat if n<>0 *)
destruct n; now auto with *.
Defined.
(* The functional can be used by an iterator to call f as many times as is needed.
Side note: One can either make an iterator that takes the maximal recursive depth d as a nat argument, and recurses on d, but then one has to provide d, and also a 'default value' to return in case d reaches zero and one must terminate early.
The neat thing with well-founded recursion is that the iterator can recurse on the proof of wellfoundedness and doesnt need any other structure or default value to guarantee it will terminate. *)
(* The type of Acc_iter is pretty hairy *)
Check Acc_iter :
forall (A : Type) (R : A -> A -> Prop) (P : A -> Type),
(forall x : A, (forall y : A, R y x -> P y) -> P x) -> forall x : A, Acc R x -> P x.
(* P is there because the return type could be dependent on the argument,
but in our case, f:nat->nat, and R = lt, so we have
*)
Check Acc_iter (R:=lt) (fun _:nat=>nat) :
(forall n : nat, (forall y : nat, y < n -> nat) -> nat) ->
forall n : nat, Acc lt n -> nat.
(* Here the first argument is the functional that the iterator takes, the second argument n is the input to f, and the third argument is a proof that n is accessible. The iterator returns the value of f applied to n.
Several of Acc_iter's arguments are implicit, and some can be inferred. Thus we can define f simply as follows: *)
Definition f n := Acc_iter _ F (lt_wf n).
(* It works like a charm *)
Compute (f 50). (* This prints 1275 *)
Check eq_refl : f 50 = 1275.
(* Now let's do it for Z. Here we can't use lt, or lt_wf because they are for nat. For Z we can use Zle and (Zwf c) which takes a lower bound. It needs a lower bound under which we know that the function will always terminate to guarantee termination. Here we use (Zwf 0) to say that our function will always terminate at or below 0. We also have to change the if-statement to 'if n <= 0 then 0 else ...' so we return zero for arguments less than zero. *)
Require Import ZArith.
Require Import Zwf.
Open Scope Z.
(* Now we define the function g based on the functional G *)
Definition G (n:Z) (G_rec : (forall y : Z, Zwf 0 y n -> Z)) : Z.
refine (if dec (n<?0) then 0 else n + (G_rec (n-1) _ )).
(* now we need to show that n-1 < n *)
now split; [ apply Z.ltb_ge | apply Z.lt_sub_pos].
Defined.
Definition g n := Acc_iter _ G (Zwf_well_founded 0 n).
(* But now we can't compute! *)
Compute (g 1).
(* We just get a huge term starting with
= (fix
Ffix (x : Z)
(x0 : Acc
(fun x0 x1 : Z =>
(match x1 with
| 0 => Eq
| Z.pos _ => Lt
| Z.neg _ => Gt
end = Gt -> False) /\
match x0 with
| 0 => match x1 with
| 0 => Eq
| Z.pos _ => Lt
| Z.neg _ => Gt
end
| Z.pos x2 =>
...
end) 1 (Zwf_well_founded 0 1)
: (fun _ : Z => Z) 1
)
Comment: I noticed that Zwf_well_founded is defined as Opaque in the library, so I tried to make it Transparent by copying the proof and ending the lemma with Defined. instead of Qed. but that didn't help...
Added observation:
If I define f' for nat with Fixpoint instead, and recurse on the
accesibility proof, and end with Defined. then it computes. But if I end with Qed. it doesn't reduce. Is this related? I guess there is an issue of transparency in the definition of G or g somewhere... Or am I completely mistaken?
Fixpoint f' (n:nat) (H: Acc lt n) : nat.
refine (if dec (n<=?0) then 0 else n + (f' (n-1) (Acc_inv H _))).
apply Nat.leb_gt in e.
apply Nat.sub_lt; auto with *.
Defined. (* Compute (f' 10 (lt_wf 10)). doesn't evaluate to a nat if ended with Qed. *)
Anyway, my problem persists for Z.
Fixpoint g' (n:Z) (H: Acc (Zwf 0) n) : Z.
refine (if dec (n<=?0) then 0 else n + (g' (n-1) (Acc_inv H _))).
split; now apply Z.leb_gt in e; auto with *.
Defined.
Compute (g' 10 (Zwf_well_founded 0 10)).
