Changeset 3569
 Timestamp:
 Jun 17, 2015, 5:29:02 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/variable.ma
r3567 r3569 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 n : list A≝21 let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) (def : A) on l : option (list A) ≝ 22 22 match l with 23 [ nil ⇒ match n with [ O ⇒ [a]  S m ⇒ def :: update … (nil ?) m a def ] 24  cons x xs ⇒ match n with [O ⇒ a :: xs  S m ⇒ x :: update … xs m a def] 25 ]. 23 [ nil ⇒ None ? 24  cons x xs ⇒ 25 match n with 26 [ O ⇒ return (a :: xs) 27  S m ⇒ !res ← update … xs m a def; return (x::res) ]]. 28 29 lemma nth_opt_update_hit: 30 ∀n,env,a,env'. 31 update … env a n O = return env' → 32 nth_opt … a env' = return n. 33 #n #env elim env 34 [ normalize #a #env' #abs destruct 35  #x #xs #IH #a #env' cases a 36 [ normalize #EQ destruct // 37  #m #H change with (m_bind ????? = ?) in H; 38 cases (bind_inversion ????? H) H #l * #EQ1 #EQ2 normalize in EQ1 EQ2; destruct 39 normalize @IH assumption ]] 40 qed. 26 41 27 42 definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (env  v  fp 1) n O. 28 43 29 44 definition read_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.nth_opt … (env v fp 1) env. 45 46 lemma read_frame_assign_frame_hit: 47 ∀env,v,fp,n. 48 read_frame (assign_frame env v fp n) v fp = return n. 49 normalize 30 50 31 51 let rec frame_sem_expr (env:activation_frame) (e: expr) on e : (option nat) ≝
Note: See TracChangeset
for help on using the changeset viewer.