Changeset 3573


Ignore:
Timestamp:
Jun 17, 2015, 7:46:09 PM (4 years ago)
Author:
sacerdot
Message:

...

Location:
LTS
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • LTS/frame_variable_pass.ma

    r3568 r3573  
    167167
    168168lemma map_assign_ok:
    169  ∀m,env,frame,v,val.
     169 ∀m,env,frame,v,val,env'.
    170170  environment_rel m env frame →
    171    environment_rel m (assign env v val) (assign_frame frame (m v) 0 val).
    172  #m #env #frame #v #val #Rel whd in match assign_frame; normalize nodelta
    173  elim env in Rel;
    174  [ * % // whd in ⊢ (??%?); cases daemon (* NTH-UPDATE *)
    175  | * #v' #val' #frames #IH * #Hread #Hall change with (environment_rel ???) in Hall;
     171   assign_frame frame (to_shift + m v) 0 val = return env' →
     172   environment_rel m (assign env v val) env'.
     173 #m #env #frame #v #val
     174 elim env
     175 [ #env' #_ #H % // @(read_frame_assign_frame_hit … H)
     176 | * #v' #val' #frames #IH #env' * #Hread #Hall
     177   change with (environment_rel ???) in Hall;
    176178   whd in match (assign ???);
    177179   inversion (v==v') normalize nodelta
    178    [2: #Ineq % [ cases daemon (* NTH-UPDATE *) | @IH // ]
    179    | #EQ % [ cases daemon (* NTH-UPDATE *)
    180    |change with (environment_rel ???) cases daemon (* NOT IMPLIED BY Hall BECAUSE
    181     OF DUPLICATES :-( *)]]]
     180   [2: #Ineq #H %
     181      [ <Hread @(read_frame_assign_frame_miss … H)
     182        [ cases daemon
     183        | cases daemon
     184        | @(not_to_not ??? (\Pf Ineq)) -Ineq #H
     185          cases daemon (* MANCA INIETTIVITA' DELLA M *)
     186        ]
     187      | @IH // ]
     188   | #EQ #H %
     189     [ @(read_frame_assign_frame_hit … H)
     190     |change with (environment_rel ???)
     191      cases daemon (* NOT IMPLIED BY Hall BECAUSE OF DUPLICATES :-( *)]]]
    182192qed.
    183193
  • LTS/variable.ma

    r3571 r3573  
    7171definition read_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.nth_opt … (|env| -v -fp -1) env.
    7272
    73 (*
    7473lemma read_frame_assign_frame_hit:
    75  ∀env,v,fp,n.
    76   read_frame (assign_frame env v fp n) v fp = return n.
    77  normalize
    78 *)
     74 ∀env,v,fp,n,env'.
     75  assign_frame env v fp n = return env' →
     76  read_frame env' v fp = return n.
     77 normalize #env #v #fp #n #env' #H <(len_update ????? H)
     78 @(nth_opt_update_hit  … H)
     79qed.
     80
     81lemma read_frame_assign_frame_miss:
     82 ∀n,env,v,v',fp,env'.
     83  v + fp < |env| →
     84  v' + fp < |env| →
     85  v ≠ v' →
     86  assign_frame env v fp n = return env' →
     87  read_frame env' v' fp = read_frame env v' fp.
     88 normalize #n #env #v #v' #fp #env' #Hv #Hv' #H #H1 <(len_update ????? H1)
     89 @(nth_opt_update_miss ??????? H1) @(not_to_not … H) #K -H1 -H
     90 cases daemon (*
     91 >minus_plus in K; >minus_plus >minus_plus >minus_plus #K
     92 lapply (minus_to_plus … K) [ applyS Hv ] -K >plus_minus_associative
     93 [2: applyS Hv' ]*)
     94qed.
    7995
    8096let rec frame_sem_expr (env:activation_frame) (e: expr) on e : (option nat) ≝
Note: See TracChangeset for help on using the changeset viewer.