Changeset 3563 for LTS/frame_variable_pass.ma

Timestamp:

Jun 16, 2015, 4:00:03 PM (5 years ago)

Author:

sacerdot

Message:

bind_inversion on Opt moved to utils + some progress

File:

• LTS/frame_variable_pass.ma (modified) (3 diffs)

LTS/frame_variable_pass.ma

@@ -15 +15 @@
 include "Simulation.ma".
 include "variable.ma".
+include alias "arithmetics/nat.ma".
 
 definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ 
@@ -61 +62 @@
 ].
 
+definition environment_rel : (variable → variable) → environment → activation_frame → Prop ≝ 
+λmap,st1,st2.
+ All … (λx.let 〈v,val〉 ≝ x in read_frame … st2 (to_shift + (map v)) O = return val)
+  st1.
+
 definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝ 
 λmap,st1,st2.
-All2 … (λel1,el2.\snd el1 = \snd el2 ∧ All … (λx.let 〈v,val〉 ≝ x in read_frame … (\fst el2) (to_shift + (map v)) O = return val) 
-       (\fst el1)) st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
+All2 … (λel1,el2.\snd el1 = \snd el2 ∧ environment_rel map (\fst el1) (\fst el2))
+ st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
 
 definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels → 
@@ -84 +90 @@
 cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) (cont … s1))
 (λ_.λ_.True).
+
+lemma eval_cond_ok:
+ ∀m: variable → variable.
+  ∀e: expr.
+  let e' ≝ map_exp e m in
+   ∀env: environment.
+    ∀env': activation_frame.
+     environment_rel m env env' →
+      ∀val.
+       sem_expr env e = Some … val →
+        frame_sem_expr env' e' = Some … val.
+ #m #e elim e
+ [ #v #env elim env
+   [ #env' #_ #val #abs normalize in abs; destruct
+   | * #var #val #tl #IH #env' * #RF #Htl #val'
+     whd in ⊢ (??%? → ?); inversion (?==?) #Hv_var normalize nodelta
+     [ #Hval_val' destruct >(\P Hv_var) assumption
+     | #Hread_tl @IH // assumption ]]
+ | normalize //
+ |*: #e1 #e2 #IH1 #IH2 #env #env' #Rel #v
+   change with (!x ← ?; ? = return ?) in match (sem_expr ?? = Some ??);
+   #H cases (bind_inversion ????? H) -H #v1 * #He1
+   #H cases (bind_inversion ????? H) -H #v2 * #He2
+   #H normalize in H; destruct
+   change with (m_bind ?????) in ⊢ (??%?);
+   >(IH1 … He1) // >(IH2 … He2) // ]
+qed.
 
 definition simulation_imp_frame ≝