[Why3-club] Consistency of map theory
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 :
> 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
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
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.
More information about the Why3-club