Changeset 2444


Ignore:
Timestamp:
Nov 8, 2012, 6:47:04 PM (7 years ago)
Author:
campbell
Message:

Some inversion lemmas for after_n_steps for dealing with >1 source steps.
Also, a few more coercions for IO/error equations when the type isn't
reduced.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r2428 r2444  
    426426  on _E:eq (IO ???) ?? to eq (res ?) ??.
    427427
     428(* and for an unreduced form *)
     429coercion io_monad_eq_from_res :
     430  ∀O,I,T,e,v. ∀E:err_to_io O I T e = Value O I T v. e = OK T v ≝ io_eq_to_res
     431  on _E:eq (monad (max_def (IOMonad ??)) ?) ?? to eq (res ?) ??.
     432
    428433(* Similarly for opt *)
    429434
     
    441446  on _E:eq (IO ???) ?? to eq (option ?) ??.
    442447
    443 
    444 
     448coercion io_monad_eq_from_opt :
     449  ∀O,I,T,e,m,v. ∀E:opt_to_io O I T m e = Value O I T v. e = Some T v ≝ io_eq_to_opt
     450  on _E:eq (monad (max_def (IOMonad ??)) ?) ?? to eq (option ?) ??.
     451
     452
     453
  • src/common/SmallstepExec.ma

    r2338 r2444  
    7777   and at the end reduce with whd to get the property as the goal.
    7878
    79    There's an inversion-like result to get back the information contained in
    80    the proof in Executions.ma.
     79   There are a few inversion-like results to get back the information contained in
     80   the proof below, and other that provides all the steps in an inductive form
     81   in Executions.ma.
    8182
    8283  *)
     
    118119λn,O,I,exec,g,s,P. after_aux (mk_await_value_stuff O I exec g) n s E0 P.
    119120
     121lemma after_aux_covariant : ∀avs,P,Q,tr'.
     122  (∀tr,s. P (tr'⧺tr) s → Q tr s) →
     123  ∀n,s,tr.
     124  after_aux avs n s (tr'⧺tr) P →
     125  after_aux avs n s tr Q.
     126#avs #P #Q #tr' #H #n elim n
     127[ normalize /2/
     128| #n' #IH #s #tr
     129  whd in ⊢ (% → %); cases (is_final … s) [ 2: #x * ]
     130  whd in ⊢ (% → %);
     131  cases (step … s) [1,3: normalize /2/ ]
     132  * #tr'' #s''
     133  whd in ⊢ (% → %); >Eapp_assoc @IH
     134] qed.
     135
    120136lemma after_n_covariant : ∀n,O,I,exec,g,P,Q.
    121137  (∀tr,s. P tr s → Q tr s) →
     
    123139  after_n_steps n O I exec g s P →
    124140  after_n_steps n O I exec g s Q.
    125 #n #O #I #exec #g #P #Q #H whd in ⊢ (? → % → %); generalize in match E0; elim n
    126 [ normalize /2/
    127 | #n' #IH #tr #s
    128   normalize cases (is_final … s) normalize [ 2: #_ * ] cases (step O I exec g s) normalize /4/
    129 ] qed.
     141normalize /3/
     142qed.
    130143
    131144(* for joining a couple of these together *)
     
    152165] qed.
    153166
     167(* Inversion lemmas. *)
     168
     169lemma after_1_of_n_steps : ∀n,O,I,exec,g,P,s.
     170  after_n_steps (S n) O I exec g s P →
     171  ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧
     172  after_n_steps n O I exec g s' (λtr'',s''. P (tr⧺tr'') s'').
     173#n #O #I #exec #g #P #s
     174whd in ⊢ (% → ?);
     175cases (is_final … s)
     176[ whd in ⊢ (% → ?);
     177  cases (step … s)
     178  [ #o #k *
     179  | * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER
     180    %{tr} %{s'} % // whd @(after_aux_covariant … AFTER)
     181    #tr' #s'' //
     182  | #m *
     183  ]
     184| #r *
     185] qed.
     186
     187lemma after_1_step : ∀O,I,exec,g,P,s.
     188  after_n_steps 1 O I exec g s P →
     189  ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ P tr s'.
     190#O #I #exec #g #P #s #AFTER
     191cases (after_1_of_n_steps … AFTER)
     192#tr * #s' * #STEP #FIN %{tr} %{s'} % // whd in FIN; >E0_right in FIN; //
     193qed.
     194
     195(* A typical way to use the following:
     196
     197   With a hypothesis
     198     EX : after_n_steps n ... (State ...) ...
     199   reduce it [whd in EX;] to
     200     EX : await_value ...
     201   then perform inversion
     202   [cases (await_value_bind_inv … EX) -EX * #x * #E1 #EX]
     203      x : T
     204     E1 : f = return x
     205     EX : await_value ...
     206 *)
     207
     208lemma await_value_bind_inv : ∀avs,T,f,g,P.
     209  await_value avs (f »= g) P →
     210  ∃x:T. (f = return x) ∧ await_value avs (g x) P.
     211#avs #T *
     212[ #o #k #g #P *
     213| #x #g #P #AWAIT %{x} % //
     214| #m #g #P *
     215] qed.
    154216
    155217(* A (possibly non-terminating) execution.   *)
Note: See TracChangeset for help on using the changeset viewer.