Coq can't compute a valid function on Z, but it works on nat

I am writing (for myself) an explanation of how to do informed recursion in Coq. (see, for example, the book of Kok'Art, chapter 15.2). I first made an example based function nat

and it worked fine, but then I did it again for Z

, and when I use Compute

to evaluate it, it doesn't decrease all the way to Z

. Why?

Here's my example (I put text inside comments so that all content can be copied to your editor):

(* Checking reasonable recursion *)

(* TL; DR: To do reasonable recursion, first create a "functional" and then create a recursive function using Acc_iter, an iterator for the relationships available *)

(* As an example, let's calculate the sum of a series from 1 to n, something like this sketch:

fix fn: = (if n = 0 then 0 else n + f (n-1))

Now let's not use structured recursion on n.

Instead, we use reasoned recursion on n, using that the relation less than ('lt') is wellfounded. The function f exits because the recursive call is being made on the structurally smaller member (in the decreasing Acc chain). *)

(* First we do this for nat *)

Require Import Arith.Arith.
Require Import Program.Utils. (* for 'dec' *)
Require Import Wellfounded.

      

        
        
        
      

    

(* From proof that the relationship is proven, we can get proof that a particular item is in its domain.

Verification commands are not needed here, only 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, we define a "functional" F for f. This is a function that takes a function F_rec to "recursively call" as an argument. Since we need to know n <> 0 in the second branch we use 'dec' to include a boolean if condition in sumbool We get information about it in branches.

We write most of this clarification and leave some holes to be filled 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 the iterator to call f as many times as necessary.

Side note. You can either make an iterator that takes a maximum recursive depth of d as argument nat and recursively on d, but that needs to provide d as well as a "default" value, return when d reaches zero, and terminate early.

The subtle thing with justified recursion is that an iterator can iterate on a proof of validity and does not require any other structure or default to ensure it terminates. *)

(* Acc_iter type is quite 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 may depend 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 proof that n is available. The iterator returns the value of f applied to n.

Several arguments to Acc_iter are implicit, and some of them can be deduced. So we can define f 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 this for Z. Here we cannot use lt, or lt_wf, because they are for nat. For Z, we can use Zle and (Zwf c), which takes the lower border. It needs the lower border along which we know that the function always terminates to ensure termination. Here we use (Zwf 0) to say that our function will always terminate at or below 0. We also need 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 calculate! *)

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 it Zwf_well_founded

is defined as Opaque

in a library, so I tried to make it Transparent

by copying the proof and ending the lemma Defined.

instead Qed.

, but that didn Help ...

Added observation:

If I define f'

for nat

c Fixpoint

instead and recurse on proof of validity and end c Defined.

, then it evaluates. But if I end up with Qed.

it doesn't diminish. Is it related? I think there is a transparency issue in the definition G

or G

somewhere ... Or am I completely wrong?

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)).