update proofs

examples/hoare_logic/blocking_semantics5.mlw

@@ -477,12 +477,26 @@ 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:
+lemma eval_swap_gen:
   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_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 ->
+    (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 ->

examples/hoare_logic/blocking_semantics5/blocking_semantics5_FreshVariables_eval_change_free_2.v

@@ -358,6 +358,10 @@ 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 (f:fmla),
   match f with
@@ -376,7 +380,8 @@ 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.
+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_3.v

@@ -348,16 +348,25 @@ 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.
+
 (* Why3 goal *)
 Theorem eval_change_free : forall (f:fmla),
   match f with
@@ -374,6 +383,8 @@ Theorem eval_change_free : forall (f:fmla),
       ((eval_fmla sigma pi f) -> (eval_fmla sigma (Cons (id, v) pi) f))
   end.
 destruct f; auto.
+ae.
+(*
 simpl.
 intros H sigma pi id v (H1 & H2) H3.
 destruct d.
@@ -403,6 +414,7 @@ intro b.
 pattern (Cons (i, Vbool b) (Cons (id, v) pi)); rewrite <- Append_nil_l.
 rewrite eval_swap; auto.
 simpl; apply H; auto.
+*)
 Qed.
 
 

examples/hoare_logic/blocking_semantics5/blocking_semantics5_FreshVariables_eval_change_free_4.v

@@ -354,10 +354,24 @@ Axiom eval_swap : forall (f:fmla) (sigma:(map mident value)) (pi:(list
   (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_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_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 (f:fmla),
   match f with
@@ -374,35 +388,8 @@ Theorem eval_change_free : forall (f:fmla),
       ((eval_fmla sigma (Cons (id, v) pi) f) -> (eval_fmla sigma pi f))
   end.
 destruct f; auto.
-simpl; intros.
-destruct H0.
-destruct d.
-
-(* Vvoid *)
-assert 
- (eval_fmla sigma (infix_plpl (Nil : (list (ident*value)))
-                  (Cons (i, Vvoid) (Cons (id, v) pi))) f =
- eval_fmla sigma (Cons (i, Vvoid) (Cons (id, v) pi)) f); auto.
-rewrite <- H3 in H1.
-rewrite eval_swap in H1; auto.
-simpl in H1.
-rewrite H in H1; auto.
-
-(* Vint *)
-intro n.
-rewrite <- (H _ _ id v); auto.
-replace (Cons (id, v) (Cons (i, Vint n) pi)) with
-  (infix_plpl (Nil : (list (ident*value)))
-  (Cons (id, v) (Cons (i, Vint n) pi))) by auto.
-rewrite eval_swap; auto.
-apply H1.
-
-(* Vbool *)
-intro b.
-rewrite <- (H _ _ id v); auto.
-pattern (Cons (id, v) (Cons (i, Vbool b) pi)); rewrite <- Append_nil_l.
-rewrite eval_swap; auto.
-apply H1.
+simpl; intros H sigma pi id v (h1 & h2).
+destruct d; intros; rewrite <- (H _ _ id v); ae.
 Qed.
 
 

examples/hoare_logic/blocking_semantics5/blocking_semantics5_FreshVariables_eval_swap_1.v

@@ -286,8 +286,8 @@ Axiom Cons_append : forall {a:Type} {a_WT:WhyType a}, forall (a1:a) (l1:(list
   a)) (l2:(list a)), ((Cons a1 (infix_plpl l1 l2)) = (infix_plpl (Cons a1 l1)
   l2)).
 
-Axiom Append_l_nil1 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
-  ((infix_plpl l (Nil :(list a))) = l).
+Axiom Append_nil_l : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  ((infix_plpl (Nil :(list a)) l) = l).
 
 Parameter msubst_term: term -> mident -> ident -> term.
 
@@ -374,13 +374,7 @@ Theorem eval_swap : forall (f:fmla),
   end.
 destruct f; auto.
 simpl; intros.
-destruct d.
-(* Void *)
-ae.
-(* Int *)
-intro; rewrite Cons_append; ae.
-(* Bool *)
-intro; rewrite Cons_append; ae.
+destruct d; intros; rewrite Cons_append; ae.
 Qed.
 
 

examples/hoare_logic/blocking_semantics5/blocking_semantics5_FreshVariables_eval_swap_2.v

@@ -286,8 +286,8 @@ Axiom Cons_append : forall {a:Type} {a_WT:WhyType a}, forall (a1:a) (l1:(list
   a)) (l2:(list a)), ((Cons a1 (infix_plpl l1 l2)) = (infix_plpl (Cons a1 l1)
   l2)).
 
-Axiom Append_l_nil1 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
-  ((infix_plpl l (Nil :(list a))) = l).
+Axiom Append_nil_l : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  ((infix_plpl (Nil :(list a)) l) = l).
 
 Parameter msubst_term: term -> mident -> ident -> term.
 
@@ -373,14 +373,8 @@ Theorem eval_swap : forall (f:fmla),
       f))
   end.
 destruct f; auto.
-intros.
-destruct d; simpl.
-(* Void *)
-ae.
-(* Int *)
-intro; rewrite Cons_append; ae.
-(* Bool *)
-intro; rewrite Cons_append; ae.
+simpl; intros.
+destruct d; intros; rewrite Cons_append; ae.
 Qed.
 
 

examples/hoare_logic/blocking_semantics5/blocking_semantics5_FreshVariables_eval_swap_2_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+
+(* Why3 assumption *)
+Inductive datatype  :=
+  | TYunit : datatype 
+  | TYint : datatype 
+  | TYbool : datatype .
+Axiom datatype_WhyType : WhyType datatype.
+Existing Instance datatype_WhyType.
+
+(* Why3 assumption *)
+Inductive value  :=
+  | Vvoid : value 
+  | Vint : Z -> value 
+  | Vbool : bool -> value .
+Axiom value_WhyType : WhyType value.
+Existing Instance value_WhyType.
+
+(* Why3 assumption *)
+Inductive operator  :=
+  | Oplus : operator 
+  | Ominus : operator 
+  | Omult : operator 
+  | Ole : operator .
+Axiom operator_WhyType : WhyType operator.
+Existing Instance operator_WhyType.
+
+Axiom mident : Type.
+Parameter mident_WhyType : WhyType mident.
+Existing Instance mident_WhyType.
+
+Axiom mident_decide : forall (m1:mident) (m2:mident), (m1 = m2) \/
+  ~ (m1 = m2).
+
+Axiom ident : Type.
+Parameter ident_WhyType : WhyType ident.
+Existing Instance ident_WhyType.
+
+Axiom ident_decide : forall (m1:ident) (m2:ident), (m1 = m2) \/ ~ (m1 = m2).
+
+(* Why3 assumption *)
+Inductive term  :=
+  | Tvalue : value -> term 
+  | Tvar : ident -> term 
+  | Tderef : mident -> term 
+  | Tbin : term -> operator -> term -> term .
+Axiom term_WhyType : WhyType term.
+Existing Instance term_WhyType.
+
+(* Why3 assumption *)
+Inductive fmla  :=
+  | Fterm : term -> fmla 
+  | Fand : fmla -> fmla -> fmla 
+  | Fnot : fmla -> fmla 
+  | Fimplies : fmla -> fmla -> fmla 
+  | Flet : ident -> term -> fmla -> fmla 
+  | Fforall : ident -> datatype -> fmla -> fmla .
+Axiom fmla_WhyType : WhyType fmla.
+Existing Instance fmla_WhyType.
+
+(* Why3 assumption *)
+Inductive stmt  :=
+  | Sskip : stmt 
+  | Sassign : mident -> term -> stmt 
+  | Sseq : stmt -> stmt -> stmt 
+  | Sif : term -> stmt -> stmt -> stmt 
+  | Sassert : fmla -> stmt 
+  | Swhile : term -> fmla -> stmt -> stmt .
+Axiom stmt_WhyType : WhyType stmt.
+Existing Instance stmt_WhyType.
+
+Axiom decide_is_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
+
+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).
+Existing Instance map_WhyType.
+
+Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  (map a b) -> a -> b.
+
+Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  (map a b) -> a -> b -> (map a b).
+
+Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
+  ((get (set m a1 b1) a2) = b1).
+
+Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
+  {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
+  forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
+
+Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  b -> (map a b).
+
+Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
+
+(* Why3 assumption *)
+Inductive list (a:Type) {a_WT:WhyType a} :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
+Existing Instance list_WhyType.
+Implicit Arguments Nil [[a] [a_WT]].
+Implicit Arguments Cons [[a] [a_WT]].
+
+(* Why3 assumption *)
+Definition env  := (map mident value).
+
+(* Why3 assumption *)
+Definition stack  := (list (ident* value)%type).
+
+Parameter get_stack: ident -> (list (ident* value)%type) -> value.
+
+Axiom get_stack_def : forall (i:ident) (pi:(list (ident* value)%type)),
+  match pi with
+  | Nil => ((get_stack i pi) = Vvoid)
+  | (Cons (x, v) r) => ((x = i) -> ((get_stack i pi) = v)) /\ ((~ (x = i)) ->
+      ((get_stack i pi) = (get_stack i r)))
+  end.
+
+Axiom get_stack_eq : forall (x:ident) (v:value) (r:(list (ident*
+  value)%type)), ((get_stack x (Cons (x, v) r)) = v).
+
+Axiom get_stack_neq : forall (x:ident) (i:ident) (v:value) (r:(list (ident*
+  value)%type)), (~ (x = i)) -> ((get_stack i (Cons (x, v) r)) = (get_stack i
+  r)).
+
+Parameter eval_bin: value -> operator -> value -> value.
+
+Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x,
+  y) with
+  | ((Vint x1), (Vint y1)) =>
+      match op with
+      | Oplus => ((eval_bin x op y) = (Vint (x1 + y1)%Z))
+      | Ominus => ((eval_bin x op y) = (Vint (x1 - y1)%Z))
+      | Omult => ((eval_bin x op y) = (Vint (x1 * y1)%Z))
+      | Ole => ((x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool true))) /\
+          ((~ (x1 <= y1)%Z) -> ((eval_bin x op y) = (Vbool false)))
+      end
+  | (_, _) => ((eval_bin x op y) = Vvoid)
+  end.
+
+(* Why3 assumption *)
+Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type))
+  (t:term) {struct t}: value :=
+  match t with
+  | (Tvalue v) => v
+  | (Tvar id) => (get_stack id pi)
+  | (Tderef id) => (get sigma id)
+  | (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
+      pi t2))
+  end.
+
+(* Why3 assumption *)
+Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type))
+  (f:fmla) {struct f}: Prop :=
+  match f with
+  | (Fterm t) => ((eval_term sigma pi t) = (Vbool true))
+  | (Fand f1 f2) => (eval_fmla sigma pi f1) /\ (eval_fmla sigma pi f2)
+  | (Fnot f1) => ~ (eval_fmla sigma pi f1)
+  | (Fimplies f1 f2) => (eval_fmla sigma pi f1) -> (eval_fmla sigma pi f2)
+  | (Flet x t f1) => (eval_fmla sigma (Cons (x, (eval_term sigma pi t)) pi)
+      f1)
+  | (Fforall x TYint f1) => forall (n:Z), (eval_fmla sigma (Cons (x,
+      (Vint n)) pi) f1)
+  | (Fforall x TYbool f1) => forall (b:bool), (eval_fmla sigma (Cons (x,
+      (Vbool b)) pi) f1)
+  | (Fforall x TYunit f1) => (eval_fmla sigma (Cons (x, Vvoid) pi) f1)
+  end.
+
+(* Why3 assumption *)
+Definition valid_fmla(p:fmla): Prop := forall (sigma:(map mident value))
+  (pi:(list (ident* value)%type)), (eval_fmla sigma pi p).
+
+(* Why3 assumption *)
+Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
+  -> (map mident value) -> (list (ident* value)%type) -> stmt -> Prop :=
+  | one_step_assign : forall (sigma:(map mident value)) (sigma':(map mident
+      value)) (pi:(list (ident* value)%type)) (x:mident) (t:term),
+      (sigma' = (set sigma x (eval_term sigma pi t))) -> (one_step sigma pi
+      (Sassign x t) sigma' pi Sskip)
+  | one_step_seq_noskip : forall (sigma:(map mident value)) (sigma':(map
+      mident value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
+      value)%type)) (s1:stmt) (s1':stmt) (s2:stmt), (one_step sigma pi s1
+      sigma' pi' s1') -> (one_step sigma pi (Sseq s1 s2) sigma' pi' (Sseq s1'
+      s2))
+  | one_step_seq_skip : forall (sigma:(map mident value)) (pi:(list (ident*
+      value)%type)) (s:stmt), (one_step sigma pi (Sseq Sskip s) sigma pi s)
+  | one_step_if_true : forall (sigma:(map mident value)) (pi:(list (ident*
+      value)%type)) (t:term) (s1:stmt) (s2:stmt), ((eval_term sigma pi
+      t) = (Vbool true)) -> (one_step sigma pi (Sif t s1 s2) sigma pi s1)
+  | one_step_if_false : forall (sigma:(map mident value)) (pi:(list (ident*
+      value)%type)) (t:term) (s1:stmt) (s2:stmt), ((eval_term sigma pi
+      t) = (Vbool false)) -> (one_step sigma pi (Sif t s1 s2) sigma pi s2)
+  | one_step_assert : forall (sigma:(map mident value)) (pi:(list (ident*
+      value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi
+      (Sassert f) sigma pi Sskip)
+  | one_step_while_true : forall (sigma:(map mident value)) (pi:(list (ident*
+      value)%type)) (cond:term) (inv:fmla) (body:stmt), ((eval_fmla sigma pi
+      inv) /\ ((eval_term sigma pi cond) = (Vbool true))) -> (one_step sigma
+      pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body)))
+  | one_step_while_false : forall (sigma:(map mident value)) (pi:(list
+      (ident* value)%type)) (cond:term) (inv:fmla) (body:stmt),
+      ((eval_fmla sigma pi inv) /\ ((eval_term sigma pi
+      cond) = (Vbool false))) -> (one_step sigma pi (Swhile cond inv body)
+      sigma pi Sskip).
+
+(* Why3 assumption *)
+Inductive many_steps : (map mident value) -> (list (ident* value)%type)
+  -> stmt -> (map mident value) -> (list (ident* value)%type) -> stmt
+  -> Z -> Prop :=
+  | many_steps_refl : forall (sigma:(map mident value)) (pi:(list (ident*
+      value)%type)) (s:stmt), (many_steps sigma pi s sigma pi s 0%Z)
+  | many_steps_trans : forall (sigma1:(map mident value)) (sigma2:(map mident
+      value)) (sigma3:(map mident value)) (pi1:(list (ident* value)%type))
+      (pi2:(list (ident* value)%type)) (pi3:(list (ident* value)%type))
+      (s1:stmt) (s2:stmt) (s3:stmt) (n:Z), (one_step sigma1 pi1 s1 sigma2 pi2
+      s2) -> ((many_steps sigma2 pi2 s2 sigma3 pi3 s3 n) ->
+      (many_steps sigma1 pi1 s1 sigma3 pi3 s3 (n + 1%Z)%Z)).
+
+Axiom steps_non_neg : forall (sigma1:(map mident value)) (sigma2:(map mident
+  value)) (pi1:(list (ident* value)%type)) (pi2:(list (ident* value)%type))
+  (s1:stmt) (s2:stmt) (n:Z), (many_steps sigma1 pi1 s1 sigma2 pi2 s2 n) ->
+  (0%Z <= n)%Z.
+
+(* Why3 assumption *)
+Definition reductible(sigma:(map mident value)) (pi:(list (ident*
+  value)%type)) (s:stmt): Prop := exists sigma':(map mident value),
+  exists pi':(list (ident* value)%type), exists s':stmt, (one_step sigma pi s
+  sigma' pi' s').
+
+(* 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))