[Why3-club] permut fix

Guillaume Melquiond guillaume.melquiond at inria.fr
Wed Mar 12 07:38:20 CET 2014


On 12/03/2014 05:15, Jean-Jacques Levy wrote:

> I'm also curious to understand your consistency check with Coq. How could it be ? Coq seems to prove adequacy, but not consistency. How could you avoid an inconsistent axiom ? You proved that 'True <> False' ?? But surely all lemmas of libraries should be proved (by automatic provers or Coq/Isabelle/etc). Is it what you call realizability?

Why3 comes with a set of axioms and lemmas stored in theories. They are 
then used by automatic and interactive provers to prove stuff. We say 
that the theories are consistent if one cannot deduce False from them 
(in the setting of first-order logic). As far as I understand, this is 
the proper meaning of consistency.

We prove it relatively to the consistency of Coq, that is, if Coq is 
consistent, then Why3 theories are consistent too. All the axions and 
lemmas of Why3 are translated to Coq statements, then proved in Coq. If 
it was possible to deduce False from Why3 theories in FOL, one could 
build a proof of False in Coq. So, by contraposition, we have relative 
consistency.

Adequacy would be the matter of turning as many Why3 axioms into lemmas 
as possible. While we try to ensure it, I don't think we have any way to 
prove it with Coq.

Best regards,

Guillaume



More information about the Why3-club mailing list