The Coq mailing list

[Anton Trunov <anton.a.trunov AT gmail.com>]

Hi Lars!
This is due to the fact that Zwf_well_founded’s proof uses destruction on a 
logical term:
    ...
    case (Z.le_gt_cases c y)
    ...

Just posted an answer on Stackoverflow :)
https://stackoverflow.com/questions/44186751/coq-cant-compute-a-well-founded-function-on-z-but-it-works-on-nat/

-Anton

> On 26 May 2017, at 09:30, Lars Rasmusson 
> <lars.rasmusson AT ri.se>
>  wrote:
> 
> (** *  How can I compute with integers Z in Coq?
> 
>   I write the sum of 1 to n with well-founded recursion, 
>   essentially like this.
> 
>   fix sum_n n _ := if 0 <? n then n + sum_n (n-1) _ else 0.
> 
>   When using nat I can use Compute to run the function 
>   but when  using Z the program doesn't reduce.  
> 
> *)                                        
> 
> Require Import Arith.Arith Program.Utils Wellfounded.
> 
> Fixpoint sum_n (n:nat) (H: Acc lt n) {struct H} : nat.
>  refine (if dec (0 <? n) then n + sum_n (n-1) _ else 0).
>  apply (Acc_inv H); apply Nat.ltb_lt in e; auto with *.
> Defined.
> 
> Compute (sum_n 50 (lt_wf _)). (* Prints 1275 *)
> 
> Require Import ZArith Zwf.
> Open Scope Z.
> 
> Fixpoint sum_nZ (n:Z) (H: Acc (Zwf 0) n) {struct H} : Z.
>  refine (if dec (0 <? n) then n + sum_nZ (n-1) _ else 0).
>  apply (Acc_inv H); apply Z.ltb_lt in e; split; auto with *.
> Defined.
> 
> Compute (sum_nZ 50 ((Zwf_well_founded _) _)). (* Doesn't reduce... *)
> 
>