Traces and the trace monoid

This module defines trace equivalence on lists of events (the congruence generated by swapping adjacent concurrent events), shows it is an equivalence relation and a congruence for concatenation, and builds the trace monoid as the quotient of lists of events by trace equivalence.

inductive EventStructures.TraceEquiv (es : EventStructure) : List es.Event → List es.Event → Prop

Trace equivalence: two traces are equivalent if one can be obtained from the other by swapping adjacent concurrent events.

• refl {es : EventStructure} (t : List es.Event) : TraceEquiv es t t
• swap {es : EventStructure} {e₁ e₂ : es.Event} {t₁ t₂ t₃ : List es.Event} (ind : es.concurrent e₁ e₂) : TraceEquiv es (t₁ ++ e₁ :: e₂ :: t₂) t₃ → TraceEquiv es (t₁ ++ e₂ :: e₁ :: t₂) t₃

theorem EventStructures.Trace.traceEquiv_refl (es : EventStructure) (t : List es.Event) : TraceEquiv es t t

Trace equivalence is reflexive.

theorem EventStructures.Trace.traceEquiv_trans (es : EventStructure) ⦃t₁ t₂ t₃ : List es.Event⦄ : TraceEquiv es t₁ t₂ → TraceEquiv es t₂ t₃ → TraceEquiv es t₁ t₃

Trace equivalence is transitive.

theorem EventStructures.Trace.traceEquiv_symm (es : EventStructure) ⦃t₁ t₂ : List es.Event⦄ : TraceEquiv es t₁ t₂ → TraceEquiv es t₂ t₁

Trace equivalence is symmetric.

theorem EventStructures.Trace.traceEquivEquivalence (es : EventStructure) : Equivalence (TraceEquiv es)

Trace equivalence is an equivalence relation.

@[implicit_reducible]

instance EventStructures.Trace.instTransListEventTraceEquiv (es : EventStructure) : Trans (TraceEquiv es) (TraceEquiv es) (TraceEquiv es)

Trans instance for calc proofs.

Equations

• EventStructures.Trace.instTransListEventTraceEquiv es = { trans := ⋯ }

theorem EventStructures.Trace.traceEquiv_append_left (es : EventStructure) {t₁ t₂ : List es.Event} (h : TraceEquiv es t₁ t₂) (t : List es.Event) : TraceEquiv es (t ++ t₁) (t ++ t₂)

Trace equivalence is a left congruence for append.

theorem EventStructures.Trace.traceEquiv_append_right (es : EventStructure) {t₁ t₂ : List es.Event} (h : TraceEquiv es t₁ t₂) (t : List es.Event) : TraceEquiv es (t₁ ++ t) (t₂ ++ t)

Trace equivalence is a right congruence for append.

theorem EventStructures.Trace.traceEquiv_append (es : EventStructure) {t₁ t₂ t₃ t₄ : List es.Event} (h₁ : TraceEquiv es t₁ t₂) (h₂ : TraceEquiv es t₃ t₄) : TraceEquiv es (t₁ ++ t₃) (t₂ ++ t₄)

Trace equivalence is a congruence for append.

@[implicit_reducible]

instance EventStructures.Trace.traceEquivSetoid (es : EventStructure) : Setoid (List es.Event)

Setoid instance for trace equivalence.

Equations

• EventStructures.Trace.traceEquivSetoid es = { r := EventStructures.TraceEquiv es, iseqv := ⋯ }

def EventStructures.Trace.TraceMonoid (es : EventStructure) : Type

The trace monoid: lists of events quotiented by trace equivalence.

Equations

• EventStructures.Trace.TraceMonoid es = Quotient (EventStructures.Trace.traceEquivSetoid es)

def EventStructures.Trace.Monoid.mk (es : EventStructure) (t : List es.Event) : TraceMonoid es

Lift a list to the trace monoid.

Equations

• EventStructures.Trace.Monoid.mk es t = Quotient.mk (EventStructures.Trace.traceEquivSetoid es) t

@[implicit_reducible]

instance EventStructures.Trace.Monoid.instMulTraceMonoid (es : EventStructure) : Mul (TraceMonoid es)

Multiplication in the trace monoid (concatenation of traces).

Equations

• EventStructures.Trace.Monoid.instMulTraceMonoid es = { mul := Quotient.lift₂ (fun (t₁ t₂ : List es.Event) => EventStructures.Trace.Monoid.mk es (t₁ ++ t₂)) ⋯ }

@[implicit_reducible]

instance EventStructures.Trace.Monoid.instOneTraceMonoid (es : EventStructure) : One (TraceMonoid es)

Identity element in the trace monoid (empty trace).

Equations

• EventStructures.Trace.Monoid.instOneTraceMonoid es = { one := EventStructures.Trace.Monoid.mk es [] }

theorem EventStructures.Trace.Monoid.one_mul (es : EventStructure) (x : TraceMonoid es) : 1 * x = x

Left identity law for trace monoid.

theorem EventStructures.Trace.Monoid.mul_one (es : EventStructure) (x : TraceMonoid es) : x * 1 = x

Right identity law for trace monoid.

theorem EventStructures.Trace.Monoid.mul_assoc (es : EventStructure) (x y z : TraceMonoid es) : x * y * z = x * (y * z)

Associativity law for trace monoid.

@[implicit_reducible]

instance EventStructures.Trace.Monoid.instMonoidTraceMonoid (es : EventStructure) : Monoid (TraceMonoid es)

The trace monoid is a monoid.

Equations

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

theorem EventStructures.Trace.Monoid.move_head_full (es : EventStructure) (hfull : ∀ (e₁ e₂ : es.Event), es.concurrent e₁ e₂) (e : es.Event) (t : List es.Event) : TraceEquiv es (e :: t) (t ++ [e])

If the concurrency relation is full, the head of the list can be moved to the end

theorem EventStructures.Trace.Monoid.mul_comm_full (es : EventStructure) (hfull : ∀ (e₁ e₂ : es.Event), es.concurrent e₁ e₂) (t₁ t₂ : List es.Event) : TraceEquiv es (t₁ ++ t₂) (t₂ ++ t₁)

If the concurrency relation is full, the monoid is commutative.

theorem EventStructures.Trace.Monoid.traceEquiv_eq_empty (es : EventStructure) (hempty : ∀ (e₁ e₂ : es.Event), ¬es.concurrent e₁ e₂) {t₁ t₂ : List es.Event} (h : TraceEquiv es t₁ t₂) : t₁ = t₂

If the concurrency relation is empty, trace equivalence is just list equality.

theorem EventStructures.Trace.Monoid.mul_not_comm_empty (es : EventStructure) (hempty : ∀ (e₁ e₂ : es.Event), ¬es.concurrent e₁ e₂) (hdistinct : ∃ (e₁ : es.Event), ∃ (e₂ : es.Event), e₁ ≠ e₂) : ∃ (t₁ : List es.Event), ∃ (t₂ : List es.Event), ¬TraceEquiv es (t₁ ++ t₂) (t₂ ++ t₁)

If the concurrency relation is empty and there are at least two distinct events, then the monoid is not commutative.