Changeset 3569 for LTS


Ignore:
Timestamp:
Jun 17, 2015, 5:29:02 PM (4 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable.ma

    r3567 r3569  
    1919definition activation_frame ≝ DeqSet_List DeqNat.
    2020
    21 let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) (def : A) on n : list A
     21let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) (def : A) on l : option (list A)
    2222match 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
     29lemma 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 ]]
     40qed.
    2641
    2742definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (|env| - v - fp -1) n O.
    2843
    2944definition read_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.nth_opt … (|env| -v -fp -1) env.
     45
     46lemma 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
    3050
    3151let rec frame_sem_expr (env:activation_frame) (e: expr) on e : (option nat) ≝
Note: See TracChangeset for help on using the changeset viewer.