[Why3-club] permut fix
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
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.
More information about the Why3-club