[Why3-club] Consistency of map theory

Guillaume Melquiond guillaume.melquiond at inria.fr
Thu Nov 22 20:21:02 CET 2012


Le jeudi 22 novembre 2012 à 13:05 +0100, Benedikt Huber a écrit :
> Hello!
> 
> I recently started playing around with Why3 (using coq+Z3), and I'm 
> really impressed so far.
> 
> However, I believe that the lemma 'permut_eq' (theory map.why) is wrong. 
> While playing with the VCs of the quicksort example, I found that it is 
> possible to prove that "all maps Z->Z are equal" using this lemma (see 
> below). Does this imply the map theory is inconsistent, or did I miss 
> something?

Good catch. The map theory seems like it was originally consistent and
then someone changed the permut_refl case 18 months ago from

    forall a : map int 'a. forall l u : int. permut_sub a a l u

to

    forall a1 a2 : map int 'a. forall l u : int. 
    map_eq_sub a1 a2 l u -> permut_sub a1 a2 l u

I will change it back and see how much of the testsuite breaks.

> In general, maybe it would be desirable to proof all the lemmas in 
> theories provided with why3 to avoid problems like this?

Sure. And if you take a look at the lib/coq subdirectory of why3, you
will notice that the work has already started. Unfortunately, no one has
handled map.why yet.

Best regards,

Guillaume




More information about the Why3-club mailing list