Changeset 392


Ignore:
Timestamp:
Dec 8, 2010, 4:56:24 PM (9 years ago)
Author:
campbell
Message:

Work around cofixpoint unfolding problem. We only use axioms in partially
ported ancillary files (like the need for proof irrelevance in the integers)
now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIOcomplete.ma

    r389 r392  
    780780nqed.
    781781
    782 nlet corec show_reactive ge s
     782(* A slightly different version of the above, to work around a problem with the
     783   next result. *)
     784nlet corec reactive_traceinf'' ge s
     785  (REACTIVE0: Σx.execution_isteps (\fst x) s (exec_inf_aux ge (exec_step ge s)) (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    783786  (REACTIVE: ∀tr,s1,e1.
    784787    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
    785788    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    786   : execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)) ≝ ?.
    787 napply daemon; (*
    788 nrewrite > (unroll_traceinf' (reactive_traceinf' …));
    789 (* FIXME: want to unfold and do case analysis on REACTIVE …, but can't until bug is fixed. *)
    790 ncases (reactive_traceinf' ge s REACTIVE);
    791 #tr tr' NE; nwhd in ⊢ (?(?%)??); nrewrite > (traceinf_traceinfp_app …);
    792 napply (reacting … NE);
     789  : traceinf' ≝ ?.
     790ncases REACTIVE0; #x; ncases x; #tr; #y; ncases y; #s' e; *; #STEPS H;
     791    @ tr ? H;
     792    napply (reactive_traceinf'' ge s');
     793    ##[ napply REACTIVE; ##[ ##2: nlapply (exec_over_isteps' … STEPS);
     794                                  #E; nrewrite > E in STEPS;
     795                                  #STEPS; napply STEPS; ##]
     796    ##|
     797    #tr1 s1 e1 STEPS1;
     798    napply REACTIVE;
     799    ##[ ##2: nrewrite > (exec_over_isteps' … STEPS) in STEPS1; #STEPS1;
     800        napply (isteps_trans … STEPS STEPS1);
     801    ##| ##skip
     802    ##]
     803##]
     804nqed.
     805
     806(* We want to prove
     807
     808nlemma show_reactive : ∀ge,s.
     809  ∀REACTIVE:∀tr,s1,e1.
     810    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     811    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
     812  execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
     813 
     814but the current matita won't unfold reactive_traceinf' so that we can do case
     815analysis on (REACTIVE …).  Instead we take an "applied" version of REACTIVE that
     816we can do case analysis on, then get it into the desired form afterwards.
    793817*)
    794 nqed.
     818nlet corec show_reactive' ge s
     819  (REACTIVE0: Σx.execution_isteps (\fst x) s (exec_inf_aux ge (exec_step ge s)) (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     820  (REACTIVE: ∀tr1,s1,e1.
     821    execution_isteps tr1 s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     822    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     823  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s REACTIVE0 REACTIVE)) s (exec_inf_aux ge (exec_step ge s)) ≝ ?.
     824(*nrewrite > (unroll_traceinf' (reactive_traceinf'' …));*)
     825napply (match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]);
     826ncases REACTIVE0;
     827#x; ncases x; #tr1; #y; ncases y; #s1 e1; #z; ncases z; #STEPS NOTSILENT;
     828nwhd in ⊢ (?(?%)??);
     829(*nrewrite > (traceinf_traceinfp_app …);*)
     830napply (match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]);
     831napply (reacting … STEPS NOTSILENT);
     832(*nrewrite < (exec_over_isteps' … STEPS) in ⊢ (???%);*)
     833napply (match (exec_over_isteps' … STEPS) return λe'.λ_.
     834?(?(reactive_traceinf'' ??
     835(REACTIVE ??? (eq_ind_r execution e1 (λx.λ_.execution_isteps ???? e1 → ?) (λS.S) ? (exec_over_isteps' ???? e1 STEPS) STEPS))
     836(λtr2,s2,e2,S1.REACTIVE ? s2 e2 (eq_ind_r execution e1 (λx.λ_:x=e1.execution_isteps tr2 s1 x s2 e2 → ?) (λS.isteps_trans ?????? e1 ? STEPS S) ? (exec_over_isteps' ???? e1 STEPS) S1))
     837))? e'
     838 with [ refl ⇒ ? ]);
     839napply show_reactive';
     840nqed.
     841
     842nlemma show_reactive : ∀ge,s.
     843  ∀REACTIVE:∀tr,s1,e1.
     844    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     845    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
     846  execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s ? REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
     847##[
     848#ge s REACTIVE;
     849napply show_reactive';
     850##| napply (REACTIVE … (isteps_none …));
     851##] nqed.
    795852
    796853nlemma execution_characterisation_complete:
Note: See TracChangeset for help on using the changeset viewer.