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 predi
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
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
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 f
