Re: [Why3-club] constructive Why3 logic ?
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 : > 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
Re: [Why3-club] constructive Why3 logic ?
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
Re: [Why3-club] constructive Why3 logic ?
Guillaume, many thanks for your answer. But: Le 9 mai 2014 à 16:22, Guillaume Melquiond a écrit : >> 2- is it fair to use Classical logic in the Coq stubs translated from Why3 >> goals/lemmas ? > > 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!! -JJ- ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
Re: [Why3-club] constructive Why3 logic ?
On 06/05/2014 04:54, Jean-Jacques Levy wrote: Dear Why3 Friends! from time to time, I met difficulties in making a constructive Coq proof corresponding to a Why3 goal. Has anybody met same problem ? Must of time it comes from translation of Why3 predicates into Prop's, instead of a Coq predicate (with truth values). Then it’s hard to express excluded middle which I think that automatic solvers use frequently. Although many folks repeated to me that constructive proofs are nicer, I have 2 questions: 1- is there any way to get a proof certificate out of automatic solvers ? Not from Why3. But some solvers, e.g. Z3, produce them on their own. You can take a look at Chantal Keller's work to see how to recover a Coq proof from it, if needed. 2- is it fair to use Classical logic in the Coq stubs translated from Why3 goals/lemmas ? 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. Should I move to Isabelle/HOL ? I can't answer that part, as I haven't played enough with it to know what the shortcomings are, if any. Perhaps Stefan Berghofer can fill you in on that part. Best regards, Guillaume ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
[Why3-club] constructive Why3 logic ?
Dear Why3 Friends! from time to time, I met difficulties in making a constructive Coq proof corresponding to a Why3 goal. Has anybody met same problem ? Must of time it comes from translation of Why3 predicates into Prop's, instead of a Coq predicate (with truth values). Then it’s hard to express excluded middle which I think that automatic solvers use frequently. Although many folks repeated to me that constructive proofs are nicer, I have 2 questions: 1- is there any way to get a proof certificate out of automatic solvers ? 2- is it fair to use Classical logic in the Coq stubs translated from Why3 goals/lemmas ? Should I move to Isabelle/HOL ? Thanks for help! -JJ- ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
