Changeset 3571 for LTS


Ignore:
Timestamp:
Jun 17, 2015, 6:01:11 PM (4 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable.ma

    r3570 r3571  
    1919definition activation_frame ≝ DeqSet_List DeqNat.
    2020
    21 let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) (def : A) on l : option (list A) ≝
     21let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) on l : option (list A) ≝
    2222match l with
    2323[ nil ⇒ None ?
     
    2525   match n with
    2626   [ O ⇒ return (a :: xs)
    27    | S m ⇒ !res ← update … xs m a def; return (x::res) ]].
     27   | S m ⇒ !res ← update … xs m a; return (x::res) ]].
    2828
    2929lemma nth_opt_update_hit:
    30  ∀n,env,a,env'.
    31   update … env a n O = return env' →
     30 ∀A,n,env,a,env'.
     31  update A env a n = return env' →
    3232  nth_opt … a env' = return n.
    33  #n #env elim env
     33 #A #n #env elim env
    3434 [ normalize #a #env' #abs destruct
    3535 | #x #xs #IH #a #env' cases a
     
    4040qed.
    4141
    42 definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (|env| - v - fp -1) n O.
     42lemma len_update:
     43 ∀A,env,n,a,env'.
     44  update A env n a = return env' →
     45   |env| = |env'|.
     46#A #env elim env normalize
     47[ #n #a #env' #abs destruct
     48| #hd #tl #IH * normalize
     49  [ #a #env' #EQ destruct //
     50  | #m #a #env' change with (m_bind ????? = return ? → ?) #H
     51    cases (bind_inversion ????? H) #l * #EQ1 #EQ2 normalize in EQ1 EQ2; destruct
     52    @eq_f @(IH … EQ1) ]]
     53qed.
     54
     55lemma nth_opt_update_miss:
     56 ∀A,n,env,a,a',env'.
     57  a ≠ a' →
     58  update A env a n = return env' →
     59  nth_opt … a' env' = nth_opt … a' env.
     60 #A #n #env elim env
     61 [ normalize #a #a' #env' #aa #abs destruct
     62 | #x #xs #IH #a #a' #env' cases a
     63   [ normalize cases a' [ * #ABS cases ABS // ] #a2 #aa #EQ destruct //
     64   | #m #aa #H change with (m_bind ????? = ?) in H;
     65     cases (bind_inversion ????? H) -H #l * #EQ1 #EQ2 normalize in EQ1 EQ2; destruct
     66     cases a' in aa; normalize // #m2 #DIFF @(IH … EQ1) /2 by not_to_not/ ]]
     67qed.
     68
     69definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (|env| - v - fp -1) n.
    4370
    4471definition read_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.nth_opt … (|env| -v -fp -1) env.
Note: See TracChangeset for help on using the changeset viewer.