Commit 77d4d9e1 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid

blocking semantic

parent 9966d214
......@@ -415,6 +415,7 @@ lemma subst_fresh :
forall f:fmla, x:ident, v:ident.
fresh_in_fmla x f -> subst f x v = f
(* Not needed *)
(* lemma let_subst: *)
(* forall t:term, f:fmla, x id':ident, id :mident. *)
......@@ -809,9 +810,6 @@ predicate expr_writes (s:expr) (w:Set.set mident) =
function fresh_from (f:fmla) (s:expr) : ident
lemma msubst_fresh :
forall f:fmla, x:mident, s:expr.
msubst f x (fresh_from f s) = f
(* Need it for monotonicity*)
axiom fresh_from_fmla: forall s:expr, f:fmla.
......
......@@ -4,7 +4,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require set.Set.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
......@@ -612,32 +611,109 @@ Definition total_valid_triple(p:fmla) (e:expr) (q:fmla): Prop :=
exists pi':(list (ident* value)%type), exists n:Z, (many_steps sigma pi e
sigma' pi' (Evalue Vvoid) n) /\ (eval_fmla sigma' pi' q).
Axiom set1 : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set1_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set1 a).
Existing Instance set1_WhyType.
Parameter mem1: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) <-> (mem1 x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) -> (mem1 x s2).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) ->
(subset s1 s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set1 a).
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set1 a)): Prop :=
forall (x:a), ~ (mem1 x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set1
a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1 a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set1 a)), (mem1 x (add y s)) <-> ((x = y) \/ (mem1 x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1
a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set1 a)), (mem1 x (remove y s)) <-> ((~ (x = y)) /\ (mem1 x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set1
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (union s1 s2)) <-> ((mem1 x s1) \/ (mem1 x
s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (inter s1 s2)) <-> ((mem1 x s1) /\ (mem1 x
s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (diff s1 s2)) <-> ((mem1 x s1) /\ ~ (mem1 x
s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
(~ (is_empty s)) -> (mem1 (choose s) s).
Parameter all: forall {a:Type} {a_WT:WhyType a}, (set1 a).
Axiom all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem1 x
(all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set.Set.set mident))
(sigma':(map mident value)): Prop := forall (i:mident), (~ (set.Set.mem i
a)) -> ((get sigma i) = (get sigma' i)).
Definition assigns(sigma:(map mident value)) (a:(set1 mident)) (sigma':(map
mident value)): Prop := forall (i:mident), (~ (mem1 i a)) -> ((get sigma
i) = (get sigma' i)).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set.Set.set
mident)), (assigns sigma a sigma).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set1 mident)),
(assigns sigma a sigma).
Axiom assigns_trans : forall (sigma1:(map mident value)) (sigma2:(map mident
value)) (sigma3:(map mident value)) (a:(set.Set.set mident)),
((assigns sigma1 a sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1
a sigma3).
value)) (sigma3:(map mident value)) (a:(set1 mident)), ((assigns sigma1 a
sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
Axiom assigns_union_left : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s1 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s1
sigma') -> (assigns sigma (union s1 s2) sigma').
Axiom assigns_union_right : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s2 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s2
sigma') -> (assigns sigma (union s1 s2) sigma').
(* Why3 assumption *)
Fixpoint expr_writes(s:expr) (w:(set.Set.set mident)) {struct s}: Prop :=
Fixpoint expr_writes(s:expr) (w:(set1 mident)) {struct s}: Prop :=
match s with
| ((Evalue _)|((Evar _)|((Ederef _)|(Eassert _)))) => True
| (Eassign id _) => (set.Set.mem id w)
| (Eassign id _) => (mem1 id w)
| (Eseq e1 e2) => (expr_writes e1 w) /\ (expr_writes e2 w)
| (Eif e1 e2 e3) => (expr_writes e1 w) /\ ((expr_writes e2 w) /\
(expr_writes e3 w))
......@@ -713,3 +789,5 @@ simpl.
intros.
apply H; auto.
Qed.
......@@ -4,7 +4,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require set.Set.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
......@@ -612,32 +611,109 @@ Definition total_valid_triple(p:fmla) (e:expr) (q:fmla): Prop :=
exists pi':(list (ident* value)%type), exists n:Z, (many_steps sigma pi e
sigma' pi' (Evalue Vvoid) n) /\ (eval_fmla sigma' pi' q).
Axiom set1 : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set1_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set1 a).
Existing Instance set1_WhyType.
Parameter mem1: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) <-> (mem1 x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) -> (mem1 x s2).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) ->
(subset s1 s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set1 a).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set.Set.set mident))
(sigma':(map mident value)): Prop := forall (i:mident), (~ (set.Set.mem i
a)) -> ((get sigma i) = (get sigma' i)).
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set1 a)): Prop :=
forall (x:a), ~ (mem1 x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set1
a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1 a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set1 a)), (mem1 x (add y s)) <-> ((x = y) \/ (mem1 x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1
a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set1 a)), (mem1 x (remove y s)) <-> ((~ (x = y)) /\ (mem1 x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set1
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set.Set.set
mident)), (assigns sigma a sigma).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (union s1 s2)) <-> ((mem1 x s1) \/ (mem1 x
s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (inter s1 s2)) <-> ((mem1 x s1) /\ (mem1 x
s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (diff s1 s2)) <-> ((mem1 x s1) /\ ~ (mem1 x
s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
(~ (is_empty s)) -> (mem1 (choose s) s).
Parameter all: forall {a:Type} {a_WT:WhyType a}, (set1 a).
Axiom all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem1 x
(all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set1 mident)) (sigma':(map
mident value)): Prop := forall (i:mident), (~ (mem1 i a)) -> ((get sigma
i) = (get sigma' i)).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set1 mident)),
(assigns sigma a sigma).
Axiom assigns_trans : forall (sigma1:(map mident value)) (sigma2:(map mident
value)) (sigma3:(map mident value)) (a:(set.Set.set mident)),
((assigns sigma1 a sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1
a sigma3).
value)) (sigma3:(map mident value)) (a:(set1 mident)), ((assigns sigma1 a
sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
Axiom assigns_union_left : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s1 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s1
sigma') -> (assigns sigma (union s1 s2) sigma').
Axiom assigns_union_right : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s2 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s2
sigma') -> (assigns sigma (union s1 s2) sigma').
(* Why3 assumption *)
Fixpoint expr_writes(s:expr) (w:(set.Set.set mident)) {struct s}: Prop :=
Fixpoint expr_writes(s:expr) (w:(set1 mident)) {struct s}: Prop :=
match s with
| ((Evalue _)|((Evar _)|((Ederef _)|(Eassert _)))) => True
| (Eassign id _) => (set.Set.mem id w)
| (Eassign id _) => (mem1 id w)
| (Eseq e1 e2) => (expr_writes e1 w) /\ (expr_writes e2 w)
| (Eif e1 e2 e3) => (expr_writes e1 w) /\ ((expr_writes e2 w) /\
(expr_writes e3 w))
......@@ -721,10 +797,27 @@ pose (id1 := (fresh_from p s)); fold id1.
pose (id2 := (fresh_from q s)); fold id2.
intros.
assert (forall (id : ident), (msubst_term (Tvalue Vvoid) m id)= (Tvalue Vvoid)).
apply H0 with (p := (Flet id1 (Tvar result)
(Flet result (msubst_term (Tvalue Vvoid) m id1) (msubst p m id1)))).
intros.
simpl in *.
assert (forall (id : ident), (msubst_term (Tvalue Vvoid) m id)
= (Tvalue Vvoid)).
ae.
rewrite H2 in *.
assert (forall (p : fmla), (msubst p m (fresh_from p s))= p).
rewrite H3.
simpl.
apply eval_msubst; auto.
apply fresh_from_fmla.
clear H0 H1 H2.
destruct (ident_decide id2 result).
(* id2 = result*)
rewrite H0.
rewrite get_stack_eq; auto.
admit.
rewrite get_stack_neq; auto.
rewrite get_stack_eq; auto.
apply H.
ae.
Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment