Changeset 379


Ignore:
Timestamp:
Dec 6, 2010, 4:03:36 PM (9 years ago)
Author:
campbell
Message:

More whole execution equivalence - need ability to unfold cofixpoints though.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIOcomplete.ma

    r378 r379  
    513513##] nqed.
    514514
    515 ninductive execution_characterisation : execution → Type
     515ninductive execution_characterisation : execution → Prop
    516516| ec_terminates: ∀s,s',e,tr.
    517517    execution_terminates tr s e s' →
     
    622622nqed.
    623623
     624nlemma not_ex_all_not:
     625  ∀A:Type.∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
     626#A P; *; #H x; @; #H';
     627napply H; @ x; napply H';
     628nqed.
     629
    624630nlemma not_imply_elim:
    625631  ∀classic:(∀P:Prop.P ∨ ¬P).
     
    643649##| napply (not_imply_elim2 P Q H);
    644650##] nqed.
     651
     652nlemma not_and_to_imply:
     653  ∀classic:(∀P:Prop.P ∨ ¬P).
     654  ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q.
     655#classic P Q; *; #H H';
     656@; #H''; napply H; @; //;
     657nqed.
    645658
    646659ninductive execution_not_over : execution → Prop ≝
     
    726739##] nqed.
    727740
     741nlemma exec_over_isteps': ∀ge,tr,s,s',e'.
     742  execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s' e' →
     743  exec_inf_aux ge (exec_step ge s') = e'.
     744#ge tr s s' e'; nletin e ≝ (exec_inf_aux ge (exec_step ge s)); #H;
     745napply (exec_over_isteps … H (refl ??));
     746nqed.
     747
    728748nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
    729749  exec_inf_aux ge (exec_step ge s) = e_interact o k →
     
    747767##] nqed.
    748768
     769nlet corec reactive_traceinf' ge s
     770  (REACTIVE: ∀tr,s1,e1.
     771    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     772    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     773  : traceinf' ≝ ?.
     774nlapply (REACTIVE E0 s (exec_inf_aux ge (exec_step ge s)) ?);
     775##[ napply isteps_none
     776##| *; #x; ncases x; #tr; #y; ncases y; #s' e; *; #STEPS H;
     777    @ tr ? H;
     778    napply (reactive_traceinf' ge s');
     779    #tr1 s1 e1 STEPS1;
     780    napply REACTIVE;
     781    ##[ ##2: nrewrite > (exec_over_isteps' … STEPS) in STEPS1; #STEPS1;
     782        napply (isteps_trans … STEPS STEPS1);
     783    ##| ##skip
     784    ##]
     785##]
     786nqed.
     787
     788nlet corec show_reactive ge s
     789  (REACTIVE: ∀tr,s1,e1.
     790    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     791    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     792  : execution_reacts (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)) ≝ ?.
     793napply daemon; (*
     794nrewrite > (unroll_traceinf' (reactive_traceinf' …));
     795(* FIXME: want to unfold and do case analysis on REACTIVE …, but can't until bug is fixed. *)
     796ncases (reactive_traceinf' ge s REACTIVE);
     797#tr tr' NE; nwhd in ⊢ (?(?%)??); nrewrite > (traceinf_traceinfp_app …);
     798napply (reacting … NE);
     799*)
     800nqed.
     801
    749802nlemma execution_characterisation_complete:
    750803  ∀classic:(∀P:Prop.P ∨ ¬P).
     804  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
    751805   ∀ge,s. ¬ (∃r. final_state s r) →
    752806   execution_characterisation (exec_inf_aux ge (Value ??? 〈E0,s〉)).
    753 #classic ge s; *; #NOTFINAL;
     807#classic constructive_indefinite_description ge s; *; #NOTFINAL;
    754808nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (?%);
    755809ncases (is_final_state s); ##[ #x; ncases x; #r FINAL; napply False_rect_Type0; napply NOTFINAL; @r; napply FINAL ##]
     
    780834      ##]
    781835
    782  (* FINISH *)
    783   ##| *; #REACTIVE;
    784      (* napply ec_reacts;*)
    785  (* FINISH *)
     836  ##| *; #NOTUNREACTIVE;
     837      ncut (∀tr,s1,e1.execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     838            ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0);
     839      ##[ #tr s1 e1 STEPS;
     840          napply (classical_doubleneg classic); @; #NOREACTION;
     841          napply NOTUNREACTIVE;
     842          @ tr; @s1; @e1; @; //;
     843          #tr2 s2 e2 STEPS2;
     844          nlapply (not_ex_all_not … NOREACTION); #NR1;
     845          nlapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2;
     846          napply (classical_doubleneg classic);
     847          napply NR2; //;
     848      ##| #REACTIVE;
     849          napply ec_reacts;
     850          ##[ ##2: napply (show_reactive ge s …);
     851                   #tr s1 e1 STEPS;
     852                   napply constructive_indefinite_description;
     853                   napply (REACTIVE … tr s1 e1 STEPS);
     854          ##| ##skip
     855          ##]
     856      ##]
    786857  ##]
    787858 
     
    847918    ##]
    848919##]
    849    
    850 
    851 ndefinition behaviour_of_execution:
    852  execution_characterisation → program_behavior ≝
    853 λexec.match exec with
     920nqed.   
     921
     922ndefinition behaviour_of_execution: ∀e.
     923 execution_characterisation e → program_behavior ≝
     924λe,exec.match exec with
    854925[ ec_terminates s s' e tr H ⇒ Terminates tr ?
    855 | ec_diverges e tr H ⇒ Diverges tr
     926| ec_diverges _ e tr H ⇒ Diverges tr
    856927| ec_reacts s e tr H ⇒ Reacts tr
    857928| ec_wrong e s s' tr H ⇒ Goes_wrong tr
  • C-semantics/Events.ma

    r175 r379  
    131131  repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq.
    132132*)
     133
     134(* Ported from CompCert 1.7.1 >>> *)
     135
     136(* * An alternate presentation of infinite traces as
     137  infinite concatenations of nonempty finite traces. *)
     138
     139ncoinductive traceinf': Type ≝
     140  | Econsinf': ∀t: trace. ∀T: traceinf'. t ≠ E0 → traceinf'.
     141
     142ndefinition split_traceinf' : ∀t:trace. traceinf' → t ≠ E0 → event × traceinf' ≝
     143λt,T.
     144  match t return λt0.t0 ≠ E0 → ? with
     145  [ nil ⇒ ?
     146  | cons e t' ⇒ λ_.
     147     (match t' return λt0. t' = t0 → ? with
     148     [ nil ⇒ λ_.〈e, T〉
     149     | cons e' t'' ⇒ λE.〈e, Econsinf' t' T ?〉
     150     ]) (refl ? t')
     151  ].
     152##[ *; #NE; napply False_rect_Type0; napply NE; napply refl;
     153##| @; #E'; nrewrite > E' in E; #E; nwhd in E:(??%%); ndestruct (E);
     154##] nqed.
     155
     156nlet corec traceinf_of_traceinf' (T': traceinf') : traceinf ≝
     157  match T' with
     158  [ Econsinf' t T'' NOTEMPTY ⇒
     159      match split_traceinf' t T'' NOTEMPTY with [ mk_pair e tl ⇒
     160      Econsinf e (traceinf_of_traceinf' tl) ]
     161  ].
     162
     163nremark unroll_traceinf':
     164  ∀T. T = match T with [ Econsinf' t T' NE ⇒ Econsinf' t T' NE ].
     165#T; ncases T; //; nqed.
     166
     167nremark unroll_traceinf:
     168  ∀T. T = match T with [ Econsinf t T' ⇒ Econsinf t T' ].
     169#T; ncases T; //;
     170nqed.
     171
     172nlemma traceinf_traceinfp_app:
     173  ∀t,T,NE.
     174  traceinf_of_traceinf' (Econsinf' t T NE) = t ⧻ traceinf_of_traceinf' T.
     175#t; nelim t;
     176##[ #T NE; ncases NE; #NE'; napply False_ind; napply NE'; napply refl;
     177##| #h t'; ncases t'; ##[ ##2: #h' t''; ##] #IH T NE;
     178    nrewrite > (unroll_traceinf (traceinf_of_traceinf' ?));
     179    nwhd in ⊢ (??%?); //; nrewrite > (IH …); napply refl;
     180##] nqed.
     181
     182(* <<< *)
     183
    133184(* * The predicate [event_match ef vargs t vres] expresses that
    134185  the event [t] is generated when invoking external function [ef]
Note: See TracChangeset for help on using the changeset viewer.