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
