maybe this kind of approach may be useful: Producing Certified Functional Code from Inductive Specifications http://cedric.cnam.fr/~delahaye/papers/relext-coq%20(CPP'12).pdf
cheers. 2014-05-09 11:18 GMT+02:00 Guillaume Melquiond <guillaume.melqui...@inria.fr >: > On 09/05/2014 10:42, Jean-Jacques Levy wrote: > > Yes, it is fair, since the logic of Why3 already assumes it. >>> >>> In practice, I never had to assume it though, when doing a Coq proof. >>> Indeed, most of the predicates I get from Why3 are trivially boolean in >>> nature, and thus do not need excluded middle. >>> >> >> what do you mean by "most of the predicates I get from Why3 are trivially >> boolean in nature" ? In the Coq files that I get from Why3, I see Coq >> ‘Prop’s translated from Why3 predicates!! >> > > Sure, Why3 is using Prop for predicates, but that does reduce in any way > their expressiveness. Suppose you have the following predicate P: > > Definition P (x : Z) : Prop := (0 <= x /\ x <= 5)%Z. > > As a user, you can easily define a (P_bool : Z -> bool) function and prove > the following lemma: > > Lemma P_spec : forall x : Z, P x <-> P_bool x = true. > > And you don't need excluded middle to prove it. That is what I mean when I > say that most predicates coming from Why3 are boolean in nature (even if > they are in Prop). > > In an ideal world, Why3 would directly generate the boolean version of the > predicates. Unfortunately, there are two shortcomings. First, if you are > not an SSReflect user, boolean predicates are a pain to use in Coq. Second, > the logic of Why3 supports some predicates that are not boolean in nature: > inductive predicates. And because of that, all the predicates have to be in > Prop. > > Best regards, > > Guillaume > > > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club > -- Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year. Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
