structure Edge (es : EventStructure) (c₁ c₂ : Conf es) : Type

An edge in the configuration graph of an event structure: from configuration c₁ to configuration c₂ by adding event e.

• event : es.Event
• conf₁_enables : Configuration.enables es (↑c₁) self.event
• conf₂_equals : ↑c₂ = ↑c₁ ∪ {self.event}

inductive Path (es : EventStructure) : Conf es → Conf es → Type

A path in the configuration graph of an event structure.

• refl {es : EventStructure} {c : Conf es} : Path es c c
• step {es : EventStructure} {c₁ c₂ c₃ : Conf es} (hEdge : Edge es c₁ c₂) (hPath : Path es c₂ c₃) : Path es c₁ c₃

def Path.path_id (es : EventStructure) (c : Conf es) : Path es c c

Identity path.

Equations

• Path.path_id es c = Path.refl

def Path.path_comp (es : EventStructure) {c₁ c₂ c₃ : Conf es} (h₁₂ : Path es c₁ c₂) (h₂₃ : Path es c₂ c₃) : Path es c₁ c₃

Composition of paths.

Equations

• Path.path_comp es Path.refl h₂₃_2 = h₂₃_2
• Path.path_comp es (Path.step hEdge hPath) h₂₃ = Path.step hEdge (Path.path_comp es hPath h₂₃)

def Path.nextConf (es : EventStructure) (c : Conf es) (e : es.Event) (h : Configuration.enables es (↑c) e) : Conf es

Next configuration after executing an enabled event.

Equations

• Path.nextConf es c e h = ⟨↑c ∪ {e}, ⋯⟩

inductive Path.ExecList (es : EventStructure) : Conf es → List es.Event → Conf es → Type

Execute a list of events from a configuration.

• nil {es : EventStructure} (c : Conf es) : ExecList es c [] c
• cons {es : EventStructure} {c c' : Conf es} {t : List es.Event} (e : es.Event) (h : Configuration.enables es (↑c) e) (hnext : ExecList es (nextConf es c e h) t c') : ExecList es c (e :: t) c'

theorem Path.path_comp_id (es : EventStructure) {c₁ c₂ : Conf es} (h : Path es c₁ c₂) : path_comp es h (path_id es c₂) = h

Left identity law: composing with the identity path on the right.

theorem Path.path_id_comp (es : EventStructure) {c₁ c₂ : Conf es} (h : Path es c₁ c₂) : path_comp es (path_id es c₁) h = h

Right identity law: composing with the identity path on the left.

theorem Path.path_comp_assoc (es : EventStructure) {c₁ c₂ c₃ c₄ : Conf es} (h₁₂ : Path es c₁ c₂) (h₂₃ : Path es c₂ c₃) (h₃₄ : Path es c₃ c₄) : path_comp es (path_comp es h₁₂ h₂₃) h₃₄ = path_comp es h₁₂ (path_comp es h₂₃ h₃₄)

Associativity law: composition of paths is associative.

def Path.trace (es : EventStructure) {c₁ c₂ : Conf es} (hPath : Path es c₁ c₂) : List es.Event

Trace of the path

Equations

• Path.trace es Path.refl = []
• Path.trace es (Path.step hEdge hPath') = hEdge.event :: Path.trace es hPath'

def Path.length (es : EventStructure) {c₁ c₂ : Conf es} (hPath : Path es c₁ c₂) : ℕ

Length of a path, defined as the length of its trace.

Equations

• Path.length es hPath = (Path.trace es hPath).length

@[simp]

theorem Path.length_refl (es : EventStructure) {c : Conf es} : length es refl = 0

@[simp]

theorem Path.length_step (es : EventStructure) {c₁ c₂ c₃ : Conf es} (hEdge : Edge es c₁ c₂) (hPath : Path es c₂ c₃) : length es (step hEdge hPath) = (length es hPath).succ

def Path.execList_to_path (es : EventStructure) {c₁ c₂ : Conf es} {t : List es.Event} (h : ExecList es c₁ t c₂) : Path es c₁ c₂

Build a path from an executable list.

Equations

• Path.execList_to_path es (Path.ExecList.nil c₂) = Path.refl
• Path.execList_to_path es (Path.ExecList.cons e h_2 hnext) = Path.step { event := e, conf₁_enables := h_2, conf₂_equals := ⋯ } (Path.execList_to_path es hnext)

@[simp]

theorem Path.execList_trace (es : EventStructure) {c₁ c₂ : Conf es} {t : List es.Event} (h : ExecList es c₁ t c₂) : trace es (execList_to_path es h) = t

@[simp]

theorem Path.execList_length (es : EventStructure) {c₁ c₂ : Conf es} {t : List es.Event} (h : ExecList es c₁ t c₂) : length es (execList_to_path es h) = t.length

theorem Path.execList_target_eq_union (es : EventStructure) {c₁ c₂ : Conf es} {t : List es.Event} (h : ExecList es c₁ t c₂) : ↑c₂ = ↑c₁ ∪ {e : es.Event | e ∈ t}

Target configuration from an exec list is the source plus the list's events.

noncomputable def Path.execList_lift (es : EventStructure) {c_small c_large c_target : Conf es} {t : List es.Event} (hsub : ↑c_small ⊆ ↑c_large) (hmono : ∀ {c₁ c₂ : Conf es} {e : es.Event}, ↑c₁ ⊆ ↑c₂ → Configuration.enables es (↑c₁) e → Configuration.enables es (↑c₂) e) (h : ExecList es c_small t c_target) : (c_target' : Conf es) × ExecList es c_large t c_target'

Lift an exec list from a smaller configuration to a larger one, assuming monotone enabling under subset.

Equations

• One or more equations did not get rendered due to their size.

theorem Path.pathLengthExists (es : EventStructure) {c₁ c₂ : Conf es} (h : Nonempty (Path es c₁ c₂)) : ∃ (n : ℕ) (p : Path es c₁ c₂), length es p = n

Existence of a path length.

noncomputable def Path.minPathLength (es : EventStructure) {c₁ c₂ : Conf es} (h : Nonempty (Path es c₁ c₂)) : ℕ

Minimal path length between two configurations, given existence of a path.

Equations

• Path.minPathLength es h = Nat.find ⋯

theorem Path.minPathLength_spec (es : EventStructure) {c₁ c₂ : Conf es} (h : Nonempty (Path es c₁ c₂)) : ∃ (p : Path es c₁ c₂), length es p = minPathLength es h

theorem Path.minPathLength_le (es : EventStructure) {c₁ c₂ : Conf es} (h : Nonempty (Path es c₁ c₂)) (p : Path es c₁ c₂) : minPathLength es h ≤ length es p

theorem Path.execList_to_path_trace (es : EventStructure) {c₁ c₂ : Conf es} {t : List es.Event} (h : ExecList es c₁ t c₂) : trace es (execList_to_path es h) = t

The trace of an execList_to_path is exactly the original list.

def Path.execList_of_path (es : EventStructure) {c₁ c₂ : Conf es} (p : Path es c₁ c₂) : ExecList es c₁ (trace es p) c₂

Extract an executable list from a path.

Equations

• Path.execList_of_path es Path.refl = Path.ExecList.nil c₁
• Path.execList_of_path es (Path.step hEdge hPath) = Path.ExecList.cons hEdge.event ⋯ (⋯.mpr (Path.execList_of_path es hPath))

instance Path.pathSetoid (es : EventStructure) (c₁ c₂ : Conf es) : Setoid (Path es c₁ c₂)

Path equivalence is the kernel of the trace function.

Equations

• Path.pathSetoid es c₁ c₂ = Setoid.ker (Path.trace es)

def Path.PathEquiv (es : EventStructure) {c₁ c₂ : Conf es} (p₁ p₂ : Path es c₁ c₂) : Prop

Two paths are equivalent if their traces are trace equivalent

Equations

• Path.PathEquiv es p₁ p₂ = (Path.pathSetoid es c₁ c₂) p₁ p₂

theorem Path.pathEquiv_refl (es : EventStructure) {c₁ c₂ : Conf es} : Reflexive (PathEquiv es)

Path equivalence is reflexive.

theorem Path.pathEquiv_symm (es : EventStructure) {c₁ c₂ : Conf es} : Symmetric (PathEquiv es)

Path equivalence is symmetric.

theorem Path.pathEquiv_trans (es : EventStructure) {c₁ c₂ : Conf es} : Transitive (PathEquiv es)

Path equivalence is transitive.

theorem Path.trace_comp (es : EventStructure) {c₁ c₂ c₃ : Conf es} (p₁₂ : Path es c₁ c₂) (p₂₃ : Path es c₂ c₃) : trace es (path_comp es p₁₂ p₂₃) = trace es p₁₂ ++ trace es p₂₃

Trace of path composition is concatenation of traces.

def Path.Async (es : EventStructure) (c₁ c₂ : Conf es) : Type

Asynchronous path: paths quotiented by path equivalence.

Equations

• Path.Async es c₁ c₂ = Quotient (Path.pathSetoid es c₁ c₂)

def Path.Async.mk (es : EventStructure) {c₁ c₂ : Conf es} (p : Path es c₁ c₂) : Async es c₁ c₂

Lift a path to an asynchronous path.

Equations

• Path.Async.mk es p = ⟦p⟧

def Path.Async.async_path_id (es : EventStructure) (c : Conf es) : Async es c c

Identity asynchronous path.

Equations

• Path.Async.async_path_id es c = Path.Async.mk es (Path.path_id es c)

def Path.Async.async_path_comp (es : EventStructure) {c₁ c₂ c₃ : Conf es} (p₁₂ : Async es c₁ c₂) (p₂₃ : Async es c₂ c₃) : Async es c₁ c₃

Composition of asynchronous paths.

Equations

• Path.Async.async_path_comp es p₁₂ p₂₃ = Quotient.lift₂ (fun (p₁₂ : Path es c₁ c₂) (p₂₃ : Path es c₂ c₃) => Path.Async.mk es (Path.path_comp es p₁₂ p₂₃)) ⋯ p₁₂ p₂₃

theorem Path.Async.async_path_id_comp (es : EventStructure) {c₁ c₂ : Conf es} (p : Async es c₁ c₂) : async_path_comp es (async_path_id es c₁) p = p

Left identity law for asynchronous path composition.

theorem Path.Async.async_path_comp_id (es : EventStructure) {c₁ c₂ : Conf es} (p : Async es c₁ c₂) : async_path_comp es p (async_path_id es c₂) = p

Right identity law for asynchronous path composition.

theorem Path.Async.assoc (es : EventStructure) {c₁ c₂ c₃ c₄ : Conf es} (p₁₂ : Async es c₁ c₂) (p₂₃ : Async es c₂ c₃) (p₃₄ : Async es c₃ c₄) : async_path_comp es (async_path_comp es p₁₂ p₂₃) p₃₄ = async_path_comp es p₁₂ (async_path_comp es p₂₃ p₃₄)

Associativity law for asynchronous path composition.

@[simp]

theorem Path.trace_length_eq_length (es : EventStructure) {c₁ c₂ : Conf es} (p : Path es c₁ c₂) : (trace es p).length = length es p

For a path from c₁ to c₂, every event in the trace appears exactly once.

theorem Path.path_subset (es : EventStructure) {c₁ c₂ : Conf es} (p : Path es c₁ c₂) : ↑c₁ ⊆ ↑c₂

Paths are monotone: the source configuration is a subset of the target.

theorem Path.trace_of_path (es : EventStructure) {c₁ c₂ : Conf es} (p : Path es c₁ c₂) (e : es.Event) : e ∈ trace es p → e ∈ ↑c₂

Events executed in a path must be added to reach the target configuration.

theorem Path.path_length_ge_trace_length (es : EventStructure) {c₁ c₂ : Conf es} (p : Path es c₁ c₂) : length es p = (trace es p).length

A path requires executing at least the events in its trace.

instance pathCategory (es : EventStructure) : CategoryTheory.Category.{0, 0} (Conf es)

The path category of an event structure.

Equations

• pathCategory es = { Hom := Path es, id := Path.path_id es, comp := fun {X Y Z : Conf es} => Path.path_comp es, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

instance asyncPathCategory (es : EventStructure) : CategoryTheory.Category.{0, 0} (Conf es)

The asynchronous path category of an event structure.

Equations

• asyncPathCategory es = { Hom := Path.Async es, id := Path.Async.async_path_id es, comp := fun {X Y Z : Conf es} => Path.Async.async_path_comp es, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }