[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