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 yes_size x + es_size y
    | merge _ x yes_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 _ ee
    | before _ x ymax y
    | merge _ x ymax 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.