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
