diff --git a/PolyFun.lean b/PolyFun.lean index 9aa92432..565e8dc1 100644 --- a/PolyFun.lean +++ b/PolyFun.lean @@ -125,6 +125,7 @@ public import PolyFun.Interaction.UC.OpenProcessCoherence public import PolyFun.Interaction.UC.OpenProcessFactorization public import PolyFun.Interaction.UC.OpenProcessInterleave public import PolyFun.Interaction.UC.OpenProcessModel +public import PolyFun.Interaction.UC.OpenProcessSamplerCoherence public import PolyFun.Interaction.UC.OpenProcessSamplerEquiv public import PolyFun.Interaction.UC.OpenProcessSamplerFactorization public import PolyFun.Interaction.UC.OpenSyntax.AtomSubTheory diff --git a/PolyFun/Interaction/UC/OpenProcessCoherence.lean b/PolyFun/Interaction/UC/OpenProcessCoherence.lean index 34d70578..c99944cc 100644 --- a/PolyFun/Interaction/UC/OpenProcessCoherence.lean +++ b/PolyFun/Interaction/UC/OpenProcessCoherence.lean @@ -43,6 +43,7 @@ namespace Interaction namespace UC open Concurrent +open PFunctor.FreeM.Displayed (Decoration) variable {m : Type w → Type w'} {Party : Type u} @@ -133,6 +134,107 @@ theorem isSilentStep_interleave_right_iff {Δ₁ Δ₂ Δ : PortBoundary} end OpenProcess +/-! ## Branches of a composite step -/ + +namespace OpenProcess + +variable {Δ₁ Δ₂ Δ Δ' : PortBoundary} + (p₁ : OpenProcess.{u, v, w, w'} m Party Δ₁) (p₂ : OpenProcess.{u, v, w, w'} m Party Δ₂) + (f₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ)) + (f₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ)) + (c : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)) (σ : m (ULift.{w, 0} Bool)) + (g : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ) + (OpenNodeContext.{u, w} Party Δ')) + (s₁ : p₁.Proc) (s₂ : p₂.Proc) + +/-- A left-scheduled composite step is silent when the scheduler node is and +the re-decorated component step is. -/ +theorem isSilentStep_interleave_left_iff_decoration (tr : (p₁.step s₁).tree.Path) : + IsSilentStep (p₁.interleave p₂ f₁ f₂ c σ) (s₁, s₂) ⟨⟨true⟩, tr⟩ ↔ + c.boundary.isActivated = false ∧ + IsSilentDecoration (Decoration.map f₁ _ (p₁.step s₁).semantics) tr := by + simp only [IsSilentStep, OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep, + PFunctor.DynSystem.expose_mk', IsSilentDecoration] + +/-- A right-scheduled composite step is silent when the scheduler node is and +the re-decorated component step is. -/ +theorem isSilentStep_interleave_right_iff_decoration (tr : (p₂.step s₂).tree.Path) : + IsSilentStep (p₁.interleave p₂ f₁ f₂ c σ) (s₁, s₂) ⟨⟨false⟩, tr⟩ ↔ + c.boundary.isActivated = false ∧ + IsSilentDecoration (Decoration.map f₂ _ (p₂.step s₂).semantics) tr := by + simp only [IsSilentStep, OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep, + PFunctor.DynSystem.expose_mk', IsSilentDecoration] + +/-- Silence of the left branch of a re-decorated composite step. -/ +theorem isSilentDecoration_map_interleave_left (tr : (p₁.step s₁).tree.Path) : + IsSilentDecoration + (Decoration.map g _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics) + ⟨⟨true⟩, tr⟩ ↔ + (g _ c).boundary.isActivated = false ∧ + IsSilentDecoration (Decoration.map g _ (Decoration.map f₁ _ (p₁.step s₁).semantics)) + tr := by + simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep, + PFunctor.DynSystem.expose_mk', OpenNodeContext.decoration_map_node, IsSilentDecoration] + +/-- Silence of the right branch of a re-decorated composite step. -/ +theorem isSilentDecoration_map_interleave_right (tr : (p₂.step s₂).tree.Path) : + IsSilentDecoration + (Decoration.map g _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics) + ⟨⟨false⟩, tr⟩ ↔ + (g _ c).boundary.isActivated = false ∧ + IsSilentDecoration (Decoration.map g _ (Decoration.map f₂ _ (p₂.step s₂).semantics)) + tr := by + simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep, + PFunctor.DynSystem.expose_mk', OpenNodeContext.decoration_map_node, IsSilentDecoration] + +/-- The boundary trace of a left-scheduled composite step. -/ +theorem boundaryTrace_interleave_left (tr : (p₁.step s₁).tree.Path) : + OpenNodeContext.boundaryTrace _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics + ⟨⟨true⟩, tr⟩ = + c.boundary.emit ⟨true⟩ * + OpenNodeContext.boundaryTrace _ (Decoration.map f₁ _ (p₁.step s₁).semantics) tr := by + simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep, + PFunctor.DynSystem.expose_mk'] + exact OpenNodeContext.boundaryTrace_node _ _ _ _ + +/-- The boundary trace of a right-scheduled composite step. -/ +theorem boundaryTrace_interleave_right (tr : (p₂.step s₂).tree.Path) : + OpenNodeContext.boundaryTrace _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics + ⟨⟨false⟩, tr⟩ = + c.boundary.emit ⟨false⟩ * + OpenNodeContext.boundaryTrace _ (Decoration.map f₂ _ (p₂.step s₂).semantics) tr := by + simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep, + PFunctor.DynSystem.expose_mk'] + exact OpenNodeContext.boundaryTrace_node _ _ _ _ + +/-- The boundary trace of the left branch of a re-decorated composite step. -/ +theorem boundaryTrace_map_interleave_left (tr : (p₁.step s₁).tree.Path) : + OpenNodeContext.boundaryTrace _ + (Decoration.map g _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics) + ⟨⟨true⟩, tr⟩ = + (g _ c).boundary.emit ⟨true⟩ * + OpenNodeContext.boundaryTrace _ + (Decoration.map g _ (Decoration.map f₁ _ (p₁.step s₁).semantics)) tr := by + simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep, + PFunctor.DynSystem.expose_mk', OpenNodeContext.decoration_map_node] + exact OpenNodeContext.boundaryTrace_node _ _ _ _ + +/-- The boundary trace of the right branch of a re-decorated composite step. -/ +theorem boundaryTrace_map_interleave_right (tr : (p₂.step s₂).tree.Path) : + OpenNodeContext.boundaryTrace _ + (Decoration.map g _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics) + ⟨⟨false⟩, tr⟩ = + (g _ c).boundary.emit ⟨false⟩ * + OpenNodeContext.boundaryTrace _ + (Decoration.map g _ (Decoration.map f₂ _ (p₂.step s₂).semantics)) tr := by + simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep, + PFunctor.DynSystem.expose_mk', OpenNodeContext.decoration_map_node] + exact OpenNodeContext.boundaryTrace_node _ _ _ _ + +end OpenProcess + /-! ## The three coherence shapes -/ section Shapes diff --git a/PolyFun/Interaction/UC/OpenProcessFactorization.lean b/PolyFun/Interaction/UC/OpenProcessFactorization.lean index d27c908a..7cddb171 100644 --- a/PolyFun/Interaction/UC/OpenProcessFactorization.lean +++ b/PolyFun/Interaction/UC/OpenProcessFactorization.lean @@ -7,6 +7,7 @@ Authors: Devon Tuma module public import PolyFun.Interaction.UC.OpenProcessModel +public import PolyFun.Interaction.UC.OpenProcessSamplerCoherence /-! # Plug factorization for the process model, up to activation equivalence @@ -41,8 +42,9 @@ with the context, and the inner pair is commuted under composite under `OpenProcess.interleave_congr_left`. `OpenProcessFactorization.sourceSchedule`, `leftSchedule`, and `rightSchedule` -record the scheduler truth tables of the two sides; the sampler-aware laws -consume them. +record the scheduler truth tables of the two sides, indexed by the leaf type +`OpenProcessFactorization.Leaf` of `OpenProcessSamplerCoherence`; the +sampler-aware laws consume them. -/ public section @@ -63,14 +65,6 @@ variable (schedulerSampler : m (ULift.{w, 0} Bool)) namespace OpenProcessFactorization -/-- The component selected after flattening either side of a plug -factorization. -/ -inductive Leaf where - | first - | second - | context - deriving DecidableEq, Repr - /-- Scheduler choices on the source shape `plug (compose W₁ W₂) K`. The outer choice is listed first; the inner choice is present only when the composite is selected. -/ diff --git a/PolyFun/Interaction/UC/OpenProcessInterleave.lean b/PolyFun/Interaction/UC/OpenProcessInterleave.lean index 1e7c1bc4..ebc171a1 100644 --- a/PolyFun/Interaction/UC/OpenProcessInterleave.lean +++ b/PolyFun/Interaction/UC/OpenProcessInterleave.lean @@ -47,6 +47,7 @@ namespace Interaction namespace UC open Concurrent +open PFunctor.FreeM.Displayed (Decoration) /-! ## Activation-preserving context homs -/ @@ -106,6 +107,182 @@ theorem preservesActivation_close (Δ : PortBoundary) : intro X ons simp [OpenNodeContext.close, BoundaryAction.closed] +/-! ## Internal nodes and trace relabelling + +The sampler-level coherence theorems compare boundary traces, so they need two +finer pieces of data about a hom than activation preservation: whether a node +is fully internal after the hom, and how the hom acts on emitted traces. -/ + +/-- A node that is neither activated nor emits anything: the boundary action +of a scheduler node after any of the theory's boundary adaptations. -/ +@[expose] +def IsInternalNode {Δ : PortBoundary} {X : Type w} (c : OpenNodeContext.{u, w} Party Δ X) : + Prop := + c.boundary = BoundaryAction.internal Δ X + +theorem IsInternalNode.isActivated {Δ : PortBoundary} {X : Type w} + {c : OpenNodeContext.{u, w} Party Δ X} (hc : IsInternalNode c) : + c.boundary.isActivated = false := by + rw [hc]; rfl + +theorem IsInternalNode.emit {Δ : PortBoundary} {X : Type w} + {c : OpenNodeContext.{u, w} Party Δ X} (hc : IsInternalNode c) (x : X) : + c.boundary.emit x = 1 := by + rw [hc]; rfl + +theorem IsInternalNode.map {Δ₁ Δ₂ : PortBoundary} {X : Type w} + {c : OpenNodeContext.{u, w} Party Δ₁ X} (hc : IsInternalNode c) (φ : PortBoundary.Hom Δ₁ Δ₂) : + IsInternalNode (OpenNodeContext.map Party φ X c) := by + unfold IsInternalNode at hc ⊢ + simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, hc, BoundaryAction.mapBoundary, + BoundaryAction.internal] + +theorem IsInternalNode.inlTensor {Δ₁ : PortBoundary} (Δ₂ : PortBoundary) {X : Type w} + {c : OpenNodeContext.{u, w} Party Δ₁ X} (hc : IsInternalNode c) : + IsInternalNode (OpenNodeContext.inlTensor Party Δ₁ Δ₂ X c) := by + unfold IsInternalNode at hc ⊢ + simp [OpenNodeContext.inlTensor, hc, BoundaryAction.embedInlTensor, BoundaryAction.internal] + +theorem IsInternalNode.inrTensor (Δ₁ : PortBoundary) {Δ₂ : PortBoundary} {X : Type w} + {c : OpenNodeContext.{u, w} Party Δ₂ X} (hc : IsInternalNode c) : + IsInternalNode (OpenNodeContext.inrTensor Party Δ₁ Δ₂ X c) := by + unfold IsInternalNode at hc ⊢ + simp [OpenNodeContext.inrTensor, hc, BoundaryAction.embedInrTensor, BoundaryAction.internal] + +theorem IsInternalNode.wireLeft {Δ₁ Γ : PortBoundary} (Δ₂ : PortBoundary) {X : Type w} + {c : OpenNodeContext.{u, w} Party (PortBoundary.tensor Δ₁ Γ) X} (hc : IsInternalNode c) : + IsInternalNode (OpenNodeContext.wireLeft Party Δ₁ Γ Δ₂ X c) := by + unfold IsInternalNode at hc ⊢ + simp [OpenNodeContext.wireLeft, hc, BoundaryAction.wireLeft, BoundaryAction.internal] + +theorem IsInternalNode.wireRight (Δ₁ : PortBoundary) {Γ Δ₂ : PortBoundary} {X : Type w} + {c : OpenNodeContext.{u, w} Party (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂) X} + (hc : IsInternalNode c) : + IsInternalNode (OpenNodeContext.wireRight Party Δ₁ Γ Δ₂ X c) := by + unfold IsInternalNode at hc ⊢ + simp [OpenNodeContext.wireRight, hc, BoundaryAction.wireRight, BoundaryAction.internal] + +theorem IsInternalNode.close {Δ : PortBoundary} {X : Type w} + {c : OpenNodeContext.{u, w} Party Δ X} (hc : IsInternalNode c) : + IsInternalNode (OpenNodeContext.close Party Δ X c) := by + unfold IsInternalNode at hc ⊢ + simp [OpenNodeContext.close, hc, BoundaryAction.closed, BoundaryAction.internal] + +/-- A hom **emits along** a partial relabelling `g` of output packets when it +acts on every node's emitted trace by `g`. All of the theory's boundary +adaptations do. -/ +@[expose] +def EmitsAlong {Δ₁ Δ₂ : PortBoundary} + (h : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ₂)) + (g : PFunctor.Idx Δ₁.Out → Option (PFunctor.Idx Δ₂.Out)) : Prop := + ∀ (X : Type w) (ons : OpenNodeContext Party Δ₁ X), + (h X ons).boundary.emit = PFunctor.Trace.mapPartial g ons.boundary.emit + +theorem emitsAlong_id (Δ : PortBoundary) : + EmitsAlong (TypeTree.Node.ContextHom.id (OpenNodeContext.{u, w} Party Δ)) + (fun i => some i) := by + intro X ons + simp [TypeTree.Node.ContextHom.id] + +theorem EmitsAlong.comp {Δ₁ Δ₂ Δ₃ : PortBoundary} + {h₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ₃)} + {h₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ₂)} + {g₂ : PFunctor.Idx Δ₂.Out → Option (PFunctor.Idx Δ₃.Out)} + {g₁ : PFunctor.Idx Δ₁.Out → Option (PFunctor.Idx Δ₂.Out)} + (hh₂ : EmitsAlong h₂ g₂) (hh₁ : EmitsAlong h₁ g₁) : + EmitsAlong (TypeTree.Node.ContextHom.comp h₂ h₁) (fun i => (g₁ i).bind g₂) := by + intro X ons + change (h₂ X (h₁ X ons)).boundary.emit = _ + rw [hh₂, hh₁, PFunctor.Trace.mapPartial_comp] + +theorem emitsAlong_map {Δ₁ Δ₂ : PortBoundary} (φ : PortBoundary.Hom Δ₁ Δ₂) : + EmitsAlong (OpenNodeContext.map.{u, w} Party φ) + (fun i => some (PFunctor.Chart.mapIdx φ.onOut i)) := by + intro X ons + simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, BoundaryAction.mapBoundary, + PFunctor.Trace.mapChart] + +theorem emitsAlong_inlTensor (Δ₁ Δ₂ : PortBoundary) : + EmitsAlong (OpenNodeContext.inlTensor.{u, w} Party Δ₁ Δ₂) + (fun i => some (PFunctor.Chart.mapIdx (Interface.Hom.inl Δ₁.Out Δ₂.Out) i)) := by + intro X ons + simp [OpenNodeContext.inlTensor, BoundaryAction.embedInlTensor, PFunctor.Trace.mapChart] + +theorem emitsAlong_inrTensor (Δ₁ Δ₂ : PortBoundary) : + EmitsAlong (OpenNodeContext.inrTensor.{u, w} Party Δ₁ Δ₂) + (fun i => some (PFunctor.Chart.mapIdx (Interface.Hom.inr Δ₁.Out Δ₂.Out) i)) := by + intro X ons + simp [OpenNodeContext.inrTensor, BoundaryAction.embedInrTensor, PFunctor.Trace.mapChart] + +theorem emitsAlong_wireLeft (Δ₁ Γ Δ₂ : PortBoundary) : + EmitsAlong (OpenNodeContext.wireLeft.{u, w} Party Δ₁ Γ Δ₂) + (fun + | ⟨Sum.inl a₁, m⟩ => some ⟨Sum.inl a₁, m⟩ + | ⟨Sum.inr _, _⟩ => none) := by + intro X ons + simp only [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] + exact congrArg (fun g => PFunctor.Trace.mapPartial g _) + (funext fun i => by rcases i with ⟨(_ | _), _⟩ <;> rfl) + +theorem emitsAlong_wireRight (Δ₁ Γ Δ₂ : PortBoundary) : + EmitsAlong (OpenNodeContext.wireRight.{u, w} Party Δ₁ Γ Δ₂) + (fun + | ⟨Sum.inl _, _⟩ => none + | ⟨Sum.inr a₂, m⟩ => some ⟨Sum.inr a₂, m⟩) := by + intro X ons + simp only [OpenNodeContext.wireRight, BoundaryAction.wireRight] + exact congrArg (fun g => PFunctor.Trace.mapPartial g _) + (funext fun i => by rcases i with ⟨(_ | _), _⟩ <;> rfl) + +theorem emitsAlong_close (Δ : PortBoundary) : + EmitsAlong (OpenNodeContext.close.{u, w} Party Δ) (fun _ => none) := by + intro X ons + funext x + simp only [OpenNodeContext.close, BoundaryAction.closed, PFunctor.Trace.mapPartial_apply] + exact (List.filterMap_eq_nil_iff.mpr fun _ _ => rfl).symm + +/-- Re-decorating a node applies the hom at the node and recursively below. -/ +theorem decoration_map_node {Δ₁ Δ₂ : PortBoundary} + (h : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ₂)) + {X : Type w} (rest : X → TypeTree.{w}) + (d : Decoration (OpenNodeContext.{u, w} Party Δ₁) (TypeTree.node X rest)) : + Decoration.map h (TypeTree.node X rest) d = + ⟨h X d.1, fun x => Decoration.map h (rest x) (d.2 x)⟩ := + rfl + +/-- Re-decorating twice is re-decorating along the composite. -/ +theorem decoration_map_map {Δ₁ Δ₂ Δ₃ : PortBoundary} + (g : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ₃)) + (f : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ₂)) + (spec : TypeTree.{w}) (d : Decoration (OpenNodeContext.{u, w} Party Δ₁) spec) : + Decoration.map g spec (Decoration.map f spec d) = + Decoration.map (TypeTree.Node.ContextHom.comp g f) spec d := + TypeTree.Decoration.map_comp g f spec d + +/-- Boundary traces after a hom that emits along `g` are the `g`-relabelled +traces. -/ +theorem boundaryTrace_map_of_emitsAlong {Δ₁ Δ₂ : PortBoundary} + {h : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ₂)} + {g : PFunctor.Idx Δ₁.Out → Option (PFunctor.Idx Δ₂.Out)} (hg : EmitsAlong h g) : + ∀ {spec : TypeTree.{w}} (d : Decoration (OpenNodeContext.{u, w} Party Δ₁) spec) + (tr : spec.Path), + boundaryTrace spec (Decoration.map h spec d) tr = + PFunctor.TraceList.mapPartial g (boundaryTrace spec d tr) + | .done, _, _ => by + rw [boundaryTrace_done, boundaryTrace_done, PFunctor.TraceList.mapPartial_one] + | .node _ rest, d, ⟨x, tr⟩ => by + rw [decoration_map_node, boundaryTrace_node, boundaryTrace_node, + boundaryTrace_map_of_emitsAlong hg (d.2 x) tr, hg, PFunctor.TraceList.mapPartial_mul] + rfl + + end OpenNodeContext namespace OpenProcess diff --git a/PolyFun/Interaction/UC/OpenProcessSamplerCoherence.lean b/PolyFun/Interaction/UC/OpenProcessSamplerCoherence.lean new file mode 100644 index 00000000..946b3634 --- /dev/null +++ b/PolyFun/Interaction/UC/OpenProcessSamplerCoherence.lean @@ -0,0 +1,1179 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ + +module + +import all PolyFun.Interaction.Basic.Sampler +import all PolyFun.Interaction.UC.OpenProcess +import all PolyFun.Interaction.UC.OpenProcessSamplerEquiv +public import PolyFun.Interaction.Basic.Sampler +public import PolyFun.Interaction.UC.OpenProcessCoherence +public import PolyFun.Interaction.UC.OpenProcessSamplerEquiv + +/-! +# Coherence of interleaving up to sampler equivalence + +`OpenProcessCoherence` proves the coherence shapes of `OpenProcess.interleave` +up to activation equivalence, which erases sampler effects. This module proves +the same shapes up to `OpenProcessSamplerEquiv R`, the strong one-step matching +that retains sampled paths relative to a relation family `R`. + +A regrouping of nested interleavings only moves scheduler nodes, so the two +sides decorate every leaf identically once the injections are composed. That +is the hypothesis form used here: the composite injections of a leaf on the two +sides are *equal*, and every scheduler node is an internal node +(`OpenNodeContext.IsInternalNode`: silent and emitting nothing). What a +regrouping does change is the encoding of the scheduler draw, and the single +remaining hypothesis of each shape is that the two nested draws are `R`-related: + +* `interleave_factorLeft_samplerEquiv`: `(p₁ ∥ p₂) ∥ p₃ ≈ p₁ ∥ (p₃ ∥ p₂)`, + the left plug factorization, given + `R.rel (nestedDrawLeft σOut σIn) (nestedDrawFactorLeft τOut τIn)`; +* `interleave_factorRight_samplerEquiv`: `(p₁ ∥ p₂) ∥ p₃ ≈ p₂ ∥ (p₃ ∥ p₁)`, + the right plug factorization; +* `interleave_comm_samplerEquiv`: `p₁ ∥ p₂ ≈ p₂ ∥ p₁`, given + `R.rel (schedulerFlip <$> σ) τ`; +* `interleave_rehome_samplerEquiv`: the same interleaving under another + internal scheduler node, given `R.rel σ τ`; +* `interleave_assoc_samplerEquiv`: `(p₁ ∥ p₂) ∥ p₃ ≈ p₁ ∥ (p₂ ∥ p₃)`, derived + from the left factorization and commutation of the inner pair. + +The draws take two scheduler samplers per nesting so that both the shared +sampler of `openTheory` and the mass-dependent samplers of +`scheduledOpenTheory` are instances. Unit absorption has no sampler-level +version: a silent unit adds a path to every step, so no path bijection exists. + +Sampler equivalence is also a congruence for `interleave` and `mapHom` +(`OpenProcess.interleave_congr_{left,right}_samplerEquiv`, +`OpenProcess.mapHom_congr_samplerEquiv`), which needs the relation family to be +a congruence for the continuation of `bind` as well +(`MonadRelFamily.IsBindCongr`) and the injections to act on boundary traces by +relabelling (`OpenNodeContext.EmitsAlong`). +-/ + +public section + +universe u v w w' + +namespace Interaction +namespace UC + +open Concurrent +open PFunctor.FreeM.Displayed (Decoration) + +/- Lean 4.33 compares assigned metavariable types at implicit transparency; +the proofs below rewrite through the interleaved dynamical model there. +`implicit_reducible` (unlike `reducible`) stays invisible to simp validation and +instance search. -/ +attribute [local implicit_reducible] PFunctor.DynSystem.expose PFunctor.DynSystem.update + PFunctor.DynSystem.mk' Concurrent.ProcessOver.interleave OpenProcess.mapHom + OpenProcess.interleave + +/-! ## Right-continuation congruence -/ + +/-- A relation family is **bind-congruent on the right** when binding a common +computation against pointwise related continuations gives related results. +Together with `MonadRelFamily.bind_congr` this makes the family a congruence +for `bind`. Equality and the everything-relation satisfy it, as does equality +of output distributions. -/ +class MonadRelFamily.IsBindCongr {m : Type w → Type w'} [Monad m] + (R : MonadRelFamily m) : Prop where + /-- Binding against pointwise related continuations preserves the relation. -/ + bind_congr_right : ∀ {α β : Type w} (x : m α) {f g : α → m β}, + (∀ a, R.rel (f a) (g a)) → R.rel (x >>= f) (x >>= g) + +theorem MonadRelFamily.bind_congr_right {m : Type w → Type w'} [Monad m] + (R : MonadRelFamily m) [R.IsBindCongr] {α β : Type w} (x : m α) {f g : α → m β} + (h : ∀ a, R.rel (f a) (g a)) : R.rel (x >>= f) (x >>= g) := + IsBindCongr.bind_congr_right x h + +instance MonadRelFamily.eq_isBindCongr {m : Type w → Type w'} [Monad m] : + (MonadRelFamily.eq m).IsBindCongr where + bind_congr_right := by + intro α β x f g h + exact (MonadRelFamily.eq_rel _ _).mpr + (congrArg (x >>= ·) (funext fun a => (MonadRelFamily.eq_rel _ _).mp (h a))) + +instance MonadRelFamily.top_isBindCongr {m : Type w → Type w'} [Monad m] : + (MonadRelFamily.top m).IsBindCongr where + bind_congr_right := by + intro α β x f g _ + exact MonadRelFamily.top_rel _ _ + +/-! ## Leaves and nested scheduler draws -/ + +namespace OpenProcessFactorization + +/-- The leaf selected by a ternary regrouping of interleavings. `context` names +the third leaf; in the plug factorizations it is the closing context. -/ +inductive Leaf where + | first + | second + | context + deriving DecidableEq, Repr + +end OpenProcessFactorization + +open OpenProcessFactorization (Leaf) + +/-- The leaf reached by the source nesting `(first ∥ second) ∥ context`: the +outer coin selects the pair, the inner coin its component. -/ +@[expose] +def nestedDrawLeft {m : Type w → Type w'} [Monad m] (σOut σIn : m (ULift.{w, 0} Bool)) : + m (ULift.{w, 0} Leaf) := + σOut >>= fun + | ⟨true⟩ => σIn >>= fun + | ⟨true⟩ => pure ⟨.first⟩ + | ⟨false⟩ => pure ⟨.second⟩ + | ⟨false⟩ => pure ⟨.context⟩ + +/-- The leaf reached by the left-factored nesting `first ∥ (context ∥ second)`. -/ +@[expose] +def nestedDrawFactorLeft {m : Type w → Type w'} [Monad m] (τOut τIn : m (ULift.{w, 0} Bool)) : + m (ULift.{w, 0} Leaf) := + τOut >>= fun + | ⟨true⟩ => pure ⟨.first⟩ + | ⟨false⟩ => τIn >>= fun + | ⟨true⟩ => pure ⟨.context⟩ + | ⟨false⟩ => pure ⟨.second⟩ + +/-- The leaf reached by the right-factored nesting `second ∥ (context ∥ first)`. -/ +@[expose] +def nestedDrawFactorRight {m : Type w → Type w'} [Monad m] (τOut τIn : m (ULift.{w, 0} Bool)) : + m (ULift.{w, 0} Leaf) := + τOut >>= fun + | ⟨true⟩ => pure ⟨.second⟩ + | ⟨false⟩ => τIn >>= fun + | ⟨true⟩ => pure ⟨.context⟩ + | ⟨false⟩ => pure ⟨.first⟩ + +/-- Binding the source nesting's draw against a per-leaf continuation is the +flattened two-coin computation. -/ +theorem nestedDrawLeft_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] + (σOut σIn : m (ULift.{w, 0} Bool)) {α : Type w} (h : ULift.{w, 0} Leaf → m α) : + nestedDrawLeft σOut σIn >>= h = + σOut >>= fun + | ⟨true⟩ => σIn >>= fun + | ⟨true⟩ => h ⟨.first⟩ + | ⟨false⟩ => h ⟨.second⟩ + | ⟨false⟩ => h ⟨.context⟩ := by + simp only [nestedDrawLeft, bind_assoc] + refine bind_congr fun b => ?_ + obtain ⟨bb⟩ := b + cases bb + · simp only [pure_bind] + · simp only [bind_assoc] + refine bind_congr fun b' => ?_ + obtain ⟨bb'⟩ := b' + cases bb' <;> simp only [pure_bind] + +/-- Binding the left-factored draw against a per-leaf continuation is the +flattened two-coin computation. -/ +theorem nestedDrawFactorLeft_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] + (τOut τIn : m (ULift.{w, 0} Bool)) {α : Type w} (h : ULift.{w, 0} Leaf → m α) : + nestedDrawFactorLeft τOut τIn >>= h = + τOut >>= fun + | ⟨true⟩ => h ⟨.first⟩ + | ⟨false⟩ => τIn >>= fun + | ⟨true⟩ => h ⟨.context⟩ + | ⟨false⟩ => h ⟨.second⟩ := by + simp only [nestedDrawFactorLeft, bind_assoc] + refine bind_congr fun b => ?_ + obtain ⟨bb⟩ := b + cases bb + · simp only [bind_assoc] + refine bind_congr fun b' => ?_ + obtain ⟨bb'⟩ := b' + cases bb' <;> simp only [pure_bind] + · simp only [pure_bind] + +/-- Binding the right-factored draw against a per-leaf continuation is the +flattened two-coin computation. -/ +theorem nestedDrawFactorRight_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] + (τOut τIn : m (ULift.{w, 0} Bool)) {α : Type w} (h : ULift.{w, 0} Leaf → m α) : + nestedDrawFactorRight τOut τIn >>= h = + τOut >>= fun + | ⟨true⟩ => h ⟨.second⟩ + | ⟨false⟩ => τIn >>= fun + | ⟨true⟩ => h ⟨.context⟩ + | ⟨false⟩ => h ⟨.first⟩ := by + simp only [nestedDrawFactorRight, bind_assoc] + refine bind_congr fun b => ?_ + obtain ⟨bb⟩ := b + cases bb + · simp only [bind_assoc] + refine bind_congr fun b' => ?_ + obtain ⟨bb'⟩ := b' + cases bb' <;> simp only [pure_bind] + · simp only [pure_bind] + +/-! ## Scheduler re-encodings -/ + +/-- Negate a lifted scheduler coin: the path re-encoding of commutation. -/ +@[expose] +def schedulerFlip : ULift.{w, 0} Bool → ULift.{w, 0} Bool := + fun b => ULift.up !b.down + +@[simp] theorem schedulerFlip_up_true : + schedulerFlip.{w} (ULift.up true) = ULift.up false := rfl + +@[simp] theorem schedulerFlip_up_false : + schedulerFlip.{w} (ULift.up false) = ULift.up true := rfl + +/-- Flip the scheduler coin at the root of a binary-choice interleaving tree, +exchanging the two branches. -/ +@[expose] +def flipInterleavePathEquiv (t₁ t₂ : TypeTree.{w}) : + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => t₂) ≃ + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₂ + | ⟨false⟩ => t₁) where + toFun := fun + | ⟨⟨true⟩, tr⟩ => ⟨⟨false⟩, tr⟩ + | ⟨⟨false⟩, tr⟩ => ⟨⟨true⟩, tr⟩ + invFun := fun + | ⟨⟨true⟩, tr⟩ => ⟨⟨false⟩, tr⟩ + | ⟨⟨false⟩, tr⟩ => ⟨⟨true⟩, tr⟩ + left_inv := by rintro ⟨⟨b⟩, tr⟩; cases b <;> rfl + right_inv := by rintro ⟨⟨b⟩, tr⟩; cases b <;> rfl + +theorem flipInterleavePathEquiv_apply_true (t₁ t₂ : TypeTree.{w}) + (tr : TypeTree.Path t₁) : + flipInterleavePathEquiv t₁ t₂ ⟨⟨true⟩, tr⟩ = ⟨⟨false⟩, tr⟩ := rfl + +theorem flipInterleavePathEquiv_apply_false (t₁ t₂ : TypeTree.{w}) + (tr : TypeTree.Path t₂) : + flipInterleavePathEquiv t₁ t₂ ⟨⟨false⟩, tr⟩ = ⟨⟨true⟩, tr⟩ := rfl + +/-- Regroup the nested scheduler coins of `(t₁ ∥ t₂) ∥ tk` onto the +left-factored shape `t₁ ∥ (tk ∥ t₂)`: the first leaf keeps a single `true` +coin, the second moves under two `false` coins, and the third under +`false, true`. -/ +@[expose] +def parLeftPathEquiv (t₁ t₂ tk : TypeTree.{w}) : + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => t₂ + | ⟨false⟩ => tk) ≃ + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => tk + | ⟨false⟩ => t₂) where + toFun := fun + | ⟨⟨true⟩, ⟨⟨true⟩, tr⟩⟩ => ⟨⟨true⟩, tr⟩ + | ⟨⟨true⟩, ⟨⟨false⟩, tr⟩⟩ => ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ + | ⟨⟨false⟩, tr⟩ => ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ + invFun := fun + | ⟨⟨true⟩, tr⟩ => ⟨⟨true⟩, ⟨⟨true⟩, tr⟩⟩ + | ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ => ⟨⟨false⟩, tr⟩ + | ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ => ⟨⟨true⟩, ⟨⟨false⟩, tr⟩⟩ + left_inv := by + rintro ⟨⟨b⟩, tr⟩ + cases b + · rfl + · obtain ⟨⟨b'⟩, tr'⟩ := tr + cases b' <;> rfl + right_inv := by + rintro ⟨⟨b⟩, tr⟩ + cases b + · obtain ⟨⟨b'⟩, tr'⟩ := tr + cases b' <;> rfl + · rfl + +theorem parLeftPathEquiv_apply_first (t₁ t₂ tk : TypeTree.{w}) + (tr : TypeTree.Path t₁) : + parLeftPathEquiv t₁ t₂ tk ⟨⟨true⟩, ⟨⟨true⟩, tr⟩⟩ = ⟨⟨true⟩, tr⟩ := rfl + +theorem parLeftPathEquiv_apply_second (t₁ t₂ tk : TypeTree.{w}) + (tr : TypeTree.Path t₂) : + parLeftPathEquiv t₁ t₂ tk ⟨⟨true⟩, ⟨⟨false⟩, tr⟩⟩ = ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ := rfl + +theorem parLeftPathEquiv_apply_context (t₁ t₂ tk : TypeTree.{w}) + (tr : TypeTree.Path tk) : + parLeftPathEquiv t₁ t₂ tk ⟨⟨false⟩, tr⟩ = ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ := rfl + +/-- Regroup the nested scheduler coins of `(t₁ ∥ t₂) ∥ tk` onto the +right-factored shape `t₂ ∥ (tk ∥ t₁)`: the second leaf keeps a single `true` +coin, the first moves under two `false` coins, and the third under +`false, true`. -/ +@[expose] +def parRightPathEquiv (t₁ t₂ tk : TypeTree.{w}) : + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => t₂ + | ⟨false⟩ => tk) ≃ + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₂ + | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => tk + | ⟨false⟩ => t₁) where + toFun := fun + | ⟨⟨true⟩, ⟨⟨true⟩, tr⟩⟩ => ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ + | ⟨⟨true⟩, ⟨⟨false⟩, tr⟩⟩ => ⟨⟨true⟩, tr⟩ + | ⟨⟨false⟩, tr⟩ => ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ + invFun := fun + | ⟨⟨true⟩, tr⟩ => ⟨⟨true⟩, ⟨⟨false⟩, tr⟩⟩ + | ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ => ⟨⟨false⟩, tr⟩ + | ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ => ⟨⟨true⟩, ⟨⟨true⟩, tr⟩⟩ + left_inv := by + rintro ⟨⟨b⟩, tr⟩ + cases b + · rfl + · obtain ⟨⟨b'⟩, tr'⟩ := tr + cases b' <;> rfl + right_inv := by + rintro ⟨⟨b⟩, tr⟩ + cases b + · obtain ⟨⟨b'⟩, tr'⟩ := tr + cases b' <;> rfl + · rfl + +theorem parRightPathEquiv_apply_first (t₁ t₂ tk : TypeTree.{w}) + (tr : TypeTree.Path t₁) : + parRightPathEquiv t₁ t₂ tk ⟨⟨true⟩, ⟨⟨true⟩, tr⟩⟩ = ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ := rfl + +theorem parRightPathEquiv_apply_second (t₁ t₂ tk : TypeTree.{w}) + (tr : TypeTree.Path t₂) : + parRightPathEquiv t₁ t₂ tk ⟨⟨true⟩, ⟨⟨false⟩, tr⟩⟩ = ⟨⟨true⟩, tr⟩ := rfl + +theorem parRightPathEquiv_apply_context (t₁ t₂ tk : TypeTree.{w}) + (tr : TypeTree.Path tk) : + parRightPathEquiv t₁ t₂ tk ⟨⟨false⟩, tr⟩ = ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ := rfl + +/-- Re-encode the left branch of a binary-choice interleaving tree along a +path equivalence of the left subtree. -/ +@[expose] +def leftBranchPathEquiv {t₁ t₁' : TypeTree.{w}} (e : TypeTree.Path t₁ ≃ TypeTree.Path t₁') + (t₂ : TypeTree.{w}) : + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => t₂) ≃ + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁' + | ⟨false⟩ => t₂) where + toFun := fun + | ⟨⟨true⟩, tr⟩ => ⟨⟨true⟩, e tr⟩ + | ⟨⟨false⟩, tr⟩ => ⟨⟨false⟩, tr⟩ + invFun := fun + | ⟨⟨true⟩, tr⟩ => ⟨⟨true⟩, e.symm tr⟩ + | ⟨⟨false⟩, tr⟩ => ⟨⟨false⟩, tr⟩ + left_inv := by + rintro ⟨⟨b⟩, tr⟩ + cases b + · rfl + · change (⟨⟨true⟩, e.symm (e tr)⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => t₂)) = ⟨⟨true⟩, tr⟩ + rw [Equiv.symm_apply_apply] + right_inv := by + rintro ⟨⟨b⟩, tr⟩ + cases b + · rfl + · change (⟨⟨true⟩, e (e.symm tr)⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁' + | ⟨false⟩ => t₂)) = ⟨⟨true⟩, tr⟩ + rw [Equiv.apply_symm_apply] + +theorem leftBranchPathEquiv_apply_true {t₁ t₁' : TypeTree.{w}} + (e : TypeTree.Path t₁ ≃ TypeTree.Path t₁') (t₂ : TypeTree.{w}) (tr : TypeTree.Path t₁) : + leftBranchPathEquiv e t₂ ⟨⟨true⟩, tr⟩ = ⟨⟨true⟩, e tr⟩ := rfl + +theorem leftBranchPathEquiv_apply_false {t₁ t₁' : TypeTree.{w}} + (e : TypeTree.Path t₁ ≃ TypeTree.Path t₁') (t₂ : TypeTree.{w}) (tr : TypeTree.Path t₂) : + leftBranchPathEquiv e t₂ ⟨⟨false⟩, tr⟩ = ⟨⟨false⟩, tr⟩ := rfl + +/-- Re-encode the right branch of a binary-choice interleaving tree along a +path equivalence of the right subtree. -/ +@[expose] +def rightBranchPathEquiv (t₁ : TypeTree.{w}) {t₂ t₂' : TypeTree.{w}} + (e : TypeTree.Path t₂ ≃ TypeTree.Path t₂') : + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => t₂) ≃ + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => t₂') where + toFun := fun + | ⟨⟨true⟩, tr⟩ => ⟨⟨true⟩, tr⟩ + | ⟨⟨false⟩, tr⟩ => ⟨⟨false⟩, e tr⟩ + invFun := fun + | ⟨⟨true⟩, tr⟩ => ⟨⟨true⟩, tr⟩ + | ⟨⟨false⟩, tr⟩ => ⟨⟨false⟩, e.symm tr⟩ + left_inv := by + rintro ⟨⟨b⟩, tr⟩ + cases b + · change (⟨⟨false⟩, e.symm (e tr)⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => t₂)) = ⟨⟨false⟩, tr⟩ + rw [Equiv.symm_apply_apply] + · rfl + right_inv := by + rintro ⟨⟨b⟩, tr⟩ + cases b + · change (⟨⟨false⟩, e (e.symm tr)⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => t₂')) = ⟨⟨false⟩, tr⟩ + rw [Equiv.apply_symm_apply] + · rfl + +theorem rightBranchPathEquiv_apply_true (t₁ : TypeTree.{w}) {t₂ t₂' : TypeTree.{w}} + (e : TypeTree.Path t₂ ≃ TypeTree.Path t₂') (tr : TypeTree.Path t₁) : + rightBranchPathEquiv t₁ e ⟨⟨true⟩, tr⟩ = ⟨⟨true⟩, tr⟩ := rfl + +theorem rightBranchPathEquiv_apply_false (t₁ : TypeTree.{w}) {t₂ t₂' : TypeTree.{w}} + (e : TypeTree.Path t₂ ≃ TypeTree.Path t₂') (tr : TypeTree.Path t₂) : + rightBranchPathEquiv t₁ e ⟨⟨false⟩, tr⟩ = ⟨⟨false⟩, e tr⟩ := rfl + +/-! ## Sampled paths of nested interleavings -/ + +section SampledPaths + +variable {m : Type w → Type w'} [Monad m] [LawfulMonad m] + +/-- Flipping the scheduler coin of an interleaved sample is sampling the +branch-swapped interleave under the flipped scheduler draw. -/ +theorem samplePath_interleave_flip {spec₁ spec₂ : TypeTree.{w}} + (σ : m (ULift.{w, 0} Bool)) + (samp₁ : TypeTree.Sampler m spec₁) (samp₂ : TypeTree.Sampler m spec₂) : + (fun tr => flipInterleavePathEquiv spec₁ spec₂ tr) <$> + TypeTree.samplePath _ (TypeTree.Sampler.interleave σ samp₁ samp₂) = + TypeTree.samplePath _ + (TypeTree.Sampler.interleave (schedulerFlip <$> σ) samp₂ samp₁) := by + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind, + bind_map_left] + refine bind_congr fun b => ?_ + obtain ⟨bb⟩ := b + cases bb <;> simp only [map_pure] <;> rfl + +omit [LawfulMonad m] in +/-- Interleaved samples with the same branch samplers and `R`-related +scheduler draws are `R`-related. -/ +theorem samplePath_interleave_congr_scheduler (R : MonadRelFamily m) + {spec₁ spec₂ : TypeTree.{w}} {σ σ' : m (ULift.{w, 0} Bool)} + (h : R.rel σ' σ) + (samp₁ : TypeTree.Sampler m spec₁) (samp₂ : TypeTree.Sampler m spec₂) : + R.rel + (TypeTree.samplePath _ (TypeTree.Sampler.interleave σ' samp₁ samp₂)) + (TypeTree.samplePath _ (TypeTree.Sampler.interleave σ samp₁ samp₂)) := by + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] + exact R.bind_congr _ h + +variable {t₁ t₂ tk : TypeTree.{w}} + (samp₁ : TypeTree.Sampler m t₁) (samp₂ : TypeTree.Sampler m t₂) (sampk : TypeTree.Sampler m tk) + +/-- The source nesting `(t₁ ∥ t₂) ∥ tk` of three step trees. -/ +abbrev nestedLeftTree (t₁ t₂ tk : TypeTree.{w}) : TypeTree.{w} := + TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => t₂ + | ⟨false⟩ => tk + +/-- The left-factored nesting `t₁ ∥ (tk ∥ t₂)` of three step trees. -/ +abbrev factorLeftTree (t₁ t₂ tk : TypeTree.{w}) : TypeTree.{w} := + TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₁ + | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => tk + | ⟨false⟩ => t₂ + +/-- The right-factored nesting `t₂ ∥ (tk ∥ t₁)` of three step trees. -/ +abbrev factorRightTree (t₁ t₂ tk : TypeTree.{w}) : TypeTree.{w} := + TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => t₂ + | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => tk + | ⟨false⟩ => t₁ + +/-- Inject a leaf's sampled path into the left-factored nesting +`t₁ ∥ (tk ∥ t₂)`. -/ +def factorLeftContinuation : ULift.{w, 0} Leaf → m (TypeTree.Path (factorLeftTree t₁ t₂ tk)) + | ⟨.first⟩ => TypeTree.samplePath _ samp₁ >>= fun tr => + pure (⟨⟨true⟩, tr⟩ : TypeTree.Path (factorLeftTree t₁ t₂ tk)) + | ⟨.second⟩ => TypeTree.samplePath _ samp₂ >>= fun tr => + pure (⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ : TypeTree.Path (factorLeftTree t₁ t₂ tk)) + | ⟨.context⟩ => TypeTree.samplePath _ sampk >>= fun tr => + pure (⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ : TypeTree.Path (factorLeftTree t₁ t₂ tk)) + +/-- Inject a leaf's sampled path into the right-factored nesting +`t₂ ∥ (tk ∥ t₁)`. -/ +def factorRightContinuation : + ULift.{w, 0} Leaf → m (TypeTree.Path (factorRightTree t₁ t₂ tk)) + | ⟨.first⟩ => TypeTree.samplePath _ samp₁ >>= fun tr => + pure (⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ : TypeTree.Path (factorRightTree t₁ t₂ tk)) + | ⟨.second⟩ => TypeTree.samplePath _ samp₂ >>= fun tr => + pure (⟨⟨true⟩, tr⟩ : TypeTree.Path (factorRightTree t₁ t₂ tk)) + | ⟨.context⟩ => TypeTree.samplePath _ sampk >>= fun tr => + pure (⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ : TypeTree.Path (factorRightTree t₁ t₂ tk)) + +/-- The source nesting's sample, re-encoded onto the left-factored shape, is +the source draw bound against the leaf samplers. -/ +theorem samplePath_nestedLeft_factorLeft (σOut σIn : m (ULift.{w, 0} Bool)) : + (fun tr => parLeftPathEquiv t₁ t₂ tk tr) <$> + TypeTree.samplePath (nestedLeftTree t₁ t₂ tk) + (TypeTree.Sampler.interleave σOut + (TypeTree.Sampler.interleave σIn samp₁ samp₂) sampk) = + nestedDrawLeft σOut σIn >>= factorLeftContinuation samp₁ samp₂ sampk := by + rw [nestedDrawLeft_bind] + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] + refine bind_congr fun b => ?_ + obtain ⟨bb⟩ := b + cases bb + · simp only [map_pure] + rfl + · simp only [TypeTree.samplePath, bind_assoc, map_pure, pure_bind] + refine bind_congr fun b' => ?_ + obtain ⟨bb'⟩ := b' + cases bb' <;> rfl + +/-- The left-factored nesting's sample is the left-factored draw bound against +the leaf samplers. -/ +theorem samplePath_factorLeft (τOut τIn : m (ULift.{w, 0} Bool)) : + TypeTree.samplePath (factorLeftTree t₁ t₂ tk) + (TypeTree.Sampler.interleave τOut samp₁ + (TypeTree.Sampler.interleave τIn sampk samp₂)) = + nestedDrawFactorLeft τOut τIn >>= factorLeftContinuation samp₁ samp₂ sampk := by + rw [nestedDrawFactorLeft_bind] + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] + refine bind_congr fun b => ?_ + obtain ⟨bb⟩ := b + cases bb + · simp only [TypeTree.samplePath, bind_assoc, pure_bind] + refine bind_congr fun b' => ?_ + obtain ⟨bb'⟩ := b' + cases bb' <;> rfl + · rfl + +/-- The source nesting's sample, re-encoded onto the right-factored shape, is +the source draw bound against the leaf samplers. -/ +theorem samplePath_nestedLeft_factorRight (σOut σIn : m (ULift.{w, 0} Bool)) : + (fun tr => parRightPathEquiv t₁ t₂ tk tr) <$> + TypeTree.samplePath (nestedLeftTree t₁ t₂ tk) + (TypeTree.Sampler.interleave σOut + (TypeTree.Sampler.interleave σIn samp₁ samp₂) sampk) = + nestedDrawLeft σOut σIn >>= factorRightContinuation samp₁ samp₂ sampk := by + rw [nestedDrawLeft_bind] + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] + refine bind_congr fun b => ?_ + obtain ⟨bb⟩ := b + cases bb + · simp only [map_pure] + rfl + · simp only [TypeTree.samplePath, bind_assoc, map_pure, pure_bind] + refine bind_congr fun b' => ?_ + obtain ⟨bb'⟩ := b' + cases bb' <;> rfl + +/-- The right-factored nesting's sample is the right-factored draw bound +against the leaf samplers. -/ +theorem samplePath_factorRight (τOut τIn : m (ULift.{w, 0} Bool)) : + TypeTree.samplePath (factorRightTree t₁ t₂ tk) + (TypeTree.Sampler.interleave τOut samp₂ + (TypeTree.Sampler.interleave τIn sampk samp₁)) = + nestedDrawFactorRight τOut τIn >>= factorRightContinuation samp₁ samp₂ sampk := by + rw [nestedDrawFactorRight_bind] + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] + refine bind_congr fun b => ?_ + obtain ⟨bb⟩ := b + cases bb + · simp only [TypeTree.samplePath, bind_assoc, pure_bind] + refine bind_congr fun b' => ?_ + obtain ⟨bb'⟩ := b' + cases bb' <;> rfl + · rfl + +/-- Source and left-factored nested samples are related whenever their draws +are. -/ +theorem samplePath_factorLeft_rel (R : MonadRelFamily m) + {σOut σIn τOut τIn : m (ULift.{w, 0} Bool)} + (hσ : R.rel (nestedDrawLeft σOut σIn) (nestedDrawFactorLeft τOut τIn)) : + R.rel + ((fun tr => parLeftPathEquiv t₁ t₂ tk tr) <$> + TypeTree.samplePath (nestedLeftTree t₁ t₂ tk) + (TypeTree.Sampler.interleave σOut + (TypeTree.Sampler.interleave σIn samp₁ samp₂) sampk)) + (TypeTree.samplePath (factorLeftTree t₁ t₂ tk) + (TypeTree.Sampler.interleave τOut samp₁ + (TypeTree.Sampler.interleave τIn sampk samp₂))) := by + rw [samplePath_nestedLeft_factorLeft, samplePath_factorLeft] + exact R.bind_congr _ hσ + +/-- Source and right-factored nested samples are related whenever their draws +are. -/ +theorem samplePath_factorRight_rel (R : MonadRelFamily m) + {σOut σIn τOut τIn : m (ULift.{w, 0} Bool)} + (hσ : R.rel (nestedDrawLeft σOut σIn) (nestedDrawFactorRight τOut τIn)) : + R.rel + ((fun tr => parRightPathEquiv t₁ t₂ tk tr) <$> + TypeTree.samplePath (nestedLeftTree t₁ t₂ tk) + (TypeTree.Sampler.interleave σOut + (TypeTree.Sampler.interleave σIn samp₁ samp₂) sampk)) + (TypeTree.samplePath (factorRightTree t₁ t₂ tk) + (TypeTree.Sampler.interleave τOut samp₂ + (TypeTree.Sampler.interleave τIn sampk samp₁))) := by + rw [samplePath_nestedLeft_factorRight, samplePath_factorRight] + exact R.bind_congr _ hσ + +end SampledPaths + +/-! ## The coherence shapes up to sampler equivalence -/ + +section Shapes + +variable {m : Type w → Type w'} [Monad m] [LawfulMonad m] {Party : Type u} + {Δ₁ Δ₂ Δ₃ Δ₁₂ Δ₃₂ Δ : PortBoundary} + (R : MonadRelFamily m) + (p₁ : OpenProcess.{u, v, w, w'} m Party Δ₁) + (p₂ : OpenProcess.{u, v, w, w'} m Party Δ₂) + (p₃ : OpenProcess.{u, v, w, w'} m Party Δ₃) + +open OpenProcess OpenNodeContext + +/-- **Left factorization.** `(p₁ ∥ p₂) ∥ p₃` is sampler equivalent to +`p₁ ∥ (p₃ ∥ p₂)` when both sides decorate each leaf identically, every +scheduler node is internal, and the source and left-factored scheduler draws +are related. -/ +theorem interleave_factorLeft_samplerEquiv + {f₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ₁₂)} + {f₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ₁₂)} + {g₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁₂) + (OpenNodeContext.{u, w} Party Δ)} + {g₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₃) + (OpenNodeContext.{u, w} Party Δ)} + {cIn : OpenNodeContext.{u, w} Party Δ₁₂ (ULift.{w, 0} Bool)} + {cOut : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} + (σIn σOut : m (ULift.{w, 0} Bool)) + {f₁' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₃) + (OpenNodeContext.{u, w} Party Δ₃₂)} + {f₂' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ₃₂)} + {g₁' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ)} + {g₂' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₃₂) + (OpenNodeContext.{u, w} Party Δ)} + {dIn : OpenNodeContext.{u, w} Party Δ₃₂ (ULift.{w, 0} Bool)} + {dOut : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} + (τIn τOut : m (ULift.{w, 0} Bool)) + (h₁ : TypeTree.Node.ContextHom.comp g₁ f₁ = g₁') + (h₂ : TypeTree.Node.ContextHom.comp g₁ f₂ = TypeTree.Node.ContextHom.comp g₂' f₂') + (h₃ : g₂ = TypeTree.Node.ContextHom.comp g₂' f₁') + (hcOut : IsInternalNode cOut) (hcIn : IsInternalNode (g₁ _ cIn)) + (hdOut : IsInternalNode dOut) (hdIn : IsInternalNode (g₂' _ dIn)) + (hσ : R.rel (nestedDrawLeft σOut σIn) (nestedDrawFactorLeft τOut τIn)) : + OpenProcessSamplerEquiv R + ((p₁.interleave p₂ f₁ f₂ cIn σIn).interleave p₃ g₁ g₂ cOut σOut) + (p₁.interleave (p₃.interleave p₂ f₁' f₂' dIn τIn) g₁' g₂' dOut τOut) := by + refine ⟨fun (⟨⟨s₁, s₂⟩, s₃⟩ : (p₁.Proc × p₂.Proc) × p₃.Proc) + (⟨s₁', s₃', s₂'⟩ : p₁.Proc × p₃.Proc × p₂.Proc) => s₁ = s₁' ∧ s₂ = s₂' ∧ s₃ = s₃', + ⟨?_⟩, + fun ⟨⟨s₁, s₂⟩, s₃⟩ => ⟨⟨s₁, s₃, s₂⟩, rfl, rfl, rfl⟩, + fun ⟨s₁, s₃, s₂⟩ => ⟨⟨⟨s₁, s₂⟩, s₃⟩, rfl, rfl, rfl⟩⟩ + rintro ⟨⟨s₁, s₂⟩, s₃⟩ ⟨s₁', s₃', s₂'⟩ ⟨h1, h2, h3⟩ + subst h1 + subst h2 + subst h3 + refine ⟨parLeftPathEquiv (p₁.step s₁).tree (p₂.step s₂).tree (p₃.step s₃).tree, + ?_, ?_, ?_, ?_⟩ + · -- silence: the regrouping only moves internal nodes + rintro ⟨⟨b⟩, rest⟩ + cases b + · rw [parLeftPathEquiv_apply_context, isSilentStep_interleave_right_iff_decoration, + isSilentStep_interleave_right_iff_decoration, isSilentDecoration_map_interleave_left, + hcOut.isActivated, hdOut.isActivated, hdIn.isActivated, + OpenNodeContext.decoration_map_map, ← h₃] + simp + · obtain ⟨⟨b'⟩, rest'⟩ := rest + cases b' + · rw [parLeftPathEquiv_apply_second, isSilentStep_interleave_left_iff_decoration, + isSilentDecoration_map_interleave_right, isSilentStep_interleave_right_iff_decoration, + isSilentDecoration_map_interleave_right, hcOut.isActivated, hcIn.isActivated, + hdOut.isActivated, hdIn.isActivated, OpenNodeContext.decoration_map_map, + OpenNodeContext.decoration_map_map, h₂] + · rw [parLeftPathEquiv_apply_first, isSilentStep_interleave_left_iff_decoration, + isSilentDecoration_map_interleave_left, isSilentStep_interleave_left_iff_decoration, + hcOut.isActivated, hcIn.isActivated, hdOut.isActivated, + OpenNodeContext.decoration_map_map, h₁] + simp + · -- boundary traces: internal nodes emit nothing + rintro ⟨⟨b⟩, rest⟩ + cases b + · rw [parLeftPathEquiv_apply_context, boundaryTrace_interleave_right, + boundaryTrace_interleave_right, boundaryTrace_map_interleave_left, hcOut.emit, hdOut.emit, + hdIn.emit, one_mul, one_mul, one_mul, OpenNodeContext.decoration_map_map, ← h₃] + · obtain ⟨⟨b'⟩, rest'⟩ := rest + cases b' + · rw [parLeftPathEquiv_apply_second, boundaryTrace_interleave_left, + boundaryTrace_map_interleave_right, boundaryTrace_interleave_right, + boundaryTrace_map_interleave_right, hcOut.emit, hcIn.emit, hdOut.emit, hdIn.emit, + one_mul, one_mul, one_mul, one_mul, OpenNodeContext.decoration_map_map, + OpenNodeContext.decoration_map_map, h₂] + · rw [parLeftPathEquiv_apply_first, boundaryTrace_interleave_left, + boundaryTrace_map_interleave_left, boundaryTrace_interleave_left, hcOut.emit, hcIn.emit, + hdOut.emit, one_mul, one_mul, one_mul, OpenNodeContext.decoration_map_map, h₁] + · -- successors are componentwise equal after the regrouping + rintro ⟨⟨b⟩, rest⟩ + cases b + · exact ⟨rfl, rfl, rfl⟩ + · obtain ⟨⟨b'⟩, rest'⟩ := rest + cases b' <;> exact ⟨rfl, rfl, rfl⟩ + · -- sampled paths are related by the draw transport fact + exact samplePath_factorLeft_rel (p₁.stepSampler s₁) (p₂.stepSampler s₂) (p₃.stepSampler s₃) + R hσ + +/-- **Right factorization.** `(p₁ ∥ p₂) ∥ p₃` is sampler equivalent to +`p₂ ∥ (p₃ ∥ p₁)` when both sides decorate each leaf identically, every +scheduler node is internal, and the source and right-factored scheduler draws +are related. -/ +theorem interleave_factorRight_samplerEquiv + {f₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ₁₂)} + {f₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ₁₂)} + {g₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁₂) + (OpenNodeContext.{u, w} Party Δ)} + {g₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₃) + (OpenNodeContext.{u, w} Party Δ)} + {cIn : OpenNodeContext.{u, w} Party Δ₁₂ (ULift.{w, 0} Bool)} + {cOut : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} + (σIn σOut : m (ULift.{w, 0} Bool)) + {f₁' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₃) + (OpenNodeContext.{u, w} Party Δ₃₂)} + {f₂' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ₃₂)} + {g₁' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ)} + {g₂' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₃₂) + (OpenNodeContext.{u, w} Party Δ)} + {dIn : OpenNodeContext.{u, w} Party Δ₃₂ (ULift.{w, 0} Bool)} + {dOut : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} + (τIn τOut : m (ULift.{w, 0} Bool)) + (h₁ : TypeTree.Node.ContextHom.comp g₁ f₁ = TypeTree.Node.ContextHom.comp g₂' f₂') + (h₂ : TypeTree.Node.ContextHom.comp g₁ f₂ = g₁') + (h₃ : g₂ = TypeTree.Node.ContextHom.comp g₂' f₁') + (hcOut : IsInternalNode cOut) (hcIn : IsInternalNode (g₁ _ cIn)) + (hdOut : IsInternalNode dOut) (hdIn : IsInternalNode (g₂' _ dIn)) + (hσ : R.rel (nestedDrawLeft σOut σIn) (nestedDrawFactorRight τOut τIn)) : + OpenProcessSamplerEquiv R + ((p₁.interleave p₂ f₁ f₂ cIn σIn).interleave p₃ g₁ g₂ cOut σOut) + (p₂.interleave (p₃.interleave p₁ f₁' f₂' dIn τIn) g₁' g₂' dOut τOut) := by + refine ⟨fun (⟨⟨s₁, s₂⟩, s₃⟩ : (p₁.Proc × p₂.Proc) × p₃.Proc) + (⟨s₂', s₃', s₁'⟩ : p₂.Proc × p₃.Proc × p₁.Proc) => s₁ = s₁' ∧ s₂ = s₂' ∧ s₃ = s₃', + ⟨?_⟩, + fun ⟨⟨s₁, s₂⟩, s₃⟩ => ⟨⟨s₂, s₃, s₁⟩, rfl, rfl, rfl⟩, + fun ⟨s₂, s₃, s₁⟩ => ⟨⟨⟨s₁, s₂⟩, s₃⟩, rfl, rfl, rfl⟩⟩ + rintro ⟨⟨s₁, s₂⟩, s₃⟩ ⟨s₂', s₃', s₁'⟩ ⟨h1, h2, h3⟩ + subst h1 + subst h2 + subst h3 + refine ⟨parRightPathEquiv (p₁.step s₁).tree (p₂.step s₂).tree (p₃.step s₃).tree, + ?_, ?_, ?_, ?_⟩ + · -- silence: the regrouping only moves internal nodes + rintro ⟨⟨b⟩, rest⟩ + cases b + · rw [parRightPathEquiv_apply_context, isSilentStep_interleave_right_iff_decoration, + isSilentStep_interleave_right_iff_decoration, isSilentDecoration_map_interleave_left, + hcOut.isActivated, hdOut.isActivated, hdIn.isActivated, + OpenNodeContext.decoration_map_map, ← h₃] + simp + · obtain ⟨⟨b'⟩, rest'⟩ := rest + cases b' + · rw [parRightPathEquiv_apply_second, isSilentStep_interleave_left_iff_decoration, + isSilentDecoration_map_interleave_right, isSilentStep_interleave_left_iff_decoration, + hcOut.isActivated, hcIn.isActivated, hdOut.isActivated, + OpenNodeContext.decoration_map_map, h₂] + simp + · rw [parRightPathEquiv_apply_first, isSilentStep_interleave_left_iff_decoration, + isSilentDecoration_map_interleave_left, isSilentStep_interleave_right_iff_decoration, + isSilentDecoration_map_interleave_right, hcOut.isActivated, hcIn.isActivated, + hdOut.isActivated, hdIn.isActivated, OpenNodeContext.decoration_map_map, + OpenNodeContext.decoration_map_map, h₁] + · -- boundary traces: internal nodes emit nothing + rintro ⟨⟨b⟩, rest⟩ + cases b + · rw [parRightPathEquiv_apply_context, boundaryTrace_interleave_right, + boundaryTrace_interleave_right, boundaryTrace_map_interleave_left, hcOut.emit, hdOut.emit, + hdIn.emit, one_mul, one_mul, one_mul, OpenNodeContext.decoration_map_map, ← h₃] + · obtain ⟨⟨b'⟩, rest'⟩ := rest + cases b' + · rw [parRightPathEquiv_apply_second, boundaryTrace_interleave_left, + boundaryTrace_map_interleave_right, boundaryTrace_interleave_left, hcOut.emit, hcIn.emit, + hdOut.emit, one_mul, one_mul, one_mul, OpenNodeContext.decoration_map_map, h₂] + · rw [parRightPathEquiv_apply_first, boundaryTrace_interleave_left, + boundaryTrace_map_interleave_left, boundaryTrace_interleave_right, + boundaryTrace_map_interleave_right, hcOut.emit, hcIn.emit, hdOut.emit, hdIn.emit, + one_mul, one_mul, one_mul, one_mul, OpenNodeContext.decoration_map_map, + OpenNodeContext.decoration_map_map, h₁] + · -- successors are componentwise equal after the regrouping + rintro ⟨⟨b⟩, rest⟩ + cases b + · exact ⟨rfl, rfl, rfl⟩ + · obtain ⟨⟨b'⟩, rest'⟩ := rest + cases b' <;> exact ⟨rfl, rfl, rfl⟩ + · -- sampled paths are related by the draw transport fact + exact samplePath_factorRight_rel (p₁.stepSampler s₁) (p₂.stepSampler s₂) (p₃.stepSampler s₃) + R hσ + +/-- **Commutation.** Interleaving in either order gives sampler-equivalent +composites when both scheduler nodes are internal and the flipped draw of one +side is related to the draw of the other. -/ +theorem interleave_comm_samplerEquiv + {f₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ)} + {f₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ)} + {c : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} (σ : m (ULift.{w, 0} Bool)) + {d : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} (τ : m (ULift.{w, 0} Bool)) + (hc : IsInternalNode c) (hd : IsInternalNode d) + (hστ : R.rel (schedulerFlip <$> σ) τ) : + OpenProcessSamplerEquiv R (p₁.interleave p₂ f₁ f₂ c σ) (p₂.interleave p₁ f₂ f₁ d τ) := by + refine ⟨fun (⟨s₁, s₂⟩ : p₁.Proc × p₂.Proc) (⟨s₂', s₁'⟩ : p₂.Proc × p₁.Proc) => + s₁ = s₁' ∧ s₂ = s₂', + ⟨?_⟩, + fun ⟨s₁, s₂⟩ => ⟨⟨s₂, s₁⟩, rfl, rfl⟩, + fun ⟨s₂, s₁⟩ => ⟨⟨s₁, s₂⟩, rfl, rfl⟩⟩ + rintro ⟨s₁, s₂⟩ ⟨s₂', s₁'⟩ ⟨h1, h2⟩ + subst h1 + subst h2 + refine ⟨flipInterleavePathEquiv (p₁.step s₁).tree (p₂.step s₂).tree, ?_, ?_, ?_, ?_⟩ + · rintro ⟨⟨b⟩, tr⟩ + cases b + · rw [flipInterleavePathEquiv_apply_false, isSilentStep_interleave_right_iff_decoration, + isSilentStep_interleave_left_iff_decoration, hc.isActivated, hd.isActivated] + · rw [flipInterleavePathEquiv_apply_true, isSilentStep_interleave_left_iff_decoration, + isSilentStep_interleave_right_iff_decoration, hc.isActivated, hd.isActivated] + · rintro ⟨⟨b⟩, tr⟩ + cases b + · rw [flipInterleavePathEquiv_apply_false, boundaryTrace_interleave_right, + boundaryTrace_interleave_left, hc.emit, hd.emit] + · rw [flipInterleavePathEquiv_apply_true, boundaryTrace_interleave_left, + boundaryTrace_interleave_right, hc.emit, hd.emit] + · rintro ⟨⟨b⟩, tr⟩ + cases b <;> exact ⟨rfl, rfl⟩ + · change R.rel + ((fun tr => flipInterleavePathEquiv (p₁.step s₁).tree (p₂.step s₂).tree tr) <$> + TypeTree.samplePath _ + (TypeTree.Sampler.interleave σ (p₁.stepSampler s₁) (p₂.stepSampler s₂))) + (TypeTree.samplePath _ + (TypeTree.Sampler.interleave τ (p₂.stepSampler s₂) (p₁.stepSampler s₁))) + rw [samplePath_interleave_flip] + exact samplePath_interleave_congr_scheduler R hστ _ _ + +/-- **Re-homing.** The same interleaving under another internal scheduler node +and a related scheduler draw is sampler equivalent. -/ +theorem interleave_rehome_samplerEquiv + {f₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ)} + {f₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ)} + {c : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} (σ : m (ULift.{w, 0} Bool)) + {d : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} (τ : m (ULift.{w, 0} Bool)) + (hc : IsInternalNode c) (hd : IsInternalNode d) (hστ : R.rel σ τ) : + OpenProcessSamplerEquiv R (p₁.interleave p₂ f₁ f₂ c σ) (p₁.interleave p₂ f₁ f₂ d τ) := by + refine ⟨fun s s' => s = s', ⟨?_⟩, fun s => ⟨s, rfl⟩, fun s => ⟨s, rfl⟩⟩ + rintro ⟨s₁, s₂⟩ _ rfl + refine ⟨Equiv.refl _, ?_, ?_, ?_, ?_⟩ + · rintro ⟨⟨b⟩, tr⟩ + cases b + · rw [Equiv.refl_apply, isSilentStep_interleave_right_iff_decoration, + isSilentStep_interleave_right_iff_decoration, hc.isActivated, hd.isActivated] + · rw [Equiv.refl_apply, isSilentStep_interleave_left_iff_decoration, + isSilentStep_interleave_left_iff_decoration, hc.isActivated, hd.isActivated] + · rintro ⟨⟨b⟩, tr⟩ + cases b + · rw [Equiv.refl_apply, boundaryTrace_interleave_right, boundaryTrace_interleave_right, + hc.emit, hd.emit] + · rw [Equiv.refl_apply, boundaryTrace_interleave_left, boundaryTrace_interleave_left, + hc.emit, hd.emit] + · rintro ⟨⟨b⟩, tr⟩ + cases b <;> rfl + · change R.rel + ((fun tr => (Equiv.refl _) tr) <$> + TypeTree.samplePath _ + (TypeTree.Sampler.interleave σ (p₁.stepSampler s₁) (p₂.stepSampler s₂))) + (TypeTree.samplePath _ + (TypeTree.Sampler.interleave τ (p₁.stepSampler s₁) (p₂.stepSampler s₂))) + have heq : (fun tr => (Equiv.refl _) tr) <$> + TypeTree.samplePath _ + (TypeTree.Sampler.interleave σ (p₁.stepSampler s₁) (p₂.stepSampler s₂)) = + TypeTree.samplePath _ + (TypeTree.Sampler.interleave σ (p₁.stepSampler s₁) (p₂.stepSampler s₂)) := by + simp only [Equiv.refl_apply, id_map'] + rw [heq] + exact samplePath_interleave_congr_scheduler R hστ _ _ + +end Shapes + +/-! ## Congruence -/ + +section Congruence + +variable {m : Type w → Type w'} [Monad m] [LawfulMonad m] {Party : Type u} + {Δ₁ Δ₂ Δ : PortBoundary} (R : MonadRelFamily m) [R.IsBindCongr] + (p₁ : OpenProcess.{u, v, w, w'} m Party Δ₁) + (p₂ : OpenProcess.{u, v, w, w'} m Party Δ₂) + {f₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ)} + {f₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ)} + {c : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} + +open OpenProcess OpenNodeContext + +/-- Sampler equivalence is preserved by interleaving on the left, when the +left injection preserves activation and relabels traces. The scheduler node +is arbitrary: both sides carry the same one. -/ +theorem OpenProcess.interleave_congr_left_samplerEquiv + (hf₁ : PreservesActivation f₁) + {g : PFunctor.Idx Δ₁.Out → Option (PFunctor.Idx Δ.Out)} (hg : EmitsAlong f₁ g) + (σ : m (ULift.{w, 0} Bool)) + {q₁ : OpenProcess.{u, v, w, w'} m Party Δ₁} (h : OpenProcessSamplerEquiv R p₁ q₁) : + OpenProcessSamplerEquiv R (p₁.interleave p₂ f₁ f₂ c σ) (q₁.interleave p₂ f₁ f₂ c σ) := by + obtain ⟨rel, hbisim, htot₁, htot₂⟩ := h + refine ⟨fun (⟨s₁, s₂⟩ : p₁.Proc × p₂.Proc) (⟨s₁', s₂'⟩ : q₁.Proc × p₂.Proc) => + rel s₁ s₁' ∧ s₂ = s₂', ⟨?_⟩, ?_, ?_⟩ + · rintro ⟨s₁, s₂⟩ ⟨s₁', s₂'⟩ ⟨hrel, h2⟩ + subst h2 + obtain ⟨e, hsil, htr, hnext, hsam⟩ := hbisim.step_equiv s₁ s₁' hrel + refine ⟨leftBranchPathEquiv e (p₂.step s₂).tree, ?_, ?_, ?_, ?_⟩ + · rintro ⟨⟨b⟩, tr⟩ + cases b + · rw [leftBranchPathEquiv_apply_false, isSilentStep_interleave_right_iff_decoration, + isSilentStep_interleave_right_iff_decoration] + · rw [leftBranchPathEquiv_apply_true, isSilentStep_interleave_left_iff_decoration, + isSilentStep_interleave_left_iff_decoration, isSilentDecoration_iff_map f₁ hf₁, + isSilentDecoration_iff_map f₁ hf₁] + have hs := hsil tr + unfold IsSilentStep at hs + exact and_congr Iff.rfl hs + · rintro ⟨⟨b⟩, tr⟩ + cases b + · rw [leftBranchPathEquiv_apply_false, boundaryTrace_interleave_right, + boundaryTrace_interleave_right] + · rw [leftBranchPathEquiv_apply_true, boundaryTrace_interleave_left, + boundaryTrace_interleave_left, boundaryTrace_map_of_emitsAlong hg, + boundaryTrace_map_of_emitsAlong hg, htr tr] + · rintro ⟨⟨b⟩, tr⟩ + cases b + · exact ⟨hrel, rfl⟩ + · exact ⟨hnext tr, rfl⟩ + · change R.rel + ((fun tr => leftBranchPathEquiv e (p₂.step s₂).tree tr) <$> + TypeTree.samplePath _ + (TypeTree.Sampler.interleave σ (p₁.stepSampler s₁) (p₂.stepSampler s₂))) + (TypeTree.samplePath _ + (TypeTree.Sampler.interleave σ (q₁.stepSampler s₁') (p₂.stepSampler s₂))) + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] + refine R.bind_congr_right σ fun b => ?_ + obtain ⟨bb⟩ := b + cases bb + · simp only [map_pure] + change R.rel + (TypeTree.samplePath _ (p₂.stepSampler s₂) >>= fun tr => + pure (⟨⟨false⟩, tr⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => (q₁.step s₁').tree + | ⟨false⟩ => (p₂.step s₂).tree))) + (TypeTree.samplePath _ (p₂.stepSampler s₂) >>= fun tr => + pure (⟨⟨false⟩, tr⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => (q₁.step s₁').tree + | ⟨false⟩ => (p₂.step s₂).tree))) + exact R.refl _ + · simp only [map_pure] + change R.rel + (TypeTree.samplePath _ (p₁.stepSampler s₁) >>= fun tr => + pure (⟨⟨true⟩, e tr⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => (q₁.step s₁').tree + | ⟨false⟩ => (p₂.step s₂).tree))) + (TypeTree.samplePath _ (q₁.stepSampler s₁') >>= fun tr => + pure (⟨⟨true⟩, tr⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => (q₁.step s₁').tree + | ⟨false⟩ => (p₂.step s₂).tree))) + have h' := R.bind_congr (fun tr => pure (⟨⟨true⟩, tr⟩ : + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => (q₁.step s₁').tree + | ⟨false⟩ => (p₂.step s₂).tree))) hsam + rw [bind_map_left] at h' + exact h' + · rintro ⟨s₁, s₂⟩ + obtain ⟨s₁', hs⟩ := htot₁ s₁ + exact ⟨⟨s₁', s₂⟩, hs, rfl⟩ + · rintro ⟨s₁', s₂⟩ + obtain ⟨s₁, hs⟩ := htot₂ s₁' + exact ⟨⟨s₁, s₂⟩, hs, rfl⟩ + +/-- Sampler equivalence is preserved by interleaving on the right, when the +right injection preserves activation and relabels traces. -/ +theorem OpenProcess.interleave_congr_right_samplerEquiv + (hf₂ : PreservesActivation f₂) + {g : PFunctor.Idx Δ₂.Out → Option (PFunctor.Idx Δ.Out)} (hg : EmitsAlong f₂ g) + (σ : m (ULift.{w, 0} Bool)) + {q₂ : OpenProcess.{u, v, w, w'} m Party Δ₂} (h : OpenProcessSamplerEquiv R p₂ q₂) : + OpenProcessSamplerEquiv R (p₁.interleave p₂ f₁ f₂ c σ) (p₁.interleave q₂ f₁ f₂ c σ) := by + obtain ⟨rel, hbisim, htot₁, htot₂⟩ := h + refine ⟨fun (⟨s₁, s₂⟩ : p₁.Proc × p₂.Proc) (⟨s₁', s₂'⟩ : p₁.Proc × q₂.Proc) => + s₁ = s₁' ∧ rel s₂ s₂', ⟨?_⟩, ?_, ?_⟩ + · rintro ⟨s₁, s₂⟩ ⟨s₁', s₂'⟩ ⟨h1, hrel⟩ + subst h1 + obtain ⟨e, hsil, htr, hnext, hsam⟩ := hbisim.step_equiv s₂ s₂' hrel + refine ⟨rightBranchPathEquiv (p₁.step s₁).tree e, ?_, ?_, ?_, ?_⟩ + · rintro ⟨⟨b⟩, tr⟩ + cases b + · rw [rightBranchPathEquiv_apply_false, isSilentStep_interleave_right_iff_decoration, + isSilentStep_interleave_right_iff_decoration, isSilentDecoration_iff_map f₂ hf₂, + isSilentDecoration_iff_map f₂ hf₂] + have hs := hsil tr + unfold IsSilentStep at hs + exact and_congr Iff.rfl hs + · rw [rightBranchPathEquiv_apply_true, isSilentStep_interleave_left_iff_decoration, + isSilentStep_interleave_left_iff_decoration] + · rintro ⟨⟨b⟩, tr⟩ + cases b + · rw [rightBranchPathEquiv_apply_false, boundaryTrace_interleave_right, + boundaryTrace_interleave_right, boundaryTrace_map_of_emitsAlong hg, + boundaryTrace_map_of_emitsAlong hg, htr tr] + · rw [rightBranchPathEquiv_apply_true, boundaryTrace_interleave_left, + boundaryTrace_interleave_left] + · rintro ⟨⟨b⟩, tr⟩ + cases b + · exact ⟨rfl, hnext tr⟩ + · exact ⟨rfl, hrel⟩ + · change R.rel + ((fun tr => rightBranchPathEquiv (p₁.step s₁).tree e tr) <$> + TypeTree.samplePath _ + (TypeTree.Sampler.interleave σ (p₁.stepSampler s₁) (p₂.stepSampler s₂))) + (TypeTree.samplePath _ + (TypeTree.Sampler.interleave σ (p₁.stepSampler s₁) (q₂.stepSampler s₂'))) + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] + refine R.bind_congr_right σ fun b => ?_ + obtain ⟨bb⟩ := b + cases bb + · simp only [map_pure] + change R.rel + (TypeTree.samplePath _ (p₂.stepSampler s₂) >>= fun tr => + pure (⟨⟨false⟩, e tr⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => (p₁.step s₁).tree + | ⟨false⟩ => (q₂.step s₂').tree))) + (TypeTree.samplePath _ (q₂.stepSampler s₂') >>= fun tr => + pure (⟨⟨false⟩, tr⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => (p₁.step s₁).tree + | ⟨false⟩ => (q₂.step s₂').tree))) + have h' := R.bind_congr (fun tr => pure (⟨⟨false⟩, tr⟩ : + TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => (p₁.step s₁).tree + | ⟨false⟩ => (q₂.step s₂').tree))) hsam + rw [bind_map_left] at h' + exact h' + · simp only [map_pure] + change R.rel + (TypeTree.samplePath _ (p₁.stepSampler s₁) >>= fun tr => + pure (⟨⟨true⟩, tr⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => (p₁.step s₁).tree + | ⟨false⟩ => (q₂.step s₂').tree))) + (TypeTree.samplePath _ (p₁.stepSampler s₁) >>= fun tr => + pure (⟨⟨true⟩, tr⟩ : TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => (p₁.step s₁).tree + | ⟨false⟩ => (q₂.step s₂').tree))) + exact R.refl _ + · rintro ⟨s₁, s₂⟩ + obtain ⟨s₂', hs⟩ := htot₁ s₂ + exact ⟨⟨s₁, s₂'⟩, rfl, hs⟩ + · rintro ⟨s₁, s₂'⟩ + obtain ⟨s₂, hs⟩ := htot₂ s₂' + exact ⟨⟨s₁, s₂⟩, rfl, hs⟩ + +omit [LawfulMonad m] [R.IsBindCongr] in +/-- Sampler equivalence is preserved by re-decoration along an +activation-preserving hom that relabels traces. -/ +theorem OpenProcess.mapHom_congr_samplerEquiv + {h : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ₂)} + (hh : PreservesActivation h) + {g : PFunctor.Idx Δ₁.Out → Option (PFunctor.Idx Δ₂.Out)} (hg : EmitsAlong h g) + {p q : OpenProcess.{u, v, w, w'} m Party Δ₁} (hpq : OpenProcessSamplerEquiv R p q) : + OpenProcessSamplerEquiv R (p.mapHom h) (q.mapHom h) := by + obtain ⟨rel, hbisim, htot₁, htot₂⟩ := hpq + refine ⟨rel, ⟨?_⟩, htot₁, htot₂⟩ + intro s₁ s₂ hrel + obtain ⟨e, hsil, htr, hnext, hsam⟩ := hbisim.step_equiv s₁ s₂ hrel + refine ⟨e, ?_, ?_, hnext, hsam⟩ + · intro tr + exact (isSilentStep_mapHom_iff hh p s₁ tr).trans + ((hsil tr).trans (isSilentStep_mapHom_iff hh q s₂ (e tr)).symm) + · intro tr + exact (boundaryTrace_map_of_emitsAlong hg (p.step s₁).semantics tr).trans + ((congrArg (PFunctor.TraceList.mapPartial g) (htr tr)).trans + (boundaryTrace_map_of_emitsAlong hg (q.step s₂).semantics (e tr)).symm) + +end Congruence + +/-! ## Derived reassociation -/ + +section Assoc + +variable {m : Type w → Type w'} [Monad m] [LawfulMonad m] {Party : Type u} + {Δ₁ Δ₂ Δ₃ Δ₁₂ Δ₂₃ Δ : PortBoundary} + (R : MonadRelFamily m) [R.IsBindCongr] + (p₁ : OpenProcess.{u, v, w, w'} m Party Δ₁) + (p₂ : OpenProcess.{u, v, w, w'} m Party Δ₂) + (p₃ : OpenProcess.{u, v, w, w'} m Party Δ₃) + +open OpenProcess OpenNodeContext + +/-- **Reassociation.** `(p₁ ∥ p₂) ∥ p₃` is sampler equivalent to +`p₁ ∥ (p₂ ∥ p₃)`: the left factorization followed by commutation of the inner +pair under the congruence. The inner scheduler draw `τIn'` of the factored +shape is related to the flipped inner draw `τIn` of the target. -/ +theorem interleave_assoc_samplerEquiv + {f₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ₁₂)} + {f₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ₁₂)} + {g₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁₂) + (OpenNodeContext.{u, w} Party Δ)} + {g₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₃) + (OpenNodeContext.{u, w} Party Δ)} + {cIn : OpenNodeContext.{u, w} Party Δ₁₂ (ULift.{w, 0} Bool)} + {cOut : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} + (σIn σOut : m (ULift.{w, 0} Bool)) + {f₁' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂) + (OpenNodeContext.{u, w} Party Δ₂₃)} + {f₂' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₃) + (OpenNodeContext.{u, w} Party Δ₂₃)} + {g₁' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁) + (OpenNodeContext.{u, w} Party Δ)} + {g₂' : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂₃) + (OpenNodeContext.{u, w} Party Δ)} + {dIn : OpenNodeContext.{u, w} Party Δ₂₃ (ULift.{w, 0} Bool)} + {dOut : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)} + (τIn τIn' τOut : m (ULift.{w, 0} Bool)) + (h₁ : TypeTree.Node.ContextHom.comp g₁ f₁ = g₁') + (h₂ : TypeTree.Node.ContextHom.comp g₁ f₂ = TypeTree.Node.ContextHom.comp g₂' f₁') + (h₃ : g₂ = TypeTree.Node.ContextHom.comp g₂' f₂') + (hcOut : IsInternalNode cOut) (hcIn : IsInternalNode (g₁ _ cIn)) + (hdOut : IsInternalNode dOut) (hdIn : IsInternalNode dIn) + (hdIn' : IsInternalNode (g₂' _ dIn)) + (hg₂' : PreservesActivation g₂') + {gg : PFunctor.Idx Δ₂₃.Out → Option (PFunctor.Idx Δ.Out)} (hgg : EmitsAlong g₂' gg) + (hσ : R.rel (nestedDrawLeft σOut σIn) (nestedDrawFactorLeft τOut τIn')) + (hτ : R.rel (schedulerFlip <$> τIn') τIn) : + OpenProcessSamplerEquiv R + ((p₁.interleave p₂ f₁ f₂ cIn σIn).interleave p₃ g₁ g₂ cOut σOut) + (p₁.interleave (p₂.interleave p₃ f₁' f₂' dIn τIn) g₁' g₂' dOut τOut) := + (interleave_factorLeft_samplerEquiv R p₁ p₂ p₃ σIn σOut τIn' τOut h₁ h₂ h₃ hcOut hcIn hdOut + hdIn' hσ).trans + (OpenProcess.interleave_congr_right_samplerEquiv R p₁ _ hg₂' hgg τOut + (interleave_comm_samplerEquiv R p₃ p₂ τIn' τIn hdIn hdIn hτ)) + +end Assoc + +end UC +end Interaction diff --git a/PolyFun/Interaction/UC/OpenProcessSamplerFactorization.lean b/PolyFun/Interaction/UC/OpenProcessSamplerFactorization.lean index bd39c441..357155b9 100644 --- a/PolyFun/Interaction/UC/OpenProcessSamplerFactorization.lean +++ b/PolyFun/Interaction/UC/OpenProcessSamplerFactorization.lean @@ -6,11 +6,10 @@ Authors: Devon Tuma module -import all PolyFun.Interaction.Basic.Sampler -import all PolyFun.Interaction.UC.OpenProcessModel -import all PolyFun.Interaction.UC.OpenProcessSamplerEquiv +import all PolyFun.Interaction.UC.OpenProcess public import PolyFun.Interaction.UC.OpenProcessFactorization public import PolyFun.Interaction.UC.OpenProcessModel +public import PolyFun.Interaction.UC.OpenProcessSamplerCoherence public import PolyFun.Interaction.UC.OpenProcessSamplerEquiv /-! @@ -18,22 +17,29 @@ public import PolyFun.Interaction.UC.OpenProcessSamplerEquiv The structural coherence laws of `openTheory` hold up to `OpenProcessActivationEquiv`, which erases sampler effects and uses delay -matching. This module strengthens them to `OpenProcessSamplerEquiv`, which -retains sampled-path effects, **conditionally on named scheduler-transport hypotheses**: a -single shared `schedulerSampler` does not preserve per-step scheduling -distributions across reassociation, so each law takes exactly the -`MonadRelFamily` fact about reassociated scheduler draws that it needs. -`MonadRelFamily.top` discharges every such hypothesis trivially, recovering -sampler-blind strong path equivalences unconditionally. +matching. This module strengthens the plug laws to `OpenProcessSamplerEquiv`, +which retains sampled-path effects, **conditionally on named +scheduler-transport hypotheses**: a single shared `schedulerSampler` does not +preserve per-step scheduling distributions across reassociation, so each law +takes exactly the `MonadRelFamily` fact about reassociated scheduler draws +that it needs. `MonadRelFamily.top` discharges every such hypothesis +trivially, recovering sampler-blind strong path equivalences unconditionally. + +Each law is one instance of the shapes in `OpenProcessSamplerCoherence`: after +the normalization equalities push boundary adaptation into the injections, the +composite injections of every leaf agree on both sides — everything is closed, +so only activation survives — and the scheduler nodes are internal. + +`plug` commutation needs the scheduler to be `R`-fair: flipping the scheduler +coin must be invisible to the relation family +(`R.rel schedulerSampler (schedulerFlip <$> schedulerSampler)`). The +factorizations need the source-shaped draw `sourceDraw` to be related to the +left- or right-factored draw. The activation-equivalence laws in `OpenProcessModel` and `OpenProcessFactorization` keep their direct proofs rather than becoming corollaries: they hold for an arbitrary `m` with no `Monad` instance, while sampled paths — and hence this module — require `[Monad m] [LawfulMonad m]`. - -`plug` commutation needs the scheduler to be `R`-fair: flipping the scheduler -coin must be invisible to the relation family -(`R.rel schedulerSampler (schedulerFlip <$> schedulerSampler)`). -/ public section @@ -45,20 +51,6 @@ namespace UC open Concurrent -/-! ## Scheduler re-encodings -/ - -/-- Negate a lifted scheduler coin: the path re-encoding of `plug` -commutation. -/ -@[expose] -def schedulerFlip : ULift.{w, 0} Bool → ULift.{w, 0} Bool := - fun b => ULift.up !b.down - -@[simp] theorem schedulerFlip_up_true : - schedulerFlip.{w} (ULift.up true) = ULift.up false := rfl - -@[simp] theorem schedulerFlip_up_false : - schedulerFlip.{w} (ULift.up false) = ULift.up true := rfl - /-! ## The empty boundary carries no traffic -/ /-- Any two traces over the empty interface are equal: the interface has no @@ -70,55 +62,6 @@ theorem traceList_interface_empty_eq | ⟨a, _⟩ :: _, _ => a.elim | [], ⟨a, _⟩ :: _ => a.elim -/-! ## Path re-encoding and sampling laws for the scheduler node -/ - -/-- Flip the scheduler coin at the root of a binary-choice interleaving tree, -exchanging the two branches. -/ -def flipInterleavePathEquiv (t₁ t₂ : TypeTree.{w}) : - TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => t₁ - | ⟨false⟩ => t₂) ≃ - TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => t₂ - | ⟨false⟩ => t₁) where - toFun := fun - | ⟨⟨true⟩, tr⟩ => ⟨⟨false⟩, tr⟩ - | ⟨⟨false⟩, tr⟩ => ⟨⟨true⟩, tr⟩ - invFun := fun - | ⟨⟨true⟩, tr⟩ => ⟨⟨false⟩, tr⟩ - | ⟨⟨false⟩, tr⟩ => ⟨⟨true⟩, tr⟩ - left_inv := by rintro ⟨⟨b⟩, tr⟩; cases b <;> rfl - right_inv := by rintro ⟨⟨b⟩, tr⟩; cases b <;> rfl - -/-- Flipping the scheduler coin of an interleaved sample is sampling the -branch-swapped interleave under the flipped scheduler draw. -/ -theorem samplePath_interleave_flip {m : Type w → Type w'} - [Monad m] [LawfulMonad m] {spec₁ spec₂ : TypeTree.{w}} - (σ : m (ULift.{w, 0} Bool)) - (samp₁ : TypeTree.Sampler m spec₁) (samp₂ : TypeTree.Sampler m spec₂) : - (fun tr => flipInterleavePathEquiv spec₁ spec₂ tr) <$> - TypeTree.samplePath _ (TypeTree.Sampler.interleave σ samp₁ samp₂) = - TypeTree.samplePath _ - (TypeTree.Sampler.interleave (schedulerFlip <$> σ) samp₂ samp₁) := by - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind, - bind_map_left] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb <;> simp only [map_pure] <;> rfl - -/-- Interleaved samples with the same branch samplers and `R`-related -scheduler draws are `R`-related. -/ -theorem samplePath_interleave_congr_scheduler {m : Type w → Type w'} - [Monad m] (R : MonadRelFamily m) - {spec₁ spec₂ : TypeTree.{w}} {σ σ' : m (ULift.{w, 0} Bool)} - (h : R.rel σ' σ) - (samp₁ : TypeTree.Sampler m spec₁) (samp₂ : TypeTree.Sampler m spec₂) : - R.rel - (TypeTree.samplePath _ (TypeTree.Sampler.interleave σ' samp₁ samp₂)) - (TypeTree.samplePath _ (TypeTree.Sampler.interleave σ samp₁ samp₂)) := by - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] - exact R.bind_congr _ h - /-! ## Scheduler draws for the factorization reassociations -/ namespace OpenProcessFactorization @@ -128,37 +71,19 @@ namespace OpenProcessFactorization @[expose] def sourceDraw {m : Type w → Type w'} [Monad m] (σ : m (ULift.{w, 0} Bool)) : m (ULift.{w, 0} Leaf) := - σ >>= fun b => - match b with - | ⟨true⟩ => σ >>= fun b' => - match b' with - | ⟨true⟩ => pure ⟨.first⟩ - | ⟨false⟩ => pure ⟨.second⟩ - | ⟨false⟩ => pure ⟨.context⟩ + nestedDrawLeft σ σ /-- Draw a `Leaf` with the left-factored coin encoding (`leftSchedule`). -/ @[expose] def leftDraw {m : Type w → Type w'} [Monad m] (σ : m (ULift.{w, 0} Bool)) : m (ULift.{w, 0} Leaf) := - σ >>= fun b => - match b with - | ⟨true⟩ => pure ⟨.first⟩ - | ⟨false⟩ => σ >>= fun b' => - match b' with - | ⟨true⟩ => pure ⟨.context⟩ - | ⟨false⟩ => pure ⟨.second⟩ + nestedDrawFactorLeft σ σ /-- Draw a `Leaf` with the right-factored coin encoding (`rightSchedule`). -/ @[expose] def rightDraw {m : Type w → Type w'} [Monad m] (σ : m (ULift.{w, 0} Bool)) : m (ULift.{w, 0} Leaf) := - σ >>= fun b => - match b with - | ⟨true⟩ => pure ⟨.second⟩ - | ⟨false⟩ => σ >>= fun b' => - match b' with - | ⟨true⟩ => pure ⟨.context⟩ - | ⟨false⟩ => pure ⟨.first⟩ + nestedDrawFactorRight σ σ /-- Binding a source draw against a per-leaf continuation is the flattened two-coin computation. -/ @@ -172,16 +97,8 @@ theorem sourceDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] match b' with | ⟨true⟩ => h ⟨.first⟩ | ⟨false⟩ => h ⟨.second⟩ - | ⟨false⟩ => h ⟨.context⟩ := by - simp only [sourceDraw, bind_assoc] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [pure_bind] - · simp only [bind_assoc] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> simp only [pure_bind] + | ⟨false⟩ => h ⟨.context⟩ := + nestedDrawLeft_bind σ σ h /-- Binding a left-factored draw against a per-leaf continuation is the flattened two-coin computation. -/ @@ -195,16 +112,8 @@ theorem leftDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] | ⟨false⟩ => σ >>= fun b' => match b' with | ⟨true⟩ => h ⟨.context⟩ - | ⟨false⟩ => h ⟨.second⟩ := by - simp only [leftDraw, bind_assoc] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [bind_assoc] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> simp only [pure_bind] - · simp only [pure_bind] + | ⟨false⟩ => h ⟨.second⟩ := + nestedDrawFactorLeft_bind σ σ h /-- Binding a right-factored draw against a per-leaf continuation is the flattened two-coin computation. -/ @@ -218,16 +127,8 @@ theorem rightDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] | ⟨false⟩ => σ >>= fun b' => match b' with | ⟨true⟩ => h ⟨.context⟩ - | ⟨false⟩ => h ⟨.first⟩ := by - simp only [rightDraw, bind_assoc] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [bind_assoc] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> simp only [pure_bind] - · simp only [pure_bind] + | ⟨false⟩ => h ⟨.first⟩ := + nestedDrawFactorRight_bind σ σ h /-! The deterministic identity-monad cases make the reassociation obstruction directly executable for downstream users. -/ @@ -258,47 +159,273 @@ directly executable for downstream users. -/ end OpenProcessFactorization -/-! ## Path re-encoding for the left par/wire factorizations -/ - -/-- Regroup the nested scheduler coins of `plug (par/wire ⋯) K` onto the -left-factored shape: the first component keeps a single `true` coin, the -second component moves under two `false` coins, and the context moves under -`false, true`. -/ -def parLeftPathEquiv (t₁ t₂ tk : TypeTree.{w}) : - TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => t₁ - | ⟨false⟩ => t₂ - | ⟨false⟩ => tk) ≃ - TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => t₁ - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => tk - | ⟨false⟩ => t₂) where - toFun := fun - | ⟨⟨true⟩, ⟨⟨true⟩, tr⟩⟩ => ⟨⟨true⟩, tr⟩ - | ⟨⟨true⟩, ⟨⟨false⟩, tr⟩⟩ => ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ - | ⟨⟨false⟩, tr⟩ => ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ - invFun := fun - | ⟨⟨true⟩, tr⟩ => ⟨⟨true⟩, ⟨⟨true⟩, tr⟩⟩ - | ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ => ⟨⟨false⟩, tr⟩ - | ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ => ⟨⟨true⟩, ⟨⟨false⟩, tr⟩⟩ - left_inv := by - rintro ⟨⟨b⟩, tr⟩ - cases b - · rfl - · obtain ⟨⟨b'⟩, tr'⟩ := tr - cases b' <;> rfl - right_inv := by - rintro ⟨⟨b⟩, tr⟩ - cases b - · obtain ⟨⟨b'⟩, tr'⟩ := tr - cases b' <;> rfl - · rfl +/-! ## Closed composites of the theory's injections + +Every injection used by `openTheory` keeps the closed-world node data and the +activation flag. A closing context therefore decorates a leaf identically +whichever adaptations precede it, which is what the sampler-level shapes ask +of the two sides of a plug factorization. -/ + +section ClosedComposites + +variable (Party : Type u) + +/- The injections are unfolded only here, to check that composites agree +nodewise. Traces are compared as lists, so `FreeMonoid` and `Idx` stay +transparent to `rw` and `apply` at implicit transparency. -/ +attribute [local implicit_reducible] FreeMonoid PFunctor.Idx + +attribute [local simp] TypeTree.Node.ContextHom.comp OpenNodeContext.close + OpenNodeContext.inlTensor OpenNodeContext.inrTensor OpenNodeContext.map + OpenNodeContext.wireLeft OpenNodeContext.wireRight OpenNodeProfile.mapBoundary + BoundaryAction.closed BoundaryAction.embedInlTensor BoundaryAction.embedInrTensor + BoundaryAction.mapBoundary BoundaryAction.wireLeft BoundaryAction.wireRight + +theorem close_comp_inlTensor (Δ₁ Δ₂ : PortBoundary) : + TypeTree.Node.ContextHom.comp (OpenNodeContext.close.{u, w} Party (PortBoundary.tensor Δ₁ Δ₂)) + (OpenNodeContext.inlTensor Party Δ₁ Δ₂) = + OpenNodeContext.close Party Δ₁ := by + funext X ons + simp + +theorem close_comp_inrTensor (Δ₁ Δ₂ : PortBoundary) : + TypeTree.Node.ContextHom.comp (OpenNodeContext.close.{u, w} Party (PortBoundary.tensor Δ₁ Δ₂)) + (OpenNodeContext.inrTensor Party Δ₁ Δ₂) = + OpenNodeContext.close Party Δ₂ := by + funext X ons + simp + +theorem close_comp_wireLeft (Δ₁ Γ Δ₂ : PortBoundary) : + TypeTree.Node.ContextHom.comp (OpenNodeContext.close.{u, w} Party (PortBoundary.tensor Δ₁ Δ₂)) + (OpenNodeContext.wireLeft Party Δ₁ Γ Δ₂) = + OpenNodeContext.close Party (PortBoundary.tensor Δ₁ Γ) := by + funext X ons + simp + +theorem close_comp_wireRight (Δ₁ Γ Δ₂ : PortBoundary) : + TypeTree.Node.ContextHom.comp (OpenNodeContext.close.{u, w} Party (PortBoundary.tensor Δ₁ Δ₂)) + (OpenNodeContext.wireRight Party Δ₁ Γ Δ₂) = + OpenNodeContext.close Party (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂) := by + funext X ons + simp + +/-- The closing context after adapting a wired pair on the left is the +closing context of the pair's left factor. -/ +theorem close_comp_map_comp_wireLeft {Δ₁ Γ Δ₂ Δ : PortBoundary} + (φ : PortBoundary.Hom (PortBoundary.tensor Δ₁ Δ₂) Δ) : + TypeTree.Node.ContextHom.comp (OpenNodeContext.close.{u, w} Party Δ) + (TypeTree.Node.ContextHom.comp (OpenNodeContext.map Party φ) + (OpenNodeContext.wireLeft Party Δ₁ Γ Δ₂)) = + OpenNodeContext.close Party (PortBoundary.tensor Δ₁ Γ) := by + funext X ons + simp + +/-- The closing context after adapting a wired pair on the right, and the +right factor before wiring, is the closing context of that factor. -/ +theorem close_comp_map_comp_wireRight_comp_map {Δ₁ Γ Δ₂ Δ Δ' : PortBoundary} + (φ : PortBoundary.Hom (PortBoundary.tensor Δ₁ Δ₂) Δ) + (ψ : PortBoundary.Hom Δ' (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)) : + TypeTree.Node.ContextHom.comp (OpenNodeContext.close.{u, w} Party Δ) + (TypeTree.Node.ContextHom.comp + (TypeTree.Node.ContextHom.comp (OpenNodeContext.map Party φ) + (OpenNodeContext.wireRight Party Δ₁ Γ Δ₂)) + (OpenNodeContext.map Party ψ)) = + OpenNodeContext.close Party Δ' := by + funext X ons + simp + +/-- The closing context after adapting a wired pair on the left, and the +left factor before wiring, is the closing context of that factor. -/ +theorem close_comp_map_comp_wireLeft_comp_map {Δ₁ Γ Δ₂ Δ Δ' : PortBoundary} + (φ : PortBoundary.Hom (PortBoundary.tensor Δ₁ Δ₂) Δ) + (ψ : PortBoundary.Hom Δ' (PortBoundary.tensor Δ₁ Γ)) : + TypeTree.Node.ContextHom.comp (OpenNodeContext.close.{u, w} Party Δ) + (TypeTree.Node.ContextHom.comp + (TypeTree.Node.ContextHom.comp (OpenNodeContext.map Party φ) + (OpenNodeContext.wireLeft Party Δ₁ Γ Δ₂)) + (OpenNodeContext.map Party ψ)) = + OpenNodeContext.close Party Δ' := by + funext X ons + simp + +/-- The closing context after adapting a wired pair on the right is the +closing context of the pair's right factor. -/ +theorem close_comp_map_comp_wireRight {Δ₁ Γ Δ₂ Δ : PortBoundary} + (φ : PortBoundary.Hom (PortBoundary.tensor Δ₁ Δ₂) Δ) : + TypeTree.Node.ContextHom.comp (OpenNodeContext.close.{u, w} Party Δ) + (TypeTree.Node.ContextHom.comp (OpenNodeContext.map Party φ) + (OpenNodeContext.wireRight Party Δ₁ Γ Δ₂)) = + OpenNodeContext.close Party (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂) := by + funext X ons + simp + +/-- The closing context after wiring and adapting the right factor is the +closing context of that factor. -/ +theorem close_comp_wireRight_comp_map {Δ₁ Γ Δ₂ Δ' : PortBoundary} + (ψ : PortBoundary.Hom Δ' (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)) : + TypeTree.Node.ContextHom.comp (OpenNodeContext.close.{u, w} Party (PortBoundary.tensor Δ₁ Δ₂)) + (TypeTree.Node.ContextHom.comp (OpenNodeContext.wireRight Party Δ₁ Γ Δ₂) + (OpenNodeContext.map Party ψ)) = + OpenNodeContext.close Party Δ' := by + funext X ons + simp + +/-- The closing context after wiring and adapting the left factor is the +closing context of that factor. -/ +theorem close_comp_wireLeft_comp_map {Δ₁ Γ Δ₂ Δ' : PortBoundary} + (ψ : PortBoundary.Hom Δ' (PortBoundary.tensor Δ₁ Γ)) : + TypeTree.Node.ContextHom.comp (OpenNodeContext.close.{u, w} Party (PortBoundary.tensor Δ₁ Δ₂)) + (TypeTree.Node.ContextHom.comp (OpenNodeContext.wireLeft Party Δ₁ Γ Δ₂) + (OpenNodeContext.map Party ψ)) = + OpenNodeContext.close Party Δ' := by + funext X ons + simp + +/-! ### Tensor equivalences reindex the injections + +Pushing a boundary equivalence through an injection is another injection, or a +composite of injections, because the equivalences only relabel positions. -/ + +theorem map_tensorComm_comp_inlTensor (Δ₁ Δ₂ : PortBoundary) : + TypeTree.Node.ContextHom.comp + (OpenNodeContext.map.{u, w} Party (PortBoundary.Equiv.tensorComm Δ₁ Δ₂).toHom) + (OpenNodeContext.inlTensor Party Δ₁ Δ₂) = + OpenNodeContext.inrTensor Party Δ₂ Δ₁ := by + funext X ons + simp only [TypeTree.Node.ContextHom.comp, Function.comp_apply, OpenNodeContext.map, + OpenNodeProfile.mapBoundary, OpenNodeContext.inlTensor, BoundaryAction.embedInlTensor, + BoundaryAction.mapBoundary, OpenNodeContext.inrTensor, BoundaryAction.embedInrTensor, + OpenNodeProfile.mk.injEq, BoundaryAction.mk.injEq, true_and] + rw [← PFunctor.Trace.mapChart_comp] + refine congrArg (PFunctor.Trace.mapChart · ons.boundary.emit) ?_ + refine PFunctor.Chart.ext _ _ (fun a => ?_) (fun a => ?_) + · rfl + · funext b; rfl + +theorem map_tensorComm_comp_inrTensor (Δ₁ Δ₂ : PortBoundary) : + TypeTree.Node.ContextHom.comp + (OpenNodeContext.map.{u, w} Party (PortBoundary.Equiv.tensorComm Δ₁ Δ₂).toHom) + (OpenNodeContext.inrTensor Party Δ₁ Δ₂) = + OpenNodeContext.inlTensor Party Δ₂ Δ₁ := by + funext X ons + simp only [TypeTree.Node.ContextHom.comp, Function.comp_apply, OpenNodeContext.map, + OpenNodeProfile.mapBoundary, OpenNodeContext.inlTensor, BoundaryAction.embedInlTensor, + BoundaryAction.mapBoundary, OpenNodeContext.inrTensor, BoundaryAction.embedInrTensor, + OpenNodeProfile.mk.injEq, BoundaryAction.mk.injEq, true_and] + rw [← PFunctor.Trace.mapChart_comp] + refine congrArg (PFunctor.Trace.mapChart · ons.boundary.emit) ?_ + refine PFunctor.Chart.ext _ _ (fun a => ?_) (fun a => ?_) + · rfl + · funext b; rfl + +theorem map_tensorAssoc_comp_inlTensor_comp_inlTensor (Δ₁ Δ₂ Δ₃ : PortBoundary) : + TypeTree.Node.ContextHom.comp + (TypeTree.Node.ContextHom.comp + (OpenNodeContext.map.{u, w} Party (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom) + (OpenNodeContext.inlTensor Party (PortBoundary.tensor Δ₁ Δ₂) Δ₃)) + (OpenNodeContext.inlTensor Party Δ₁ Δ₂) = + OpenNodeContext.inlTensor Party Δ₁ (PortBoundary.tensor Δ₂ Δ₃) := by + funext X ons + simp only [TypeTree.Node.ContextHom.comp, Function.comp_apply, OpenNodeContext.map, + OpenNodeProfile.mapBoundary, OpenNodeContext.inlTensor, BoundaryAction.embedInlTensor, + BoundaryAction.mapBoundary, OpenNodeProfile.mk.injEq, BoundaryAction.mk.injEq, true_and] + rw [← PFunctor.Trace.mapChart_comp, ← PFunctor.Trace.mapChart_comp] + refine congrArg (PFunctor.Trace.mapChart · ons.boundary.emit) ?_ + refine PFunctor.Chart.ext _ _ (fun a => ?_) (fun a => ?_) + · rfl + · funext b; rfl + +theorem map_tensorAssoc_comp_inlTensor_comp_inrTensor (Δ₁ Δ₂ Δ₃ : PortBoundary) : + TypeTree.Node.ContextHom.comp + (TypeTree.Node.ContextHom.comp + (OpenNodeContext.map.{u, w} Party (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom) + (OpenNodeContext.inlTensor Party (PortBoundary.tensor Δ₁ Δ₂) Δ₃)) + (OpenNodeContext.inrTensor Party Δ₁ Δ₂) = + TypeTree.Node.ContextHom.comp + (OpenNodeContext.inrTensor Party Δ₁ (PortBoundary.tensor Δ₂ Δ₃)) + (OpenNodeContext.inlTensor Party Δ₂ Δ₃) := by + funext X ons + simp only [TypeTree.Node.ContextHom.comp, Function.comp_apply, OpenNodeContext.map, + OpenNodeProfile.mapBoundary, OpenNodeContext.inlTensor, BoundaryAction.embedInlTensor, + BoundaryAction.mapBoundary, OpenNodeContext.inrTensor, BoundaryAction.embedInrTensor, + OpenNodeProfile.mk.injEq, BoundaryAction.mk.injEq, true_and] + rw [← PFunctor.Trace.mapChart_comp, ← PFunctor.Trace.mapChart_comp, + ← PFunctor.Trace.mapChart_comp] + refine congrArg (PFunctor.Trace.mapChart · ons.boundary.emit) ?_ + refine PFunctor.Chart.ext _ _ (fun a => ?_) (fun a => ?_) + · rfl + · funext b; rfl + +theorem map_tensorAssoc_comp_inrTensor (Δ₁ Δ₂ Δ₃ : PortBoundary) : + TypeTree.Node.ContextHom.comp + (OpenNodeContext.map.{u, w} Party (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom) + (OpenNodeContext.inrTensor Party (PortBoundary.tensor Δ₁ Δ₂) Δ₃) = + TypeTree.Node.ContextHom.comp + (OpenNodeContext.inrTensor Party Δ₁ (PortBoundary.tensor Δ₂ Δ₃)) + (OpenNodeContext.inrTensor Party Δ₂ Δ₃) := by + funext X ons + simp only [TypeTree.Node.ContextHom.comp, Function.comp_apply, OpenNodeContext.map, + OpenNodeProfile.mapBoundary, OpenNodeContext.inrTensor, BoundaryAction.embedInrTensor, + BoundaryAction.mapBoundary, OpenNodeProfile.mk.injEq, BoundaryAction.mk.injEq, true_and] + rw [← PFunctor.Trace.mapChart_comp, ← PFunctor.Trace.mapChart_comp] + refine congrArg (PFunctor.Trace.mapChart · ons.boundary.emit) ?_ + refine PFunctor.Chart.ext _ _ (fun a => ?_) (fun a => ?_) + · rfl + · funext b; rfl + +/-- Commuting a wire's two factors turns the left wiring of the swapped right +factor into the right wiring of the original. -/ +theorem map_tensorComm_comp_wireLeft_comp_map_tensorComm (Δ₁ Γ Δ₂ : PortBoundary) : + TypeTree.Node.ContextHom.comp + (TypeTree.Node.ContextHom.comp + (OpenNodeContext.map.{u, w} Party (PortBoundary.Equiv.tensorComm Δ₂ Δ₁).toHom) + (OpenNodeContext.wireLeft Party Δ₂ (PortBoundary.swap Γ) Δ₁)) + (OpenNodeContext.map Party + (PortBoundary.Equiv.tensorComm (PortBoundary.swap Γ) Δ₂).toHom) = + OpenNodeContext.wireRight Party Δ₁ Γ Δ₂ := by + funext X ons + simp only [TypeTree.Node.ContextHom.comp, Function.comp_apply, OpenNodeContext.map, + OpenNodeProfile.mapBoundary, BoundaryAction.mapBoundary, OpenNodeContext.wireLeft, + BoundaryAction.wireLeft, OpenNodeContext.wireRight, BoundaryAction.wireRight, + OpenNodeProfile.mk.injEq, BoundaryAction.mk.injEq, true_and] + funext x + simp only [PFunctor.Trace.mapChart_apply, PFunctor.Trace.mapPartial_apply, + List.filterMap_filterMap] + apply List.filterMap_congr + rintro ⟨(_ | _), _⟩ _ <;> rfl + +/-- Commuting a wire's two factors turns the right wiring of the swapped left +factor into the left wiring of the original. -/ +theorem map_tensorComm_comp_wireRight_comp_map_tensorComm (Δ₁ Γ Δ₂ : PortBoundary) : + TypeTree.Node.ContextHom.comp + (TypeTree.Node.ContextHom.comp + (OpenNodeContext.map.{u, w} Party (PortBoundary.Equiv.tensorComm Δ₂ Δ₁).toHom) + (OpenNodeContext.wireRight Party Δ₂ (PortBoundary.swap Γ) Δ₁)) + (OpenNodeContext.map Party (PortBoundary.Equiv.tensorComm Δ₁ Γ).toHom) = + OpenNodeContext.wireLeft Party Δ₁ Γ Δ₂ := by + funext X ons + simp only [TypeTree.Node.ContextHom.comp, Function.comp_apply, OpenNodeContext.map, + OpenNodeProfile.mapBoundary, BoundaryAction.mapBoundary, OpenNodeContext.wireLeft, + BoundaryAction.wireLeft, OpenNodeContext.wireRight, BoundaryAction.wireRight, + OpenNodeProfile.mk.injEq, BoundaryAction.mk.injEq, true_and] + funext x + simp only [PFunctor.Trace.mapChart_apply, PFunctor.Trace.mapPartial_apply, + List.filterMap_filterMap] + apply List.filterMap_congr + rintro ⟨(_ | _), _⟩ _ <;> rfl + +end ClosedComposites + +/-- The scheduler node is internal. -/ +theorem isInternalNode_schedulerNode (Party : Type u) (Δ : PortBoundary) : + OpenNodeContext.IsInternalNode (schedulerNode.{u, w} Party Δ) := + rfl variable (Party : Type u) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) +open OpenProcessFactorization + /-! ## Sampler-aware plug commutation -/ /-- `plug` is commutative up to sampler equivalence, provided the scheduler is @@ -318,46 +445,12 @@ theorem openTheory_plug_comm_sampler_equiv [Monad m] [LawfulMonad m] OpenProcessSamplerEquiv R ((openTheory Party m schedulerSampler).plug W K) ((openTheory Party m schedulerSampler).plug K W) := by - refine ⟨fun (⟨s₁, s₂⟩ : W.Proc × K.Proc) (⟨s₂', s₁'⟩ : K.Proc × W.Proc) => - s₁ = s₁' ∧ s₂ = s₂', - ⟨?_⟩, - fun ⟨s₁, s₂⟩ => ⟨⟨s₂, s₁⟩, rfl, rfl⟩, - fun ⟨s₂, s₁⟩ => ⟨⟨s₁, s₂⟩, rfl, rfl⟩⟩ - rintro ⟨s₁, s₂⟩ ⟨s₂', s₁'⟩ ⟨h1, h2⟩ - subst h1 - subst h2 - refine ⟨flipInterleavePathEquiv (W.step s₁).tree (K.step s₂).tree, - ?_, ?_, ?_, ?_⟩ - · -- Silence is preserved: the scheduler node is never activated and the - -- branch decorations differ only by activation-preserving close maps. - rintro ⟨⟨b⟩, tr⟩ - cases b <;> - exact and_congr Iff.rfl - (((isSilentDecoration_iff_map _ (fun X ons => by - simp [OpenNodeContext.close, BoundaryAction.closed]) _ _).trans - (isSilentDecoration_iff_map _ (fun X ons => by - simp [OpenNodeContext.close, BoundaryAction.closed]) _ _).symm)) - · -- Both boundary traces live over the empty boundary. - intro tr - exact traceList_interface_empty_eq _ _ - · -- Successors are componentwise equal after the swap. - rintro ⟨⟨b⟩, tr⟩ - cases b <;> exact ⟨rfl, rfl⟩ - · -- The sampled paths are related by scheduler fairness. - change R.rel - ((fun tr => flipInterleavePathEquiv (W.step s₁).tree (K.step s₂).tree tr) - <$> TypeTree.samplePath _ - (TypeTree.Sampler.interleave schedulerSampler - (W.stepSampler s₁) (K.stepSampler s₂))) - (TypeTree.samplePath _ - (TypeTree.Sampler.interleave schedulerSampler - (K.stepSampler s₂) (W.stepSampler s₁))) - rw [samplePath_interleave_flip] - exact samplePath_interleave_congr_scheduler R (R.symm hfair) _ _ - -/-! ## Sampler-aware left par factorization -/ - -open OpenProcessFactorization in + simp only [openTheory] + exact interleave_comm_samplerEquiv R W K schedulerSampler schedulerSampler + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _) (R.symm hfair) + +/-! ## Sampler-aware left factorizations -/ + /-- Closing a parallel composition factors through its left component, up to sampler equivalence, conditionally on the scheduler-transport fact `R.rel (sourceDraw schedulerSampler) (leftDraw schedulerSampler)`: the source @@ -387,204 +480,24 @@ theorem openTheory_plug_par_left_sampler_equiv [Monad m] [LawfulMonad m] K (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyRight Δ₂).symm.toHom W₂)))) := by - refine ⟨fun (⟨⟨s₁, s₂⟩, k⟩ : (W₁.Proc × W₂.Proc) × K.Proc) - (⟨s₁', k', s₂'⟩ : W₁.Proc × K.Proc × W₂.Proc) => - s₁ = s₁' ∧ s₂ = s₂' ∧ k = k', - ⟨?_⟩, - fun ⟨⟨s₁, s₂⟩, k⟩ => ⟨⟨s₁, k, s₂⟩, rfl, rfl, rfl⟩, - fun ⟨s₁, k, s₂⟩ => ⟨⟨⟨s₁, s₂⟩, k⟩, rfl, rfl, rfl⟩⟩ - rintro ⟨⟨s₁, s₂⟩, k⟩ ⟨s₁', k', s₂'⟩ ⟨h1, h2, h3⟩ - subst h1 - subst h2 - subst h3 - refine ⟨parLeftPathEquiv (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree, - ?_, ?_, ?_, ?_⟩ - · -- Silence is preserved through the regrouping. - rintro ⟨⟨b⟩, rest⟩ - simp only [IsSilentStep, PFunctor.FreeM.Displayed.Decoration.map, - OpenProcess.mapBoundary, StepOver.mapContext] - cases b - · -- Context path: `⟨F, tr⟩ ↦ ⟨F, ⟨T, tr⟩⟩`. - constructor - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2)))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2)))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · -- Composite paths: case on the inner coin. - obtain ⟨⟨b'⟩, rest'⟩ := rest - cases b' - · -- Second component: `⟨T, ⟨F, tr⟩⟩ ↦ ⟨F, ⟨F, tr⟩⟩`. - constructor - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2)))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.inrTensor, BoundaryAction.embedInrTensor] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2)))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.inrTensor, BoundaryAction.embedInrTensor] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · -- First component: `⟨T, ⟨T, tr⟩⟩ ↦ ⟨T, tr⟩`. - constructor - · intro h - refine ⟨rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.inlTensor, BoundaryAction.embedInlTensor] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.inlTensor, BoundaryAction.embedInlTensor] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · -- Both boundary traces live over the empty boundary. - intro tr - exact traceList_interface_empty_eq _ _ - · -- Successors are componentwise equal after the regrouping. - rintro ⟨⟨b⟩, rest⟩ - cases b - · exact ⟨rfl, rfl, rfl⟩ - · obtain ⟨⟨b'⟩, rest'⟩ := rest - cases b' <;> exact ⟨rfl, rfl, rfl⟩ - · -- The sampled paths are related by the scheduler-transport fact. - change R.rel - ((fun tr => parLeftPathEquiv - (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree tr) <$> - TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => (W₂.step s₂).tree - | ⟨false⟩ => (K.step k).tree) - (TypeTree.Sampler.interleave schedulerSampler - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) (W₂.stepSampler s₂)) - (K.stepSampler k))) - (TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₂.step s₂).tree) - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) - (TypeTree.Sampler.interleave schedulerSampler - (K.stepSampler k) (W₂.stepSampler s₂)))) - set e := parLeftPathEquiv - (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree with he - let h : ULift.{w, 0} Leaf → - m (TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₂.step s₂).tree)) := fun leaf => - match leaf with - | ⟨.first⟩ => TypeTree.samplePath _ (W₁.stepSampler s₁) >>= fun tr => - pure ⟨⟨true⟩, tr⟩ - | ⟨.second⟩ => TypeTree.samplePath _ (W₂.stepSampler s₂) >>= fun tr => - pure ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ - | ⟨.context⟩ => TypeTree.samplePath _ (K.stepSampler k) >>= fun tr => - pure ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ - have hR : TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₂.step s₂).tree) - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) - (TypeTree.Sampler.interleave schedulerSampler - (K.stepSampler k) (W₂.stepSampler s₂))) = - leftDraw schedulerSampler >>= h := by - rw [leftDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [TypeTree.samplePath, bind_assoc, pure_bind] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> rfl - · rfl - have hL : (fun tr => e tr) <$> - TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => (W₂.step s₂).tree - | ⟨false⟩ => (K.step k).tree) - (TypeTree.Sampler.interleave schedulerSampler - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) (W₂.stepSampler s₂)) - (K.stepSampler k)) = - sourceDraw schedulerSampler >>= h := by - rw [sourceDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [map_pure] - rfl - · simp only [TypeTree.samplePath, bind_assoc, map_pure, pure_bind] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> rfl - rw [hL, hR] - exact R.bind_congr h hσ - -/-! ## Sampler-aware left wire factorization -/ - -open OpenProcessFactorization in -/-- Closing a wired composition factors through its left factor, up to sampler -equivalence, conditionally on the source/left scheduler-transport fact. The -sampler-aware strengthening of -`openTheory_plug_wire_left_activation_equiv`. -/ + simp only [openTheory] + rw [OpenProcess.mapBoundary_interleave, OpenProcess.mapBoundary_eq_mapHom, + OpenProcess.interleave_mapHom_right] + exact interleave_factorLeft_samplerEquiv R W₁ W₂ K schedulerSampler schedulerSampler + schedulerSampler schedulerSampler + (close_comp_inlTensor Party Δ₁ Δ₂) + ((close_comp_inrTensor Party Δ₁ Δ₂).trans + (close_comp_map_comp_wireRight_comp_map Party (Δ₁ := PortBoundary.swap Δ₁) + (Γ := PortBoundary.swap Δ₂) (Δ₂ := PortBoundary.empty) _ _).symm) + (close_comp_map_comp_wireLeft Party (Δ₁ := PortBoundary.swap Δ₁) (Γ := PortBoundary.swap Δ₂) + (Δ₂ := PortBoundary.empty) _).symm + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _).close + (isInternalNode_schedulerNode Party _) + ((isInternalNode_schedulerNode Party _).map _).close hσ + +/-- Closing a wired composition factors through its left factor, up to +sampler equivalence, conditionally on the same scheduler-transport fact as the +parallel case. -/ theorem openTheory_plug_wire_left_sampler_equiv [Monad m] [LawfulMonad m] (R : MonadRelFamily m) (hσ : R.rel (sourceDraw schedulerSampler) (leftDraw schedulerSampler)) @@ -604,227 +517,26 @@ theorem openTheory_plug_wire_left_sampler_equiv [Monad m] [LawfulMonad m] (Δ₂ := PortBoundary.swap Γ) K (OpenProcess.mapBoundary - (PortBoundary.Equiv.tensorComm (PortBoundary.swap Γ) Δ₂).toHom - W₂))) := by - refine ⟨fun (⟨⟨s₁, s₂⟩, k⟩ : (W₁.Proc × W₂.Proc) × K.Proc) - (⟨s₁', k', s₂'⟩ : W₁.Proc × K.Proc × W₂.Proc) => - s₁ = s₁' ∧ s₂ = s₂' ∧ k = k', - ⟨?_⟩, - fun ⟨⟨s₁, s₂⟩, k⟩ => ⟨⟨s₁, k, s₂⟩, rfl, rfl, rfl⟩, - fun ⟨s₁, k, s₂⟩ => ⟨⟨⟨s₁, s₂⟩, k⟩, rfl, rfl, rfl⟩⟩ - rintro ⟨⟨s₁, s₂⟩, k⟩ ⟨s₁', k', s₂'⟩ ⟨h1, h2, h3⟩ - subst h1 - subst h2 - subst h3 - refine ⟨parLeftPathEquiv (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree, - ?_, ?_, ?_, ?_⟩ - · rintro ⟨⟨b⟩, rest⟩ - simp only [IsSilentStep, PFunctor.FreeM.Displayed.Decoration.map, - OpenProcess.mapBoundary, StepOver.mapContext] - cases b - · -- Context path: `⟨F, tr⟩ ↦ ⟨F, ⟨T, tr⟩⟩`. - constructor - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · obtain ⟨⟨b'⟩, rest'⟩ := rest - cases b' - · -- Second factor: `⟨T, ⟨F, tr⟩⟩ ↦ ⟨F, ⟨F, tr⟩⟩`. - constructor - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · -- First factor: `⟨T, ⟨T, tr⟩⟩ ↦ ⟨T, tr⟩`. - constructor - · intro h - refine ⟨rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro tr - exact traceList_interface_empty_eq _ _ - · rintro ⟨⟨b⟩, rest⟩ - cases b - · exact ⟨rfl, rfl, rfl⟩ - · obtain ⟨⟨b'⟩, rest'⟩ := rest - cases b' <;> exact ⟨rfl, rfl, rfl⟩ - · change R.rel - ((fun tr => parLeftPathEquiv - (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree tr) <$> - TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => (W₂.step s₂).tree - | ⟨false⟩ => (K.step k).tree) - (TypeTree.Sampler.interleave schedulerSampler - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) (W₂.stepSampler s₂)) - (K.stepSampler k))) - (TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₂.step s₂).tree) - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) - (TypeTree.Sampler.interleave schedulerSampler - (K.stepSampler k) (W₂.stepSampler s₂)))) - set e := parLeftPathEquiv - (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree with he - let h : ULift.{w, 0} Leaf → - m (TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₂.step s₂).tree)) := fun leaf => - match leaf with - | ⟨.first⟩ => TypeTree.samplePath _ (W₁.stepSampler s₁) >>= fun tr => - pure ⟨⟨true⟩, tr⟩ - | ⟨.second⟩ => TypeTree.samplePath _ (W₂.stepSampler s₂) >>= fun tr => - pure ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ - | ⟨.context⟩ => TypeTree.samplePath _ (K.stepSampler k) >>= fun tr => - pure ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ - have hR : TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₂.step s₂).tree) - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) - (TypeTree.Sampler.interleave schedulerSampler - (K.stepSampler k) (W₂.stepSampler s₂))) = - leftDraw schedulerSampler >>= h := by - rw [leftDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [TypeTree.samplePath, bind_assoc, pure_bind] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> rfl - · rfl - have hL : (fun tr => e tr) <$> - TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => (W₂.step s₂).tree - | ⟨false⟩ => (K.step k).tree) - (TypeTree.Sampler.interleave schedulerSampler - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) (W₂.stepSampler s₂)) - (K.stepSampler k)) = - sourceDraw schedulerSampler >>= h := by - rw [sourceDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [map_pure] - rfl - · simp only [TypeTree.samplePath, bind_assoc, map_pure, pure_bind] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> rfl - rw [hL, hR] - exact R.bind_congr h hσ - -/-! ## Path re-encoding for the right par/wire factorizations -/ - -/-- Regroup the nested scheduler coins of `plug (par/wire ⋯) K` onto the -right-factored shape: the second component keeps a single `true` coin, the -first component moves under two `false` coins, and the context moves under -`false, true`. -/ -def parRightPathEquiv (t₁ t₂ tk : TypeTree.{w}) : - TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => t₁ - | ⟨false⟩ => t₂ - | ⟨false⟩ => tk) ≃ - TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => t₂ - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => tk - | ⟨false⟩ => t₁) where - toFun := fun - | ⟨⟨true⟩, ⟨⟨true⟩, tr⟩⟩ => ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ - | ⟨⟨true⟩, ⟨⟨false⟩, tr⟩⟩ => ⟨⟨true⟩, tr⟩ - | ⟨⟨false⟩, tr⟩ => ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ - invFun := fun - | ⟨⟨true⟩, tr⟩ => ⟨⟨true⟩, ⟨⟨false⟩, tr⟩⟩ - | ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ => ⟨⟨false⟩, tr⟩ - | ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ => ⟨⟨true⟩, ⟨⟨true⟩, tr⟩⟩ - left_inv := by - rintro ⟨⟨b⟩, tr⟩ - cases b - · rfl - · obtain ⟨⟨b'⟩, tr'⟩ := tr - cases b' <;> rfl - right_inv := by - rintro ⟨⟨b⟩, tr⟩ - cases b - · obtain ⟨⟨b'⟩, tr'⟩ := tr - cases b' <;> rfl - · rfl - -/-! ## Sampler-aware right par factorization -/ - -open OpenProcessFactorization in + (PortBoundary.Equiv.tensorComm (PortBoundary.swap Γ) Δ₂).toHom W₂))) := by + simp only [openTheory] + rw [OpenProcess.mapBoundary_eq_mapHom, OpenProcess.interleave_mapHom_right] + exact interleave_factorLeft_samplerEquiv R W₁ W₂ K schedulerSampler schedulerSampler + schedulerSampler schedulerSampler + (close_comp_wireLeft Party Δ₁ Γ Δ₂) + ((close_comp_wireRight Party Δ₁ Γ Δ₂).trans + (close_comp_wireRight_comp_map Party (Δ₁ := PortBoundary.swap Δ₁) + (Γ := PortBoundary.swap Δ₂) (Δ₂ := PortBoundary.swap Γ) _).symm) + (close_comp_wireLeft Party (PortBoundary.swap Δ₁) (PortBoundary.swap Δ₂) + (PortBoundary.swap Γ)).symm + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _).close + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _).close hσ + +/-! ## Sampler-aware right factorizations -/ + /-- Closing a parallel composition factors through its right component, up to -sampler equivalence, conditionally on the source/right scheduler-transport -fact. The sampler-aware strengthening of -`openTheory_plug_par_right_activation_equiv`. -/ +sampler equivalence, conditionally on the scheduler-transport fact +`R.rel (sourceDraw schedulerSampler) (rightDraw schedulerSampler)`. The +mirror of `openTheory_plug_par_left_sampler_equiv`. -/ theorem openTheory_plug_par_right_sampler_equiv [Monad m] [LawfulMonad m] (R : MonadRelFamily m) (hσ : R.rel (sourceDraw schedulerSampler) (rightDraw schedulerSampler)) @@ -847,205 +559,26 @@ theorem openTheory_plug_par_right_sampler_equiv [Monad m] [LawfulMonad m] (PortBoundary.swap Δ₁) (PortBoundary.swap Δ₂)).toHom K) (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyRight Δ₁).symm.toHom W₁)))) := by - refine ⟨fun (⟨⟨s₁, s₂⟩, k⟩ : (W₁.Proc × W₂.Proc) × K.Proc) - (⟨s₂', k', s₁'⟩ : W₂.Proc × K.Proc × W₁.Proc) => - s₁ = s₁' ∧ s₂ = s₂' ∧ k = k', - ⟨?_⟩, - fun ⟨⟨s₁, s₂⟩, k⟩ => ⟨⟨s₂, k, s₁⟩, rfl, rfl, rfl⟩, - fun ⟨s₂, k, s₁⟩ => ⟨⟨⟨s₁, s₂⟩, k⟩, rfl, rfl, rfl⟩⟩ - rintro ⟨⟨s₁, s₂⟩, k⟩ ⟨s₂', k', s₁'⟩ ⟨h1, h2, h3⟩ - subst h1 - subst h2 - subst h3 - refine ⟨parRightPathEquiv (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree, - ?_, ?_, ?_, ?_⟩ - · rintro ⟨⟨b⟩, rest⟩ - simp only [IsSilentStep, PFunctor.FreeM.Displayed.Decoration.map, - OpenProcess.mapBoundary, StepOver.mapContext] - cases b - · -- Context path: `⟨F, tr⟩ ↦ ⟨F, ⟨T, tr⟩⟩`. - constructor - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · obtain ⟨⟨b'⟩, rest'⟩ := rest - cases b' - · -- Second component: `⟨T, ⟨F, tr⟩⟩ ↦ ⟨T, tr⟩`. - constructor - · intro h - refine ⟨rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.inrTensor, BoundaryAction.embedInrTensor] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.inrTensor, BoundaryAction.embedInrTensor] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · -- First component: `⟨T, ⟨T, tr⟩⟩ ↦ ⟨F, ⟨F, tr⟩⟩`. - constructor - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2)))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.inlTensor, BoundaryAction.embedInlTensor] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2)))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.inlTensor, BoundaryAction.embedInlTensor] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro tr - exact traceList_interface_empty_eq _ _ - · rintro ⟨⟨b⟩, rest⟩ - cases b - · exact ⟨rfl, rfl, rfl⟩ - · obtain ⟨⟨b'⟩, rest'⟩ := rest - cases b' <;> exact ⟨rfl, rfl, rfl⟩ - · change R.rel - ((fun tr => parRightPathEquiv - (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree tr) <$> - TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => (W₂.step s₂).tree - | ⟨false⟩ => (K.step k).tree) - (TypeTree.Sampler.interleave schedulerSampler - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) (W₂.stepSampler s₂)) - (K.stepSampler k))) - (TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₂.step s₂).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₁.step s₁).tree) - (TypeTree.Sampler.interleave schedulerSampler - (W₂.stepSampler s₂) - (TypeTree.Sampler.interleave schedulerSampler - (K.stepSampler k) (W₁.stepSampler s₁)))) - set e := parRightPathEquiv - (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree with he - let h : ULift.{w, 0} Leaf → - m (TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₂.step s₂).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₁.step s₁).tree)) := fun leaf => - match leaf with - | ⟨.first⟩ => TypeTree.samplePath _ (W₁.stepSampler s₁) >>= fun tr => - pure ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ - | ⟨.second⟩ => TypeTree.samplePath _ (W₂.stepSampler s₂) >>= fun tr => - pure ⟨⟨true⟩, tr⟩ - | ⟨.context⟩ => TypeTree.samplePath _ (K.stepSampler k) >>= fun tr => - pure ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ - have hR : TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₂.step s₂).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₁.step s₁).tree) - (TypeTree.Sampler.interleave schedulerSampler - (W₂.stepSampler s₂) - (TypeTree.Sampler.interleave schedulerSampler - (K.stepSampler k) (W₁.stepSampler s₁))) = - rightDraw schedulerSampler >>= h := by - rw [rightDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [TypeTree.samplePath, bind_assoc, pure_bind] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> rfl - · rfl - have hL : (fun tr => e tr) <$> - TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => (W₂.step s₂).tree - | ⟨false⟩ => (K.step k).tree) - (TypeTree.Sampler.interleave schedulerSampler - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) (W₂.stepSampler s₂)) - (K.stepSampler k)) = - sourceDraw schedulerSampler >>= h := by - rw [sourceDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [map_pure] - rfl - · simp only [TypeTree.samplePath, bind_assoc, map_pure, pure_bind] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> rfl - rw [hL, hR] - exact R.bind_congr h hσ - -/-! ## Sampler-aware right wire factorization -/ - -open OpenProcessFactorization in + simp only [openTheory] + rw [OpenProcess.mapBoundary_interleave] + simp only [OpenProcess.mapBoundary_eq_mapHom] + rw [OpenProcess.interleave_mapHom_left, OpenProcess.interleave_mapHom_right] + exact interleave_factorRight_samplerEquiv R W₁ W₂ K schedulerSampler schedulerSampler + schedulerSampler schedulerSampler + ((close_comp_inlTensor Party Δ₁ Δ₂).trans + (close_comp_map_comp_wireRight_comp_map Party (Δ₁ := PortBoundary.swap Δ₂) + (Γ := PortBoundary.swap Δ₁) (Δ₂ := PortBoundary.empty) _ _).symm) + (close_comp_inrTensor Party Δ₁ Δ₂) + (close_comp_map_comp_wireLeft_comp_map Party (Δ₁ := PortBoundary.swap Δ₂) + (Γ := PortBoundary.swap Δ₁) (Δ₂ := PortBoundary.empty) + (Δ' := PortBoundary.swap (PortBoundary.tensor Δ₁ Δ₂)) _ _).symm + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _).close + (isInternalNode_schedulerNode Party _) + ((isInternalNode_schedulerNode Party _).map _).close hσ + /-- Closing a wired composition factors through its right factor, up to -sampler equivalence, conditionally on the source/right scheduler-transport -fact. The sampler-aware strengthening of -`openTheory_plug_wire_right_activation_equiv`. -/ +sampler equivalence, conditionally on the same scheduler-transport fact as the +parallel case. The mirror of `openTheory_plug_wire_left_sampler_equiv`. -/ theorem openTheory_plug_wire_right_sampler_equiv [Monad m] [LawfulMonad m] (R : MonadRelFamily m) (hσ : R.rel (sourceDraw schedulerSampler) (rightDraw schedulerSampler)) @@ -1069,191 +602,194 @@ theorem openTheory_plug_wire_right_sampler_equiv [Monad m] [LawfulMonad m] (PortBoundary.Equiv.tensorComm (PortBoundary.swap Δ₁) (PortBoundary.swap Δ₂)).toHom K) W₁))) := by - refine ⟨fun (⟨⟨s₁, s₂⟩, k⟩ : (W₁.Proc × W₂.Proc) × K.Proc) - (⟨s₂', k', s₁'⟩ : W₂.Proc × K.Proc × W₁.Proc) => - s₁ = s₁' ∧ s₂ = s₂' ∧ k = k', - ⟨?_⟩, - fun ⟨⟨s₁, s₂⟩, k⟩ => ⟨⟨s₂, k, s₁⟩, rfl, rfl, rfl⟩, - fun ⟨s₂, k, s₁⟩ => ⟨⟨⟨s₁, s₂⟩, k⟩, rfl, rfl, rfl⟩⟩ - rintro ⟨⟨s₁, s₂⟩, k⟩ ⟨s₂', k', s₁'⟩ ⟨h1, h2, h3⟩ - subst h1 - subst h2 - subst h3 - refine ⟨parRightPathEquiv (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree, - ?_, ?_, ?_, ?_⟩ - · rintro ⟨⟨b⟩, rest⟩ - simp only [IsSilentStep, PFunctor.FreeM.Displayed.Decoration.map, - OpenProcess.mapBoundary, StepOver.mapContext] - cases b - · -- Context path: `⟨F, tr⟩ ↦ ⟨F, ⟨T, tr⟩⟩`. - constructor - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · obtain ⟨⟨b'⟩, rest'⟩ := rest - cases b' - · -- Second factor: `⟨T, ⟨F, tr⟩⟩ ↦ ⟨T, tr⟩`. - constructor - · intro h - refine ⟨rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · -- First factor: `⟨T, ⟨T, tr⟩⟩ ↦ ⟨F, ⟨F, tr⟩⟩`. - constructor - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro h - refine ⟨rfl, rfl, (isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mpr - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp - ((isSilentDecoration_iff_map _ ?_ _ _).mp h.2.2))))⟩ - all_goals intro X ons - · simp [OpenNodeContext.close, BoundaryAction.closed] - · simp [OpenNodeContext.wireLeft, BoundaryAction.wireLeft] - · simp [OpenNodeContext.wireRight, BoundaryAction.wireRight] - · simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, - BoundaryAction.mapBoundary] - · simp [OpenNodeContext.close, BoundaryAction.closed] - · intro tr - exact traceList_interface_empty_eq _ _ - · rintro ⟨⟨b⟩, rest⟩ - cases b - · exact ⟨rfl, rfl, rfl⟩ - · obtain ⟨⟨b'⟩, rest'⟩ := rest - cases b' <;> exact ⟨rfl, rfl, rfl⟩ - · change R.rel - ((fun tr => parRightPathEquiv - (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree tr) <$> - TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => (W₂.step s₂).tree - | ⟨false⟩ => (K.step k).tree) - (TypeTree.Sampler.interleave schedulerSampler - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) (W₂.stepSampler s₂)) - (K.stepSampler k))) - (TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₂.step s₂).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₁.step s₁).tree) - (TypeTree.Sampler.interleave schedulerSampler - (W₂.stepSampler s₂) - (TypeTree.Sampler.interleave schedulerSampler - (K.stepSampler k) (W₁.stepSampler s₁)))) - set e := parRightPathEquiv - (W₁.step s₁).tree (W₂.step s₂).tree (K.step k).tree with he - let h : ULift.{w, 0} Leaf → - m (TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₂.step s₂).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₁.step s₁).tree)) := fun leaf => - match leaf with - | ⟨.first⟩ => TypeTree.samplePath _ (W₁.stepSampler s₁) >>= fun tr => - pure ⟨⟨false⟩, ⟨⟨false⟩, tr⟩⟩ - | ⟨.second⟩ => TypeTree.samplePath _ (W₂.stepSampler s₂) >>= fun tr => - pure ⟨⟨true⟩, tr⟩ - | ⟨.context⟩ => TypeTree.samplePath _ (K.stepSampler k) >>= fun tr => - pure ⟨⟨false⟩, ⟨⟨true⟩, tr⟩⟩ - have hR : TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₂.step s₂).tree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (K.step k).tree - | ⟨false⟩ => (W₁.step s₁).tree) - (TypeTree.Sampler.interleave schedulerSampler - (W₂.stepSampler s₂) - (TypeTree.Sampler.interleave schedulerSampler - (K.stepSampler k) (W₁.stepSampler s₁))) = - rightDraw schedulerSampler >>= h := by - rw [rightDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [TypeTree.samplePath, bind_assoc, pure_bind] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> rfl - · rfl - have hL : (fun tr => e tr) <$> - TypeTree.samplePath - (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => (W₁.step s₁).tree - | ⟨false⟩ => (W₂.step s₂).tree - | ⟨false⟩ => (K.step k).tree) - (TypeTree.Sampler.interleave schedulerSampler - (TypeTree.Sampler.interleave schedulerSampler - (W₁.stepSampler s₁) (W₂.stepSampler s₂)) - (K.stepSampler k)) = - sourceDraw schedulerSampler >>= h := by - rw [sourceDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] - refine bind_congr fun b => ?_ - obtain ⟨bb⟩ := b - cases bb - · simp only [map_pure] - rfl - · simp only [TypeTree.samplePath, bind_assoc, map_pure, pure_bind] - refine bind_congr fun b' => ?_ - obtain ⟨bb'⟩ := b' - cases bb' <;> rfl - rw [hL, hR] - exact R.bind_congr h hσ + simp only [openTheory] + rw [OpenProcess.mapBoundary_interleave, OpenProcess.mapBoundary_eq_mapHom, + OpenProcess.interleave_mapHom_left] + exact interleave_factorRight_samplerEquiv R W₁ W₂ K schedulerSampler schedulerSampler + schedulerSampler schedulerSampler + ((close_comp_wireLeft Party Δ₁ Γ Δ₂).trans + (close_comp_map_comp_wireRight Party (Δ₁ := PortBoundary.swap Δ₂) + (Γ := PortBoundary.swap Δ₁) (Δ₂ := Γ) _).symm) + (close_comp_wireRight Party Δ₁ Γ Δ₂) + (close_comp_map_comp_wireLeft_comp_map Party (Δ₁ := PortBoundary.swap Δ₂) + (Γ := PortBoundary.swap Δ₁) (Δ₂ := Γ) + (Δ' := PortBoundary.swap (PortBoundary.tensor Δ₁ Δ₂)) _ _).symm + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _).close + (isInternalNode_schedulerNode Party _) + ((isInternalNode_schedulerNode Party _).map _).close hσ + +/-! ## Sampler-aware monoidal laws + +The open laws move packets across the tensor equivalences, so their leaves are +decorated by reindexed injections; the reindexing lemmas above make the two +sides' composite injections equal. -/ + +/-- Parallel composition is commutative up to sampler equivalence, provided +the scheduler is `R`-fair. -/ +theorem openTheory_par_comm_sampler_equiv [Monad m] [LawfulMonad m] + (R : MonadRelFamily m) + (hfair : R.rel schedulerSampler (schedulerFlip <$> schedulerSampler)) + {Δ₁ Δ₂ : PortBoundary} + (W₁ : OpenProcess.{u, v, w, w'} m Party Δ₁) + (W₂ : OpenProcess.{u, v, w, w'} m Party Δ₂) : + OpenProcessSamplerEquiv R + (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorComm Δ₁ Δ₂).toHom + ((openTheory Party m schedulerSampler).par W₁ W₂)) + ((openTheory Party m schedulerSampler).par W₂ W₁) := by + simp only [openTheory] + rw [OpenProcess.mapBoundary_interleave, map_tensorComm_comp_inlTensor, + map_tensorComm_comp_inrTensor] + exact interleave_comm_samplerEquiv R W₁ W₂ schedulerSampler schedulerSampler + ((isInternalNode_schedulerNode Party _).map _) (isInternalNode_schedulerNode Party _) + (R.symm hfair) + +/-- Parallel composition is associative up to sampler equivalence, provided +the scheduler is `R`-fair, the left-factored transport fact holds, and `R` is +bind-congruent: the left factorization followed by commutation of the inner +pair. -/ +theorem openTheory_par_assoc_sampler_equiv [Monad m] [LawfulMonad m] + (R : MonadRelFamily m) [R.IsBindCongr] + (hfair : R.rel schedulerSampler (schedulerFlip <$> schedulerSampler)) + (hσ : R.rel (sourceDraw schedulerSampler) (leftDraw schedulerSampler)) + {Δ₁ Δ₂ Δ₃ : PortBoundary} + (W₁ : OpenProcess.{u, v, w, w'} m Party Δ₁) + (W₂ : OpenProcess.{u, v, w, w'} m Party Δ₂) + (W₃ : OpenProcess.{u, v, w, w'} m Party Δ₃) : + OpenProcessSamplerEquiv R + (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom + ((openTheory Party m schedulerSampler).par + ((openTheory Party m schedulerSampler).par W₁ W₂) W₃)) + ((openTheory Party m schedulerSampler).par W₁ + ((openTheory Party m schedulerSampler).par W₂ W₃)) := by + simp only [openTheory] + rw [OpenProcess.mapBoundary_interleave] + exact interleave_assoc_samplerEquiv R W₁ W₂ W₃ schedulerSampler schedulerSampler + schedulerSampler schedulerSampler schedulerSampler + (map_tensorAssoc_comp_inlTensor_comp_inlTensor Party Δ₁ Δ₂ Δ₃) + (map_tensorAssoc_comp_inlTensor_comp_inrTensor Party Δ₁ Δ₂ Δ₃) + (map_tensorAssoc_comp_inrTensor Party Δ₁ Δ₂ Δ₃) + ((isInternalNode_schedulerNode Party _).map _) + (((isInternalNode_schedulerNode Party _).inlTensor _).map _) + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _) + ((isInternalNode_schedulerNode Party _).inrTensor _) + (OpenNodeContext.preservesActivation_inrTensor Δ₁ _) + (OpenNodeContext.emitsAlong_inrTensor Δ₁ _) hσ (R.symm hfair) + +/-- Wiring is commutative up to sampler equivalence and boundary reshaping, +provided the scheduler is `R`-fair. -/ +theorem openTheory_wire_comm_sampler_equiv [Monad m] [LawfulMonad m] + (R : MonadRelFamily m) + (hfair : R.rel schedulerSampler (schedulerFlip <$> schedulerSampler)) + {Δ₁ Γ Δ₂ : PortBoundary} + (W₁ : OpenProcess.{u, v, w, w'} m Party (PortBoundary.tensor Δ₁ Γ)) + (W₂ : OpenProcess.{u, v, w, w'} m Party + (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)) : + OpenProcessSamplerEquiv R + ((openTheory Party m schedulerSampler).wire W₁ W₂) + (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorComm Δ₂ Δ₁).toHom + ((openTheory Party m schedulerSampler).wire + (OpenProcess.mapBoundary + (PortBoundary.Equiv.tensorComm (PortBoundary.swap Γ) Δ₂).toHom W₂) + (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorComm Δ₁ Γ).toHom W₁))) := by + simp only [openTheory] + rw [OpenProcess.mapBoundary_interleave] + simp only [OpenProcess.mapBoundary_eq_mapHom] + rw [OpenProcess.interleave_mapHom_left, OpenProcess.interleave_mapHom_right, + map_tensorComm_comp_wireLeft_comp_map_tensorComm, + map_tensorComm_comp_wireRight_comp_map_tensorComm] + exact interleave_comm_samplerEquiv R W₁ W₂ schedulerSampler schedulerSampler + (isInternalNode_schedulerNode Party _) ((isInternalNode_schedulerNode Party _).map _) + (R.symm hfair) + +/-! ## Sampler equivalence is a congruence for the theory + +Given the relation family is a congruence for the continuation of `bind` +(`MonadRelFamily.IsBindCongr`), each operation of `openTheory` preserves +sampler equivalence in each argument: every injection preserves activation and +relabels traces. -/ + +section Congruence + +variable [Monad m] [LawfulMonad m] (R : MonadRelFamily m) [R.IsBindCongr] + +open OpenNodeContext + +omit [LawfulMonad m] [R.IsBindCongr] in +theorem openTheory_map_congr_sampler_equiv {Δ₁ Δ₂ : PortBoundary} + (φ : PortBoundary.Hom Δ₁ Δ₂) {W W' : OpenProcess.{u, v, w, w'} m Party Δ₁} + (h : OpenProcessSamplerEquiv R W W') : + OpenProcessSamplerEquiv R + ((openTheory Party m schedulerSampler).map φ W) + ((openTheory Party m schedulerSampler).map φ W') := by + simp only [openTheory] + rw [OpenProcess.mapBoundary_eq_mapHom, OpenProcess.mapBoundary_eq_mapHom] + exact OpenProcess.mapHom_congr_samplerEquiv R (preservesActivation_map φ) (emitsAlong_map φ) h + +theorem openTheory_par_congr_left_sampler_equiv {Δ₁ Δ₂ : PortBoundary} + {W₁ W₁' : OpenProcess.{u, v, w, w'} m Party Δ₁} (W₂ : OpenProcess.{u, v, w, w'} m Party Δ₂) + (h : OpenProcessSamplerEquiv R W₁ W₁') : + OpenProcessSamplerEquiv R + ((openTheory Party m schedulerSampler).par W₁ W₂) + ((openTheory Party m schedulerSampler).par W₁' W₂) := by + simp only [openTheory] + exact OpenProcess.interleave_congr_left_samplerEquiv R W₁ W₂ + (preservesActivation_inlTensor Δ₁ Δ₂) (emitsAlong_inlTensor Δ₁ Δ₂) schedulerSampler h + +theorem openTheory_par_congr_right_sampler_equiv {Δ₁ Δ₂ : PortBoundary} + (W₁ : OpenProcess.{u, v, w, w'} m Party Δ₁) {W₂ W₂' : OpenProcess.{u, v, w, w'} m Party Δ₂} + (h : OpenProcessSamplerEquiv R W₂ W₂') : + OpenProcessSamplerEquiv R + ((openTheory Party m schedulerSampler).par W₁ W₂) + ((openTheory Party m schedulerSampler).par W₁ W₂') := by + simp only [openTheory] + exact OpenProcess.interleave_congr_right_samplerEquiv R W₁ W₂ + (preservesActivation_inrTensor Δ₁ Δ₂) (emitsAlong_inrTensor Δ₁ Δ₂) schedulerSampler h + +theorem openTheory_wire_congr_left_sampler_equiv {Δ₁ Γ Δ₂ : PortBoundary} + {W₁ W₁' : OpenProcess.{u, v, w, w'} m Party (PortBoundary.tensor Δ₁ Γ)} + (W₂ : OpenProcess.{u, v, w, w'} m Party (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)) + (h : OpenProcessSamplerEquiv R W₁ W₁') : + OpenProcessSamplerEquiv R + ((openTheory Party m schedulerSampler).wire W₁ W₂) + ((openTheory Party m schedulerSampler).wire W₁' W₂) := by + simp only [openTheory] + exact OpenProcess.interleave_congr_left_samplerEquiv R W₁ W₂ + (preservesActivation_wireLeft Δ₁ Γ Δ₂) (emitsAlong_wireLeft Δ₁ Γ Δ₂) schedulerSampler h + +theorem openTheory_wire_congr_right_sampler_equiv {Δ₁ Γ Δ₂ : PortBoundary} + (W₁ : OpenProcess.{u, v, w, w'} m Party (PortBoundary.tensor Δ₁ Γ)) + {W₂ W₂' : OpenProcess.{u, v, w, w'} m Party (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} + (h : OpenProcessSamplerEquiv R W₂ W₂') : + OpenProcessSamplerEquiv R + ((openTheory Party m schedulerSampler).wire W₁ W₂) + ((openTheory Party m schedulerSampler).wire W₁ W₂') := by + simp only [openTheory] + exact OpenProcess.interleave_congr_right_samplerEquiv R W₁ W₂ + (preservesActivation_wireRight Δ₁ Γ Δ₂) (emitsAlong_wireRight Δ₁ Γ Δ₂) schedulerSampler h + +theorem openTheory_plug_congr_left_sampler_equiv {Δ : PortBoundary} + {W W' : OpenProcess.{u, v, w, w'} m Party Δ} + (K : OpenProcess.{u, v, w, w'} m Party (PortBoundary.swap Δ)) + (h : OpenProcessSamplerEquiv R W W') : + OpenProcessSamplerEquiv R + ((openTheory Party m schedulerSampler).plug W K) + ((openTheory Party m schedulerSampler).plug W' K) := by + simp only [openTheory] + exact OpenProcess.interleave_congr_left_samplerEquiv R W K + (preservesActivation_close Δ) (emitsAlong_close Δ) schedulerSampler h + +theorem openTheory_plug_congr_right_sampler_equiv {Δ : PortBoundary} + (W : OpenProcess.{u, v, w, w'} m Party Δ) + {K K' : OpenProcess.{u, v, w, w'} m Party (PortBoundary.swap Δ)} + (h : OpenProcessSamplerEquiv R K K') : + OpenProcessSamplerEquiv R + ((openTheory Party m schedulerSampler).plug W K) + ((openTheory Party m schedulerSampler).plug W K') := by + simp only [openTheory] + exact OpenProcess.interleave_congr_right_samplerEquiv R W K + (preservesActivation_close _) (emitsAlong_close _) schedulerSampler h + +end Congruence end UC end Interaction diff --git a/PolyFun/Interaction/UC/ScheduledOpenProcessModel.lean b/PolyFun/Interaction/UC/ScheduledOpenProcessModel.lean index 58c37513..22ef4f0e 100644 --- a/PolyFun/Interaction/UC/ScheduledOpenProcessModel.lean +++ b/PolyFun/Interaction/UC/ScheduledOpenProcessModel.lean @@ -24,7 +24,9 @@ process APIs continue to apply. Unlike `openTheory`, however, the scheduler sampler at a composition node depends on the masses of both subtrees. `BinaryScheduler.IsFlat` is the scheduler contract needed by the separate sampler-factorization layer to prove that this choice is independent of how -composition is parenthesized. +composition is parenthesized. The theory is `IsLawful`: every naturality law +is the corresponding `openTheory` law at the scheduler draw for the component +masses, since boundary adaptation preserves mass. -/ public section @@ -200,5 +202,47 @@ instance lawfulMap_scheduledOpenTheory (Party : Type u) (m : Type w → Type w') · exact OpenTheory.IsLawfulMap.map_comp (T := openTheory Party m (scheduler mass mass)) g f process +/-- Parallel composition in the mass-aware theory is natural in boundary +adaptation: masses add on both sides, and the underlying process law is the +`openTheory` law at the scheduler draw for the two component masses. -/ +instance lawfulPar_scheduledOpenTheory (Party : Type u) (m : Type w → Type w') + (scheduler : BinaryScheduler m) : + OpenTheory.IsLawfulPar + (scheduledOpenTheory.{u, v, w, w'} Party m scheduler) where + __ := lawfulMap_scheduledOpenTheory Party m scheduler + map_par f₁ f₂ W₁ W₂ := by + apply ScheduledOpenProcess.ext + · rfl + · exact OpenTheory.IsLawfulPar.map_par + (T := openTheory Party m (scheduler W₁.mass W₂.mass)) f₁ f₂ W₁.process W₂.process + +/-- Wiring in the mass-aware theory is natural in the still-exposed outer +boundaries. -/ +instance lawfulWire_scheduledOpenTheory (Party : Type u) (m : Type w → Type w') + (scheduler : BinaryScheduler m) : + OpenTheory.IsLawfulWire + (scheduledOpenTheory.{u, v, w, w'} Party m scheduler) where + __ := lawfulMap_scheduledOpenTheory Party m scheduler + map_wire f₁ f₂ W₁ W₂ := by + apply ScheduledOpenProcess.ext + · rfl + · exact OpenTheory.IsLawfulWire.map_wire + (T := openTheory Party m (scheduler W₁.mass W₂.mass)) f₁ f₂ W₁.process W₂.process + +/-- Plugging in the mass-aware theory is natural in boundary adaptation. -/ +instance lawfulPlug_scheduledOpenTheory (Party : Type u) (m : Type w → Type w') + (scheduler : BinaryScheduler m) : + OpenTheory.IsLawfulPlug + (scheduledOpenTheory.{u, v, w, w'} Party m scheduler) where + __ := lawfulMap_scheduledOpenTheory Party m scheduler + map_plug f W K := by + apply ScheduledOpenProcess.ext + · rfl + · exact OpenTheory.IsLawfulPlug.map_plug + (T := openTheory Party m (scheduler W.mass K.mass)) f W.process K.process + +instance (Party : Type u) (m : Type w → Type w') (scheduler : BinaryScheduler m) : + OpenTheory.IsLawful (scheduledOpenTheory.{u, v, w, w'} Party m scheduler) where + end UC end Interaction diff --git a/PolyFun/Interaction/UC/ScheduledSamplerFactorization.lean b/PolyFun/Interaction/UC/ScheduledSamplerFactorization.lean index f8f3a429..b1b2b917 100644 --- a/PolyFun/Interaction/UC/ScheduledSamplerFactorization.lean +++ b/PolyFun/Interaction/UC/ScheduledSamplerFactorization.lean @@ -1,33 +1,44 @@ /- Copyright (c) 2026 PolyFun Contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Quang Dao +Authors: Quang Dao, Devon Tuma -/ module -import all PolyFun.Interaction.UC.OpenProcessSamplerFactorization -import all PolyFun.Interaction.UC.Scheduler +import all PolyFun.Interaction.UC.Emulates +import all PolyFun.Interaction.UC.OpenProcessSamplerEquiv +import all PolyFun.Interaction.UC.ScheduledOpenProcessModel public import PolyFun.Interaction.UC.OpenProcessSamplerFactorization +public import PolyFun.Interaction.UC.SamplerObservation public import PolyFun.Interaction.UC.Scheduler +public import PolyFun.Interaction.UC.ScheduledOpenProcessModel /-! # Path-sampler factorization for mass-aware scheduling The structural UC factorization maps already identify the leaves of the -source and reassociated binary process trees. This module proves the missing -sampler statement for the mass-aware scheduler: after applying those path -maps, both hierarchical samplers bind the same component sampler whenever the -binary scheduler satisfies `BinaryScheduler.IsCoherent`. - -This is the generic bridge between the scheduler algebra and process-level UC -factorization. It remains independent of probability; downstream models only -need to prove the scheduler coherence law for their observation relation. +source and reassociated binary process trees. This module proves the sampler +statements for the mass-aware scheduler: whenever the binary scheduler +satisfies `BinaryScheduler.IsCoherent`, the hierarchical draws of both sides of +a regrouping are related, so the generic shapes of `OpenProcessSamplerCoherence` +apply. + +Concretely, `BinaryScheduler.sourceDraw`, `leftDraw`, and `rightDraw` are the +nested draws `nestedDrawLeft`, `nestedDrawFactorLeft`, and +`nestedDrawFactorRight` at the scheduler calls a composition makes, so +`IsCoherent` supplies exactly the transport facts the shapes ask for. The +theory `scheduledOpenTheory` then satisfies plug commutation and the four plug +factorizations up to `OpenProcessSamplerEquiv R` on the underlying processes, +and `Observation.scheduledSampler` packages that as an observation respecting +factorization. Everything remains independent of probability; downstream +models only need to prove the scheduler coherence law for their observation +relation. -/ public section -universe w w' +universe u v w w' namespace Interaction namespace UC @@ -36,9 +47,56 @@ open Concurrent OpenProcessFactorization namespace BinaryScheduler +variable {m : Type w → Type w'} [Monad m] + +/-- The source-shaped mass-aware draw is the source nesting's draw at the two +scheduler calls of `plug (compose W₁ W₂) K`. -/ +theorem sourceDraw_eq_nestedDrawLeft (scheduler : BinaryScheduler m) + (first second context : ℕ+) : + sourceDraw scheduler first second context = + nestedDrawLeft (scheduler (first + second) context) (scheduler first second) := by + unfold sourceDraw nestedDrawLeft + refine congrArg (_ >>= ·) (funext fun outer => ?_) + obtain ⟨b⟩ := outer + cases b + · rfl + · refine congrArg (_ >>= ·) (funext fun inner => ?_) + obtain ⟨b'⟩ := inner + cases b' <;> rfl + +/-- The left-factored mass-aware draw is the left-factored nesting's draw at +the two scheduler calls of `plug W₁ (wire K W₂)`. -/ +theorem leftDraw_eq_nestedDrawFactorLeft (scheduler : BinaryScheduler m) + (first second context : ℕ+) : + leftDraw scheduler first second context = + nestedDrawFactorLeft (scheduler first (context + second)) (scheduler context second) := by + unfold leftDraw nestedDrawFactorLeft + refine congrArg (_ >>= ·) (funext fun outer => ?_) + obtain ⟨b⟩ := outer + cases b + · refine congrArg (_ >>= ·) (funext fun inner => ?_) + obtain ⟨b'⟩ := inner + cases b' <;> rfl + · rfl + +/-- The right-factored mass-aware draw is the right-factored nesting's draw at +the two scheduler calls of `plug W₂ (wire K W₁)`. -/ +theorem rightDraw_eq_nestedDrawFactorRight (scheduler : BinaryScheduler m) + (first second context : ℕ+) : + rightDraw scheduler first second context = + nestedDrawFactorRight (scheduler second (context + first)) (scheduler context first) := by + unfold rightDraw nestedDrawFactorRight + refine congrArg (_ >>= ·) (funext fun outer => ?_) + obtain ⟨b⟩ := outer + cases b + · refine congrArg (_ >>= ·) (funext fun inner => ?_) + obtain ⟨b'⟩ := inner + cases b' <;> rfl + · rfl + /-- Binding the source-shaped mass-aware draw against a continuation exposes the two scheduler calls used by the nested process sampler. -/ -theorem sourceDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] +theorem sourceDraw_bind [LawfulMonad m] (scheduler : BinaryScheduler m) (first second context : ℕ+) {α : Type w} (h : ULift.{w, 0} Leaf → m α) : sourceDraw scheduler first second context >>= h = @@ -60,7 +118,7 @@ theorem sourceDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] /-- Binding the left-factored mass-aware draw exposes the scheduler calls used by the left-reassociated process sampler. -/ -theorem leftDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] +theorem leftDraw_bind [LawfulMonad m] (scheduler : BinaryScheduler m) (first second context : ℕ+) {α : Type w} (h : ULift.{w, 0} Leaf → m α) : leftDraw scheduler first second context >>= h = @@ -82,7 +140,7 @@ theorem leftDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] /-- Binding the right-factored mass-aware draw exposes the scheduler calls used by the right-reassociated process sampler. -/ -theorem rightDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] +theorem rightDraw_bind [LawfulMonad m] (scheduler : BinaryScheduler m) (first second context : ℕ+) {α : Type w} (h : ULift.{w, 0} Leaf → m α) : rightDraw scheduler first second context >>= h = @@ -102,6 +160,36 @@ theorem rightDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] cases choice <;> simp only [Bool.false_eq_true, ↓reduceIte, pure_bind] · simp only [↓reduceIte, pure_bind] +/-! ### Coherence in the form the shapes consume -/ + +variable {R : MonadRelFamily m} {scheduler : BinaryScheduler m} + +/-- The flipped draw for two masses is related to the draw for the swapped +masses. -/ +theorem IsCoherent.flip_rel (h : IsCoherent R scheduler) (left right : ℕ+) : + R.rel (schedulerFlip <$> scheduler left right) (scheduler right left) := + R.symm (h.swap right left) + +/-- The source nesting's draw is related to the left-factored nesting's draw +at the scheduler calls of a left plug factorization. -/ +theorem IsCoherent.nestedDrawLeft_rel_factorLeft (h : IsCoherent R scheduler) + (first second context : ℕ+) : + R.rel (nestedDrawLeft (scheduler (first + second) context) (scheduler first second)) + (nestedDrawFactorLeft (scheduler first (context + second)) + (scheduler context second)) := by + rw [← sourceDraw_eq_nestedDrawLeft, ← leftDraw_eq_nestedDrawFactorLeft] + exact h.left first second context + +/-- The source nesting's draw is related to the right-factored nesting's draw +at the scheduler calls of a right plug factorization. -/ +theorem IsCoherent.nestedDrawLeft_rel_factorRight (h : IsCoherent R scheduler) + (first second context : ℕ+) : + R.rel (nestedDrawLeft (scheduler (first + second) context) (scheduler first second)) + (nestedDrawFactorRight (scheduler second (context + first)) + (scheduler context first)) := by + rw [← sourceDraw_eq_nestedDrawLeft, ← rightDraw_eq_nestedDrawFactorRight] + exact h.right first second context + end BinaryScheduler /-! ## Reassociated path samplers -/ @@ -128,68 +216,9 @@ theorem samplePath_interleave_assoc_left {m : Type w → Type w'} (TypeTree.Sampler.interleave (scheduler firstMass (contextMass + secondMass)) firstSampler (TypeTree.Sampler.interleave (scheduler contextMass secondMass) - contextSampler secondSampler))) := by - let continuation : ULift.{w, 0} Leaf → - m (TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => firstTree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => contextTree - | ⟨false⟩ => secondTree)) := fun leaf => - match leaf with - | ⟨.first⟩ => TypeTree.samplePath _ firstSampler >>= fun path => - pure ⟨⟨true⟩, path⟩ - | ⟨.second⟩ => TypeTree.samplePath _ secondSampler >>= fun path => - pure ⟨⟨false⟩, ⟨⟨false⟩, path⟩⟩ - | ⟨.context⟩ => TypeTree.samplePath _ contextSampler >>= fun path => - pure ⟨⟨false⟩, ⟨⟨true⟩, path⟩⟩ - have source_eq : - ((fun path => parLeftPathEquiv firstTree secondTree contextTree path) <$> - TypeTree.samplePath _ - (TypeTree.Sampler.interleave - (scheduler (firstMass + secondMass) contextMass) - (TypeTree.Sampler.interleave (scheduler firstMass secondMass) - firstSampler secondSampler) - contextSampler)) = - BinaryScheduler.sourceDraw scheduler firstMass secondMass contextMass >>= - continuation := by - rw [BinaryScheduler.sourceDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] - refine bind_congr fun outer => ?_ - obtain ⟨choice⟩ := outer - cases choice - · simp only [Bool.false_eq_true, ↓reduceIte, map_pure] - rfl - · simp only [↓reduceIte, TypeTree.samplePath, bind_assoc, map_pure, - pure_bind] - refine bind_congr fun inner => ?_ - obtain ⟨choice⟩ := inner - cases choice <;> rfl - have target_eq : - TypeTree.samplePath _ - (TypeTree.Sampler.interleave - (scheduler firstMass (contextMass + secondMass)) firstSampler - (TypeTree.Sampler.interleave (scheduler contextMass secondMass) - contextSampler secondSampler)) = - BinaryScheduler.leftDraw scheduler firstMass secondMass contextMass >>= - continuation := by - rw [BinaryScheduler.leftDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] - refine bind_congr fun outer => ?_ - obtain ⟨choice⟩ := outer - cases choice - · simp only [Bool.false_eq_true, ↓reduceIte, TypeTree.samplePath, bind_assoc, - pure_bind] - refine bind_congr fun inner => ?_ - obtain ⟨choice⟩ := inner - cases choice <;> rfl - · simp only [↓reduceIte] - rfl - have draws_related := R.bind_congr continuation - (coherent.left firstMass secondMass contextMass) - exact Eq.mp - (congrArg₂ (fun left right => R.rel left right) - source_eq.symm target_eq.symm) - draws_related + contextSampler secondSampler))) := + samplePath_factorLeft_rel firstSampler secondSampler contextSampler R + (coherent.nestedDrawLeft_rel_factorLeft firstMass secondMass contextMass) /-- The source-shaped and right-factored nested path samplers are related after applying the structural right-reassociation path equivalence. -/ @@ -213,68 +242,238 @@ theorem samplePath_interleave_assoc_right {m : Type w → Type w'} (TypeTree.Sampler.interleave (scheduler secondMass (contextMass + firstMass)) secondSampler (TypeTree.Sampler.interleave (scheduler contextMass firstMass) - contextSampler firstSampler))) := by - let continuation : ULift.{w, 0} Leaf → - m (TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => secondTree - | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun - | ⟨true⟩ => contextTree - | ⟨false⟩ => firstTree)) := fun leaf => - match leaf with - | ⟨.first⟩ => TypeTree.samplePath _ firstSampler >>= fun path => - pure ⟨⟨false⟩, ⟨⟨false⟩, path⟩⟩ - | ⟨.second⟩ => TypeTree.samplePath _ secondSampler >>= fun path => - pure ⟨⟨true⟩, path⟩ - | ⟨.context⟩ => TypeTree.samplePath _ contextSampler >>= fun path => - pure ⟨⟨false⟩, ⟨⟨true⟩, path⟩⟩ - have source_eq : - ((fun path => parRightPathEquiv firstTree secondTree contextTree path) <$> - TypeTree.samplePath _ - (TypeTree.Sampler.interleave - (scheduler (firstMass + secondMass) contextMass) - (TypeTree.Sampler.interleave (scheduler firstMass secondMass) - firstSampler secondSampler) - contextSampler)) = - BinaryScheduler.sourceDraw scheduler firstMass secondMass contextMass >>= - continuation := by - rw [BinaryScheduler.sourceDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] - refine bind_congr fun outer => ?_ - obtain ⟨choice⟩ := outer - cases choice - · simp only [Bool.false_eq_true, ↓reduceIte, map_pure] - rfl - · simp only [↓reduceIte, TypeTree.samplePath, bind_assoc, map_pure, - pure_bind] - refine bind_congr fun inner => ?_ - obtain ⟨choice⟩ := inner - cases choice <;> rfl - have target_eq : - TypeTree.samplePath _ - (TypeTree.Sampler.interleave - (scheduler secondMass (contextMass + firstMass)) secondSampler - (TypeTree.Sampler.interleave (scheduler contextMass firstMass) - contextSampler firstSampler)) = - BinaryScheduler.rightDraw scheduler firstMass secondMass contextMass >>= - continuation := by - rw [BinaryScheduler.rightDraw_bind] - simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] - refine bind_congr fun outer => ?_ - obtain ⟨choice⟩ := outer - cases choice - · simp only [Bool.false_eq_true, ↓reduceIte, TypeTree.samplePath, bind_assoc, - pure_bind] - refine bind_congr fun inner => ?_ - obtain ⟨choice⟩ := inner - cases choice <;> rfl - · simp only [↓reduceIte] - rfl - have draws_related := R.bind_congr continuation - (coherent.right firstMass secondMass contextMass) - exact Eq.mp - (congrArg₂ (fun left right => R.rel left right) - source_eq.symm target_eq.symm) - draws_related + contextSampler firstSampler))) := + samplePath_factorRight_rel firstSampler secondSampler contextSampler R + (coherent.nestedDrawLeft_rel_factorRight firstMass secondMass contextMass) + +/-! ## Sampler-aware laws of the mass-aware theory -/ + +section ScheduledLaws + +variable (Party : Type u) (m : Type w → Type w') [Monad m] [LawfulMonad m] + (scheduler : BinaryScheduler m) (R : MonadRelFamily m) + +/-- `plug` is commutative in the mass-aware theory up to sampler equivalence +of the underlying processes, under a coherent scheduler. -/ +theorem scheduledOpenTheory_plug_comm_sampler_equiv (coherent : scheduler.IsCoherent R) + {Δ : PortBoundary} + (W : ScheduledOpenProcess.{u, v, w, w'} m Party Δ) + (K : ScheduledOpenProcess.{u, v, w, w'} m Party (PortBoundary.swap Δ)) : + OpenProcessSamplerEquiv R + ((scheduledOpenTheory Party m scheduler).plug W K).process + ((scheduledOpenTheory Party m scheduler).plug K W).process := by + simp only [scheduledOpenTheory, ScheduledOpenProcess.process_interleave] + exact interleave_comm_samplerEquiv R W.process K.process _ _ + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _) + (coherent.flip_rel _ _) + +/-- Closing a parallel composition factors through its left component in the +mass-aware theory, up to sampler equivalence of the underlying processes, +under a coherent scheduler. -/ +theorem scheduledOpenTheory_plug_par_left_sampler_equiv (coherent : scheduler.IsCoherent R) + {Δ₁ Δ₂ : PortBoundary} + (W₁ : ScheduledOpenProcess.{u, v, w, w'} m Party Δ₁) + (W₂ : ScheduledOpenProcess.{u, v, w, w'} m Party Δ₂) + (K : ScheduledOpenProcess.{u, v, w, w'} m Party + (PortBoundary.swap (PortBoundary.tensor Δ₁ Δ₂))) : + OpenProcessSamplerEquiv R + ((scheduledOpenTheory Party m scheduler).plug + ((scheduledOpenTheory Party m scheduler).par W₁ W₂) K).process + ((scheduledOpenTheory Party m scheduler).plug W₁ + ((scheduledOpenTheory Party m scheduler).map + (PortBoundary.Equiv.tensorEmptyRight (PortBoundary.swap Δ₁)).toHom + ((scheduledOpenTheory Party m scheduler).wire + (Γ := PortBoundary.swap Δ₂) + (Δ₂ := PortBoundary.empty) + K + ((scheduledOpenTheory Party m scheduler).map + (PortBoundary.Equiv.tensorEmptyRight Δ₂).symm.toHom W₂)))).process := by + simp only [scheduledOpenTheory, ScheduledOpenProcess.process_interleave, + ScheduledOpenProcess.process_mapBoundary, ScheduledOpenProcess.mass_interleave, + ScheduledOpenProcess.mass_mapBoundary] + rw [OpenProcess.mapBoundary_interleave, OpenProcess.mapBoundary_eq_mapHom, + OpenProcess.interleave_mapHom_right] + exact interleave_factorLeft_samplerEquiv R W₁.process W₂.process K.process _ _ _ _ + (close_comp_inlTensor Party Δ₁ Δ₂) + ((close_comp_inrTensor Party Δ₁ Δ₂).trans + (close_comp_map_comp_wireRight_comp_map Party (Δ₁ := PortBoundary.swap Δ₁) + (Γ := PortBoundary.swap Δ₂) (Δ₂ := PortBoundary.empty) _ _).symm) + (close_comp_map_comp_wireLeft Party (Δ₁ := PortBoundary.swap Δ₁) (Γ := PortBoundary.swap Δ₂) + (Δ₂ := PortBoundary.empty) _).symm + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _).close + (isInternalNode_schedulerNode Party _) + ((isInternalNode_schedulerNode Party _).map _).close + (coherent.nestedDrawLeft_rel_factorLeft _ _ _) + +/-- Closing a wired composition factors through its left factor in the +mass-aware theory, up to sampler equivalence of the underlying processes, +under a coherent scheduler. -/ +theorem scheduledOpenTheory_plug_wire_left_sampler_equiv (coherent : scheduler.IsCoherent R) + {Δ₁ Γ Δ₂ : PortBoundary} + (W₁ : ScheduledOpenProcess.{u, v, w, w'} m Party (PortBoundary.tensor Δ₁ Γ)) + (W₂ : ScheduledOpenProcess.{u, v, w, w'} m Party + (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)) + (K : ScheduledOpenProcess.{u, v, w, w'} m Party + (PortBoundary.swap (PortBoundary.tensor Δ₁ Δ₂))) : + OpenProcessSamplerEquiv R + ((scheduledOpenTheory Party m scheduler).plug + ((scheduledOpenTheory Party m scheduler).wire W₁ W₂) K).process + ((scheduledOpenTheory Party m scheduler).plug W₁ + ((scheduledOpenTheory Party m scheduler).wire + (Δ₁ := PortBoundary.swap Δ₁) + (Γ := PortBoundary.swap Δ₂) + (Δ₂ := PortBoundary.swap Γ) + K + ((scheduledOpenTheory Party m scheduler).map + (PortBoundary.Equiv.tensorComm (PortBoundary.swap Γ) Δ₂).toHom W₂))).process := by + simp only [scheduledOpenTheory, ScheduledOpenProcess.process_interleave, + ScheduledOpenProcess.process_mapBoundary, ScheduledOpenProcess.mass_interleave, + ScheduledOpenProcess.mass_mapBoundary] + rw [OpenProcess.mapBoundary_eq_mapHom, OpenProcess.interleave_mapHom_right] + exact interleave_factorLeft_samplerEquiv R W₁.process W₂.process K.process _ _ _ _ + (close_comp_wireLeft Party Δ₁ Γ Δ₂) + ((close_comp_wireRight Party Δ₁ Γ Δ₂).trans + (close_comp_wireRight_comp_map Party (Δ₁ := PortBoundary.swap Δ₁) + (Γ := PortBoundary.swap Δ₂) (Δ₂ := PortBoundary.swap Γ) _).symm) + (close_comp_wireLeft Party (PortBoundary.swap Δ₁) (PortBoundary.swap Δ₂) + (PortBoundary.swap Γ)).symm + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _).close + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _).close + (coherent.nestedDrawLeft_rel_factorLeft _ _ _) + +/-- Closing a parallel composition factors through its right component in the +mass-aware theory, up to sampler equivalence of the underlying processes, +under a coherent scheduler. -/ +theorem scheduledOpenTheory_plug_par_right_sampler_equiv (coherent : scheduler.IsCoherent R) + {Δ₁ Δ₂ : PortBoundary} + (W₁ : ScheduledOpenProcess.{u, v, w, w'} m Party Δ₁) + (W₂ : ScheduledOpenProcess.{u, v, w, w'} m Party Δ₂) + (K : ScheduledOpenProcess.{u, v, w, w'} m Party + (PortBoundary.swap (PortBoundary.tensor Δ₁ Δ₂))) : + OpenProcessSamplerEquiv R + ((scheduledOpenTheory Party m scheduler).plug + ((scheduledOpenTheory Party m scheduler).par W₁ W₂) K).process + ((scheduledOpenTheory Party m scheduler).plug W₂ + ((scheduledOpenTheory Party m scheduler).map + (PortBoundary.Equiv.tensorEmptyRight (PortBoundary.swap Δ₂)).toHom + ((scheduledOpenTheory Party m scheduler).wire + (Γ := PortBoundary.swap Δ₁) + (Δ₂ := PortBoundary.empty) + ((scheduledOpenTheory Party m scheduler).map + (PortBoundary.Equiv.tensorComm + (PortBoundary.swap Δ₁) (PortBoundary.swap Δ₂)).toHom K) + ((scheduledOpenTheory Party m scheduler).map + (PortBoundary.Equiv.tensorEmptyRight Δ₁).symm.toHom W₁)))).process := by + simp only [scheduledOpenTheory, ScheduledOpenProcess.process_interleave, + ScheduledOpenProcess.process_mapBoundary, ScheduledOpenProcess.mass_interleave, + ScheduledOpenProcess.mass_mapBoundary] + rw [OpenProcess.mapBoundary_interleave] + simp only [OpenProcess.mapBoundary_eq_mapHom] + rw [OpenProcess.interleave_mapHom_left, OpenProcess.interleave_mapHom_right] + exact interleave_factorRight_samplerEquiv R W₁.process W₂.process K.process _ _ _ _ + ((close_comp_inlTensor Party Δ₁ Δ₂).trans + (close_comp_map_comp_wireRight_comp_map Party (Δ₁ := PortBoundary.swap Δ₂) + (Γ := PortBoundary.swap Δ₁) (Δ₂ := PortBoundary.empty) _ _).symm) + (close_comp_inrTensor Party Δ₁ Δ₂) + (close_comp_map_comp_wireLeft_comp_map Party (Δ₁ := PortBoundary.swap Δ₂) + (Γ := PortBoundary.swap Δ₁) (Δ₂ := PortBoundary.empty) + (Δ' := PortBoundary.swap (PortBoundary.tensor Δ₁ Δ₂)) _ _).symm + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _).close + (isInternalNode_schedulerNode Party _) + ((isInternalNode_schedulerNode Party _).map _).close + (coherent.nestedDrawLeft_rel_factorRight _ _ _) + +/-- Closing a wired composition factors through its right factor in the +mass-aware theory, up to sampler equivalence of the underlying processes, +under a coherent scheduler. -/ +theorem scheduledOpenTheory_plug_wire_right_sampler_equiv (coherent : scheduler.IsCoherent R) + {Δ₁ Γ Δ₂ : PortBoundary} + (W₁ : ScheduledOpenProcess.{u, v, w, w'} m Party (PortBoundary.tensor Δ₁ Γ)) + (W₂ : ScheduledOpenProcess.{u, v, w, w'} m Party + (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)) + (K : ScheduledOpenProcess.{u, v, w, w'} m Party + (PortBoundary.swap (PortBoundary.tensor Δ₁ Δ₂))) : + OpenProcessSamplerEquiv R + ((scheduledOpenTheory Party m scheduler).plug + ((scheduledOpenTheory Party m scheduler).wire W₁ W₂) K).process + ((scheduledOpenTheory Party m scheduler).plug W₂ + ((scheduledOpenTheory Party m scheduler).map + (PortBoundary.Equiv.tensorComm (PortBoundary.swap Δ₂) Γ).toHom + ((scheduledOpenTheory Party m scheduler).wire + (Δ₁ := PortBoundary.swap Δ₂) + (Γ := PortBoundary.swap Δ₁) + (Δ₂ := Γ) + ((scheduledOpenTheory Party m scheduler).map + (PortBoundary.Equiv.tensorComm + (PortBoundary.swap Δ₁) (PortBoundary.swap Δ₂)).toHom K) + W₁))).process := by + simp only [scheduledOpenTheory, ScheduledOpenProcess.process_interleave, + ScheduledOpenProcess.process_mapBoundary, ScheduledOpenProcess.mass_interleave, + ScheduledOpenProcess.mass_mapBoundary] + rw [OpenProcess.mapBoundary_interleave, OpenProcess.mapBoundary_eq_mapHom, + OpenProcess.interleave_mapHom_left] + exact interleave_factorRight_samplerEquiv R W₁.process W₂.process K.process _ _ _ _ + ((close_comp_wireLeft Party Δ₁ Γ Δ₂).trans + (close_comp_map_comp_wireRight Party (Δ₁ := PortBoundary.swap Δ₂) + (Γ := PortBoundary.swap Δ₁) (Δ₂ := Γ) _).symm) + (close_comp_wireRight Party Δ₁ Γ Δ₂) + (close_comp_map_comp_wireLeft_comp_map Party (Δ₁ := PortBoundary.swap Δ₂) + (Γ := PortBoundary.swap Δ₁) (Δ₂ := Γ) + (Δ' := PortBoundary.swap (PortBoundary.tensor Δ₁ Δ₂)) _ _).symm + (isInternalNode_schedulerNode Party _) (isInternalNode_schedulerNode Party _).close + (isInternalNode_schedulerNode Party _) + ((isInternalNode_schedulerNode Party _).map _).close + (coherent.nestedDrawLeft_rel_factorRight _ _ _) + +/-! ### The scheduled sampler observation -/ + +/-- Sampler equivalence of the underlying processes, as an observation on the +mass-aware theory. -/ +def Observation.scheduledSampler : + Observation (scheduledOpenTheory.{u, v, w, w'} Party m scheduler) where + rel c₁ c₂ := OpenProcessSamplerEquiv R c₁.process c₂.process + equiv := + ⟨fun c => OpenProcessSamplerEquiv.refl c.process, + OpenProcessSamplerEquiv.symm, + OpenProcessSamplerEquiv.trans⟩ + +@[simp] +theorem Observation.scheduledSampler_rel + {c₁ c₂ : (scheduledOpenTheory.{u, v, w, w'} Party m scheduler).Closed} : + (Observation.scheduledSampler Party m scheduler R).rel c₁ c₂ ↔ + OpenProcessSamplerEquiv R c₁.process c₂.process := + Iff.rfl + +/-- Under a coherent scheduler, any observation on the mass-aware theory that +cannot distinguish sampler-equivalent underlying processes respects plug +commutation and factorization. -/ +theorem Observation.respectsFactorization_of_scheduledSamplerInvariant + (coherent : scheduler.IsCoherent R) + {Obs : Observation (scheduledOpenTheory.{u, v, w, w'} Party m scheduler)} + (hInv : ∀ {c₁ c₂ : (scheduledOpenTheory.{u, v, w, w'} Party m scheduler).Closed}, + OpenProcessSamplerEquiv R c₁.process c₂.process → Obs.rel c₁ c₂) : + Obs.RespectsFactorization where + plug_comm W K := hInv + (scheduledOpenTheory_plug_comm_sampler_equiv Party m scheduler R coherent W K) + close_par_left W₁ W₂ K := hInv + (scheduledOpenTheory_plug_par_left_sampler_equiv Party m scheduler R coherent W₁ W₂ K) + close_par_right W₁ W₂ K := hInv + (scheduledOpenTheory_plug_par_right_sampler_equiv Party m scheduler R coherent W₁ W₂ K) + close_wire_left W₁ W₂ K := hInv + (scheduledOpenTheory_plug_wire_left_sampler_equiv Party m scheduler R coherent W₁ W₂ K) + close_wire_right W₁ W₂ K := hInv + (scheduledOpenTheory_plug_wire_right_sampler_equiv Party m scheduler R coherent W₁ W₂ K) + +/-- The scheduled sampler observation respects plug commutation and +factorization under a coherent scheduler. Unlike the shared-sampler theory, no +further transport hypothesis is needed: coherence of the scheduler is the +whole obligation. -/ +theorem Observation.respectsFactorization_scheduledSampler (coherent : scheduler.IsCoherent R) : + (Observation.scheduledSampler.{u, v, w, w'} Party m scheduler R).RespectsFactorization := + Observation.respectsFactorization_of_scheduledSamplerInvariant Party m scheduler R coherent + fun h => h + +end ScheduledLaws end UC end Interaction diff --git a/PolyFun/PFunctor/Trace.lean b/PolyFun/PFunctor/Trace.lean index 0549b136..d2e73796 100644 --- a/PolyFun/PFunctor/Trace.lean +++ b/PolyFun/PFunctor/Trace.lean @@ -176,6 +176,24 @@ theorem getAt?_append_self_occurrences {P : PFunctor.{uA, uB}} [DecidableEq P.A] simpa [occurrences] using ih · simpa [occurrences, h] using ih +/-- Relabel-and-filter the events of a trace list along a partial map of +indices: `List.filterMap` with the monoid structure of `TraceList` made +explicit. `Trace.mapPartial` is this operation pointwise. -/ +def mapPartial {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} + (f : Idx P → Option (Idx Q)) (t : TraceList P) : TraceList Q := + List.filterMap f t + +@[simp] theorem mapPartial_one {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} + (f : Idx P → Option (Idx Q)) : mapPartial f (1 : TraceList P) = 1 := + rfl + +theorem mapPartial_mul {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} + (f : Idx P → Option (Idx Q)) (a b : TraceList P) : + mapPartial f (a * b) = mapPartial f a * mapPartial f b := by + change List.filterMap f (FreeMonoid.toList a ++ FreeMonoid.toList b) = + List.filterMap f a ++ List.filterMap f b + exact List.filterMap_append + end TraceList /-- diff --git a/PolyFunTest/Interaction/UC/SamplerCoherenceExamples.lean b/PolyFunTest/Interaction/UC/SamplerCoherenceExamples.lean new file mode 100644 index 00000000..ac5a7b9c --- /dev/null +++ b/PolyFunTest/Interaction/UC/SamplerCoherenceExamples.lean @@ -0,0 +1,115 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ + +module + +public import PolyFun.Interaction.UC.ScheduledSamplerFactorization + +/-! +# Sampler-coherence examples + +Regression checks for the sampler-level coherence shapes and their two +instances: the shared-sampler theory `openTheory`, whose laws are conditional +on scheduler-transport facts, and the mass-aware theory `scheduledOpenTheory`, +whose laws follow from `BinaryScheduler.IsCoherent` alone. At +`MonadRelFamily.top` every hypothesis is trivial, so both sampler observations +respect factorization outright and the whole `Emulates` composition suite +applies. Sampler equivalence is also a congruence for the theory once the +relation family is bind-congruent, which the exact and forgetful families are. +-/ + +@[expose] public section + +universe u v w w' + +namespace Interaction.UC.SamplerCoherenceExamples + +open OpenProcessFactorization + +variable {Party : Type u} {m : Type w → Type w'} [Monad m] [LawfulMonad m] + {schedulerSampler : m (ULift.{w, 0} Bool)} {scheduler : BinaryScheduler m} + +/-- The exact and forgetful relation families are bind-congruent. -/ +example : (MonadRelFamily.eq m).IsBindCongr := inferInstance +example : (MonadRelFamily.top m).IsBindCongr := inferInstance + +omit [LawfulMonad m] in +/-- Every scheduler is coherent for the forgetful relation family. -/ +theorem isCoherent_top : scheduler.IsCoherent (MonadRelFamily.top m) where + swap _ _ := MonadRelFamily.top_rel _ _ + left _ _ _ := MonadRelFamily.top_rel _ _ + right _ _ _ := MonadRelFamily.top_rel _ _ + +/-- The mass-aware sampler observation respects factorization at the forgetful +relation family, with no transport hypothesis. -/ +example : + (Observation.scheduledSampler.{u, v, w, w'} Party m scheduler + (MonadRelFamily.top m)).RespectsFactorization := + Observation.respectsFactorization_scheduledSampler Party m scheduler + (MonadRelFamily.top m) isCoherent_top + +/-- The composition suite applies to the mass-aware theory: it is lawful, and +its sampler observation respects factorization under a coherent scheduler. -/ +example {Δ₁ Δ₂ : PortBoundary} + {real₁ ideal₁ : (scheduledOpenTheory.{u, v, w, w'} Party m scheduler).Obj Δ₁} + {real₂ ideal₂ : (scheduledOpenTheory.{u, v, w, w'} Party m scheduler).Obj Δ₂} + (h₁ : Emulates real₁ ideal₁ + (Observation.scheduledSampler Party m scheduler (MonadRelFamily.top m))) + (h₂ : Emulates real₂ ideal₂ + (Observation.scheduledSampler Party m scheduler (MonadRelFamily.top m))) : + Emulates ((scheduledOpenTheory Party m scheduler).par real₁ real₂) + ((scheduledOpenTheory Party m scheduler).par ideal₁ ideal₂) + (Observation.scheduledSampler Party m scheduler (MonadRelFamily.top m)) := + letI := Observation.respectsFactorization_scheduledSampler Party m scheduler + (MonadRelFamily.top m) isCoherent_top + Emulates.par_compose h₁ h₂ + +/-- Sampler equivalence of a component lifts through any closing context: the +congruence laws chain along the structure of the composite. -/ +example (R : MonadRelFamily m) [R.IsBindCongr] {Δ₁ Δ₂ : PortBoundary} + {real ideal : OpenProcess.{u, v, w, w'} m Party Δ₁} + (W : OpenProcess.{u, v, w, w'} m Party Δ₂) + (K : OpenProcess.{u, v, w, w'} m Party (PortBoundary.swap (PortBoundary.tensor Δ₁ Δ₂))) + (h : OpenProcessSamplerEquiv R real ideal) : + OpenProcessSamplerEquiv R + ((openTheory Party m schedulerSampler).plug + ((openTheory Party m schedulerSampler).par real W) K) + ((openTheory Party m schedulerSampler).plug + ((openTheory Party m schedulerSampler).par ideal W) K) := + openTheory_plug_congr_left_sampler_equiv Party m schedulerSampler R K + (openTheory_par_congr_left_sampler_equiv Party m schedulerSampler R W h) + +/-- At the forgetful relation family the monoidal laws of the shared-sampler +theory hold up to sampler equivalence outright: fairness, the transport fact, +and bind-congruence are all trivial. -/ +example {Δ₁ Δ₂ Δ₃ : PortBoundary} + (W₁ : OpenProcess.{u, v, w, w'} m Party Δ₁) (W₂ : OpenProcess.{u, v, w, w'} m Party Δ₂) + (W₃ : OpenProcess.{u, v, w, w'} m Party Δ₃) : + OpenProcessSamplerEquiv (MonadRelFamily.top m) + (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom + ((openTheory Party m schedulerSampler).par + ((openTheory Party m schedulerSampler).par W₁ W₂) W₃)) + ((openTheory Party m schedulerSampler).par W₁ + ((openTheory Party m schedulerSampler).par W₂ W₃)) := + openTheory_par_assoc_sampler_equiv Party m schedulerSampler (MonadRelFamily.top m) + (MonadRelFamily.top_rel _ _) (MonadRelFamily.top_rel _ _) W₁ W₂ W₃ + +example {Δ₁ Δ₂ : PortBoundary} + (W₁ : OpenProcess.{u, v, w, w'} m Party Δ₁) (W₂ : OpenProcess.{u, v, w, w'} m Party Δ₂) : + OpenProcessSamplerEquiv (MonadRelFamily.top m) + (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorComm Δ₁ Δ₂).toHom + ((openTheory Party m schedulerSampler).par W₁ W₂)) + ((openTheory Party m schedulerSampler).par W₂ W₁) := + openTheory_par_comm_sampler_equiv Party m schedulerSampler (MonadRelFamily.top m) + (MonadRelFamily.top_rel _ _) W₁ W₂ + +/-- The shared-sampler plug factorization is the mass-aware one at constant +mass: the hierarchical draws coincide, so the transport facts do. -/ +example (σ : m (ULift.{w, 0} Bool)) : + BinaryScheduler.sourceDraw (fun _ _ => σ) 1 1 1 = sourceDraw σ := + BinaryScheduler.sourceDraw_eq_nestedDrawLeft (fun _ _ => σ) 1 1 1 + +end Interaction.UC.SamplerCoherenceExamples diff --git a/PolyFunTest/ModuleAPI/Interaction.lean b/PolyFunTest/ModuleAPI/Interaction.lean index c0f6bfed..53447ffe 100644 --- a/PolyFunTest/ModuleAPI/Interaction.lean +++ b/PolyFunTest/ModuleAPI/Interaction.lean @@ -15,6 +15,7 @@ import PolyFun.Interaction.UC.OpenProcessCoherence import PolyFun.Interaction.UC.OpenTheory.PlugFactorization import PolyFun.Interaction.UC.ScheduledOpenProcessModel import PolyFun.Interaction.UC.ScheduledSamplerFactorization +import PolyFun.Interaction.UC.OpenProcessSamplerCoherence /-! # Ordinary-import canaries for the interaction API @@ -189,6 +190,55 @@ example {m : Type → Type} {Party : Type} (σ : m (ULift Bool)) {Δ₁ Δ₂ Γ ((UC.openTheory Party m σ).par W₁ ((UC.openTheory Party m σ).wire W₂ W₃))) := UC.openTheory_wire_par_superpose_activation_equiv Party m σ W₁ W₂ W₃ +/-! ## Sampler-level coherence -/ + +example {m : Type → Type} [Monad m] [LawfulMonad m] (σOut σIn : m (ULift Bool)) {α : Type} + (h : ULift UC.OpenProcessFactorization.Leaf → m α) : + UC.nestedDrawLeft σOut σIn >>= h = + σOut >>= fun + | ⟨true⟩ => σIn >>= fun + | ⟨true⟩ => h ⟨.first⟩ + | ⟨false⟩ => h ⟨.second⟩ + | ⟨false⟩ => h ⟨.context⟩ := + UC.nestedDrawLeft_bind σOut σIn h + +example {m : Type → Type} [Monad m] (R : UC.MonadRelFamily m) [R.IsBindCongr] {α β : Type} + (x : m α) {f g : α → m β} (h : ∀ a, R.rel (f a) (g a)) : + R.rel (x >>= f) (x >>= g) := + R.bind_congr_right x h + +example {m : Type → Type} [Monad m] [LawfulMonad m] {Party : Type} {Δ₁ Δ₂ Δ : UC.PortBoundary} + (R : UC.MonadRelFamily m) + (p₁ : UC.OpenProcess m Party Δ₁) (p₂ : UC.OpenProcess m Party Δ₂) + {f₁ : TypeTree.Node.ContextHom (UC.OpenNodeContext Party Δ₁) (UC.OpenNodeContext Party Δ)} + {f₂ : TypeTree.Node.ContextHom (UC.OpenNodeContext Party Δ₂) (UC.OpenNodeContext Party Δ)} + {c : UC.OpenNodeContext Party Δ (ULift Bool)} (σ : m (ULift Bool)) + {d : UC.OpenNodeContext Party Δ (ULift Bool)} (τ : m (ULift Bool)) + (hc : UC.OpenNodeContext.IsInternalNode c) (hd : UC.OpenNodeContext.IsInternalNode d) + (hστ : R.rel (UC.schedulerFlip <$> σ) τ) : + UC.OpenProcessSamplerEquiv R (p₁.interleave p₂ f₁ f₂ c σ) (p₂.interleave p₁ f₂ f₁ d τ) := + UC.interleave_comm_samplerEquiv R p₁ p₂ σ τ hc hd hστ + +example {m : Type → Type} [Monad m] [LawfulMonad m] {Party : Type} + (scheduler : UC.BinaryScheduler m) (R : UC.MonadRelFamily m) + (coherent : scheduler.IsCoherent R) : + (UC.Observation.scheduledSampler Party m scheduler R).RespectsFactorization := + UC.Observation.respectsFactorization_scheduledSampler Party m scheduler R coherent + +example {m : Type → Type} [Monad m] [LawfulMonad m] {Party : Type} (σ : m (ULift Bool)) + (R : UC.MonadRelFamily m) (hfair : R.rel σ (UC.schedulerFlip <$> σ)) + {Δ₁ Γ Δ₂ : UC.PortBoundary} + (W₁ : UC.OpenProcess m Party (UC.PortBoundary.tensor Δ₁ Γ)) + (W₂ : UC.OpenProcess m Party (UC.PortBoundary.tensor (UC.PortBoundary.swap Γ) Δ₂)) : + UC.OpenProcessSamplerEquiv R + ((UC.openTheory Party m σ).wire W₁ W₂) + (UC.OpenProcess.mapBoundary (UC.PortBoundary.Equiv.tensorComm Δ₂ Δ₁).toHom + ((UC.openTheory Party m σ).wire + (UC.OpenProcess.mapBoundary + (UC.PortBoundary.Equiv.tensorComm (UC.PortBoundary.swap Γ) Δ₂).toHom W₂) + (UC.OpenProcess.mapBoundary (UC.PortBoundary.Equiv.tensorComm Δ₁ Γ).toHom W₁))) := + UC.openTheory_wire_comm_sampler_equiv Party m σ R hfair W₁ W₂ + /-! ## Plug factorization laws -/ example {T : UC.OpenTheory} [UC.OpenTheory.HasPlugFactorization T] diff --git a/docs/reading/uc-complexity-roadmap.md b/docs/reading/uc-complexity-roadmap.md index 5433140a..a5e8e5b5 100644 --- a/docs/reading/uc-complexity-roadmap.md +++ b/docs/reading/uc-complexity-roadmap.md @@ -127,7 +127,10 @@ computation equality, and generally equality of distributions for the current binary scheduler, does not satisfy all reassociation facts. A distributional VCVio observation obtains `RespectsFactorization` only after choosing scheduler semantics or a coarser relation that proves the three transport facts, plus its -sampler-equivalence invariance (adequacy); see `docs/wiki/uc.md`. +sampler-equivalence invariance (adequacy); see `docs/wiki/uc.md`. With the +mass-aware `scheduledOpenTheory` (now `IsLawful`) the transport facts collapse +to `BinaryScheduler.IsCoherent`, and `ScheduledSamplerFactorization` supplies +the five plug laws and `Observation.scheduledSampler` from coherence alone. The remaining concrete steps are `PPTProcessWitness` and `pptSubTheory`. diff --git a/docs/wiki/gotchas.md b/docs/wiki/gotchas.md index 2debd431..1d4135d6 100644 --- a/docs/wiki/gotchas.md +++ b/docs/wiki/gotchas.md @@ -157,6 +157,24 @@ the documented API, expose that predicate narrowly and add an ordinary-import canary for the exact spelling, as in [`PolyFunTest/ModuleAPI/Interaction.lean`](../../PolyFunTest/ModuleAPI/Interaction.lean). +### 8g. Pattern-matching lambdas in statements are declaration-local + +A `fun | ⟨true⟩ => t₁ | ⟨false⟩ => t₂` inside a theorem statement elaborates to +an auxiliary matcher constant owned by that declaration. Two statements that +spell the same tree this way are definitionally but not syntactically equal, so +`rw` and `simp` with one lemma fail on the other's goal while `exact` succeeds. +Name the shape once (`nestedLeftTree`, `factorLeftTree` in +`OpenProcessSamplerCoherence`) and state every lemma with the abbreviation, or +close the gap with `exact`/`change` inside the consuming proof. The same +applies to `IsSilentStep`/`boundaryTrace` goals about composite steps: rewrite +them with the branch lemmas (`isSilentStep_interleave_left_iff_decoration`, +`boundaryTrace_interleave_left`) rather than unfolding `interleave` in place. + +Exported theorems cannot close goals by `rfl` through a non-exposed `def`, even +in the defining module and even under `import all`: state the fact as an +equation lemma of the def, or expose the def when it is data meant to compute +(the path re-encodings and nested draws are `@[expose]` for this reason). + ## Proof Patterns ### 8b. Keep one canonical concrete-step relation type diff --git a/docs/wiki/interaction.md b/docs/wiki/interaction.md index 3d0f1eb1..b0f26411 100644 --- a/docs/wiki/interaction.md +++ b/docs/wiki/interaction.md @@ -681,12 +681,12 @@ import PolyFun.Interaction.UC.OpenProcessModel | `OpenSyntax/Interp.lean` | `Interp` (tagless-final), granular `HasUnit` / `HasIdWire` / `IsMonoidal` / `IsTraced` / `IsCompactClosed` / `HasPlugWireFactor` instances | | `OpenSyntax/Expr.lean` | `Expr` (quotient of `Raw`), granular `OpenTheory` lawfulness instances, `Expr.toInterp` | | `OpenProcess.lean` | `BoundaryAction`, `OpenNodeProfile`, `OpenNodeContext` (with polynomial-product bridge `productView` and structural `boundaryTrace`), `OpenProcess m Party Δ` (monad-parametric, with intrinsic `stepSampler`), `toProcess`, `OpenProcessActivationEquiv` | -| `OpenProcessInterleave.lean` | `OpenProcess.mapHom` (re-decoration along any node-context hom; `mapBoundary` is the boundary-morphism case), `OpenNodeContext.PreservesActivation` with instances for every structural hom, `isSilentStep_mapHom_iff`, `OpenProcess.Route` / `interleaveRouted` with samplers, `interleave_eq_interleaveRouted`, the `mapHom` distribution laws, and the public extensionality helpers `ext_of_step_eq` / `heq_step_of_processOver_eq` | -| `OpenProcessCoherence.lean` | `isSilentStep_interleave_{left,right}_iff`, the generic shapes `interleave_assoc_activationEquiv` / `interleave_comm_activationEquiv` / `interleave_rehome_activationEquiv` / `interleave_unit_{left,right}_activationEquiv` for arbitrary activation-preserving injections and silent scheduler nodes, and the congruences `interleave_congr_{left,right}` / `mapHom_congr` (activation equivalence is preserved by interleaving and re-decoration). Structural coherence only; nothing here sees packets or samplers. | +| `OpenProcessInterleave.lean` | `OpenProcess.mapHom` (re-decoration along any node-context hom; `mapBoundary` is the boundary-morphism case), `OpenNodeContext.PreservesActivation` with instances for every injection of the theory, `OpenNodeContext.IsInternalNode` (silent and emitting nothing) and `OpenNodeContext.EmitsAlong` (the hom relabels traces by a partial index map) with `boundaryTrace_map_of_emitsAlong`, the routed interleaving `OpenProcess.interleaveRouted` with its samplers, the normalization equalities `mapBoundary_interleave` / `interleave_mapHom_{left,right}` pushing re-decoration into the injections, and the public extensionality helpers | +| `OpenProcessCoherence.lean` | `isSilentStep_interleave_{left,right}_iff`, the silence and boundary-trace unfoldings of each branch of a composite step, the generic shapes `interleave_assoc_activationEquiv` / `interleave_comm_activationEquiv` / `interleave_rehome_activationEquiv` / `interleave_unit_{left,right}_activationEquiv` for arbitrary activation-preserving injections and silent scheduler nodes, and the congruences `interleave_congr_{left,right}` / `mapHom_congr` (activation equivalence is preserved by interleaving and re-decoration). Structural coherence only; nothing here sees packets or samplers. | | `OpenProcessModel.lean` | `openTheory m Party schedulerSampler` (concrete model threading `TypeTree.Sampler` through `map` / `par` / `wire` / `plug`), `IsLawful`, and every monoidal, traced, and compact-closed law up to `OpenProcessActivationEquiv` (`openTheory_{par_assoc,par_comm,plug_comm,wire_assoc,wire_par_superpose,wire_comm,par_left_unit,par_right_unit,wire_id_wire,wire_id_wire_right,plug_eq_wire,unit_eq}_activation_equiv`), each one instance of the `OpenProcessCoherence` shapes after normalization | | `Scheduler.lean` | Positive-natural (`PNat`) frontier masses, mass-aware `BinaryScheduler`, hierarchical source/left/right draws, and `BinaryScheduler.IsFlat` / `IsCoherent`. `IsFlat` requires every binary encoding of a three-component choice to agree with one direct flat choice relative to a downstream `MonadRelFamily`. | -| `ScheduledOpenProcessModel.lean` | `ScheduledOpenProcess` and `scheduledOpenTheory`, the additive migration model that preserves positive frontier mass through `map` and adds it through `par` / `wire` / `plug`; each binary scheduler node receives the two subtree masses. | -| `ScheduledSamplerFactorization.lean` | Public bind equations for the mass-aware hierarchical draws and `samplePath_interleave_assoc_left` / `samplePath_interleave_assoc_right`, which lift scheduler coherence through arbitrary component samplers along the structural path reassociations. | +| `ScheduledOpenProcessModel.lean` | `ScheduledOpenProcess` and `scheduledOpenTheory`, the additive migration model that preserves positive frontier mass through `map` and adds it through `par` / `wire` / `plug`; each binary scheduler node receives the two subtree masses. The theory is `IsLawful`: each naturality law is the `openTheory` law at the draw for the component masses. | +| `ScheduledSamplerFactorization.lean` | `BinaryScheduler.{source,left,right}Draw` as the nested draws at the scheduler calls of a composition, `IsCoherent` restated in the form the shapes consume (`flip_rel`, `nestedDrawLeft_rel_factor{Left,Right}`), the public bind equations, `samplePath_interleave_assoc_{left,right}`, the five plug laws `scheduledOpenTheory_plug_{comm,par_left,par_right,wire_left,wire_right}_sampler_equiv` of the mass-aware theory with scheduler coherence as the whole obligation, and `Observation.scheduledSampler` with `respectsFactorization_scheduledSampler`. | | `SubTheory.lean` | `SubTheory` (a boundary-indexed membership predicate on `T.Obj` closed under `map` / `par` / `wire`), the `IsPlugClosed` and `IsStructural` mixins, standard `PartialOrder` / `OrderTop` / `SemilatticeInf` instances, ordinary `generated`, and the separately named least plug-closed construction `plugGenerated`. This is structural membership only: resource, efficiency, realizability, protocol-class, and corruption readings require explicit bridges. | | `Emulates.lean` | `Observation`, `Emulates`, `UCSecure`. Contextual emulation and UC security stated abstractly over an `Observation` (an equivalence relation on closed systems), with no probability monad and no concrete security predicate. Composition takes its exact structural input from the observation via `Observation.RespectsPlugComm` / `Observation.RespectsFactorization`; theories with `HasPlugFactorization` (in particular every strict `HasPlugWireFactor` theory) satisfy both automatically. Process-backed security observations must prove these laws without erasing security-visible packet, action, or sampler data. | | `EmulatesWithin.lean` | `EmulatesWithin` (emulation quantified only over `SubTheory`-allowed closing contexts) and its relativized composition suite, plus `UCSecureWithin` and `SubTheory.PreservesAllowedness`. The latter says only that the chosen simulator maps allowed contexts to allowed contexts; it does not prove simulator realizability or efficiency. Real/ideal protocol membership is also separate. Each composition theorem requests the precise component membership needed to build its residual context. `emulatesWithin_top_iff` shows the layer is a conservative extension. | @@ -696,7 +696,8 @@ import PolyFun.Interaction.UC.OpenProcessModel | `GlobalSubroutine.lean` | `OpenTheory.withGlobal` (wire a shared global resource onto a protocol's subroutine face), directional `SecurelyEmulatesWithGlobal`, and the stronger symmetric `EmulatesWithGlobal` / `EmulatesWithGlobalWithin`. `wire_outer` / `wire_compose_outer` compose only the symmetric relation; secure UCGS still needs structural simulators. | | `SecureEmulation.lean` | `SecurelyEmulates` / `SecurelyEmulatesWithin`, the existential context-transformer judgment, its reconciliation with `Emulates` and `UCSecure`, and its local preorder. This is not yet FKKKT26's resource preorder: no resource-category translation or structural simulator morphism is present, and consequently no `par`/`wire` monotonicity is claimed. | | `OpenProcessSamplerEquiv.lean` | `MonadRelFamily` (the abstract relation family on `m`-computations a downstream semantics supplies; `.top` forgets sampler effects), `IsSamplerBisimulation` (strong one-to-one path matching preserving silence, boundary traces, successor relatedness, and `R`-related sampled paths), and `OpenProcessSamplerEquiv` with refl/symm/trans and `toActivationEquiv`. Scheduler-transport facts are deliberately hypotheses of the sampler-aware factorization theorems, not theorems here — a shared scheduler does not preserve per-step scheduling distributions across reassociation. | -| `OpenProcessSamplerFactorization.lean` | The five sampler-aware coherence laws `openTheory_plug_{comm,par_left,par_right,wire_left,wire_right}_sampler_equiv`, each conditional on its named scheduler-transport fact (`schedulerFlip`-fairness, `sourceDraw`/`leftDraw`/`rightDraw` relatedness); the path re-encodings `flipInterleavePathEquiv` / `parLeftPathEquiv` / `parRightPathEquiv`; and the sampling laws for the scheduler node. The activation-equivalence laws keep their direct monad-free proofs; these strengthen them for lawful monads. | +| `OpenProcessSamplerCoherence.lean` | `MonadRelFamily.IsBindCongr` (right-continuation congruence; instances for `eq` and `top`), `OpenProcessFactorization.Leaf`, the nested scheduler draws `nestedDrawLeft` / `nestedDrawFactorLeft` / `nestedDrawFactorRight` with their bind equations, the path re-encodings `flipInterleavePathEquiv` / `parLeftPathEquiv` / `parRightPathEquiv` / `{left,right}BranchPathEquiv`, the sampled-path flattening lemmas, the shapes `interleave_factor{Left,Right}_samplerEquiv` / `interleave_comm_samplerEquiv` / `interleave_rehome_samplerEquiv` / `interleave_assoc_samplerEquiv` (identically decorated leaves, internal scheduler nodes, related nested draws), and the congruences `OpenProcess.interleave_congr_{left,right}_samplerEquiv` / `mapHom_congr_samplerEquiv`. No unit absorption: a silent unit adds a path to every step. | +| `OpenProcessSamplerFactorization.lean` | The five sampler-aware plug laws `openTheory_plug_{comm,par_left,par_right,wire_left,wire_right}_sampler_equiv`, each conditional on its named scheduler-transport fact (`schedulerFlip`-fairness, `sourceDraw`/`leftDraw`/`rightDraw` relatedness) and each one instance of a sampler-level shape after normalization; the monoidal laws `openTheory_{par_comm,wire_comm}_sampler_equiv` (fairness) and `openTheory_par_assoc_sampler_equiv` (fairness, the left transport fact, and `IsBindCongr`); the closed composites and tensor reindexings of the theory's injections; and the congruence laws `openTheory_{map,par,wire,plug}_congr_*_sampler_equiv` under `MonadRelFamily.IsBindCongr`. The activation-equivalence laws keep their direct monad-free proofs; these strengthen them for lawful monads. | | `SamplerObservation.lean` | `Observation.respectsFactorization_of_samplerInvariant` — any observation invariant under sampler equivalence respects plug commutation and factorization, given the transport facts — and the canonical sampled-path observation `Observation.sampler`. This exposes rather than solves the distributional scheduler obstruction: exact equality generally cannot prove the transport premises, and packet/action adequacy remains downstream. | | `Notation.lean` | UC notation helpers (`∥`, `⊞`, `⊠`, `⊗ᵇ`, `ᵛ`); see [`notation.md`](notation.md) | | `MachineId.lean` | machine identifiers | diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md index 9a80a0d1..78805a4c 100644 --- a/docs/wiki/repo-map.md +++ b/docs/wiki/repo-map.md @@ -311,17 +311,30 @@ Interaction/UC/{OpenProcessModel, Scheduler} additive mass-aware open-process theory; concrete proportional sampling and distributional adequacy remain downstream) -Interaction/UC/{OpenProcessSamplerFactorization, Scheduler} - -> Interaction/UC/ScheduledSamplerFactorization - (the scheduler coherence law lifted through arbitrary component samplers - along the existing left/right structural path reassociations) +Interaction/UC/{OpenProcessCoherence, OpenProcessSamplerEquiv} + -> Interaction/UC/OpenProcessSamplerCoherence + -> Interaction/UC/OpenProcessFactorization + (the coherence shapes up to sampler equivalence — left/right plug + factorization, commutation, re-homing, derived reassociation — for + internal scheduler nodes and identically decorated leaves, with the nested + scheduler draws as the only transport hypothesis; the `IsBindCongr` mixin + and the congruence of sampler equivalence under `interleave` and `mapHom`; + the leaf type and path re-encodings the factorization files index by) Interaction/UC/{OpenProcessModel, OpenProcessFactorization, - OpenProcessSamplerEquiv} + OpenProcessSamplerCoherence} -> Interaction/UC/OpenProcessSamplerFactorization - (the five coherence laws at sampler equivalence, conditional on named - scheduler-transport hypotheses; the activation laws keep their direct - monad-free proofs) + (the five plug laws of `openTheory` at sampler equivalence, conditional on + named scheduler-transport hypotheses, and the congruence laws of the + theory; each one instance of a sampler-level shape) + +Interaction/UC/{OpenProcessSamplerFactorization, SamplerObservation, + Scheduler, ScheduledOpenProcessModel} + -> Interaction/UC/ScheduledSamplerFactorization + (`IsCoherent` in the form the shapes consume, the plug laws of + `scheduledOpenTheory` at sampler equivalence with coherence as the whole + obligation, and the scheduled sampler observation respecting + factorization) Interaction/UC/{Emulates, OpenProcessSamplerFactorization} -> Interaction/UC/SamplerObservation diff --git a/docs/wiki/uc.md b/docs/wiki/uc.md index b5a6a47c..b6222f9b 100644 --- a/docs/wiki/uc.md +++ b/docs/wiki/uc.md @@ -37,7 +37,7 @@ the activation-equivalence factorization theorems in | Paper surface | PolyFun surface | Status | | --- | --- | --- | -| symmetric monoidal category `C` of interactive systems | `OpenTheory`, with `par`, `wire`, and a granular lawfulness ladder | Candidate model; the free syntax models satisfy the strict laws, while `openTheory` is only `IsLawful` strictly and satisfies the monoidal, traced, and compact-closed laws up to `OpenProcessActivationEquiv`. `HasPlugFactorization` isolates the five factorization equalities the composition theorems consume; it is the strict target a process model can honestly aim for, since unit and snake laws fail at strong sampler equivalence | +| symmetric monoidal category `C` of interactive systems | `OpenTheory`, with `par`, `wire`, and a granular lawfulness ladder | Candidate model; the free syntax models satisfy the strict laws, while `openTheory` is only `IsLawful` strictly, satisfies the monoidal, traced, and compact-closed laws up to `OpenProcessActivationEquiv`, and satisfies `par_assoc`, `par_comm`, `wire_comm`, and the plug laws up to `OpenProcessSamplerEquiv R` under scheduler-transport hypotheses; unit and zig-zag laws have no sampler-level version. `HasPlugFactorization` isolates the five factorization equalities the composition theorems consume; it is the strict target a process model can honestly aim for, since unit and snake laws fail at strong sampler equivalence | | backdoor category `C_bd` | adversarial ports can be represented by ordinary typed boundary components | Representation strategy only; no equivalence with the paper's backdoor construction or quotient is proved | | nested `D_real ⊆ D_bd` | ordered `SubTheory` values | Structural carrier plus `realizableSubTheory` / `generatedRealizableSubTheory`; corruption and concrete efficiency still require explicit instances | | corruption restriction defining `D_real` | `CorruptionModel`, `MomentaryCorruption` | Vocabulary only; no bridge to `SubTheory.mem` | @@ -122,10 +122,15 @@ relation family `MonadRelFamily` their atomic frontier, binary nodes receive both subtree masses, and a downstream scheduler proves that all hierarchical three-way draws denote one flat choice. Probability and the concrete proportional scheduler remain - VCVio responsibilities. `samplePath_interleave_assoc_left` and - `samplePath_interleave_assoc_right` lift the resulting coherence law through - arbitrary component samplers along the existing structural path - reassociations. + VCVio responsibilities. For the mass-aware theory `scheduledOpenTheory`, + `BinaryScheduler.IsCoherent` is the whole obligation: + `scheduledOpenTheory_plug_{comm,par_left,par_right,wire_left,wire_right}_sampler_equiv` + and `Observation.respectsFactorization_scheduledSampler` take coherence and + nothing else. Both theories' laws are instances of the sampler-level shapes + in `OpenProcessSamplerCoherence`, whose only transport hypothesis is that + the two nested scheduler draws of a regrouping are `R`-related; sampler + equivalence is moreover a congruence for `map`/`par`/`wire`/`plug` once + `R` is bind-congruent on the right (`MonadRelFamily.IsBindCongr`). 2. **Initial-state correspondence.** The totality fields of `OpenProcessSamplerEquiv` expose the regrouping bijection on states, so corresponding initial states are chosen definitionally.