eval_swap proof

examples/hoare_logic/blocking_semantics3.mlw

@@ -6,7 +6,7 @@
 theory ImpExpr
 
 use import int.Int
-use import int.MinMaxw
+use import int.MinMax
 use import bool.Bool
 use export list.List
 use export list.Append
@@ -295,23 +295,12 @@ lemma fresh_in_binop:
     fresh_in_term v (mk_tbin t op t') ->
       fresh_in_term v t  /\ fresh_in_term v t'
  
-lemma eval_msubst_term:
-  forall e:term, sigma:env, pi:stack, x:mident, v:ident.
-    fresh_in_term v e ->
-    eval_term sigma pi (msubst_term e x v) =
-    eval_term (IdMap.set sigma x (get_stack v pi)) pi e
-
 (* lemma eval_subst_term: *)
 (*   forall sigma:env, pi:stack, e:term, x:ident, v:ident. *)
 (*     fresh_in_term v e -> *)
 (*     eval_term sigma pi (subst_term e x v) = *)
 (*     eval_term sigma (Cons (x, (get_stack v pi)) pi) e *)
 
-lemma eval_term_change_free :
-  forall t:term, sigma:env, pi:stack, id:ident, v:value.
-    fresh_in_term id t ->
-    eval_term sigma (Cons (id,v) pi) t = eval_term sigma pi t
-
 predicate fresh_in_fmla (id:ident) (f:fmla) =
   match f with
   | Fterm e -> fresh_in_term id e
@@ -342,6 +331,10 @@ function msubst (f:fmla) (x:mident) (v:ident) : fmla =
   | Fforall y ty f -> Fforall y ty (msubst f x v)
   end
 
+lemma subst_fresh_term :
+  forall t:term, x:ident, v:ident.
+   fresh_in_term x t -> subst_term t x v = t
+
 lemma subst_fresh :
   forall f:fmla, x:ident, v:ident.
    fresh_in_fmla x f -> subst f x v = f
@@ -351,6 +344,12 @@ lemma subst_fresh :
 (*     forall t:term, f:fmla, x id':ident, id :mident. *)
 (*     msubst (Flet x t f) id id' = Flet x (msubst_term t id id') (msubst f id id') *)
 
+lemma eval_msubst_term:
+  forall e:term, sigma:env, pi:stack, x:mident, v:ident.
+    fresh_in_term v e ->
+    eval_term sigma pi (msubst_term e x v) =
+    eval_term (IdMap.set sigma x (get_stack v pi)) pi e
+
 (* Need it for monotonicity and wp_reduction *)
 lemma eval_msubst:
   forall f:fmla, sigma:env, pi:stack, x:mident, v:ident.
@@ -374,7 +373,7 @@ lemma eval_msubst:
 (*     eval_fmla sigma (Cons (id,v1) (Cons (id,v2) pi)) f <-> *)
 (*     eval_fmla sigma (Cons (id,v1) pi) f *)
 
-lemma eval_swap_term_any:
+lemma eval_swap_term:
 forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
 id1 <> id2 ->
 (eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
@@ -386,17 +385,22 @@ eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)
 (*     (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_any:
+lemma eval_swap:
   forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
     id1 <> id2 ->
     (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: *)
-(*   forall f:fmla, sigma:env, pi:stack, id1 id2:ident, v1 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) *)
+lemma eval_swap:
+  forall f:fmla, sigma:env, pi:stack, id1 id2:ident, v1 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)
+
+lemma eval_term_change_free :
+  forall t:term, sigma:env, pi:stack, id:ident, v:value.
+    fresh_in_term id t ->
+    eval_term sigma (Cons (id,v) pi) t = eval_term sigma pi t
 
  (* Need it for monotonicity*)
 lemma eval_change_free :

examples/hoare_logic/blocking_semantics3/blocking_semantics3_ImpExpr_eval_msubst_term_1.v

@@ -426,7 +426,6 @@ rewrite H1.
 rewrite H2; auto.
 apply fresh_in_binop with (t:=t) (t':=t') (op := op).
 apply fresh_in_binop with (t:=t) (t':=t') (op := op).
-admit.
 Qed.
 
 

examples/hoare_logic/blocking_semantics3/blocking_semantics3_ImpExpr_eval_swap_1.v

@@ -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,34 +409,31 @@ 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_same_var_term : forall (t:term) (sigma:(map mident value))
-  (pi:(list (ident* value)%type)) (id:ident) (v1:value) (v2:value),
-  ((eval_term sigma (Cons (id, v1) (Cons (id, v2) pi)) t) = (eval_term sigma
-  (Cons (id, v1) pi) t)).
-
-Axiom eval_same_var : forall (f:fmla) (sigma:(map mident value)) (pi:(list
-  (ident* value)%type)) (id:ident) (v1:value) (v2:value), (eval_fmla sigma
-  (Cons (id, v1) (Cons (id, v2) pi)) f) <-> (eval_fmla sigma (Cons (id, v1)
-  pi) f).
-
 Axiom eval_swap_term : 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_any : 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)).
+  (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)).
+
+Require Import Why3.
+
+Ltac ae := why3 "alt-ergo" timelimit 3.
 
 (* Why3 goal *)
 Theorem eval_swap : forall (f:fmla),
@@ -454,42 +442,42 @@ Theorem eval_swap : forall (f:fmla),
   | (Fand f1 f2) => True
   | (Fnot f1) => True
   | (Fimplies f1 f2) => True
-  | (Flet i t f1) => (forall (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)) f1) <-> (eval_fmla sigma (Cons (id2, v2) (Cons (id1, v1) pi))
+  | (Flet i t f1) => True
+  | (Fforall i d f1) => (forall (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))) f1) <->
+      (eval_fmla sigma (infix_plpl l (Cons (id2, v2) (Cons (id1, v1) pi)))
       f1))) -> forall (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))
-  | (Fforall i d f1) => True
+      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))
   end.
 destruct f; auto.
-intros H sigma pi id1 id2 v1 v2 H1 H2.
-simpl in *.
-rewrite eval_swap_term in H2; auto.
-destruct (ident_decide i id2).
-(* i = id1*)
-subst.
-apply H in H2; auto.
-destruct (ident_decide i id1).
-(* i = id1*)
-subst.
-apply H; auto.
-
-
-
+intros.
 simpl in *.
-rewrite eval_swap_term in H2; auto.
-apply eval_same_var.
-
-
-
-
- eval_same_var_term.
-
-(* i <> id2*)
-
+assert (h: forall (l1 l2 : list (ident*value)) (a : (ident*value)), 
+   (Cons a (infix_plpl l1 l2)) = (infix_plpl (Cons a l1) l2)).
+intros.
+induction l1.
+simpl; auto.
+simpl; auto.
+destruct d; auto.
+(* Void *)
+ae.
+(*rewrite h.
+rewrite h in H1.
+apply H; auto.*)
+(* Int *)
+intros.
+rewrite h.
+ae.
+(* Bool *)
+intros.
+rewrite h.
+ae.
 Qed.
 
 

examples/hoare_logic/blocking_semantics3/blocking_semantics3_ImpExpr_eval_swap_2.v

@@ -14,6 +14,53 @@ Existing Instance list_WhyType.
 Implicit Arguments Nil [[a] [a_WT]].
 Implicit Arguments Cons [[a] [a_WT]].
 
+(* Why3 assumption *)
+Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list
+  a)) {struct l1}: (list a) :=
+  match l1 with
+  | Nil => l2
+  | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
+  end.
+
+Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
+  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
+
+Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  ((infix_plpl l (Nil :(list a))) = l).
+
+(* Why3 assumption *)
+Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil => 0%Z
+  | (Cons _ r) => (1%Z + (length r))%Z
+  end.
+
+Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
+  a)), (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil :(list a))).
+
+Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)), ((length (infix_plpl l1
+  l2)) = ((length l1) + (length l2))%Z).
+
+(* Why3 assumption *)
+Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+
+Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
+  a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
+  l2)).
+
+Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
+  a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
+  (l = (infix_plpl l1 (Cons x l2))).
+
 Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
 Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
   (b:Type) {b_WT:WhyType b}, WhyType (map a b).
@@ -328,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
@@ -371,28 +409,31 @@ 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_same_var_term : forall (t:term) (sigma:(map mident value))
-  (pi:(list (ident* value)%type)) (id:ident) (v1:value) (v2:value),
-  ((eval_term sigma (Cons (id, v1) (Cons (id, v2) pi)) t) = (eval_term sigma
-  (Cons (id, v1) pi) t)).
+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_same_var : forall (f:fmla) (sigma:(map mident value)) (pi:(list
-  (ident* value)%type)) (id:ident) (v1:value) (v2:value), (eval_fmla sigma
-  (Cons (id, v1) (Cons (id, v2) pi)) f) <-> (eval_fmla sigma (Cons (id, v1)
-  pi) f).
+Require Import Why3.
 
-Axiom eval_swap_term : 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)).
+Ltac ae := why3 "alt-ergo" timelimit 3.
 
 (* Why3 goal *)
 Theorem eval_swap : forall (f:fmla),
@@ -403,26 +444,40 @@ Theorem eval_swap : forall (f:fmla),
   | (Fimplies f1 f2) => True
   | (Flet i t f1) => True
   | (Fforall i d f1) => (forall (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)) f1) <-> (eval_fmla sigma (Cons (id2, v2) (Cons (id1, v1) pi))
+      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))) f1) <->
+      (eval_fmla sigma (infix_plpl l (Cons (id2, v2) (Cons (id1, v1) pi)))
       f1))) -> forall (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))
+      value)%type)) (l:(list (ident* value)%type)) (id1:ident) (id2:ident)
+      (v1:value) (v2:value), (~ (id1 = id2)) -> ((eval_fmla sigma
+      (infix_plpl l (Cons (id2, v2) (Cons (id1, v1) pi))) f) ->
+      (eval_fmla sigma (infix_plpl l (Cons (id1, v1) (Cons (id2, v2) pi)))
+      f))
   end.
 destruct f; auto.
-intros H_induc sigma pi id1 id2 v1 v2 H H1.
+intros.
 simpl in *.
-destruct d.
-
-(* i : TYunit*)
-
-(* i : TYint*)
-
-(* i : TYbool*)
-
-
+assert (h: forall (l1 l2 : list (ident*value)) (a : (ident*value)), 
+   (Cons a (infix_plpl l1 l2)) = (infix_plpl (Cons a l1) l2)).
+intros.
+induction l1.
+simpl; auto.
+simpl; auto.
+destruct d; auto.
+(* Void *)
+ae.
+(*rewrite h.
+rewrite h in H1.
+apply H; auto.*)
+(* Int *)
+intros.
+rewrite h.
+ae.
+(* Bool *)
+intros.
+rewrite h.
+ae.
 Qed.