[Why3-club] Consistency of map theory

Benedikt Huber benedikt.huber at gmail.com
Thu Nov 22 13:05:35 CET 2012


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?

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

Kind Regards,
Benedikt Huber


(* I used the Coq environment generated by Why3's Coq driver for
    the verification of quicksort.mlw (from the gallery) *)

(* Proof that all Z-maps are equal (i.e., map.why is inconsistent) *)

(* (1) If (l > u) then (map_eq_sub a1 a2 l u) for any map a1,a2 *)
Lemma map_eq_sub_empty:
   forall (a1:(map Z Z)) (a2:(map Z Z)),
   forall (l:Z) (u:Z),
   (l > u)%Z -> map_eq_sub a1 a2 l u.
intros a1 a2 l u H.
red; intros; try omega. Qed.

(* (2) If (l > u) then (permut_sub a1 a2 l u) for any map a1,a2 *)
Lemma permut_sub_empty:
   forall (a1:(map Z Z)) (a2:(map Z Z)),
   forall (l:Z) (u:Z),
   (l > u)%Z -> permut_sub a1 a2 l u.
intros. apply permut_refl. apply map_eq_sub_empty. auto. Qed.

(* (3) Therefore, (get a2 i) = (get a1 i) for all i ??? *)
Lemma all_equal:
   forall (a1:(map Z Z)) (a2:(map Z Z)),
   forall (i:Z),
   (get a2 i) = (get a1 i).
intros. apply permut_eq with (l:=1%Z) (u:=0%Z); try omega.
apply permut_sub_empty; omega. Qed.



More information about the Why3-club mailing list