Changeset 3571
 Timestamp:
 Jun 17, 2015, 6:01:11 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/variable.ma
r3570 r3571 19 19 definition activation_frame ≝ DeqSet_List DeqNat. 20 20 21 let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) (def : A)on l : option (list A) ≝21 let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) on l : option (list A) ≝ 22 22 match l with 23 23 [ nil ⇒ None ? … … 25 25 match n with 26 26 [ 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) ]]. 28 28 29 29 lemma 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' → 32 32 nth_opt … a env' = return n. 33 # n #env elim env33 #A #n #env elim env 34 34 [ normalize #a #env' #abs destruct 35 35  #x #xs #IH #a #env' cases a … … 40 40 qed. 41 41 42 definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (env  v  fp 1) n O. 42 lemma 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) ]] 53 qed. 54 55 lemma 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/ ]] 67 qed. 68 69 definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (env  v  fp 1) n. 43 70 44 71 definition 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.