[Why3-club] permut fix

Jean-Jacques Levy jean-jacques.levy at inria.fr
Wed Mar 12 05:15:27 CET 2014


Dear Jean-Christophe,

Le 11 mars 2014 à 17:10, Jean-Christophe Filliatre <Jean-Christophe.Filliatre at lri.fr> a écrit :

>> Many thanks. So your advice is to use the development version.
> 
> We should make a new release very soon (hopefully by the end of the
> week), notably because of this fix regarding permutations.

so I’ll wait for next release and eagerly discover how you solved the permutation issue. I’m striken by your "automatic proofs" with the 'number of occurences’ predicate, since I struggled with the one (pseudo higher-order) in 0.82 library. With which, no automatic prover could help. But maybe I did it wrong…

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?

Best, -JJ-


More information about the Why3-club mailing list