[Why3-club] permut fix

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Wed Mar 12 08:55:16 CET 2014


> ‘axioms of Why3 translated to Coq statements, then proved in Coq’!!
> It means that these axioms have other def in Coq ?? So you define a
> model starting from what ? I understand that you prove Lemmas. But
> axioms ?? 

Symbols that are uninterpreted in Why3 are given definitions in Coq.
Then axioms (in Why3) can be proved.

See for instance Why3 theory int.ComputerDivision. It provides two
uninterpreted symbols "div" and "mod" together with axioms (Div_mod,
Div_bound, etc.) Then have a look in lib/coq/int/ComputerDivision.v.
There symbols "div" and "mod" are given definitions (using the Coq
standard library) and axioms are turned into lemmas and proved.

Of course, there are typically several ways to define symbols in Coq, as
long as you can prove the axioms. For instance, there are several ways
to turn "div" and "mod" into total functions in Coq (e.g. you are fee to
choose the value you give to "div 1 0").

But the point is that, as Guillaume explained, there are no more axioms
in Coq. Thus, if false could be proved in Why3, then it could also be
proved in Coq, which would prove Coq to be inconsistent.

-- 
Jean-Christophe



More information about the Why3-club mailing list