Changeset 3565 for LTS


Ignore:
Timestamp:
Jun 16, 2015, 7:13:10 PM (4 years ago)
Author:
piccolo
Message:
 
Location:
LTS
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • LTS/stack.ma

    r3562 r3565  
    105105                 push s n
    106106| push_const n ⇒ push s n
    107 | push_plus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val1 + val2)
    108 | push_minus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val1 - val2)
    109 | push_eq ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (if eqb val1 val2 then 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)
    110110| push_not ⇒ ! 〈val1,st1〉 ← pop s;push st1 (1-val1)
    111111].
  • LTS/variable_stack_pass.ma

    r3562 r3565  
    7272 (λ_.λ_.True).
    7373
     74let rec expr_fv (e : expr) on e : list variable ≝
     75match 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].
    7481
    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' ∧
     82definition good_expr ≝  λbound : ℕ.λe : expr.All … (λv.v < bound) (expr_fv e).
     83
     84lemma good_expr_monotone : ∀n1,n2.∀e.n1 ≤ n2 → good_expr n1 e →
     85good_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]
     90qed.
     91
     92lemma 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/
     94qed.
     95
     96lemma 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/
     98qed.
     99
     100lemma frame_sem_exp_cons : ∀env.∀e.∀n1,n2.
     101to_shift ≤ |env| →
     102good_expr (|env| - to_shift) e →
     103frame_sem_expr env e = return n1 →
     104frame_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]
     122qed.
     123
     124
     125lemma eval_exp_ok : ∀st.∀env:activation_frame.∀e: expr.∀n.
     126to_shift ≤ |env| → good_expr (|env| - to_shift) e →
     127frame_current_env … st = return env →
     128frame_sem_expr env e = return n →
     129∃st'.m_fold Option … eval_combinators (trans_expr e) st = return st' ∧
     130pop st' = return 〈n,st〉.
     131** [| * #curr_env #var #rem] #sp_fp #env #e #n #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
     132lapply 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]
     155qed.
     156
    79157
    80158 
Note: See TracChangeset for help on using the changeset viewer.