Commit 3f6de048 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid

blocking semantic

parent c57ffaa6
......@@ -379,11 +379,11 @@ id1 <> id2 ->
(eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)
(* lemma eval_swap_term: *)
(* forall t:term, sigma:env, pi:stack, id1 id2:ident, v1 v2:value. *)
(* id1 <> id2 -> *)
(* (eval_term sigma (Cons (id1,v1) (Cons (id2,v2) pi)) t = *)
(* eval_term sigma (Cons (id2,v2) (Cons (id1,v1) pi)) t) *)
lemma eval_swap_term_2:
forall t:term, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_term sigma (Cons (id1,v1) (Cons (id2,v2) pi)) t =
eval_term sigma (Cons (id2,v2) (Cons (id1,v1) pi)) t)
lemma eval_swap:
forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
......
......@@ -375,15 +375,6 @@ Axiom fresh_in_binop : forall (t:term) (t':term) (op:operator) (v:ident),
(fresh_in_term v (Tbin t op t')) -> ((fresh_in_term v t) /\
(fresh_in_term v t')).
Axiom eval_msubst_term : forall (e:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (x:mident) (v:ident), (fresh_in_term v e) ->
((eval_term sigma pi (msubst_term e x v)) = (eval_term (set sigma x
(get_stack v pi)) pi e)).
Axiom eval_term_change_free : forall (t:term) (sigma:(map mident value))
(pi:(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_term id
t) -> ((eval_term sigma (Cons (id, v) pi) t) = (eval_term sigma pi t)).
(* Why3 assumption *)
Fixpoint fresh_in_fmla(id:ident) (f:fmla) {struct f}: Prop :=
match f with
......@@ -418,26 +409,52 @@ Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
| (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
end.
Axiom subst_fresh_term : forall (t:term) (x:ident) (v:ident),
(fresh_in_term x t) -> ((subst_term t x v) = t).
Axiom subst_fresh : forall (f:fmla) (x:ident) (v:ident), (fresh_in_fmla x
f) -> ((subst f x v) = f).
Axiom eval_msubst_term : forall (e:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (x:mident) (v:ident), (fresh_in_term v e) ->
((eval_term sigma pi (msubst_term e x v)) = (eval_term (set sigma x
(get_stack v pi)) pi e)).
Axiom eval_msubst : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (x:mident) (v:ident), (fresh_in_fmla v f) ->
((eval_fmla sigma pi (msubst f x v)) <-> (eval_fmla (set sigma x
(get_stack v pi)) pi f)).
Axiom eval_swap_term_any : forall (t:term) (sigma:(map mident value))
(pi:(list (ident* value)%type)) (l:(list (ident* value)%type)) (id1:ident)
Axiom eval_swap_term : forall (t:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (l:(list (ident* value)%type)) (id1:ident)
(id2:ident) (v1:value) (v2:value), (~ (id1 = id2)) -> ((eval_term sigma
(infix_plpl l (Cons (id1, v1) (Cons (id2, v2) pi))) t) = (eval_term sigma
(infix_plpl l (Cons (id2, v2) (Cons (id1, v1) pi))) t)).
Axiom eval_swap_any : forall (f:fmla) (sigma:(map mident value)) (pi:(list
Axiom eval_swap_term_2 : forall (t:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (id1:ident) (id2:ident) (v1:value) (v2:value),
(~ (id1 = id2)) -> ((eval_term sigma (Cons (id1, v1) (Cons (id2, v2) pi))
t) = (eval_term sigma (Cons (id2, v2) (Cons (id1, v1) pi)) t)).
Axiom eval_swap : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (l:(list (ident* value)%type)) (id1:ident)
(id2:ident) (v1:value) (v2:value), (~ (id1 = id2)) -> ((eval_fmla sigma
(infix_plpl l (Cons (id1, v1) (Cons (id2, v2) pi))) f) <-> (eval_fmla sigma
(infix_plpl l (Cons (id2, v2) (Cons (id1, v1) pi))) f)).
Axiom eval_swap_2 : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (id1:ident) (id2:ident) (v1:value) (v2:value),
(~ (id1 = id2)) -> ((eval_fmla sigma (Cons (id1, v1) (Cons (id2, v2) pi))
f) <-> (eval_fmla sigma (Cons (id2, v2) (Cons (id1, v1) pi)) f)).
Axiom eval_term_change_free : forall (t:term) (sigma:(map mident value))
(pi:(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_term id
t) -> ((eval_term sigma (Cons (id, v) pi) t) = (eval_term sigma pi t)).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem eval_change_free : forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (f:fmla),
......@@ -454,8 +471,7 @@ Theorem eval_change_free : forall (sigma:(map mident value)) (pi:(list
end.
destruct f; auto.
simpl.
intros H id v (H1 & H2 & h3) H4.
rewrite eval_term_change_free in H4; auto.
intros H_induc id v (H & H1 & H2) H3.
Qed.
......
......@@ -431,12 +431,22 @@ Axiom eval_swap_term : forall (t:term) (sigma:(map mident value)) (pi:(list
(infix_plpl l (Cons (id1, v1) (Cons (id2, v2) pi))) t) = (eval_term sigma
(infix_plpl l (Cons (id2, v2) (Cons (id1, v1) pi))) t)).
Axiom eval_swap_term_2 : forall (t:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (id1:ident) (id2:ident) (v1:value) (v2:value),
(~ (id1 = id2)) -> ((eval_term sigma (Cons (id1, v1) (Cons (id2, v2) pi))
t) = (eval_term sigma (Cons (id2, v2) (Cons (id1, v1) pi)) t)).
Axiom eval_swap : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (l:(list (ident* value)%type)) (id1:ident)
(id2:ident) (v1:value) (v2:value), (~ (id1 = id2)) -> ((eval_fmla sigma
(infix_plpl l (Cons (id1, v1) (Cons (id2, v2) pi))) f) <-> (eval_fmla sigma
(infix_plpl l (Cons (id2, v2) (Cons (id1, v1) pi))) f)).
Axiom eval_swap_2 : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (id1:ident) (id2:ident) (v1:value) (v2:value),
(~ (id1 = id2)) -> ((eval_fmla sigma (Cons (id1, v1) (Cons (id2, v2) pi))
f) <-> (eval_fmla sigma (Cons (id2, v2) (Cons (id1, v1) pi)) f)).
Axiom eval_term_change_free : forall (t:term) (sigma:(map mident value))
(pi:(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_term id
t) -> ((eval_term sigma (Cons (id, v) pi) t) = (eval_term sigma pi t)).
......@@ -465,7 +475,6 @@ simpl in *.
destruct d.
(* TYunit*)
destruct H0.
rewrite H in H1.
ae.
(* TYint *)
......
This source diff could not be displayed because it is too large. You can view the blob instead.
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