improved proof

examples/hoare_logic/blocking_semantics5/blocking_semantics5_FreshVariables_eval_msubst_2.v

@@ -202,14 +202,14 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
       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))))
+      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)).
+      ((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)
@@ -230,7 +230,7 @@ Axiom steps_non_neg : forall (sigma1:(map mident value)) (sigma2:(map mident
   (0%Z <= n)%Z.
 
 (* Why3 assumption *)
-Definition reducible(sigma:(map mident value)) (pi:(list (ident*
+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').
@@ -282,13 +282,35 @@ 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))).
 
+Parameter msubst_term: term -> mident -> ident -> term.
+
+Axiom msubst_term_def : forall (t:term) (x:mident) (v:ident),
+  match t with
+  | ((Tvalue _)|(Tvar _)) => ((msubst_term t x v) = t)
+  | (Tderef y) => ((x = y) -> ((msubst_term t x v) = (Tvar v))) /\
+      ((~ (x = y)) -> ((msubst_term t x v) = t))
+  | (Tbin t1 op t2) => ((msubst_term t x v) = (Tbin (msubst_term t1 x v) op
+      (msubst_term t2 x v)))
+  end.
+
+(* Why3 assumption *)
+Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
+  match f with
+  | (Fterm e) => (Fterm (msubst_term e x v))
+  | (Fand f1 f2) => (Fand (msubst f1 x v) (msubst f2 x v))
+  | (Fnot f1) => (Fnot (msubst f1 x v))
+  | (Fimplies f1 f2) => (Fimplies (msubst f1 x v) (msubst f2 x v))
+  | (Flet y t f1) => (Flet y (msubst_term t x v) (msubst f1 x v))
+  | (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
+  end.
+
 (* Why3 assumption *)
-Fixpoint fresh_in_term(x:ident) (t:term) {struct t}: Prop :=
+Fixpoint fresh_in_term(id:ident) (t:term) {struct t}: Prop :=
   match t with
   | (Tvalue _) => True
-  | (Tvar i) => ~ (x = i)
+  | (Tvar i) => ~ (id = i)
   | (Tderef _) => True
-  | (Tbin t1 _ t2) => (fresh_in_term x t1) /\ (fresh_in_term x t2)
+  | (Tbin t1 _ t2) => (fresh_in_term id t1) /\ (fresh_in_term id t2)
   end.
 
 (* Why3 assumption *)
@@ -303,28 +325,6 @@ Fixpoint fresh_in_fmla(id:ident) (f:fmla) {struct f}: Prop :=
   | (Fforall y ty f1) => (~ (id = y)) /\ (fresh_in_fmla id f1)
   end.
 
-Parameter msubst_term: term -> mident -> ident -> term.
-
-Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
-  match t with
-  | ((Tvalue _)|(Tvar _)) => ((msubst_term t r v) = t)
-  | (Tderef x) => ((r = x) -> ((msubst_term t r v) = (Tvar v))) /\
-      ((~ (r = x)) -> ((msubst_term t r v) = t))
-  | (Tbin t1 op t2) => ((msubst_term t r v) = (Tbin (msubst_term t1 r v) op
-      (msubst_term t2 r v)))
-  end.
-
-(* Why3 assumption *)
-Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
-  match f with
-  | (Fterm e) => (Fterm (msubst_term e x v))
-  | (Fand f1 f2) => (Fand (msubst f1 x v) (msubst f2 x v))
-  | (Fnot f1) => (Fnot (msubst f1 x v))
-  | (Fimplies f1 f2) => (Fimplies (msubst f1 x v) (msubst f2 x v))
-  | (Flet y t f1) => (Flet y (msubst_term t x v) (msubst f1 x v))
-  | (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
-  end.
-
 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
@@ -349,13 +349,7 @@ Theorem eval_msubst : forall (f:fmla),
       (get_stack v pi)) pi f))
   end.
 destruct f; auto.
-simpl.
-intros.
-destruct H0.
-destruct d.
-ae.
-ae.
-ae.
+simpl; ae.
 Qed.