The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

in my view it is a general design problem of the Coq standard library that it 
uses Prop for things which are easily decidable. Of cause it makes sense to 
define structures like an order in terms of Props, so that it can be used for 
cases where the order is not (easily) decidable, but I find it questionable 
that a decidable order is an order with additional decidability lemma rather 
than an order where the relational operators result in a bool right away. It 
is easy to write a module functor, type class or canonical instance which 
converts a bool based decidable order to a Prop based order in case one needs 
to plug in a decidable order structure into a Prop based structure. I think 
having both Prop and bool based relational operators around in a proof for 
decidable structures makes such proofs, especially automation, substantially 
more complicated and the libraries as a whole less obvious.

Best regards,

Michael

> -----Original Message-----
> From: 
> coq-club-request AT inria.fr
>  
> [mailto:coq-club-request AT inria.fr]
>  On Behalf
> Of Anton Trunov
> Sent: Friday, May 26, 2017 8:35 AM
> To: 
> coq-club AT inria.fr
> Subject: Re: [Coq-Club] Why doesn't compute this recursive function on Z?
> 
> 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... *)
> >
> >

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928