inductive 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 Trace.traceEquiv_refl (es : EventStructure) : Reflexive (TraceEquiv es)

Trace equivalence is reflexive.

theorem Trace.traceEquiv_trans (es : EventStructure) : Transitive (TraceEquiv es)

Trace equivalence is transitive.

theorem Trace.traceEquiv_symm (es : EventStructure) : Symmetric (TraceEquiv es)

Trace equivalence is symmetric.

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

Trans instance for calc proofs.

Equations

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

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

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

Setoid instance for trace equivalence.

Equations

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

def Trace.TraceMonoid (es : EventStructure) : Type

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

Equations

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

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

Lift a list to the trace monoid.

Equations

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

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

Multiplication in the trace monoid (concatenation of traces).

Equations

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

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

Identity element in the trace monoid (empty trace).

Equations

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

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

Left identity law for trace monoid.

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

Right identity law for trace monoid.

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

Associativity law for trace monoid.

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