Interleaving equivalence of concurrent traces

This file adds the first quotient-style refinement on top of finite concurrent traces.

Concurrent.Trace records one concrete scheduler linearization of frontier events. Concurrent.Independent then identifies pairs of frontier events that come from independent concurrent components and commute at the residual-spec level.

The present file packages that commuting behavior into an equivalence relation on traces:

• Trace.cast transports a trace along equality of residual specs;
• Trace.Equiv is the equivalence relation generated by:
  • reflexivity, symmetry, and transitivity;
  • congruence under a common leading step;
  • one local swap rule for adjacent independent frontier events.

This is still intentionally minimal. It does not yet construct quotient types, normal forms, or more elaborate partial-order objects; it only records the standard commuting conversion at the trace level.

def Interaction.Concurrent.Trace.cast {S T : Spec} (h : S = T) (trace : Trace S) : Trace T

Transport a concurrent trace along equality of residual concurrent specs.

This is the trace-level cast operation needed when two independent frontier events commute and therefore produce definitionally different but propositionally equal residual specs.

@[simp]

theorem Interaction.Concurrent.Trace.cast_rfl {S : Spec} (trace : Trace S) : cast ⋯ trace = trace

@[simp]

theorem Interaction.Concurrent.Trace.length_cast {S T : Spec} (h : S = T) (trace : Trace S) : (cast h trace).length = trace.length

inductive Interaction.Concurrent.Trace.Equiv {S : Spec} : Trace S → Trace S → Prop

Equiv trace₁ trace₂ says that the concurrent traces trace₁ and trace₂ represent the same execution up to commuting adjacent independent frontier events.

This relation is generated by:

• refl, symm, and trans, making it an equivalence relation;
• step, which preserves equivalence under a common leading event;
• swap, which performs one adjacent interchange of two independent frontier events.

• refl {S : Spec} (trace : Trace S) : trace.Equiv trace

  Every trace is interleaving-equivalent to itself.

• step {S : Spec} {event : Front S} {tail₁ tail₂ : Trace (residual event)} (h : tail₁.Equiv tail₂) : (Trace.step event tail₁).Equiv (Trace.step event tail₂)

  Equivalence is preserved under a common leading frontier event.

• swap {S : Spec} {event₁ event₂ : Front S} (h : Independent event₁ event₂) (tail : Trace (residual h.afterLeft)) : (Trace.step event₁ (Trace.step h.afterLeft tail)).Equiv (Trace.step event₂ (Trace.step h.afterRight (cast ⋯ tail)))

  Adjacent independent frontier events may be swapped, with the tail transported across the commuting residual equality from Independent.diamond.

• symm {S : Spec} {trace₁ trace₂ : Trace S} (h : trace₁.Equiv trace₂) : trace₂.Equiv trace₁

  Equivalence is symmetric.

• trans {S : Spec} {trace₁ trace₂ trace₃ : Trace S} (h₁ : trace₁.Equiv trace₂) (h₂ : trace₂.Equiv trace₃) : trace₁.Equiv trace₃

  Equivalence is transitive.

theorem Interaction.Concurrent.Trace.Equiv.length_eq {S : Spec} {trace₁ trace₂ : Trace S} : trace₁.Equiv trace₂ → trace₁.length = trace₂.length

Interleaving-equivalent traces have the same length.