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.

File:
1 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
Note: See TracChangeset for help on using the changeset viewer.