update proofs

examples/hoare_logic/blocking_semantics5.mlw

@@ -483,14 +483,6 @@ lemma eval_swap_gen:
     (eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
     eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)
 
-(*
-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:stack, id1 id2:ident, v1 v2:value.
     id1 <> id2 ->

examples/hoare_logic/blocking_semantics5/blocking_semantics5_FreshVariables_eval_change_free_1.v

@@ -348,12 +348,17 @@ 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 : forall (f:fmla) (sigma:(map mident value)) (pi:(list
+Axiom eval_swap_gen : 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 : 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)).
@@ -379,7 +384,6 @@ Theorem eval_change_free : forall (f:fmla),
 destruct f; auto.
 simpl; intros H sigma pi id v (h1 & h2 & h3) h.
 rewrite eval_term_change_free; auto.
-pattern (Cons (i, eval_term sigma pi t) (Cons (id, v) pi)); rewrite <- Append_nil_l.
 rewrite eval_swap; auto.
 apply H; auto.
 Qed.

examples/hoare_logic/blocking_semantics5/blocking_semantics5_FreshVariables_eval_change_free_2.v

@@ -348,17 +348,21 @@ 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 : forall (f:fmla) (sigma:(map mident value)) (pi:(list
+Axiom eval_swap_gen : 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 : 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.
 
@@ -380,8 +384,6 @@ Theorem eval_change_free : forall (f:fmla),
 destruct f; auto.
 simpl; intros H sigma pi id v (h1 & h2 & h3).
 rewrite eval_term_change_free; auto.
-pattern (Cons (i, eval_term sigma pi t) (Cons (id, v) pi)).
-rewrite <- Append_nil_l.
 rewrite eval_swap; auto.
 apply H; auto.
 Qed.

examples/hoare_logic/blocking_semantics5/blocking_semantics5_FreshVariables_eval_swap_gen_2.v

@@ -348,6 +348,9 @@ 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)).
 
+Require Import Why3.
+Ltac ae := why3 "alt-ergo" timelimit 3.
+
 (* Why3 goal *)
 Theorem eval_swap_gen : forall (f:fmla),
   match f with
@@ -368,18 +371,8 @@ Theorem eval_swap_gen : forall (f:fmla),
       (eval_fmla sigma (infix_plpl l (Cons (id1, v1) (Cons (id2, v2) pi)))
       f))
   end.
-intros f.
-
-Qed.
-
-
-Require Import Why3.
-
-Ltac ae := why3 "alt-ergo" timelimit 3.
-
-(* Unused content named eval_swap
 destruct f; auto.
 simpl; intros.
 destruct d; intros; rewrite Cons_append; ae.
 Qed.
- *)
+