Library Copland.Event_system



Abstract event systems.

Require Import Omega Preamble.

Set Implicit Arguments.

An event system is a set of events and a strict partial order on the events. An event system is represented by a well-structured EvSys.

Section Event_system.

The sort of an event.

  Variable A: Set.

The number associated with an event.

  Variable ev: A → nat.

  Definition ES_Range: Set := nat × nat.

An event system.

  Inductive EvSys: Set :=
  | leaf: ES_Range → A → EvSys
  | before: ES_Range → EvSys → EvSys → EvSys
  | merge: ES_Range → EvSys → EvSys → EvSys.

  Definition es_range es :=
    match es with
    | leaf r _ ⇒ r
    | before r _ _ ⇒ r
    | merge r _ _ ⇒ r
    end.

  Fixpoint es_size es :=
    match es with
    | leaf _ _⇒ 1
    | before _ x y ⇒ es_size x + es_size y
    | merge _ x y ⇒ es_size x + es_size y
    end.

Definition of a well-structured event system.

  Inductive well_structured: EvSys → Prop :=
  | ws_leaf_event:
      ∀ r e,
        snd r = S (fst r) →
        ev e = fst r →
        well_structured (leaf r e)
  | ws_before:
      ∀ r x y,
        well_structured x →
        well_structured y →
        r = (fst (es_range x), snd (es_range y)) →
        snd (es_range x) = fst (es_range y) →
        well_structured (before r x y)
  | ws_merge:
      ∀ r x y,
        well_structured x →
        well_structured y →
        r = (fst (es_range x), snd (es_range y)) →
        snd (es_range x) = fst (es_range y) →
        well_structured (merge r x y).
  Hint Constructors well_structured.

  Lemma well_structured_range:
    ∀ es,
      well_structured es →
      snd (es_range es) = fst (es_range es) + es_size es.

Is an event in an event system?

  Inductive ev_in: A → EvSys → Prop :=
  | ein_leaf: ∀ r ev,
      ev_in ev (leaf r ev)
  | ein_beforel: ∀ r ev es1 es2,
      ev_in ev es1 → ev_in ev (before r es1 es2)
  | ein_beforer: ∀ r ev es1 es2,
      ev_in ev es2 → ev_in ev (before r es1 es2)
  | ein_mergel: ∀ r ev es1 es2,
      ev_in ev es1 → ev_in ev (merge r es1 es2)
  | ein_merger: ∀ r ev es1 es2,
      ev_in ev es2 → ev_in ev (merge r es1 es2).
  Hint Constructors ev_in.

Is one event before another?

  Inductive prec: EvSys → A → A → Prop :=
  | prseq: ∀ r x y e f,
      ev_in e x → ev_in f y →
      prec (before r x y) e f
  | prseql: ∀ r x y e f,
      prec x e f →
      prec (before r x y) e f
  | prseqr: ∀ r x y e f,
      prec y e f →
      prec (before r x y) e f
  | prparl: ∀ r x y e f,
      prec x e f →
      prec (merge r x y) e f
  | prparr: ∀ r x y e f,
      prec y e f →
      prec (merge r x y) e f.
  Hint Constructors prec.

  Lemma prec_in_left:
    ∀ es ev1 ev2,
      prec es ev1 ev2 → ev_in ev1 es.

  Lemma prec_in_right:
    ∀ es ev1 ev2,
      prec es ev1 ev2 → ev_in ev2 es.

  Lemma ws_evsys_range:
    ∀ es e,
      well_structured es →
      ev_in e es →
      fst (es_range es) ≤ ev e < snd (es_range es).

  Lemma es_injective_events:
    ∀ es ev0 ev1,
      well_structured es →
      ev_in ev0 es → ev_in ev1 es →
      ev ev0 = ev ev1 →
      ev0 = ev1.

A relation is a strict partial order iff it is irreflexive and transitive.

  Lemma evsys_irreflexive:
    ∀ es ev,
      well_structured es →
      ¬prec es ev ev.

  Lemma evsys_transitive:
    ∀ es ev0 ev1 ev2,
      well_structured es →
      prec es ev0 ev1 →
      prec es ev1 ev2 →
      prec es ev0 ev2.

Merge is associative.

  Definition same_rel es0 es1 :=
    ∀ ev0 ev1,
      prec es0 ev0 ev1 ↔ prec es1 ev0 ev1.

  Lemma ws_merge1:
    ∀ r s x y z,
      well_structured (merge r x y) →
      well_structured (merge s y z) →
      well_structured (merge (fst r, snd s) x (merge s y z)).

  Lemma ws_merge2:
    ∀ r s x y z,
      well_structured (merge r x y) →
      well_structured (merge s y z) →
      well_structured (merge (fst r, snd s) (merge r x y) z).

  Lemma merge_associative:
    ∀ r s x y z,
      same_rel (merge (fst r, snd s) x (merge s y z))
               (merge (fst r, snd s) (merge r x y) z).

A more useful form of merge associative

  Lemma merge_associative_pairs:
    ∀ r0 r1 s0 s1 x y z,
      same_rel (merge (r0, s1) x (merge (s0, s1) y z))
               (merge (r0, s1) (merge (r0, r1) x y) z).

Before is associative.

  Lemma ws_before1:
    ∀ r s x y z,
      well_structured (before r x y) →
      well_structured (before s y z) →
      well_structured (before (fst r, snd s) x (before s y z)).

  Lemma ws_before2:
    ∀ r s x y z,
      well_structured (before r x y) →
      well_structured (before s y z) →
      well_structured (before (fst r, snd s) (before r x y) z).

  Lemma before_associative:
    ∀ r s x y z,
      same_rel (before (fst r, snd s) x (before s y z))
               (before (fst r, snd s) (before r x y) z).

  Lemma before_associative_pairs:
    ∀ r0 r1 s0 s1 x y z,
      same_rel (before (r0, s1) x (before (s0, s1) y z))
               (before (r0, s1) (before (r0, r1) x y) z).

  Lemma ws_exists:
    ∀ es,
      well_structured es →
      ∃ e, ev_in e es.

Maximal events.

  Definition supreme es e :=
    ev_in e es ∧ ∀ e0, ev_in e0 es → ¬prec es e e0.

Inductive version of a maximal event.

  Inductive sup: EvSys → A → Prop :=
  | sup_leaf: ∀ r e, sup (leaf r e) e
  | sup_before:
      ∀ r es0 es1 e,
        sup es1 e → sup (before r es0 es1) e
  | sup_mergel:
      ∀ r es0 es1 e,
        sup es0 e → sup (merge r es0 es1) e
  | sup_merger:
      ∀ r es0 es1 e,
        sup es1 e → sup (merge r es0 es1) e.
  Hint Constructors sup.

  Lemma before_sup:
    ∀ r x y e,
      sup (before r x y) e → sup y e.

  Lemma sup_supreme:
    ∀ es e,
      well_structured es →
      sup es e ↔ supreme es e.

Return one of possibly many maximal events.

  Fixpoint max es :=
    match es with
    | leaf _ e ⇒ e
    | before _ x y ⇒ max y
    | merge _ x y ⇒ max y
    end.

  Lemma supreme_max:
    ∀ es,
      well_structured es →
      supreme es (max es).

End Event_system.

Hint Constructors well_structured ev_in prec sup.

Unset Implicit Arguments.