Changeset 3565
 Timestamp:
 Jun 16, 2015, 7:13:10 PM (4 years ago)
 Location:
 LTS
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

LTS/stack.ma
r3562 r3565 105 105 push s n 106 106  push_const n ⇒ push s n 107  push_plus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val 1 + val2)108  push_minus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val 1  val2)109  push_eq ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (if eqb val 1 val2then 1 else O)107  push_plus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val2 + val1) 108  push_minus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val2  val1) 109  push_eq ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (if eqb val2 val1 then 1 else O) 110 110  push_not ⇒ ! 〈val1,st1〉 ← pop s;push st1 (1val1) 111 111 ]. 
LTS/variable_stack_pass.ma
r3562 r3565 72 72 (λ_.λ_.True). 73 73 74 let rec expr_fv (e : expr) on e : list variable ≝ 75 match e with 76 [ Var v ⇒ [v] 77  Const n ⇒ [] 78  Plus e1 e2 ⇒ expr_fv e1 @ expr_fv e2 79  Minus e1 e2 ⇒ expr_fv e1 @ expr_fv e2 80 ]. 74 81 75 lemma eval_exp_ok : ∀env:activation_frame.∀e: expr.∀n. 76 frame_sem_expr env e = return n → 77 ∃st'. 78 m_fold Option … eval_combinators (trans_expr e) = return st' ∧ 82 definition good_expr ≝ λbound : ℕ.λe : expr.All … (λv.v < bound) (expr_fv e). 83 84 lemma good_expr_monotone : ∀n1,n2.∀e.n1 ≤ n2 → good_expr n1 e → 85 good_expr n2 e. 86 #n1 #n2 #e lapply n1 n1 lapply n2 n2 elim e // 87 [ #v #n1 #n2 #H * #H1 * % /2/ 88 *: #e1 #e2 #IH1 #IH2 #n1 #n2 #H #H1 cases(All_inv_append … H1) #H3 #H4 @All_append /2/ 89 ] 90 qed. 91 92 lemma nth_first : ∀A.∀l1,l2 : list A.∀n : ℕ.l1 > n → nth_opt … n (l1 @ l2) = nth_opt … n l1. 93 #A #l1 elim l1 [ #l2 #n normalize #H @⊥ /2/] #x #xs #IH #l2 * // #n #H @IH normalize in H; /2/ 94 qed. 95 96 lemma nth_second : ∀A.∀l1,l2 : list A.∀n : ℕ.l1 ≤ n → nth_opt … n (l1 @ l2) = nth_opt … (n  l1) l2. 97 #A #l1 elim l1 [normalize //] #x #xs #IH #l2 * [ normalize #H @⊥ /2/] #n #H normalize @IH /2/ 98 qed. 99 100 lemma frame_sem_exp_cons : ∀env.∀e.∀n1,n2. 101 to_shift ≤ env → 102 good_expr (env  to_shift) e → 103 frame_sem_expr env e = return n1 → 104 frame_sem_expr (n2 :: env) e = return n1. 105 #env #e lapply env env elim e 106 [ #v #env #n1 #n2 #prf1 * #Hv * 107 whd in ⊢ (??%% → ?); #H change with (nth_opt ???) in ⊢ (??%?); 108 change with ([?]@?) in match ([?]@?); >nth_second 109 [ >length_append whd in ⊢ (???%); <H @eq_f2 // normalize <minus_n_O <minus_n_O 110 >(eq_minus_S_pred ? O) <minus_n_O >(eq_minus_S_pred ? O) <minus_n_O 111 >(eq_minus_S_pred ? O) <minus_n_O @eq_f <(eq_minus_S_pred ? (S v)) % 112  normalize <minus_n_O >minus_minus_comm @le_plus_to_minus_r 113 @(transitive_le … (monotonic_le_plus_r 1 ?? Hv)) normalize <(minus_Sn_m 2) // 114 ] 115  #n #env #n1 #n2 #prf1 * normalize // 116 *: #e1 #e2 #IH1 #IH2 #env #n1 #n2 #prf1 #H cases(All_inv_append … H) H #H1 #H2 117 change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) H 118 #n3 * #EQn3 #H cases(bind_inversion ????? H) H #n4 * #EQn4 whd in ⊢ (??%% → ?); 119 #EQ destruct change with (m_bind ?????) in ⊢ (??%?); >(IH1 … EQn3) // 120 >(IH2 … EQn4) // 121 ] 122 qed. 123 124 125 lemma eval_exp_ok : ∀st.∀env:activation_frame.∀e: expr.∀n. 126 to_shift ≤ env → good_expr (env  to_shift) e → 127 frame_current_env … st = return env → 128 frame_sem_expr env e = return n → 129 ∃st'.m_fold Option … eval_combinators (trans_expr e) st = return st' ∧ 130 pop st' = return 〈n,st〉. 131 ** [ * #curr_env #var #rem] #sp_fp #env #e #n #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct 132 lapply n n lapply H1 H1 lapply H2 H2 lapply env env elim e 133 [ #v #env #_ #_ #n whd in ⊢ (??%% → ?); #H %{(〈〈n::env,var〉::rem,sp_fp〉)} % try % 134 whd in ⊢ (??%?); whd in match eval_combinators; normalize nodelta 135 whd in match frame_current_env; normalize nodelta whd in match option_hd; normalize nodelta 136 >m_return_bind whd in match read_frame; normalize nodelta >H % 137  #n #env #_ #_ #m whd in ⊢ (??%% → ?); #EQ destruct %{(〈〈m::env,var〉::rem,sp_fp〉)} %% 138 *: #e1 #e2 #IH1 #IH2 #env #H1 #H2 #n change with (m_bind ?????) in ⊢ (??%? → ?); 139 #H cases(bind_inversion ????? H) H #n1 * #EQn1 140 #H cases(bind_inversion ????? H) H #n2 * #EQn2 141 whd in ⊢ (??%% → ?); #EQ destruct 142 [ %{(〈〈(n1 + n2)::env,var〉::rem,sp_fp〉)}  %{(〈〈(n1  n2)::env,var〉::rem,sp_fp〉)} ] 143 >m_fold_append cases(IH1 … EQn1) // [2,4: cases(All_inv_append … H1) //] #st1 * #EQst1 #EQpop1 >EQst1 144 >m_return_bind >m_fold_append cases(IH2 … (n1 :: env)) 145 [2,7: cases(All_inv_append … H1) #H1 #H2 @(good_expr_monotone … H2) normalize /2/ 146 3,8: normalize /2/ 147 5,10: @(frame_sem_exp_cons … EQn2) // cases(All_inv_append … H1) // 148 4,9: 149 ] 150 #st2 * #EQst2 #EQpop2 cases st1 in EQst1 EQpop1; * [2,4: * #env' #var' #rem'] #fp_sp' #EQst1 151 [3,4: whd in ⊢ (??%% → ?); #EQ destruct ] cases env' in EQst1; [2,4: #val1 #env''] #EQst1 152 whd in ⊢ (??%% → ?); #EQ destruct >EQst2 >m_return_bind % [2,4: %] whd in ⊢ (??%?); 153 whd in match eval_combinators; normalize nodelta >EQpop2 % 154 ] 155 qed. 156 79 157 80 158
Note: See TracChangeset
for help on using the changeset viewer.