Changeset 2338 for src/common


Ignore:
Timestamp:
Sep 26, 2012, 10:17:32 AM (7 years ago)
Author:
campbell
Message:

Use much nicer definition for making several steps in the labelling
simulation.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Executions.ma

    r2206 r2338  
    4141  whd in ⊢ (??(λ_.???%?)); >(plus_not_final … P2)
    4242  cases (IH F3) #tr'' #S' %{tr''} /2/
     43] qed.
     44
     45(* And similarly for after_n_steps *)
     46
     47lemma after_inv : ∀FE:fullexec io_out io_in.
     48 ∀n,g,P,s.
     49  after_n_steps (S n) … FE g s P →
     50  ∃tr,s'.
     51    P tr s' ∧
     52    match is_final ?? FE g s' with
     53    [ Some r ⇒ ∃tr'.
     54      steps ? tr (exec_inf_aux … FE g (step … FE g s))
     55                 (e_stop ??? tr' r s')
     56    | None ⇒
     57      steps ? tr (exec_inf_aux … FE g (step … FE g s))
     58                 (exec_inf_aux … FE g (step … FE g s'))
     59    ].
     60#FE #n #g #P
     61(* Rather nasty generalisation *)
     62#s whd in ⊢ (% → ?); cases (is_final … s) [2: #r * ] whd in ⊢ (% → ?); #AW
     63cut (∃tr,s'. P (E0⧺tr) s' ∧ ?) [3: #H @H | skip ]
     64generalize in match E0 in AW ⊢ %; generalize in match s; -s
     65elim n
     66[ #s #tr whd in ⊢ (% → %);
     67  cases (step … s) [ #o #K * | 3: #m * ]
     68  * #tr' #s' #AW %{tr'} %{s'} %{AW}
     69  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
     70  [ #NF whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF @steps_step
     71  | #r #F whd %{tr'} >exec_inf_aux_unfold whd in ⊢ (???%?); >F whd in ⊢ (???%?); @steps_stop
     72  ]
     73| #n' #IH #s #tr whd in ⊢ (% → ?);
     74  cases (step … s) [ #o #K * | 3: #m * ] * #tr1 #s1
     75  whd in ⊢ (% → ?); lapply (refl ? (is_final … s1)) cases (is_final … s1) in ⊢ (???% → %);
     76  [ 2: #r #_ * ] #NF1 whd in ⊢ (% → ?); #AW1
     77  cases (IH s1 ? AW1)
     78  #tr' * #s' * #p #H1 %{(tr1⧺tr')} %{s'}
     79  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
     80  [ #NF <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF1
     81    @steps_steps >NF in H1; //
     82  | #r #F <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (??(λ_.???%?)); >NF1
     83    >F in H1; whd in ⊢ (% → ?); * #tr1 #H1 %{tr1}
     84    @steps_steps @H1
     85  ]
    4386] qed.
    4487
  • src/common/SmallstepExec.ma

    r2203 r2338  
    1717[ O ⇒ Value ??? 〈E0, s〉
    1818| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
    19          repeat n' ?? exec g s1
     19         ! 〈tn,sn〉 ← repeat n' ?? exec g s1;
     20         Value ??? 〈t1⧺tn,sn〉
    2021].
    2122
     
    5152].
    5253
     54(* A third version of making several steps (!)
     55
     56   The idea here is to have a computational definition of reducing serveral
     57   steps then showing some property about the resulting trace and state.  By
     58   careful use of let rec we can ensure that reduction stops in a sensible
     59   way whenever the number of steps or the step currently being executed is
     60   not (reducible to) a value.
     61
     62   For example, we state a property to prove by something like
     63
     64     ∃n. after_n_steps n … clight_exec ge s (λtr,s'. <some property>)
     65
     66   then start reducing by giving the number of steps and reducing the
     67   definition
     68
     69     %{3} whd
     70
     71   and then whenever the reduction gets stuck, the currently reducing step is
     72   the third subterm, which we can reduce and unblock with (for example)
     73   rewriting
     74
     75     whd in ⊢ (??%?); >EXe'
     76
     77   and at the end reduce with whd to get the property as the goal.
     78
     79   There's an inversion-like result to get back the information contained in
     80   the proof in Executions.ma.
     81
     82  *)
     83
     84record await_value_stuff : Type[2] ≝ {
     85 avs_O : Type[0];
     86 avs_I : avs_O → Type[0];
     87 avs_exec : trans_system avs_O avs_I;
     88 avs_g : global ?? avs_exec
     89}.
     90
     91let rec await_value (avs:await_value_stuff)
     92 (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs))))
     93 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝
     94match v with
     95[ Value ts ⇒ P (\fst ts) (\snd ts)
     96| _ ⇒ False
     97].
     98
     99let rec after_aux (avs:await_value_stuff)
     100  (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace)
     101  (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop)
     102on n : Prop ≝
     103match n with
     104[ O ⇒ P tr s
     105| S n' ⇒
     106  match is_final … s with
     107  [ None ⇒
     108    await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s.
     109      after_aux avs n' s (tr ⧺ tr') P)
     110  | _ ⇒ False
     111  ]
     112].
     113
     114definition after_n_steps : nat →
     115 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec.
     116 state ?? exec g →
     117 (trace → state ?? exec g → Prop) → Prop ≝
     118λn,O,I,exec,g,s,P. after_aux (mk_await_value_stuff O I exec g) n s E0 P.
     119
     120lemma after_n_covariant : ∀n,O,I,exec,g,P,Q.
     121  (∀tr,s. P tr s → Q tr s) →
     122  ∀s.
     123  after_n_steps n O I exec g s P →
     124  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.
     130
     131(* for joining a couple of these together *)
     132
     133lemma after_n_m : ∀n,m,O,I,exec,g,P,Q,s,s'.
     134  after_n_steps m O I exec g s' Q →
     135  after_n_steps n O I exec g s (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
     136  after_n_steps (n+m) O I exec g s P.
     137#n #m #O #I #exec #g #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n
     138[ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2
     139  whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %;
     140  generalize in match s; -s
     141  elim m
     142  [ #s #tr' whd in ⊢ (% → %); @H2
     143  | #m' #IH #s #tr' whd in ⊢ (% → %);
     144    cases (is_final … s) [2: #r * ]
     145    whd in ⊢ (% → %);
     146    cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); >Eapp_assoc @IH ]
     147| #n' #IH #tr #s #s' #H whd in ⊢ (% → %);
     148  cases (is_final … s) [2: #r * ]
     149  whd in ⊢ (% → %);
     150  cases (step O I exec g s) [1,3: normalize // ]
     151  * #tr1 #s1 whd in ⊢ (% → %); @IH @H
     152] qed.
     153
     154
    53155(* A (possibly non-terminating) execution.   *)
    54156coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.