Coq can't compute a well-founded function on Z, but it works on nat
Question
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. *)well_founded : forall A : Type, (A -> A -> Prop) -> Prop : forall A : Type, (A -> A -> Prop) -> Proplt_wf : well_founded lt : well_founded lt(* 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. *)lt_wf 4711 : Acc lt 4711 : Acc lt 4711n: nat
F_rec: forall y : nat, y < n -> natnat(* 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 *)n: nat
F_rec: forall y : nat, y < n -> nat
e: (n =? 0) = falsen - 1 < n(* 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 *)Fix_F : 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 : 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(* 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 *)Fix_F (fun _ : nat => nat) : (forall n : nat, (forall y : nat, y < n -> nat) -> nat) -> forall n : nat, Acc lt n -> nat : (forall n : nat, (forall y : nat, y < n -> nat) -> nat) -> forall n : nat, Acc lt n -> nat= 1275 : (fun _ : nat => nat) 50(* 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 *)eq_refl : f 50 = 1275 : f 50 = 1275n: Z
G_rec: forall y : Z, Zwf 0 y n -> ZZ(* 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! *)n: Z
G_rec: forall y : Z, Zwf 0 y n -> Z
e: (n <? 0) = falseZwf 0 (n - 1) n(* We just get a huge a term *)= (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 => match x1 with | Z.pos x3 => (fix Ffix0 (x4 : comparison) (x5 x6 : positive) {struct x6} : comparison := match x5 with | (x7~1)%positive => match x6 with | (x8~1)%positive => Ffix0 x4 x7 x8 | (x8~0)%positive => Ffix0 Gt x7 x8 | 1%positive => Gt end | (x7~0)%positive => match x6 with | (x8~1)%positive => Ffix0 Lt x7 x8 | (x8~0)%positive => Ffix0 x4 x7 x8 | 1%positive => Gt end | 1%positive => match x6 with | 1%positive => x4 | _ => Lt end end) Eq x2 x3 | _ => Gt end | Z.neg x2 => match x1 with | Z.neg x3 => match (fix Ffix0 (x4 : comparison) (x5 x6 : positive) {struct x6} : comparison := match x5 with | (x7~1)%positive => match ... with | ... => Ffix0 x4 x7 x8 | ... => Ffix0 Gt x7 x8 | ... => Gt end | (x7~0)%positive => match ... with | ... => Ffix0 Lt x7 x8 | ... => Ffix0 x4 x7 x8 | ... => Gt end | 1%positive => match ... with | ... => x4 | ... => Lt end end) Eq x2 x3 with | Eq => Eq | Lt => Gt | Gt => Lt end | _ => Lt end end = Lt) x) {struct x0} : Z := match (if match match x with | 0 => Eq | Z.pos _ => Gt | Z.neg _ => Lt end with | Lt => true | _ => false end as c return ({c = true} + {c = false}) then in_left else in_right) with | in_left => 0 | right x1 => match x with | 0 => Ffix match x with | 0 => -1 | Z.pos x3~1 => Z.pos x3~0 | Z.pos x3~0 => Z.pos ((fix Ffix0 (x4 : positive) : positive := match x4 with | (x5~1)%positive => (x5~0~1)%positive | (x5~0)%positive => ((Ffix0 x5)~1)%positive | 1%positive => 1%positive end) x3) | 1 => 0 | Z.neg x2 => Z.neg ((with Ffix0 (x3 x4 : positive) {struct x3} : positive := match x3 with | (x5~1)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~0)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~1)%positive | 1%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~0)%positive end | (x5~0)%positive => match x4 with | (x6~1)%positive => ((Ffix0 x5 x6)~1)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~0)%positive | 1%positive => (x5~1)%positive end | 1%positive => match x4 with | (x5~1)%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~0)%positive | (x5~0)%positive => (x5~1)%positive | 1%positive => 2%positive end end with Ffix1 (x3 x4 : positive) {struct x3} : positive := match x3 with | (x5~1)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~1)%positive | (x6~0)%positive => ((Ffix1 x5 x6)~0)%positive | 1%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~1)%positive end | (x5~0)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~0)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~1)%positive | 1%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~0)%positive end | 1%positive => match x4 with | (x5~1)%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~1)%positive | (x5~0)%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~0)%positive | 1%positive => 3%positive end end for Ffix0) x2 1%positive) end (match x0 with | Acc_intro _ x2 => x2 end match x with | 0 => -1 | Z.pos x3~1 => Z.pos x3~0 | Z.pos x3~0 => Z.pos ((fix Ffix0 (x4 : positive) : positive := match x4 with | (x5~1)%positive => (x5~0~1)%positive | (x5~0)%positive => ((Ffix0 x5)~1)%positive | 1%positive => 1%positive end) x3) | 1 => 0 | Z.neg x2 => Z.neg ((with Ffix0 (x3 x4 : positive) {struct x3} : positive := match x3 with | (x5~1)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~0)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~1)%positive | 1%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~0)%positive end | (x5~0)%positive => match x4 with | (x6~1)%positive => ((Ffix0 x5 x6)~1)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~0)%positive | 1%positive => (x5~1)%positive end | 1%positive => match x4 with | (x5~1)%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~0)%positive | (x5~0)%positive => (x5~1)%positive | 1%positive => 2%positive end end with Ffix1 (x3 x4 : positive) {struct x3} : positive := match x3 with | (x5~1)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~1)%positive | (x6~0)%positive => ((Ffix1 x5 x6)~0)%positive | 1%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~1)%positive end | (x5~0)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~0)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~1)%positive | 1%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~0)%positive end | 1%positive => match x4 with | (x5~1)%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~1)%positive | (x5~0)%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~0)%positive | 1%positive => 3%positive end end for Ffix0) x2 1%positive) end (conj (match Z.ltb_ge x 0 with | conj x2 _ => x2 end x1) (match Z.lt_sub_pos x 1 with | conj x2 _ => x2 end eq_refl))) | Z.pos x2 => match Ffix match x with | 0 => -1 | Z.pos x4~1 => Z.pos x4~0 | Z.pos x4~0 => Z.pos ((fix Ffix0 (x5 : positive) : positive := match x5 with | (x6~1)%positive => (x6~0~1)%positive | (x6~0)%positive => ((Ffix0 x6)~1)%positive | 1%positive => 1%positive end) x4) | 1 => 0 | Z.neg x3 => Z.neg ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((...) x6)~0)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix0 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((...) x6)~0)%positive | (x6~0)%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix1 x6 x7)~0)%positive | 1%positive => (((...) x6)~1)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((...) x6)~0)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((...) x6)~1)%positive | (x6~0)%positive => (((...) x6)~0)%positive | 1%positive => 3%positive end end for Ffix0) x3 1%positive) end (match x0 with | Acc_intro _ x3 => x3 end match x with | 0 => -1 | Z.pos x4~1 => Z.pos x4~0 | Z.pos x4~0 => Z.pos ((fix Ffix0 (x5 : positive) : positive := match x5 with | (x6~1)%positive => (x6~0~1)%positive | (x6~0)%positive => ((Ffix0 x6)~1)%positive | 1%positive => 1%positive end) x4) | 1 => 0 | Z.neg x3 => Z.neg ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => ((...)~1)%positive | 1%positive => ((...)~0)%positive end | (x6~0)%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => ((...)~1)%positive end | (x6~0)%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => ((...)~1)%positive | 1%positive => ((...)~0)%positive end | 1%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => 3%positive end end for Ffix0) x3 1%positive) end (conj (match Z.ltb_ge x 0 with | conj x3 _ => x3 end x1) (match Z.lt_sub_pos x 1 with | conj x3 _ => x3 end eq_refl))) with | 0 => x | Z.pos x3 => Z.pos ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix0 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive | (x6~0)%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix1 x6 x7)~0)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~1)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~1)%positive | (x6~0)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive | 1%positive => 3%positive end end for Ffix0) x2 x3) | Z.neg x3 => (fix Ffix0 (x4 x5 : positive) {struct x5} : Z := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => match Ffix0 x6 x7 with | 0 => 0 | Z.pos x8 => Z.pos x8~0 | Z.neg x8 => Z.neg x8~0 end | (x7~0)%positive => match Ffix0 x6 x7 with | 0 => 1 | Z.pos x8 => Z.pos x8~1 | Z.neg x8 => Z.neg ((fix Ffix1 (x9 : positive) : positive := match x9 with | ...%positive => (x10~0~1)%positive | ...%positive => ((...)~1)%positive | 1%positive => 1%positive end) x8) end | 1%positive => Z.pos x6~0 end | (x6~0)%positive => match x5 with | (x7~1)%positive => match Ffix0 x6 x7 with | 0 => -1 | Z.pos x8 => Z.pos ((fix Ffix1 (x9 : positive) : positive := match x9 with | ...%positive => (x10~0~1)%positive | ...%positive => ((...)~1)%positive | 1%positive => 1%positive end) x8) | Z.neg x8 => Z.neg x8~1 end | (x7~0)%positive => match Ffix0 x6 x7 with | 0 => 0 | Z.pos x8 => Z.pos x8~0 | Z.neg x8 => Z.neg x8~0 end | 1%positive => Z.pos ((fix Ffix1 (x7 : positive) : positive := match x7 with | (x8~1)%positive => (x8~0~1)%positive | (x8~0)%positive => ((Ffix1 x8)~1)%positive | 1%positive => 1%positive end) x6) end | 1%positive => match x5 with | (x6~1)%positive => Z.neg x6~0 | (x6~0)%positive => Z.neg ((fix Ffix1 (x7 : positive) : positive := match x7 with | (x8~1)%positive => (x8~0~1)%positive | (x8~0)%positive => ((Ffix1 x8)~1)%positive | 1%positive => 1%positive end) x6) | 1%positive => 0 end end) x2 x3 end | Z.neg x2 => match Ffix match x with | 0 => -1 | Z.pos x4~1 => Z.pos x4~0 | Z.pos x4~0 => Z.pos ((fix Ffix0 (x5 : positive) : positive := match x5 with | (x6~1)%positive => (x6~0~1)%positive | (x6~0)%positive => ((Ffix0 x6)~1)%positive | 1%positive => 1%positive end) x4) | 1 => 0 | Z.neg x3 => Z.neg ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((...) x6)~0)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix0 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((...) x6)~0)%positive | (x6~0)%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix1 x6 x7)~0)%positive | 1%positive => (((...) x6)~1)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((...) x6)~0)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((...) x6)~1)%positive | (x6~0)%positive => (((...) x6)~0)%positive | 1%positive => 3%positive end end for Ffix0) x3 1%positive) end (match x0 with | Acc_intro _ x3 => x3 end match x with | 0 => -1 | Z.pos x4~1 => Z.pos x4~0 | Z.pos x4~0 => Z.pos ((fix Ffix0 (x5 : positive) : positive := match x5 with | (x6~1)%positive => (x6~0~1)%positive | (x6~0)%positive => ((Ffix0 x6)~1)%positive | 1%positive => 1%positive end) x4) | 1 => 0 | Z.neg x3 => Z.neg ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => ((...)~1)%positive | 1%positive => ((...)~0)%positive end | (x6~0)%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => ((...)~1)%positive end | (x6~0)%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => ((...)~1)%positive | 1%positive => ((...)~0)%positive end | 1%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => 3%positive end end for Ffix0) x3 1%positive) end (conj (match Z.ltb_ge x 0 with | conj x3 _ => x3 end x1) (match Z.lt_sub_pos x 1 with | conj x3 _ => x3 end eq_refl))) with | 0 => x | Z.pos x3 => (fix Ffix0 (x4 x5 : positive) {struct x5} : Z := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => match Ffix0 x6 x7 with | 0 => 0 | Z.pos x8 => Z.pos x8~0 | Z.neg x8 => Z.neg x8~0 end | (x7~0)%positive => match Ffix0 x6 x7 with | 0 => 1 | Z.pos x8 => Z.pos x8~1 | Z.neg x8 => Z.neg ((fix Ffix1 (x9 : positive) : positive := match x9 with | ...%positive => (x10~0~1)%positive | ...%positive => ((...)~1)%positive | 1%positive => 1%positive end) x8) end | 1%positive => Z.pos x6~0 end | (x6~0)%positive => match x5 with | (x7~1)%positive => match Ffix0 x6 x7 with | 0 => -1 | Z.pos x8 => Z.pos ((fix Ffix1 (x9 : positive) : positive := match x9 with | ...%positive => (x10~0~1)%positive | ...%positive => ((...)~1)%positive | 1%positive => 1%positive end) x8) | Z.neg x8 => Z.neg x8~1 end | (x7~0)%positive => match Ffix0 x6 x7 with | 0 => 0 | Z.pos x8 => Z.pos x8~0 | Z.neg x8 => Z.neg x8~0 end | 1%positive => Z.pos ((fix Ffix1 (x7 : positive) : positive := match x7 with | (x8~1)%positive => (x8~0~1)%positive | (x8~0)%positive => ((Ffix1 x8)~1)%positive | 1%positive => 1%positive end) x6) end | 1%positive => match x5 with | (x6~1)%positive => Z.neg x6~0 | (x6~0)%positive => Z.neg ((fix Ffix1 (x7 : positive) : positive := match x7 with | (x8~1)%positive => (x8~0~1)%positive | (x8~0)%positive => ((Ffix1 x8)~1)%positive | 1%positive => 1%positive end) x6) | 1%positive => 0 end end) x3 x2 | Z.neg x3 => Z.neg ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix0 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive | (x6~0)%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix1 x6 x7)~0)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~1)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~1)%positive | (x6~0)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive | 1%positive => 3%positive end end for Ffix0) x2 x3) end end 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?
f': forall n : nat, Acc lt n -> nat
n: nat
H: Acc lt nnatf': forall n : nat, Acc lt n -> nat
n: nat
H: Acc lt n
e: (n <=? 0) = falsen - 1 < napply Nat.sub_lt; auto with *. Defined. (* Compute (f' 10 (lt_wf 10)). doesn't evaluate to a nat if ended with Qed. *)f': forall n : nat, Acc lt n -> nat
n: nat
H: Acc lt n
e: 0 < nn - 1 < n
Anyway, my problem persists for Z.
g': forall n : Z, Acc (Zwf 0) n -> Z
n: Z
H: Acc (Zwf 0) nZsplit; now apply Z.leb_gt in e; auto with *. Defined.g': forall n : Z, Acc (Zwf 0) n -> Z
n: Z
H: Acc (Zwf 0) n
e: (n <=? 0) = falseZwf 0 (n - 1) n= (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 => match x1 with | Z.pos x3 => (fix Ffix0 (x4 : comparison) (x5 x6 : positive) {struct x6} : comparison := match x5 with | (x7~1)%positive => match x6 with | (x8~1)%positive => Ffix0 x4 x7 x8 | (x8~0)%positive => Ffix0 Gt x7 x8 | 1%positive => Gt end | (x7~0)%positive => match x6 with | (x8~1)%positive => Ffix0 Lt x7 x8 | (x8~0)%positive => Ffix0 x4 x7 x8 | 1%positive => Gt end | 1%positive => match x6 with | 1%positive => x4 | _ => Lt end end) Eq x2 x3 | _ => Gt end | Z.neg x2 => match x1 with | Z.neg x3 => match (fix Ffix0 (x4 : comparison) (x5 x6 : positive) {struct x6} : comparison := match x5 with | (x7~1)%positive => match ... with | ... => Ffix0 x4 x7 x8 | ... => Ffix0 Gt x7 x8 | ... => Gt end | (x7~0)%positive => match ... with | ... => Ffix0 Lt x7 x8 | ... => Ffix0 x4 x7 x8 | ... => Gt end | 1%positive => match ... with | ... => x4 | ... => Lt end end) Eq x2 x3 with | Eq => Eq | Lt => Gt | Gt => Lt end | _ => Lt end end = Lt) x) {struct x0} : Z := match (if match match x with | 0 => Eq | Z.pos _ => Gt | Z.neg _ => Lt end with | Gt => false | _ => true end as c return ({c = true} + {c = false}) then in_left else in_right) with | in_left => 0 | right x1 => match x with | 0 => Ffix match x with | 0 => -1 | Z.pos x3~1 => Z.pos x3~0 | Z.pos x3~0 => Z.pos ((fix Ffix0 (x4 : positive) : positive := match x4 with | (x5~1)%positive => (x5~0~1)%positive | (x5~0)%positive => ((Ffix0 x5)~1)%positive | 1%positive => 1%positive end) x3) | 1 => 0 | Z.neg x2 => Z.neg ((with Ffix0 (x3 x4 : positive) {struct x3} : positive := match x3 with | (x5~1)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~0)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~1)%positive | 1%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~0)%positive end | (x5~0)%positive => match x4 with | (x6~1)%positive => ((Ffix0 x5 x6)~1)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~0)%positive | 1%positive => (x5~1)%positive end | 1%positive => match x4 with | (x5~1)%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~0)%positive | (x5~0)%positive => (x5~1)%positive | 1%positive => 2%positive end end with Ffix1 (x3 x4 : positive) {struct x3} : positive := match x3 with | (x5~1)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~1)%positive | (x6~0)%positive => ((Ffix1 x5 x6)~0)%positive | 1%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~1)%positive end | (x5~0)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~0)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~1)%positive | 1%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~0)%positive end | 1%positive => match x4 with | (x5~1)%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~1)%positive | (x5~0)%positive => (((fix Ffix2 (x6 : positive) : positive := match ... with | ... => (...)~0 | ... => x7~1 | ... => 2 end) x5)~0)%positive | 1%positive => 3%positive end end for Ffix0) x2 1%positive) end (match x0 with | Acc_intro _ x2 => x2 end match x with | 0 => -1 | Z.pos x3~1 => Z.pos x3~0 | Z.pos x3~0 => Z.pos ((fix Ffix0 (x4 : positive) : positive := match x4 with | (x5~1)%positive => (x5~0~1)%positive | (x5~0)%positive => ((Ffix0 x5)~1)%positive | 1%positive => 1%positive end) x3) | 1 => 0 | Z.neg x2 => Z.neg ((with Ffix0 (x3 x4 : positive) {struct x3} : positive := match x3 with | (x5~1)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~0)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~1)%positive | 1%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~0)%positive end | (x5~0)%positive => match x4 with | (x6~1)%positive => ((Ffix0 x5 x6)~1)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~0)%positive | 1%positive => (x5~1)%positive end | 1%positive => match x4 with | (x5~1)%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~0)%positive | (x5~0)%positive => (x5~1)%positive | 1%positive => 2%positive end end with Ffix1 (x3 x4 : positive) {struct x3} : positive := match x3 with | (x5~1)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~1)%positive | (x6~0)%positive => ((Ffix1 x5 x6)~0)%positive | 1%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~1)%positive end | (x5~0)%positive => match x4 with | (x6~1)%positive => ((Ffix1 x5 x6)~0)%positive | (x6~0)%positive => ((Ffix0 x5 x6)~1)%positive | 1%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~0)%positive end | 1%positive => match x4 with | (x5~1)%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~1)%positive | (x5~0)%positive => (((fix Ffix2 ... : positive := ... ... ... ... end) x5)~0)%positive | 1%positive => 3%positive end end for Ffix0) x2 1%positive) end (conj (g'_subproof x (match Z.leb_gt x 0 with | conj x2 _ => x2 end x1)) (g'_subproof0 x))) | Z.pos x2 => match Ffix match x with | 0 => -1 | Z.pos x4~1 => Z.pos x4~0 | Z.pos x4~0 => Z.pos ((fix Ffix0 (x5 : positive) : positive := match x5 with | (x6~1)%positive => (x6~0~1)%positive | (x6~0)%positive => ((Ffix0 x6)~1)%positive | 1%positive => 1%positive end) x4) | 1 => 0 | Z.neg x3 => Z.neg ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((...) x6)~0)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix0 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((...) x6)~0)%positive | (x6~0)%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix1 x6 x7)~0)%positive | 1%positive => (((...) x6)~1)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((...) x6)~0)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((...) x6)~1)%positive | (x6~0)%positive => (((...) x6)~0)%positive | 1%positive => 3%positive end end for Ffix0) x3 1%positive) end (match x0 with | Acc_intro _ x3 => x3 end match x with | 0 => -1 | Z.pos x4~1 => Z.pos x4~0 | Z.pos x4~0 => Z.pos ((fix Ffix0 (x5 : positive) : positive := match x5 with | (x6~1)%positive => (x6~0~1)%positive | (x6~0)%positive => ((Ffix0 x6)~1)%positive | 1%positive => 1%positive end) x4) | 1 => 0 | Z.neg x3 => Z.neg ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => ((...)~1)%positive | 1%positive => ((...)~0)%positive end | (x6~0)%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => ((...)~1)%positive end | (x6~0)%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => ((...)~1)%positive | 1%positive => ((...)~0)%positive end | 1%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => 3%positive end end for Ffix0) x3 1%positive) end (conj (g'_subproof x (match Z.leb_gt x 0 with | conj x3 _ => x3 end x1)) (g'_subproof0 x))) with | 0 => x | Z.pos x3 => Z.pos ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix0 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive | (x6~0)%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix1 x6 x7)~0)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~1)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~1)%positive | (x6~0)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive | 1%positive => 3%positive end end for Ffix0) x2 x3) | Z.neg x3 => (fix Ffix0 (x4 x5 : positive) {struct x5} : Z := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => match Ffix0 x6 x7 with | 0 => 0 | Z.pos x8 => Z.pos x8~0 | Z.neg x8 => Z.neg x8~0 end | (x7~0)%positive => match Ffix0 x6 x7 with | 0 => 1 | Z.pos x8 => Z.pos x8~1 | Z.neg x8 => Z.neg ((fix Ffix1 (x9 : positive) : positive := match x9 with | ...%positive => (x10~0~1)%positive | ...%positive => ((...)~1)%positive | 1%positive => 1%positive end) x8) end | 1%positive => Z.pos x6~0 end | (x6~0)%positive => match x5 with | (x7~1)%positive => match Ffix0 x6 x7 with | 0 => -1 | Z.pos x8 => Z.pos ((fix Ffix1 (x9 : positive) : positive := match x9 with | ...%positive => (x10~0~1)%positive | ...%positive => ((...)~1)%positive | 1%positive => 1%positive end) x8) | Z.neg x8 => Z.neg x8~1 end | (x7~0)%positive => match Ffix0 x6 x7 with | 0 => 0 | Z.pos x8 => Z.pos x8~0 | Z.neg x8 => Z.neg x8~0 end | 1%positive => Z.pos ((fix Ffix1 (x7 : positive) : positive := match x7 with | (x8~1)%positive => (x8~0~1)%positive | (x8~0)%positive => ((Ffix1 x8)~1)%positive | 1%positive => 1%positive end) x6) end | 1%positive => match x5 with | (x6~1)%positive => Z.neg x6~0 | (x6~0)%positive => Z.neg ((fix Ffix1 (x7 : positive) : positive := match x7 with | (x8~1)%positive => (x8~0~1)%positive | (x8~0)%positive => ((Ffix1 x8)~1)%positive | 1%positive => 1%positive end) x6) | 1%positive => 0 end end) x2 x3 end | Z.neg x2 => match Ffix match x with | 0 => -1 | Z.pos x4~1 => Z.pos x4~0 | Z.pos x4~0 => Z.pos ((fix Ffix0 (x5 : positive) : positive := match x5 with | (x6~1)%positive => (x6~0~1)%positive | (x6~0)%positive => ((Ffix0 x6)~1)%positive | 1%positive => 1%positive end) x4) | 1 => 0 | Z.neg x3 => Z.neg ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((...) x6)~0)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix0 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((...) x6)~0)%positive | (x6~0)%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix1 x6 x7)~0)%positive | 1%positive => (((...) x6)~1)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((...) x6)~0)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((...) x6)~1)%positive | (x6~0)%positive => (((...) x6)~0)%positive | 1%positive => 3%positive end end for Ffix0) x3 1%positive) end (match x0 with | Acc_intro _ x3 => x3 end match x with | 0 => -1 | Z.pos x4~1 => Z.pos x4~0 | Z.pos x4~0 => Z.pos ((fix Ffix0 (x5 : positive) : positive := match x5 with | (x6~1)%positive => (x6~0~1)%positive | (x6~0)%positive => ((Ffix0 x6)~1)%positive | 1%positive => 1%positive end) x4) | 1 => 0 | Z.neg x3 => Z.neg ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => ((...)~1)%positive | 1%positive => ((...)~0)%positive end | (x6~0)%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => ((...)~1)%positive end | (x6~0)%positive => match x5 with | ...%positive => ((...)~0)%positive | ...%positive => ((...)~1)%positive | 1%positive => ((...)~0)%positive end | 1%positive => match x5 with | ...%positive => ((...)~1)%positive | ...%positive => ((...)~0)%positive | 1%positive => 3%positive end end for Ffix0) x3 1%positive) end (conj (g'_subproof x (match Z.leb_gt x 0 with | conj x3 _ => x3 end x1)) (g'_subproof0 x))) with | 0 => x | Z.pos x3 => (fix Ffix0 (x4 x5 : positive) {struct x5} : Z := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => match Ffix0 x6 x7 with | 0 => 0 | Z.pos x8 => Z.pos x8~0 | Z.neg x8 => Z.neg x8~0 end | (x7~0)%positive => match Ffix0 x6 x7 with | 0 => 1 | Z.pos x8 => Z.pos x8~1 | Z.neg x8 => Z.neg ((fix Ffix1 (x9 : positive) : positive := match x9 with | ...%positive => (x10~0~1)%positive | ...%positive => ((...)~1)%positive | 1%positive => 1%positive end) x8) end | 1%positive => Z.pos x6~0 end | (x6~0)%positive => match x5 with | (x7~1)%positive => match Ffix0 x6 x7 with | 0 => -1 | Z.pos x8 => Z.pos ((fix Ffix1 (x9 : positive) : positive := match x9 with | ...%positive => (x10~0~1)%positive | ...%positive => ((...)~1)%positive | 1%positive => 1%positive end) x8) | Z.neg x8 => Z.neg x8~1 end | (x7~0)%positive => match Ffix0 x6 x7 with | 0 => 0 | Z.pos x8 => Z.pos x8~0 | Z.neg x8 => Z.neg x8~0 end | 1%positive => Z.pos ((fix Ffix1 (x7 : positive) : positive := match x7 with | (x8~1)%positive => (x8~0~1)%positive | (x8~0)%positive => ((Ffix1 x8)~1)%positive | 1%positive => 1%positive end) x6) end | 1%positive => match x5 with | (x6~1)%positive => Z.neg x6~0 | (x6~0)%positive => Z.neg ((fix Ffix1 (x7 : positive) : positive := match x7 with | (x8~1)%positive => (x8~0~1)%positive | (x8~0)%positive => ((Ffix1 x8)~1)%positive | 1%positive => 1%positive end) x6) | 1%positive => 0 end end) x3 x2 | Z.neg x3 => Z.neg ((with Ffix0 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix0 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~0)%positive | 1%positive => (x6~1)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive | (x6~0)%positive => (x6~1)%positive | 1%positive => 2%positive end end with Ffix1 (x4 x5 : positive) {struct x4} : positive := match x4 with | (x6~1)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~1)%positive | (x7~0)%positive => ((Ffix1 x6 x7)~0)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~1)%positive end | (x6~0)%positive => match x5 with | (x7~1)%positive => ((Ffix1 x6 x7)~0)%positive | (x7~0)%positive => ((Ffix0 x6 x7)~1)%positive | 1%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive end | 1%positive => match x5 with | (x6~1)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~1)%positive | (x6~0)%positive => (((fix Ffix2 (x7 : positive) : positive := match x7 with | x8~1 => (Ffix2 x8)~0 | x8~0 => x8~1 | 1 => 2 end) x6)~0)%positive | 1%positive => 3%positive end end for Ffix0) x2 x3) end end end) 10 (Zwf_well_founded 0 10) : Z
A: This is a related question.
A: This one is somewhat related as well.
Answer
Making Zwf_well_founded transparent won't help, because of the way it is defined in the standard library:
Lemma Zwf_well_founded : well_founded (Zwf c).
...
case (Z.le_gt_cases c y); intro; auto with zarith.
...
Qed.If you replace the line in the proof above with
case (Z_le_gt_dec c y); intro; auto with zarith.and replace Qed. with Defined. (which you already did) everything should work. This is due the fact that the original proof depends on a logical term, and that prevents the evaluator from doing pattern-matching, because logical entity Z.le_gt_cases is opaque, while computational entity Z_le_gt_dec is transparent. See Using Coq's evaluation mechanisms in anger blog post by Xavier Leroy. You might also find useful Qed Considered Harmful post by Gregory Malecha.
Instead of modifying the proof of Zwf_well_founded you can reuse Zlt_0_rec like so:
Require Import Coq.ZArith.ZArith. Open Scope Z.x: Z
H_rec: forall y : Z, 0 <= y < x -> Z
nonneg: 0 <= xZauto with zarith. Defined. Definition h (z : Z) : Z := match Z_lt_le_dec z 0 with left _ => 0 | right pf => (Zlt_0_rec _ H z pf) end.x: Z
H_rec: forall y : Z, 0 <= y < x -> Z
nonneg: 0 <= x
n: x <> 00 <= Z.pred x < xeq_refl : h 100 = 5050 : h 100 = 5050
It's a bit less convenient because now we have to deal with negative numbers in h.