--- ./src/wp/share/why3/Memory.v.orig 2014-03-12 09:07:51.000000000 -0600
+++ ./src/wp/share/why3/Memory.v 2014-09-06 21:30:00.000000000 -0600
@@ -137,29 +137,29 @@ Definition separated (p:addr) (a:Z) (q:a
(((offset p) + a)%Z <= (offset q))%Z))).
(* Why3 assumption *)
-Definition eqmem {a:Type} {a_WT:WhyType a} (m1:(@map.Map.map
- addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT))
- (p:addr) (a1:Z): Prop := forall (q:addr), (included q 1%Z p a1) ->
+Definition eqmem {a:Type} {a_WT:WhyType a} (m1:(map.Map.map addr a))
+ (m2:(map.Map.map addr a)) (p:addr) (a1:Z): Prop :=
+ forall (q:addr), (included q 1%Z p a1) ->
((map.Map.get m1 q) = (map.Map.get m2 q)).
(* Why3 assumption *)
-Definition havoc {a:Type} {a_WT:WhyType a} (m1:(@map.Map.map
- addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT))
- (p:addr) (a1:Z): Prop := forall (q:addr), (separated q 1%Z p a1) ->
+Definition havoc {a:Type} {a_WT:WhyType a} (m1:(map.Map.map addr a))
+ (m2:(map.Map.map addr a)) (p:addr) (a1:Z): Prop :=
+ forall (q:addr), (separated q 1%Z p a1) ->
((map.Map.get m1 q) = (map.Map.get m2 q)).
(* Why3 assumption *)
-Definition valid_rd (m:(@map.Map.map Z _ Z _)) (p:addr) (n:Z): Prop :=
+Definition valid_rd (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
(0%Z < n)%Z -> ((0%Z <= (offset p))%Z /\
(((offset p) + n)%Z <= (map.Map.get m (base p)))%Z).
(* Why3 assumption *)
-Definition valid_rw (m:(@map.Map.map Z _ Z _)) (p:addr) (n:Z): Prop :=
+Definition valid_rw (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
(0%Z < n)%Z -> ((0%Z < (base p))%Z /\ ((0%Z <= (offset p))%Z /\
(((offset p) + n)%Z <= (map.Map.get m (base p)))%Z)).
(* Why3 goal *)
-Lemma valid_rw_rd : forall (m:(@map.Map.map Z _ Z _)), forall (p:addr),
+Lemma valid_rw_rd : forall (m:(map.Map.map Z Z)), forall (p:addr),
forall (n:Z), (valid_rw m p n) -> (valid_rd m p n).
intros m p n.
unfold valid_rw. unfold valid_rd.
@@ -167,7 +167,7 @@ intuition (auto with zarith).
Qed.
(* Why3 goal *)
-Lemma valid_string : forall (m:(@map.Map.map Z _ Z _)), forall (p:addr),
+Lemma valid_string : forall (m:(map.Map.map Z Z)), forall (p:addr),
((base p) < 0%Z)%Z -> (((0%Z <= (offset p))%Z /\
((offset p) < (map.Map.get m (base p)))%Z) -> ((valid_rd m p 1%Z) /\
~ (valid_rw m p 1%Z))).
@@ -227,17 +227,17 @@ Definition region: Z -> Z.
Admitted.
(* Why3 goal *)
-Definition linked: (@map.Map.map Z _ Z _) -> Prop.
+Definition linked: (map.Map.map Z Z) -> Prop.
Admitted.
(* Why3 goal *)
-Definition sconst: (@map.Map.map addr addr_WhyType Z _) -> Prop.
+Definition sconst: (map.Map.map addr Z) -> Prop.
Admitted.
(* Why3 assumption *)
-Definition framed (m:(@map.Map.map addr addr_WhyType
- addr addr_WhyType)): Prop := forall (p:addr), ((region (base (map.Map.get m
- p))) <= 0%Z)%Z.
+Definition framed (m:(map.Map.map addr addr)): Prop :=
+ forall (p:addr), ((region (base (map.Map.get m p (a_WT := addr_WhyType)
+ (b_WT := addr_WhyType)))) <= 0%Z)%Z.
(* Why3 goal *)
Lemma separated_included : forall (p:addr) (q:addr), forall (a:Z) (b:Z),
@@ -283,22 +283,22 @@ Qed.
(* Why3 goal *)
Lemma eqmem_included : forall {a:Type} {a_WT:WhyType a},
- forall (m1:(@map.Map.map addr addr_WhyType a a_WT)) (m2:(@map.Map.map
- addr addr_WhyType a a_WT)), forall (p:addr) (q:addr), forall (a1:Z) (b:Z),
+ forall (m1:(map.Map.map addr a)) (m2:(map.Map.map addr a)),
+ forall (p:addr) (q:addr), forall (a1:Z) (b:Z),
(included p a1 q b) -> ((eqmem m1 m2 q b) -> (eqmem m1 m2 p a1)).
intros a a_WT m1 m2 p q a1 b h1 h2.
Admitted.
(* Why3 goal *)
-Lemma eqmem_sym : forall {a:Type} {a_WT:WhyType a}, forall (m1:(@map.Map.map
- addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT)),
+Lemma eqmem_sym : forall {a:Type} {a_WT:WhyType a},
+ forall (m1:(map.Map.map addr a)) (m2:(map.Map.map addr a)),
forall (p:addr), forall (a1:Z), (eqmem m1 m2 p a1) -> (eqmem m2 m1 p a1).
intros A m1 m2 p a. unfold eqmem.
Admitted.
(* Why3 goal *)
-Lemma havoc_sym : forall {a:Type} {a_WT:WhyType a}, forall (m1:(@map.Map.map
- addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT)),
+Lemma havoc_sym : forall {a:Type} {a_WT:WhyType a},
+ forall (m1:(map.Map.map addr a)) (m2:(map.Map.map addr a)),
forall (p:addr), forall (a1:Z), (havoc m1 m2 p a1) -> (havoc m2 m1 p a1).
Admitted.
--- ./src/wp/share/why3/Qedlib.v.orig 2014-03-12 09:07:51.000000000 -0600
+++ ./src/wp/share/why3/Qedlib.v 2014-09-06 21:00:00.000000000 -0600
@@ -187,13 +187,14 @@ Definition real_hex := real_base 2%R.
Record farray (A B : Type) := { whytype1 : BuiltIn.WhyType A ;
whytype2 : BuiltIn.WhyType B ;
- access :> @Map.map A whytype1 B whytype2 }.
+ access :> Map.map A B }.
Definition array (A : Type) := farray Z A.
Hypothesis extensionality: forall (A B : Type) (f g : A -> B),
(forall x, f x = g x) -> f = g.
Definition select {A B : Type}
- (m : farray A B) (k : A) : B := Map.get m k.
+ (m : farray A B) (k : A) : B := Map.get m k
+ (a_WT := whytype1 m) (b_WT := whytype2 m).
Lemma farray_eq : forall A B (m1 m2 : farray A B),
whytype1 m1 = whytype1 m2 -> whytype2 m1 = whytype2 m2 ->
@@ -210,7 +211,8 @@ Qed.
Definition update {A B : Type}
(m : farray A B) (k : A) (v : B) : (farray A B) :=
- {| whytype1 := whytype1 m; whytype2 := whytype2 m; access := Map.set m k v|}.
+ {| whytype1 := whytype1 m; whytype2 := whytype2 m;
+ access := Map.set m k v (a_WT := whytype1 m) (b_WT := whytype2 m) |}.
Notation " a .[ k ] " := (select a k) (at level 60).
Notation " a .[ k <- v ] " := (update a k v) (at level 60).