Changeset 3563 for LTS


Ignore:
Timestamp:
Jun 16, 2015, 4:00:03 PM (4 years ago)
Author:
sacerdot
Message:

bind_inversion on Opt moved to utils + some progress

Location:
LTS
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3552 r3563  
    33include "../src/utilities/option.ma".
    44include "basics/jmeq.ma".
    5 
    6 lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
    7 ∀f : A → option B.∀y : B.
    8 ! x ← m; f x = return y →
    9 ∃ x.(m = return x) ∧ (f x = return y).
    10 #A #B * [| #a] #f #y normalize #EQ [destruct]
    11 %{a} %{(refl …)} //
    12 qed.
    135
    146record assembler_params : Type[1] ≝
  • LTS/frame_variable_pass.ma

    r3561 r3563  
    1515include "Simulation.ma".
    1616include "variable.ma".
     17include alias "arithmetics/nat.ma".
    1718
    1819definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝
     
    6162].
    6263
     64definition environment_rel : (variable → variable) → environment → activation_frame → Prop ≝
     65λmap,st1,st2.
     66 All … (λx.let 〈v,val〉 ≝ x in read_frame … st2 (to_shift + (map v)) O = return val)
     67  st1.
     68
    6369definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝
    6470λmap,st1,st2.
    65 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)
    66        (\fst el1)) st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
     71All2 … (λel1,el2.\snd el1 = \snd el2 ∧ environment_rel map (\fst el1) (\fst el2))
     72 st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
    6773
    6874definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels →
     
    8490cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) (cont … s1))
    8591(λ_.λ_.True).
     92
     93lemma eval_cond_ok:
     94 ∀m: variable → variable.
     95  ∀e: expr.
     96  let e' ≝ map_exp e m in
     97   ∀env: environment.
     98    ∀env': activation_frame.
     99     environment_rel m env env' →
     100      ∀val.
     101       sem_expr env e = Some … val →
     102        frame_sem_expr env' e' = Some … val.
     103 #m #e elim e
     104 [ #v #env elim env
     105   [ #env' #_ #val #abs normalize in abs; destruct
     106   | * #var #val #tl #IH #env' * #RF #Htl #val'
     107     whd in ⊢ (??%? → ?); inversion (?==?) #Hv_var normalize nodelta
     108     [ #Hval_val' destruct >(\P Hv_var) assumption
     109     | #Hread_tl @IH // assumption ]]
     110 | normalize //
     111 |*: #e1 #e2 #IH1 #IH2 #env #env' #Rel #v
     112   change with (!x ← ?; ? = return ?) in match (sem_expr ?? = Some ??);
     113   #H cases (bind_inversion ????? H) -H #v1 * #He1
     114   #H cases (bind_inversion ????? H) -H #v2 * #He2
     115   #H normalize in H; destruct
     116   change with (m_bind ?????) in ⊢ (??%?);
     117   >(IH1 … He1) // >(IH2 … He2) // ]
     118qed.
    86119
    87120definition simulation_imp_frame ≝
  • LTS/utils.ma

    r3554 r3563  
    1717include "../src/ASM/Util.ma".
    1818include "../src/utilities/option.ma".
     19
     20lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
     21∀f : A → option B.∀y : B.
     22! x ← m; f x = return y →
     23∃ x.(m = return x) ∧ (f x = return y).
     24#A #B * [| #a] #f #y normalize #EQ [destruct]
     25%{a} %{(refl …)} //
     26qed.
    1927
    2028(*NO DUPLICATES in lists*)
Note: See TracChangeset for help on using the changeset viewer.