Changeset 3569

Timestamp:

Jun 17, 2015, 5:29:02 PM (6 years ago)

Author:

sacerdot

Message:

...

File:

• LTS/variable.ma (modified) (1 diff)

LTS/variable.ma

@@ -19 +19 @@
 definition activation_frame ≝ DeqSet_List DeqNat.
 
-let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) (def : A) on n : list A ≝ 
+let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) (def : A) on l : option (list A) ≝ 
 match l with
-[ nil ⇒ match n with [ O ⇒ [a] | S m ⇒ def :: update … (nil ?) m a def ]
-| cons x xs ⇒ match n with [O ⇒ a :: xs | S m ⇒ x :: update … xs m a def]
-].
+[ nil ⇒ None ?
+| cons x xs ⇒
+   match n with
+   [ O ⇒ return (a :: xs)
+   | S m ⇒ !res ← update … xs m a def; return (x::res) ]].
+
+lemma nth_opt_update_hit:
+ ∀n,env,a,env'.
+  update … env a n O = return env' →
+  nth_opt … a env' = return n.
+ #n #env elim env
+ [ normalize #a #env' #abs destruct 
+ | #x #xs #IH #a #env' cases a
+   [ normalize #EQ destruct //
+   | #m #H change with (m_bind ????? = ?) in H;
+     cases (bind_inversion ????? H) -H #l * #EQ1 #EQ2 normalize in EQ1 EQ2; destruct
+     normalize @IH assumption ]]
+qed.
 
 definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (|env| - v - fp -1) n O.
 
 definition read_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.nth_opt … (|env| -v -fp -1) env.
+
+lemma read_frame_assign_frame_hit:
+ ∀env,v,fp,n.
+  read_frame (assign_frame env v fp n) v fp = return n.
+ normalize
 
 let rec frame_sem_expr (env:activation_frame) (e: expr) on e : (option nat) ≝