Traces up to independence

Trace equivalence over an arbitrary independence relation.

inductive TraceEquiv {α : Type u_1} (R : α → α → Prop) : List α → List α → Prop

Two traces are equivalent when one is obtained from the other by swapping adjacent independent events.

• refl {α : Type u_1} {R : α → α → Prop} (t : List α) : TraceEquiv R t t
• swap {α : Type u_1} {R : α → α → Prop} {e₁ e₂ : α} {t₁ t₂ t₃ : List α} (ind : R e₁ e₂) : TraceEquiv R (t₁ ++ e₁ :: e₂ :: t₂) t₃ → TraceEquiv R (t₁ ++ e₂ :: e₁ :: t₂) t₃

def labels {α : Type u_1} {L : Type u_2} (lbl : α → L) (t : List α) : List L

The label sequence of a trace.

Equations

• labels lbl t = List.map lbl t

def Trace.LabelEquiv {α : Type u_1} {L : Type u_2} (lbl : α → L) (t₁ t₂ : List α) : Prop

Two traces are label-equivalent if they map to the same label sequence.

Equations

• Trace.LabelEquiv lbl t₁ t₂ = (labels lbl t₁ = labels lbl t₂)

instance Trace.labelEquiv_refl {α : Type u_1} {L : Type u_2} (lbl : α → L) : Std.Refl (LabelEquiv lbl)

instance Trace.labelEquiv_symm {α : Type u_1} {L : Type u_2} (lbl : α → L) : Std.Symm (LabelEquiv lbl)

instance Trace.labelEquiv_trans {α : Type u_1} {L : Type u_2} (lbl : α → L) : IsTrans (List α) (LabelEquiv lbl)

def Trace.LabelRespecting {α : Type u_1} {L : Type u_2} (R : α → α → Prop) (lbl : α → L) : Prop

A labelling respects independence if it assigns equal labels to independent events.

Equations

• Trace.LabelRespecting R lbl = ∀ {e₁ e₂ : α}, R e₁ e₂ → lbl e₁ = lbl e₂

theorem Trace.labels_swap_iff {α : Type u_1} {L : Type u_2} (lbl : α → L) {e₁ e₂ : α} {t₁ t₂ : List α} : labels lbl (t₁ ++ e₁ :: e₂ :: t₂) = labels lbl (t₁ ++ e₂ :: e₁ :: t₂) ↔ lbl e₁ = lbl e₂

Swapping two adjacent events preserves the label sequence iff they share a label.

instance Trace.traceEquiv_refl {α : Type u_1} (R : α → α → Prop) : Std.Refl (TraceEquiv R)

Trace equivalence is reflexive.

instance Trace.traceEquiv_trans {α : Type u_1} (R : α → α → Prop) : IsTrans (List α) (TraceEquiv R)

Trace equivalence is transitive.

theorem Trace.traceEquiv_symm {α : Type u_1} (R : α → α → Prop) (hsymm : Std.Symm R) : Std.Symm (TraceEquiv R)

Trace equivalence is symmetric when independence is.

theorem Trace.traceEquiv_imp_labelEquiv {α : Type u_1} {L : Type u_2} (R : α → α → Prop) (lbl : α → L) (hresp : LabelRespecting R lbl) {t₁ t₂ : List α} (h : TraceEquiv R t₁ t₂) : LabelEquiv lbl t₁ t₂

Trace equivalence implies label equivalence for an independence-respecting labelling.

theorem Trace.traceEquivEquivalence {α : Type u_1} (R : α → α → Prop) (hsymm : Std.Symm R) : Equivalence (TraceEquiv R)

Trace equivalence is an equivalence relation when independence is symmetric.

theorem Trace.traceEquiv_append_left {α : Type u_1} (R : α → α → Prop) {t₁ t₂ : List α} (h : TraceEquiv R t₁ t₂) (t : List α) : TraceEquiv R (t ++ t₁) (t ++ t₂)

Trace equivalence is a left congruence for append.

theorem Trace.traceEquiv_append_right {α : Type u_1} (R : α → α → Prop) {t₁ t₂ : List α} (h : TraceEquiv R t₁ t₂) (t : List α) : TraceEquiv R (t₁ ++ t) (t₂ ++ t)

Trace equivalence is a right congruence for append.

theorem Trace.traceEquiv_append {α : Type u_1} (R : α → α → Prop) {t₁ t₂ t₃ t₄ : List α} (h₁ : TraceEquiv R t₁ t₂) (h₂ : TraceEquiv R t₃ t₄) : TraceEquiv R (t₁ ++ t₃) (t₂ ++ t₄)

Trace equivalence is a congruence for append.

def Trace.traceEquivSetoid {α : Type u_1} (R : α → α → Prop) (hsymm : Std.Symm R) : Setoid (List α)

Setoid of traces, for a symmetric independence relation.

Equations

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

Positional trace equivalence

For families, independence is relative to the configuration reached so far.

def reach {L : Type u_3} (F : ConfFamily L) (c : Set F.Event) (t : List F.Event) : Set F.Event

The configuration reached by running t from c.

Equations

• reach F c t = c ∪ {x : F.Event | x ∈ t}

theorem reach_append {L : Type u_3} (F : ConfFamily L) (c : Set F.Event) (t p : List F.Event) : reach F (reach F c t) p = reach F c (t ++ p)

Running t and then p is running t ++ p.

inductive ConfFamily.TraceEquivFrom {L : Type u_3} (F : ConfFamily L) (c : Set F.Event) : List F.Event → List F.Event → Prop

Traces equivalent from a configuration.

• refl {L : Type u_3} {F : ConfFamily L} {c : Set F.Event} (t : List F.Event) : F.TraceEquivFrom c t t
• swap {L : Type u_3} {F : ConfFamily L} {c : Set F.Event} {e₁ e₂ : F.Event} {p t t' : List F.Event} : F.Indep (reach F c p) e₁ e₂ → F.TraceEquivFrom c (p ++ e₁ :: e₂ :: t) t' → F.TraceEquivFrom c (p ++ e₂ :: e₁ :: t) t'

theorem ConfFamily.TraceEquivFrom.trans {L : Type u_3} {F : ConfFamily L} {c : Set F.Event} {t₁ t₂ t₃ : List F.Event} (h₁₂ : F.TraceEquivFrom c t₁ t₂) (h₂₃ : F.TraceEquivFrom c t₂ t₃) : F.TraceEquivFrom c t₁ t₃

theorem ConfFamily.TraceEquivFrom.symm {L : Type u_3} {F : ConfFamily L} {c : Set F.Event} {t₁ t₂ : List F.Event} : F.TraceEquivFrom c t₁ t₂ → F.TraceEquivFrom c t₂ t₁

theorem ConfFamily.TraceEquivFrom.reach_eq {L : Type u_3} {F : ConfFamily L} {c : Set F.Event} {t₁ t₂ : List F.Event} (h : F.TraceEquivFrom c t₁ t₂) : reach F c t₁ = reach F c t₂

Equivalent traces use the same events, so reach the same configuration.

theorem ConfFamily.TraceEquivFrom.append_left {L : Type u_3} {F : ConfFamily L} {c : Set F.Event} {t₁ t₂ : List F.Event} (h : F.TraceEquivFrom c t₁ t₂) (t : List F.Event) : F.TraceEquivFrom c (t₁ ++ t) (t₂ ++ t)

theorem ConfFamily.TraceEquivFrom.append_right {L : Type u_3} {F : ConfFamily L} {c : Set F.Event} (t : List F.Event) {t₁ t₂ : List F.Event} (h : F.TraceEquivFrom (reach F c t) t₁ t₂) : F.TraceEquivFrom c (t ++ t₁) (t ++ t₂)