structure EventStructure : Type (u_1 + 1)

An event structure with binary conflict.

• Event : Type u_1
• poEvent : PartialOrder self.Event
• conflict : self.Event → self.Event → Prop
• conflict_irrefl (e : self.Event) : ¬self.conflict e e
• conflict_symm : Symmetric self.conflict
• conflict_hereditary {e₁ e₂ e₃ : self.Event} : self.conflict e₁ e₂ → e₂ ≤ e₃ → self.conflict e₁ e₃

instance EventStructure.instPartialOrderEvent (es : EventStructure) : PartialOrder es.Event

Equations

• es.instPartialOrderEvent = es.poEvent

def EventStructure.consistent (es : EventStructure) (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₂

theorem EventStructure.consistent_refl (es : EventStructure) : Reflexive es.consistent

Consistency is reflexive.

theorem EventStructure.consistent_symm (es : EventStructure) : Symmetric es.consistent

Consistency is symmetric.

def EventStructure.concurrent (es : EventStructure) (e₁ e₂ : es.Event) : Prop

Concurrency relation: 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 EventStructure.concurrent_irrefl (es : EventStructure) (e : es.Event) : ¬es.concurrent e e

Concurrency is irreflexive.

theorem EventStructure.concurrent_symm (es : EventStructure) : Symmetric es.concurrent

Concurrency is symmetric.

def EventStructure.minimalConflict (es : EventStructure) (e₁ e₂ : es.Event) : Prop

Minimal conflict relation: (e₁, e₂) is a minimal conflicting pair if they conflict and there is no proper reduction of either that still produces a conflict. Formally: e₁ # e₂ and for all e₁' ≤ e₁, e₂' ≤ e₂, if e₁' # e₂' then e₁' = e₁ ∧ e₂' = e₂

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₂)

theorem EventStructure.minimalConflict_symm (es : EventStructure) : Symmetric es.minimalConflict

Minimal conflict is symmetric.

theorem EventStructure.minimalConflict_conflict (es : EventStructure) {e₁ e₂ : es.Event} (h : es.minimalConflict e₁ e₂) : es.conflict e₁ e₂

If (e₁, e₂) is a minimal conflict, then e₁ and e₂ conflict.

theorem EventStructure.minimalConflict_minimal (es : EventStructure) {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₂

If (e₁, e₂) is a minimal conflict and e₁' ≤ e₁, e₂' ≤ e₂ with e₁' ## e₂', then e₁' = e₁ and e₂' = e₂.

def EventStructure.past (es : EventStructure) (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 EventStructure.future (es : EventStructure) (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}

class DecidableEventStructure (es : EventStructure) : Type u_1

Decidability data for an event structure: decidable equality on events and decidable strict order. Together these yield decidable causality.

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

instance EventStructure.decLe (es : EventStructure) [DecidableEventStructure 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 ⋯