Changeset 3591 for LTS


Ignore:
Timestamp:
Jul 20, 2015, 7:08:44 PM (4 years ago)
Author:
piccolo
Message:

stared pass stack to monostack, closed the first three proof obbligations of simulation conditions

Location:
LTS
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3563 r3591  
    829829[ #st #l #prf  #t' normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
    830830#s1 #s2 #s3 #l1 #prf1 #t2 #l2 #prf2 #t3 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    831 qed.
    832 
    833 let rec chop (A : Type[0]) (l : list A) on l : list A ≝
    834 match l with
    835 [ nil ⇒ nil ?
    836 | cons x xs ⇒ match xs with [ nil ⇒ nil ? | cons _ _ ⇒ x :: chop … xs]
    837 ].
    838 
    839 lemma chop_append_singleton : ∀A : Type[0].∀x : A.∀l : list A.chop ? (l@ [x]) = l.
    840 #A #x #l elim l normalize // #y * normalize //
    841 qed.
    842 
    843 lemma chop_mem : ∀A : Type[0].∀x : A.∀l : list A. mem … x (chop ? l) → mem … x l.
    844 #A #x #l elim l [*] #y * [ normalize /2/] #z #zs #IH * [/2/] /3/
    845831qed.
    846832
  • LTS/stack_monostack_pass.ma

    r3574 r3591  
    2727λst1,st2.mono_env_store_rel (\fst st1) (\fst st2) (\fst (\snd st2)) ∧ (\snd (\snd st1)) = (\snd (\snd st2)).
    2828
     29definition mono_state_rel ≝
     30λs1 : state stack_state_params.λs2 : state mono_stack_state_params.
     31mono_store_rel … (store … s1) (store … s2) ∧ code … s1 = code … s2 ∧ cont … s1 = cont … s2
     32∧ io_info … s1 = io_info … s2.
     33
    2934definition mono_stack_relations :
    3035∀prog : Program stack_env_params stack_instr_params flat_labels.∀bound.
     
    3338(operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog) ≝
    3439λprog.λbound.
    35 mk_relations … (λs1,s2.mono_store_rel … (store … s1) (store … s2) ∧ code … s1 = code … s2 ∧ cont … s1 = cont … s2)
     40mk_relations … mono_state_rel
    3641  (λ_.λ_.True).
    3742
     
    6974qed.
    7075
     76lemma update_frame_ok :
     77∀st1,st2,fp,env,x,val,new_env.
     78mono_env_store_rel (env :: st1) st2 fp →
     79assign_frame env (to_shift + x) O val = return new_env →
     80∃new_st.
     81assign_frame st2 (to_shift + x) fp val = return new_st ∧
     82mono_env_store_rel (new_env :: st1) new_st fp.
     83#st1 #st2 #fp #env #x #val #new_env * #old_fp * #s11 * #s22 *** #EQ1 #EQ2 destruct
     84#Hrel #EQ destruct change with (update ????) in ⊢ (??%? → ?); #EQnew_env
     85%{(new_env @ s22)} %
     86[2: %{old_fp} %{(chop … new_env)} %{s22} % // % // % xxxxxx
     87qed.
     88
     89lemma list_n_plus : ∀A,a,n,m.list_n A a (n +m) = list_n A a n @ list_n A a m.
     90#A #a #n elim n // -n #m #IH #m whd in ⊢ (??%%); @eq_f @IH
     91qed.
     92
     93lemma stack_initial_mono_initial : ∀prog,bound.
     94∀s1.∀s2.
     95bool_to_Prop (lang_initial ? (stack_sem_state_params bound) prog s1) →
     96bool_to_Prop (lang_initial ? (mono_stack_sem_state_params bound) prog s2) →
     97mono_state_rel s1 s2.
     98#prog #bound #s1 #s2 whd in match lang_initial; normalize nodelta @eq_instructions_elim #EQcode_s1 [2: *]
     99@eqb_list_elim #EQcont_s1 [2: *] inversion(?==?) normalize nodelta #EQstore_s1 [2: *] normalize nodelta
     100whd in ⊢ (?% → ?); #Hio_s1 @eq_instructions_elim #EQcode_s2 [2: *] @eqb_list_elim #EQcont_s2 [2: *]
     101inversion(?==?) #EQstore_s2 [2: *] whd in ⊢ (?% → ?); #Hio_s2 % [2: >Hio_s1 >Hio_s2 %]
     102% [2: >EQcont_s1 >EQcont_s2 %] % [2: >EQcode_s1 >EQcode_s2 %] >(\P EQstore_s1) >(\P EQstore_s2)
     103% // whd whd in match (init_store ??); %{O} %{(list_n … O (pred (to_shift + bound)))}
     104%{[ ]} % // % // %
     105[ >append_nil ] change with (list_n ? O 1) in match ([0]); <list_n_plus <(commutative_plus … 1) %
     106qed.
     107
     108lemma stack_final_mono_final : ∀s1,s2.mono_state_rel s1 s2 →
     109bool_to_Prop(lang_final … s1) → bool_to_Prop (lang_final … s2).
     110#s1 #s2 #REL whd in match lang_final; normalize nodelta @eq_instructions_elim #EQcode_s1 [2: *]
     111inversion(cont … s1) [2: #z #zs #_ #_ *] #EQcont_s1 * @andb_Prop
     112cases REL ** #_ >EQcode_s1 #EQcode_s2 >EQcont_s1 #EQcont_s2 #_ [ <EQcode_s2 % | <EQcont_s2 %]
     113qed.
     114
     115lemma var_io_is_stack_io :∀s1,s2.mono_state_rel s1 s2 → lang_classify ? s2 = cl_io → lang_classify ? s1 = cl_io.
     116#s1 #s2 *** #_ #EQcode #_ #Hio whd in ⊢ (??%? → ??%?); >EQcode cases(code ??)
     117[| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     118    #lin *]
     119normalize nodelta #EQ destruct >Hio //
     120qed.
     121
     122
     123
     124
    71125definition stack_mono_stack_simulation : ∀prog : Program stack_env_params stack_instr_params flat_labels.∀bound.
    72126simulation_conditions … (mono_stack_relations prog bound) ≝λprog.λbound.mk_simulation_conditions ….
  • LTS/utils.ma

    r3579 r3591  
    398398| cons x xs ⇒ match l2 with [nil ⇒ False | cons y ys ⇒ f x y ∧ All2 … f xs ys]
    399399].
     400
     401(* chop *)
     402
     403let rec chop (A : Type[0]) (l : list A) on l : list A ≝
     404match l with
     405[ nil ⇒ nil ?
     406| cons x xs ⇒ match xs with [ nil ⇒ nil ? | cons _ _ ⇒ x :: chop … xs]
     407].
     408
     409lemma chop_append_singleton : ∀A : Type[0].∀x : A.∀l : list A.chop ? (l@ [x]) = l.
     410#A #x #l elim l normalize // #y * normalize //
     411qed.
     412
     413lemma chop_mem : ∀A : Type[0].∀x : A.∀l : list A. mem … x (chop ? l) → mem … x l.
     414#A #x #l elim l [*] #y * [ normalize /2/] #z #zs #IH * [/2/] /3/
     415qed.
Note: See TracChangeset for help on using the changeset viewer.