Changeset 3574 for LTS/stack_monostack_pass.ma
 Timestamp:
 Jun 18, 2015, 6:33:00 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/stack_monostack_pass.ma
r3572 r3574 20 20 [ nil ⇒ s2 = nil ? 21 21  cons x xs ⇒ ∃old_fp,s21,s22.s2 = s21 @ [old_fp] @ s22 ∧ 22 match x with [ nil ⇒ False  cons y ys ⇒ ys = s21] ∧22 x= s21 @ [O] ∧ 23 23 mono_env_store_rel xs s22 old_fp ∧ s22 = fp 24 24 ]. … … 35 35 mk_relations … (λs1,s2.mono_store_rel … (store … s1) (store … s2) ∧ code … s1 = code … s2 ∧ cont … s1 = cont … s2) 36 36 (λ_.λ_.True). 37 37 38 lemma minus_right_cancellable : ∀n,m,p : ℕ.n = m → np = m p. // 39 qed. 40 41 42 lemma read_frame_ok : 43 ∀st1,st2,fp,env,x,n. 44 mono_env_store_rel st1 st2 fp → option_hd … st1 = return env → 45 to_shift + x < env → 46 read_frame env (to_shift+x) O = return n → 47 read_frame st2 (to_shift+x) fp = return n. 48 #st1 elim st1 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in H7; destruct] 49 #env #tl #IH #st2 #fp #env' #x #n * #old_fp * #s21 * #s22 *** #EQ1 #EQ2 destruct #H #EQ destruct 50 whd in ⊢ (??%% → ?); #EQ destruct #H1 51 change with (nth_opt ???) in ⊢ (??%? → ?); <minus_n_O >length_append normalize in ⊢ (??(??%?)? → ?); 52 >nth_first 53 [2: normalize >minus_minus_comm >commutative_plus <(plus_minus … 1) // normalize <(minus_Sn_m … (S (S x))) 54 [2: >length_append in H1; normalize >(commutative_plus) normalize /2/] 55 normalize /2/ 56 ] 57 #H2 change with (nth_opt ???) in ⊢ (??%?); >nth_first 58 [2: >length_append >length_append normalize <plus_n_Sm normalize <(minus_minus_comm ? (s22)) 59 >commutative_plus <(plus_minus … (s22)) [2: //] <minus_n_n normalize >minus_plus <(minus_Sn_m … (S x +1)) 60 [2: normalize >commutative_plus normalize normalize in H1; >length_append in H1; normalize >commutative_plus 61 normalize /2/ ] 62 <commutative_plus normalize /2/ 63 ] 64 >length_append >length_append 65 cut((s21+([old_fp]+s22)(to_shift+x)s221) = (s21+1S (S x)1)) 66 [ normalize @minus_right_cancellable >minus_minus_comm >commutative_plus <(plus_minus … (s22)) [2: //] 67 <(minus_Sn_n … (s22)) >commutative_plus % 68 ] #EQ >EQ assumption 69 qed. 70 38 71 definition stack_mono_stack_simulation : ∀prog : Program stack_env_params stack_instr_params flat_labels.∀bound. 39 72 simulation_conditions … (mono_stack_relations prog bound) ≝λprog.λbound.mk_simulation_conditions …. 73 (*[4: #s1 #s2 #s1' #H inversion H 74 [ #st1 #st2 * #lab #instr #tl #EQcode_st1 #EQcond_st1 #EQ1 #EQ2 destruct #EQstore *) 40 75 cases daemon 41 76 qed.
Note: See TracChangeset
for help on using the changeset viewer.