Paths in the configuration graph

This module defines edges and paths in the configuration graph of an event structure, their composition, traces and lengths, the minimal path length, the quotient of paths by trace equivalence (asynchronous paths), and the resulting (synchronous and asynchronous) path categories.

structure EventStructures.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 a fresh enabled event.

• event : es.Event

  The event added along this edge.

• conf₁_enables : Configuration.enables es (↑c₁) self.event

  The source configuration enables the added event.

• conf₂_equals : ↑c₂ = ↑c₁ ∪ {self.event}

  The target configuration is the source configuration extended by the event.

inductive EventStructures.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 EventStructures.Path.pathId (es : EventStructure) (c : Conf es) : Path es c c

Identity path.

Equations

• EventStructures.Path.pathId es c = EventStructures.Path.refl

def EventStructures.Path.pathComp (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

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

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

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

inductive EventStructures.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 EventStructures.Path.path_comp_id (es : EventStructure) {c₁ c₂ : Conf es} (h : Path es c₁ c₂) : pathComp es h (pathId es c₂) = h

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

theorem EventStructures.Path.path_id_comp (es : EventStructure) {c₁ c₂ : Conf es} (h : Path es c₁ c₂) : pathComp es (pathId es c₁) h = h

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

theorem EventStructures.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₄) : pathComp es (pathComp es h₁₂ h₂₃) h₃₄ = pathComp es h₁₂ (pathComp es h₂₃ h₃₄)

Associativity law: composition of paths is associative.

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

Trace of the path

Equations

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

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

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

@[simp]

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

@[simp]

theorem EventStructures.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 EventStructures.Path.execListToPath (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

• One or more equations did not get rendered due to their size.
• EventStructures.Path.execListToPath es (EventStructures.Path.ExecList.nil c₂) = EventStructures.Path.refl

@[simp]

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

@[simp]

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

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

theorem EventStructures.Path.execList_not_mem_source (es : EventStructure) {c₁ c₂ : Conf es} {t : List es.Event} (h : ExecList es c₁ t c₂) (e : es.Event) : e ∈ t → e ∉ ↑c₁

Events executed in an exec list are not already in its source configuration.

noncomputable def EventStructures.Path.execListLift (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₂ → e ∉ ↑c₂ → Configuration.enables es (↑c₁) e → Configuration.enables es (↑c₂) e) (hfresh : ∀ e ∈ t, e ∉ ↑c_large) (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 the executed events are fresh for the larger configuration and enabling is monotone under subset for fresh events.

Equations

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

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

• EventStructures.Path.minPathLength es h = Nat.find ⋯

theorem EventStructures.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 EventStructures.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 EventStructures.Path.execList_to_path_trace (es : EventStructure) {c₁ c₂ : Conf es} {t : List es.Event} (h : ExecList es c₁ t c₂) : trace es (execListToPath es h) = t

The trace of an execListToPath is exactly the original list.

def EventStructures.Path.execListOfPath (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

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

def EventStructures.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: one trace can be obtained from the other by swapping adjacent concurrent events.

Equations

• EventStructures.Path.PathEquiv es p₁ p₂ = EventStructures.TraceEquiv es (EventStructures.Path.trace es p₁) (EventStructures.Path.trace es p₂)

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

Path equivalence is reflexive.

theorem EventStructures.Path.pathEquiv_symm (es : EventStructure) {c₁ c₂ : Conf es} ⦃p₁ p₂ : Path es c₁ c₂⦄ : PathEquiv es p₁ p₂ → PathEquiv es p₂ p₁

Path equivalence is symmetric.

theorem EventStructures.Path.pathEquiv_trans (es : EventStructure) {c₁ c₂ : Conf es} ⦃p₁ p₂ p₃ : Path es c₁ c₂⦄ : PathEquiv es p₁ p₂ → PathEquiv es p₂ p₃ → PathEquiv es p₁ p₃

Path equivalence is transitive.

theorem EventStructures.Path.pathEquivEquivalence (es : EventStructure) (c₁ c₂ : Conf es) : Equivalence (PathEquiv es)

Path equivalence is an equivalence relation.

@[implicit_reducible]

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

Paths between two configurations form a setoid under trace equivalence of their traces (the congruence generated by swaps of adjacent concurrent events), not under literal equality of traces.

Equations

• EventStructures.Path.pathSetoid es c₁ c₂ = { r := EventStructures.Path.PathEquiv es, iseqv := ⋯ }

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

Trace of path composition is concatenation of traces.

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

Asynchronous path: paths quotiented by path equivalence.

Equations

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

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

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

def EventStructures.Path.Async.asyncPathId (es : EventStructure) (c : Conf es) : Async es c c

Identity asynchronous path.

Equations

• EventStructures.Path.Async.asyncPathId es c = EventStructures.Path.Async.mk es (EventStructures.Path.pathId es c)

def EventStructures.Path.Async.asyncPathComp (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

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

theorem EventStructures.Path.Async.async_path_id_comp (es : EventStructure) {c₁ c₂ : Conf es} (p : Async es c₁ c₂) : asyncPathComp es (asyncPathId es c₁) p = p

Left identity law for asynchronous path composition.

theorem EventStructures.Path.Async.async_path_comp_id (es : EventStructure) {c₁ c₂ : Conf es} (p : Async es c₁ c₂) : asyncPathComp es p (asyncPathId es c₂) = p

Right identity law for asynchronous path composition.

theorem EventStructures.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₄) : asyncPathComp es (asyncPathComp es p₁₂ p₂₃) p₃₄ = asyncPathComp es p₁₂ (asyncPathComp es p₂₃ p₃₄)

Associativity law for asynchronous path composition.

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

The length of a path's trace equals the length of the path.

theorem EventStructures.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 EventStructures.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 EventStructures.Path.trace_not_mem_source (es : EventStructure) {c₁ c₂ : Conf es} (p : Path es c₁ c₂) (e : es.Event) : e ∈ trace es p → e ∉ ↑c₁

Events in the trace of a path are not in the source configuration: each edge adds a fresh event.

theorem EventStructures.Path.trace_nodup (es : EventStructure) {c₁ c₂ : Conf es} (p : Path es c₁ c₂) : (trace es p).Nodup

Every event in the trace of a path appears exactly once: enabling requires freshness, so no event can be executed twice along a path.

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

@[implicit_reducible]

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

The path category of an event structure.

Equations

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

@[implicit_reducible]

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

The asynchronous path category of an event structure.

Equations

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