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
