structure PES (Label : Type u_1) : Type (max u_1 (u_2 + 1))

An event structure with binary conflict; events carry labels in Label. The finite causes axiom is not assumed.

• Event : Type u_2
• poEvent : PartialOrder self.Event
• conflict : self.Event → self.Event → Prop
• label : self.Event → Label
• conflict_irrefl (e : self.Event) : ¬self.conflict e e
• conflict_symm : Std.Symm self.conflict
• conflict_hereditary {e₁ e₂ e₃ : self.Event} : self.conflict e₁ e₂ → e₂ ≤ e₃ → self.conflict e₁ e₃

@[instance_reducible]

instance PES.instPartialOrderEvent {L : Type u_1} (es : PES L) : PartialOrder es.Event

Equations

• es.instPartialOrderEvent = es.poEvent

def PES.consistent {L : Type u_1} (es : PES L) (e₁ e₂ : es.Event) : Prop

Consistency relation: two events are consistent if they are not in conflict.

Equations

• es.consistent e₁ e₂ = ¬es.conflict e₁ e₂

instance PES.consistent_refl {L : Type u_1} (es : PES L) : Std.Refl es.consistent

Consistency is reflexive.

instance PES.consistent_symm {L : Type u_1} (es : PES L) : Std.Symm es.consistent

Consistency is symmetric.

def PES.concurrent {L : Type u_1} (es : PES L) (e₁ e₂ : es.Event) : Prop

Two events are concurrent if they are consistent and causally independent.

Equations

• es.concurrent e₁ e₂ = (es.consistent e₁ e₂ ∧ ¬e₁ ≤ e₂ ∧ ¬e₂ ≤ e₁)

theorem PES.concurrent_irrefl {L : Type u_1} (es : PES L) (e : es.Event) : ¬es.concurrent e e

Concurrency is irreflexive.

instance PES.concurrent_symm {L : Type u_1} (es : PES L) : Std.Symm es.concurrent

Concurrency is symmetric.

def PES.minimalConflict {L : Type u_1} (es : PES L) (e₁ e₂ : es.Event) : Prop

e₁ and e₂ are in minimal conflict when they conflict and no pair of events below them does.

Equations

• es.minimalConflict e₁ e₂ = (es.conflict e₁ e₂ ∧ ∀ (e₁' e₂' : es.Event), e₁' ≤ e₁ → e₂' ≤ e₂ → es.conflict e₁' e₂' → e₁' = e₁ ∧ e₂' = e₂)

instance PES.minimalConflict_symm {L : Type u_1} (es : PES L) : Std.Symm es.minimalConflict

Minimal conflict is symmetric.

theorem PES.minimalConflict_conflict {L : Type u_1} (es : PES L) {e₁ e₂ : es.Event} (h : es.minimalConflict e₁ e₂) : es.conflict e₁ e₂

If (e₁, e₂) are in minimal conflict, then e₁ and e₂ conflict.

theorem PES.minimalConflict_minimal {L : Type u_1} (es : PES L) {e₁ e₂ e₁' e₂' : es.Event} (h : es.minimalConflict e₁ e₂) (he₁ : e₁' ≤ e₁) (he₂ : e₂' ≤ e₂) (hConf : es.conflict e₁' e₂') : e₁' = e₁ ∧ e₂' = e₂

A conflicting pair below a minimal conflict is that conflict.

def PES.past {L : Type u_1} (es : PES L) (e : es.Event) : Set es.Event

The strict past of an event: all events strictly preceding it.

Equations

• es.past e = {x : es.Event | x < e}

def PES.future {L : Type u_1} (es : PES L) (e : es.Event) : Set es.Event

The future (upset) of an event: all events causally succeeding it.

Equations

• es.future e = {x : es.Event | e ≤ x}

theorem PES.past_conflict_free {L : Type u_1} (es : PES L) {e e₁ e₂ : es.Event} (h₁ : e₁ ≤ e) (h₂ : e₂ ≤ e) : ¬es.conflict e₁ e₂

The past of any event is conflict-free.

class DecidablePES {L : Type u_1} (es : PES L) : Type u_2

Decidable equality on events and a decidable strict order.

• decEq : DecidableEq es.Event
• decLt : DecidableRel fun (x1 x2 : es.Event) => x1 < x2

@[instance_reducible]

instance PES.decLe {L : Type u_1} (es : PES L) [DecidablePES es] : DecidableRel fun (x1 x2 : es.Event) => x1 ≤ x2

Equations

• es.decLe a b = if hab : a = b then isTrue ⋯ else if hlt : a < b then isTrue ⋯ else isFalse ⋯