Changeset 379 for C-semantics/Events.ma


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.