Event structures

This module defines EventStructure: a set of events equipped with a causal partial order and an irreflexive, symmetric binary conflict relation, together with the derived consistency, concurrency, minimal-conflict and past/future notions used throughout the development, and decidability data for events.

structure EventStructures.EventStructure : Type (u_1 + 1)

An event structure with binary conflict.

• Event : Type u_1

  The type of events.

• poEvent : PartialOrder self.Event

  The causal partial order on events.

• conflict : self.Event → self.Event → Prop

  The binary conflict relation on events.

• conflict_irrefl (e : self.Event) : ¬self.conflict e e
• conflict_symm ⦃e₁ e₂ : self.Event⦄ : self.conflict e₁ e₂ → self.conflict e₂ e₁
• conflict_hereditary {e₁ e₂ e₃ : self.Event} : self.conflict e₁ e₂ → e₂ ≤ e₃ → self.conflict e₁ e₃

@[implicit_reducible]

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

Equations

• es.instPartialOrderEvent = es.poEvent

def EventStructures.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 EventStructures.EventStructure.consistent_refl (es : EventStructure) (e : es.Event) : es.consistent e e

Consistency is reflexive.

theorem EventStructures.EventStructure.consistent_symm (es : EventStructure) ⦃e₁ e₂ : es.Event⦄ : es.consistent e₁ e₂ → es.consistent e₂ e₁

Consistency is symmetric.

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

Concurrency is irreflexive.

theorem EventStructures.EventStructure.concurrent_symm (es : EventStructure) ⦃e₁ e₂ : es.Event⦄ : es.concurrent e₁ e₂ → es.concurrent e₂ e₁

Concurrency is symmetric.

def EventStructures.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 EventStructures.EventStructure.minimalConflict_symm (es : EventStructure) ⦃e₁ e₂ : es.Event⦄ : es.minimalConflict e₁ e₂ → es.minimalConflict e₂ e₁

Minimal conflict is symmetric.

theorem EventStructures.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 EventStructures.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 EventStructures.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 EventStructures.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 EventStructures.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

@[implicit_reducible]

instance EventStructures.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 ⋯