Independence and commuting concurrent events

This file adds the first true-concurrency refinement to the structural concurrent syntax.

The source syntax Concurrent.Spec and its frontier semantics still admit an interleaving reading: when several frontier events are enabled, a scheduler may pick one and continue with the residual spec.

To recover a more genuinely concurrent perspective, we also want to identify frontier events that come from independent concurrent components and therefore commute. This file does that in the most structural way possible.

Main definitions:

• Independent event₁ event₂ says that two frontier events of the same concurrent spec arise from distinct concurrently live components;
• afterLeft h and afterRight h transport the other event across one chosen independent event;
• diamond h is the commuting residual law: independent events yield the same residual spec regardless of which one is scheduled first.

This is intentionally the minimal true-concurrency layer. It does not yet quotient traces by independence, attach fairness assumptions, or introduce richer partial-order objects such as pomsets or event structures.

inductive Interaction.Concurrent.Independent {S : Spec} : Front S → Front S → Type (u + 1)

Independent event₁ event₂ says that the frontier events event₁ and event₂ of the same concurrent spec come from genuinely independent concurrent components.

Reading by constructors:

• left_right and right_left express that one event comes from the left branch of a parallel spec and the other from the right branch;
• left and right propagate independence recursively inside the left or right concurrent component of a larger parallel spec.

There is intentionally no constructor for two events of the same atomic node: different payload moves of one node are alternative choices, not independent concurrent events.

• left_right {left right : Spec} (eventLeft : Front left) (eventRight : Front right) : Independent eventLeft.left eventRight.right

  Frontier events from opposite sides of the same parallel node are independent.

• right_left {left right : Spec} (eventRight : Front right) (eventLeft : Front left) : Independent eventRight.right eventLeft.left

  Independence is symmetric across the two sides of a parallel node.

• left {left right : Spec} {event₁ event₂ : Front left} (h : Independent event₁ event₂) : Independent event₁.left event₂.left

  Independence inside a left concurrent component lifts to the whole parallel spec.

• right {left right : Spec} {event₁ event₂ : Front right} (h : Independent event₁ event₂) : Independent event₁.right event₂.right

  Independence inside a right concurrent component lifts to the whole parallel spec.

def Interaction.Concurrent.Independent.symm {S : Spec} {event₁ event₂ : Front S} : Independent event₁ event₂ → Independent event₂ event₁

Independence is symmetric.

If event₁ is independent of event₂, then event₂ is independent of event₁.

def Interaction.Concurrent.Independent.afterLeft {S : Spec} {event₁ event₂ : Front S} : Independent event₁ event₂ → Front (residual event₁)

afterLeft h is the residual form of the second event after first scheduling the left-hand event of the independence witness h.

So if h : Independent event₁ event₂, then afterLeft h is an enabled frontier event of the residual spec residual event₁.

def Interaction.Concurrent.Independent.afterRight {S : Spec} {event₁ event₂ : Front S} : Independent event₁ event₂ → Front (residual event₂)

afterRight h is the residual form of the first event after first scheduling the right-hand event of the independence witness h.

So if h : Independent event₁ event₂, then afterRight h is an enabled frontier event of the residual spec residual event₂.

theorem Interaction.Concurrent.Independent.diamond {S : Spec} {event₁ event₂ : Front S} (h : Independent event₁ event₂) : residual h.afterLeft = residual h.afterRight

Independent frontier events commute at the level of residual concurrent specs.

If event₁ and event₂ are independent, then performing event₁ first and then the transported event₂ yields the same residual spec as performing event₂ first and then the transported event₁.