UC composition notation

Scoped notation for open-system boundaries and the free composition syntax. All notation is scoped to Interaction.UC; use open Interaction.UC to bring it into scope.

Typeclasses

The notation is backed by three typeclasses (HasPar, HasWire, HasPlug) with instances for Raw, Expr, and Interp. Each instance is accompanied by a @[simp] bridge lemma that normalizes the typeclass method back to the concrete operation, ensuring that existing simp lemmas (e.g., interpret_par, interpret_wire) continue to fire on notation-introduced terms.

Boundary-level

Notation	Meaning	Input method
Δ₁ ⊗ᵇ Δ₂	PortBoundary.tensor Δ₁ Δ₂	\otimes ^b
Δᵛ	PortBoundary.swap Δ (dual)	\^v

Expression-level

Notation	Meaning	Precedence
e₁ ∥ e₂	HasPar.par e₁ e₂ (parallel)	70, right
e₁ ⊞ e₂	HasWire.wire e₁ e₂ (wire)	65, right
e ⊠ k	HasPlug.plug e k (plug/close)	60, right

Parsing rules

Precedence ensures natural parenthesization:

• A ∥ B ∥ C = A ∥ (B ∥ C) (right-associative)
• A ∥ B ⊞ C = (A ∥ B) ⊞ C (par binds tighter than wire)
• A ⊞ B ⊠ C = (A ⊞ B) ⊠ C (wire binds tighter than plug)
• A ∥ B ⊞ C ∥ D ⊠ E = ((A ∥ B) ⊞ (C ∥ D)) ⊠ E
• Γᵛ ⊗ᵇ Δ = tensor (swap Γ) Δ (postfix ᵛ at max precedence)
• (Δ₁ ⊗ᵇ Δ₂)ᵛ = swap (tensor Δ₁ Δ₂) (parentheses required)

Boundary-level notation

def Interaction.UC.«term_⊗ᵇ_» : Lean.TrailingParserDescr

Tensor (parallel) of port boundaries: Δ₁ ⊗ᵇ Δ₂.

def Interaction.UC.«term_ᵛ» : Lean.TrailingParserDescr

Dual (swap) of a port boundary: Δᵛ means PortBoundary.swap Δ.

The superscript v (typed \^v) visually suggests "flip" or "invert," matching the operation that swaps inputs and outputs. Avoids the Mathlib-global ᵒᵖ (which denotes Opposite).

Composition typeclasses

class Interaction.UC.HasPar (F : PortBoundary → Type u_1) : Type (max 1 u_1)

Parallel composition on boundary-indexed types.

• par {Δ₁ Δ₂ : PortBoundary} : F Δ₁ → F Δ₂ → F (Δ₁.tensor Δ₂)

class Interaction.UC.HasWire (F : PortBoundary → Type u_1) : Type (max 1 u_1)

Wiring (partial internal connection) on boundary-indexed types.

• wire {Δ₁ Γ Δ₂ : PortBoundary} : F (Δ₁.tensor Γ) → F (Γ.swap.tensor Δ₂) → F (Δ₁.tensor Δ₂)

class Interaction.UC.HasPlug (F : PortBoundary → Type u_1) : Type (max 1 u_1)

Plugging (full closure) on boundary-indexed types.

• plug {Δ : PortBoundary} : F Δ → F Δ.swap → F PortBoundary.empty

Notation

def Interaction.UC.«term_∥_» : Lean.TrailingParserDescr

Parallel composition: e₁ ∥ e₂.

def Interaction.UC.«term_⊞_» : Lean.TrailingParserDescr

Wiring: e₁ ⊞ e₂.

def Interaction.UC.«term_⊠_» : Lean.TrailingParserDescr

Plug (full closure): e ⊠ k.

Instances and bridge lemmas for Raw

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Raw.instHasPar {Atom : PortBoundary → Type u_1} : HasPar (Raw Atom)

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Raw.instHasWire {Atom : PortBoundary → Type u_1} : HasWire (Raw Atom)

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Raw.instHasPlug {Atom : PortBoundary → Type u_1} : HasPlug (Raw Atom)

@[simp]

theorem Interaction.UC.OpenSyntax.Raw.hasPar {Atom : PortBoundary → Type u_1} {Δ₁ Δ₂ : PortBoundary} (e₁ : Raw Atom Δ₁) (e₂ : Raw Atom Δ₂) : HasPar.par e₁ e₂ = e₁.par e₂

@[simp]

theorem Interaction.UC.OpenSyntax.Raw.hasWire {Atom : PortBoundary → Type u_1} {Δ₁ Δ₂ Γ : PortBoundary} (e₁ : Raw Atom (Δ₁.tensor Γ)) (e₂ : Raw Atom (Γ.swap.tensor Δ₂)) : HasWire.wire e₁ e₂ = e₁.wire e₂

@[simp]

theorem Interaction.UC.OpenSyntax.Raw.hasPlug {Atom : PortBoundary → Type u_1} {Δ₁ : PortBoundary} (e : Raw Atom Δ₁) (k : Raw Atom Δ₁.swap) : HasPlug.plug e k = e.plug k

Instances and bridge lemmas for Expr

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Expr.instHasPar {Atom : PortBoundary → Type u_1} : HasPar (Expr Atom)

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Expr.instHasWire {Atom : PortBoundary → Type u_1} : HasWire (Expr Atom)

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Expr.instHasPlug {Atom : PortBoundary → Type u_1} : HasPlug (Expr Atom)

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.hasPar {Atom : PortBoundary → Type u_1} {Δ₁ Δ₂ : PortBoundary} (e₁ : Expr Atom Δ₁) (e₂ : Expr Atom Δ₂) : HasPar.par e₁ e₂ = e₁.par e₂

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.hasWire {Atom : PortBoundary → Type u_1} {Δ₁ Δ₂ Γ : PortBoundary} (e₁ : Expr Atom (Δ₁.tensor Γ)) (e₂ : Expr Atom (Γ.swap.tensor Δ₂)) : HasWire.wire e₁ e₂ = e₁.wire e₂

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.hasPlug {Atom : PortBoundary → Type u_1} {Δ₁ : PortBoundary} (e : Expr Atom Δ₁) (k : Expr Atom Δ₁.swap) : HasPlug.plug e k = e.plug k

Instances and bridge lemmas for Interp

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Interp.instHasPar {Atom : PortBoundary → Type u_1} : HasPar (Interp Atom)

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Interp.instHasWire {Atom : PortBoundary → Type u_1} : HasWire (Interp Atom)

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Interp.instHasPlug {Atom : PortBoundary → Type u_1} : HasPlug (Interp Atom)

@[simp]

theorem Interaction.UC.OpenSyntax.Interp.hasPar {Atom : PortBoundary → Type u_1} {Δ₁ Δ₂ : PortBoundary} (e₁ : Interp Atom Δ₁) (e₂ : Interp Atom Δ₂) : HasPar.par e₁ e₂ = e₁.par e₂

@[simp]

theorem Interaction.UC.OpenSyntax.Interp.hasWire {Atom : PortBoundary → Type u_1} {Δ₁ Δ₂ Γ : PortBoundary} (e₁ : Interp Atom (Δ₁.tensor Γ)) (e₂ : Interp Atom (Γ.swap.tensor Δ₂)) : HasWire.wire e₁ e₂ = e₁.wire e₂

@[simp]

theorem Interaction.UC.OpenSyntax.Interp.hasPlug {Atom : PortBoundary → Type u_1} {Δ₁ : PortBoundary} (e : Interp Atom Δ₁) (k : Interp Atom Δ₁.swap) : HasPlug.plug e k = e.plug k

Verification

The following examples verify correct elaboration, precedence, and that bridge lemmas fire correctly with simp.