structure Edge {L : Type u_1} (F : ConfFamily L) (c₁ c₂ : F.Conf) : Type u_2

An edge in the configuration graph: from c₁ to c₂ by adding one event.

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

inductive Path {L : Type u_1} (F : ConfFamily L) : F.Conf → F.Conf → Type u_2

A path in the configuration graph of an event structure.

• refl {L : Type u_1} {F : ConfFamily L} {c : F.Conf} : Path F c c
• step {L : Type u_1} {F : ConfFamily L} {c₁ c₂ c₃ : F.Conf} (hEdge : Edge F c₁ c₂) (hPath : Path F c₂ c₃) : Path F c₁ c₃

def Path.path_id {L : Type u_1} (F : ConfFamily L) (c : F.Conf) : Path F c c

Identity path.

Equations

• Path.path_id F c = Path.refl

def Path.path_comp {L : Type u_1} (F : ConfFamily L) {c₁ c₂ c₃ : F.Conf} (h₁₂ : Path F c₁ c₂) (h₂₃ : Path F c₂ c₃) : Path F c₁ c₃

Composition of paths.

Equations

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

def Path.nextConf {L : Type u_1} (F : ConfFamily L) (c : F.Conf) (e : F.Event) (h : F.enables (↑c) e) : F.Conf

Next configuration after executing an enabled event.

Equations

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

inductive Path.ExecList {L : Type u_1} (F : ConfFamily L) : F.Conf → List F.Event → F.Conf → Type u_2

Execute a list of events from a configuration.

• nil {L : Type u_1} {F : ConfFamily L} (c : F.Conf) : ExecList F c [] c
• cons {L : Type u_1} {F : ConfFamily L} {c c' : F.Conf} {t : List F.Event} (e : F.Event) (h : F.enables (↑c) e) (hnext : ExecList F (nextConf F c e h) t c') : ExecList F c (e :: t) c'

theorem Path.path_comp_id {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (h : Path F c₁ c₂) : path_comp F h (path_id F c₂) = h

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

theorem Path.path_id_comp {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (h : Path F c₁ c₂) : path_comp F (path_id F c₁) h = h

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

theorem Path.path_comp_assoc {L : Type u_1} (F : ConfFamily L) {c₁ c₂ c₃ c₄ : F.Conf} (h₁₂ : Path F c₁ c₂) (h₂₃ : Path F c₂ c₃) (h₃₄ : Path F c₃ c₄) : path_comp F (path_comp F h₁₂ h₂₃) h₃₄ = path_comp F h₁₂ (path_comp F h₂₃ h₃₄)

Associativity law: composition of paths is associative.

def Path.trace {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (hPath : Path F c₁ c₂) : List F.Event

Trace of the path

Equations

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

def Path.length {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (hPath : Path F c₁ c₂) : ℕ

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

Equations

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

def Path.labels {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p : Path F c₁ c₂) : List L

The label sequence of a path: the trace mapped through F.label.

Equations

• Path.labels F p = List.map F.label (Path.trace F p)

@[simp]

theorem Path.length_refl {L : Type u_1} (F : ConfFamily L) {c : F.Conf} : length F refl = 0

@[simp]

theorem Path.length_step {L : Type u_1} (F : ConfFamily L) {c₁ c₂ c₃ : F.Conf} (hEdge : Edge F c₁ c₂) (hPath : Path F c₂ c₃) : length F (step hEdge hPath) = (length F hPath).succ

def Path.execList_to_path {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} {t : List F.Event} (h : ExecList F c₁ t c₂) : Path F c₁ c₂

Build a path from an executable list.

Equations

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

@[simp]

theorem Path.execList_trace {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} {t : List F.Event} (h : ExecList F c₁ t c₂) : trace F (execList_to_path F h) = t

@[simp]

theorem Path.execList_length {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} {t : List F.Event} (h : ExecList F c₁ t c₂) : length F (execList_to_path F h) = t.length

theorem Path.execList_target_eq_union {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} {t : List F.Event} (h : ExecList F c₁ t c₂) : ↑c₂ = ↑c₁ ∪ {e : F.Event | e ∈ t}

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

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

Lift an exec list from a smaller configuration to a larger one.

Equations

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

theorem Path.pathLengthExists {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (h : Nonempty (Path F c₁ c₂)) : ∃ (n : ℕ) (p : Path F c₁ c₂), length F p = n

Existence of a path length.

noncomputable def Path.minPathLength {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (h : Nonempty (Path F c₁ c₂)) : ℕ

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

Equations

• Path.minPathLength F h = Nat.find ⋯

theorem Path.minPathLength_spec {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (h : Nonempty (Path F c₁ c₂)) : ∃ (p : Path F c₁ c₂), length F p = minPathLength F h

theorem Path.minPathLength_le {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (h : Nonempty (Path F c₁ c₂)) (p : Path F c₁ c₂) : minPathLength F h ≤ length F p

theorem Path.execList_to_path_trace {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} {t : List F.Event} (h : ExecList F c₁ t c₂) : trace F (execList_to_path F h) = t

The trace of an execList_to_path is exactly the original list.

def Path.execList_of_path {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p : Path F c₁ c₂) : ExecList F c₁ (trace F p) c₂

Extract an executable list from a path.

Equations

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

@[instance_reducible]

instance Path.pathSetoid {L : Type u_1} (F : ConfFamily L) (c₁ c₂ : F.Conf) : Setoid (Path F c₁ c₂)

Paths are equivalent when their traces commute adjacent independent events.

Equations

• Path.pathSetoid F c₁ c₂ = { r := fun (p q : Path F c₁ c₂) => F.TraceEquivFrom (↑c₁) (Path.trace F p) (Path.trace F q), iseqv := ⋯ }

theorem Path.path_target_eq_reach {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p : Path F c₁ c₂) : ↑c₂ = reach F (↑c₁) (trace F p)

The target of a path is the source extended by the trace.

def Path.PathEquiv {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p₁ p₂ : Path F c₁ c₂) : Prop

Two paths are equivalent if their traces are trace equivalent

Equations

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

instance Path.pathEquiv_refl {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} : Std.Refl (PathEquiv F)

Path equivalence is reflexive.

instance Path.pathEquiv_symm {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} : Std.Symm (PathEquiv F)

Path equivalence is symmetric.

instance Path.pathEquiv_trans {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} : IsTrans (Path F c₁ c₂) (PathEquiv F)

Path equivalence is transitive.

theorem Path.pathEquivEquivalence {L : Type u_1} (F : ConfFamily L) (c₁ c₂ : F.Conf) : Equivalence (PathEquiv F)

Path equivalence is an equivalence relation.

theorem Path.trace_comp {L : Type u_1} (F : ConfFamily L) {c₁ c₂ c₃ : F.Conf} (p₁₂ : Path F c₁ c₂) (p₂₃ : Path F c₂ c₃) : trace F (path_comp F p₁₂ p₂₃) = trace F p₁₂ ++ trace F p₂₃

Trace of path composition is concatenation of traces.

theorem Path.labels_comp {L : Type u_1} (F : ConfFamily L) {c₁ c₂ c₃ : F.Conf} (p₁₂ : Path F c₁ c₂) (p₂₃ : Path F c₂ c₃) : labels F (path_comp F p₁₂ p₂₃) = labels F p₁₂ ++ labels F p₂₃

Path labels are concatenated under path composition.

def Path.Async {L : Type u_1} (F : ConfFamily L) (c₁ c₂ : F.Conf) : Type u_2

Asynchronous path: paths quotiented by path equivalence.

Equations

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

def Path.Async.mk {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p : Path F c₁ c₂) : Async F c₁ c₂

Lift a path to an asynchronous path.

Equations

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

def Path.Async.async_path_id {L : Type u_1} (F : ConfFamily L) (c : F.Conf) : Async F c c

Identity asynchronous path.

Equations

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

def Path.Async.async_path_comp {L : Type u_1} (F : ConfFamily L) {c₁ c₂ c₃ : F.Conf} (p₁₂ : Async F c₁ c₂) (p₂₃ : Async F c₂ c₃) : Async F c₁ c₃

Composition of asynchronous paths.

Equations

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

theorem Path.Async.async_path_id_comp {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p : Async F c₁ c₂) : async_path_comp F (async_path_id F c₁) p = p

Left identity law for asynchronous path composition.

theorem Path.Async.async_path_comp_id {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p : Async F c₁ c₂) : async_path_comp F p (async_path_id F c₂) = p

Right identity law for asynchronous path composition.

theorem Path.Async.assoc {L : Type u_1} (F : ConfFamily L) {c₁ c₂ c₃ c₄ : F.Conf} (p₁₂ : Async F c₁ c₂) (p₂₃ : Async F c₂ c₃) (p₃₄ : Async F c₃ c₄) : async_path_comp F (async_path_comp F p₁₂ p₂₃) p₃₄ = async_path_comp F p₁₂ (async_path_comp F p₂₃ p₃₄)

Associativity law for asynchronous path composition.

theorem Path.trace_length_eq_length {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p : Path F c₁ c₂) : (trace F p).length = length F p

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

theorem Path.path_subset {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p : Path F c₁ c₂) : ↑c₁ ⊆ ↑c₂

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

theorem Path.trace_of_path {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p : Path F c₁ c₂) (e : F.Event) : e ∈ trace F p → e ∈ ↑c₂

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

theorem Path.path_length_ge_trace_length {L : Type u_1} (F : ConfFamily L) {c₁ c₂ : F.Conf} (p : Path F c₁ c₂) : length F p = (trace F p).length

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

@[instance_reducible]

instance pathCategory {L : Type u_1} (F : ConfFamily L) : CategoryTheory.Category.{u_2, u_2} F.Conf

The path category of the configuration family.

Equations

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

@[instance_reducible]

instance asyncPathCategory {L : Type u_1} (F : ConfFamily L) : CategoryTheory.Category.{u_2, u_2} F.Conf

The asynchronous path category of the configuration family.

Equations

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