From 5c197ce4b0aa259dcfba474146440e717f299d9b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Sat, 6 Jun 2026 17:38:53 +0200 Subject: [PATCH 1/2] TODO --- TODO.md | 1 + 1 file changed, 1 insertion(+) diff --git a/TODO.md b/TODO.md index 4cdf4a7d..05405fc3 100644 --- a/TODO.md +++ b/TODO.md @@ -7,5 +7,6 @@ - [x] StringDiagram for kernels - [x] `kernel_disch` tactic - [x] Cast a kernel on product to a morphism on tensor product +- [ ] First cast to common universe, then to `SFinKer` - [ ] define attributes to automatically generate lemmas such as `reassoc` (check Thunk NameMapEnv from to_additive) - [ ] Try to leverage the property of copy-discard categories in a adaptation of the `monoidal` tactic \ No newline at end of file From e78a2946a28d13e02971c0d9b909b0873b626a1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Sat, 6 Jun 2026 18:43:37 +0200 Subject: [PATCH 2/2] MonoidalComp handling --- KernelHom/Kernel/MonoidalComp.lean | 10 +-- KernelHom/Tactic/Hom/HomKernel.lean | 47 +++++++++++++- KernelHom/Tactic/Hom/KernelHom.lean | 97 +++++++++++++++++++++++++---- KernelHom/Tactic/Hom/Utils.lean | 1 + 4 files changed, 135 insertions(+), 20 deletions(-) diff --git a/KernelHom/Kernel/MonoidalComp.lean b/KernelHom/Kernel/MonoidalComp.lean index d12ba58b..7986c430 100644 --- a/KernelHom/Kernel/MonoidalComp.lean +++ b/KernelHom/Kernel/MonoidalComp.lean @@ -106,12 +106,12 @@ scoped[ProbabilityTheory] infixr:80 " ⊗≫ₖ " => Kernel.monoComp instance monoComp_sfinite : IsSFiniteKernel (κ ⊗≫ₖ η) := by infer_instance -variable {W'' X'' Y'' Z'' : SFinKer.{max v w x y z}} (ew' : W''.carrier ≃ᵐ W) - (ex' : X''.carrier ≃ᵐ X) (ey' : Y''.carrier ≃ᵐ Y) (ez' : Z''.carrier ≃ᵐ Z) +variable {W' X' Y' Z' : SFinKer.{max v w x y z}} (ew : W'.carrier ≃ᵐ W) + (ex : X'.carrier ≃ᵐ X) (ey : Y'.carrier ≃ᵐ Y) (ez : Z'.carrier ≃ᵐ Z) -lemma hom_monoComp : @monoidalComp _ _ _ _ _ _ (monoidalCoherence ex' ey') - (hom (ex := ew') (ey := ex') κ) (hom (ex := ey') (ey := ez') η) - = hom (ex := ew') (ey := ez') (monoComp κ η):= by +lemma hom_monoComp : @monoidalComp _ _ _ _ _ _ (monoidalCoherence ex ey) + (hom (ex := ew) (ey := ex) κ) (hom (ex := ey) (ey := ez) η) + = hom (ex := ew) (ey := ez) (monoComp κ η):= by simp only [monoComp₀, fromHom, hom, monoidalComp] ext _ s hs; dsimp unfold monoidalCoherence diff --git a/KernelHom/Tactic/Hom/HomKernel.lean b/KernelHom/Tactic/Hom/HomKernel.lean index d7571a19..0b16f10a 100644 --- a/KernelHom/Tactic/Hom/HomKernel.lean +++ b/KernelHom/Tactic/Hom/HomKernel.lean @@ -194,8 +194,15 @@ partial def transformHomToKernel (eLevel : Level) (e : Expr) (op_data : List Cat let η := args[args.size - 1]! let (κ', lκ) ← transformHomToKernel eLevel κ op_data let (η', lη) ← transformHomToKernel eLevel η lκ + let (W, X, wLvl, xLvl) ← getTypesFromKernel κ' + let (Y, Z, yLvl, zLvl) ← getTypesFromKernel η' + let (sfinkerOfW, ew) ← computeEquivAndSFinKerOf W wLvl eLevel + let (sfinkerOfX, ex) ← computeEquivAndSFinKerOf X xLvl eLevel + let (sfinkerOfY, ey) ← computeEquivAndSFinKerOf Y yLvl eLevel + let (sfinkerOfZ, ez) ← computeEquivAndSFinKerOf Z zLvl eLevel + let MonoOP := .MonoidalComp sfinkerOfW ew sfinkerOfX ex sfinkerOfY ey sfinkerOfZ ez return (← mkAppOptM ``Kernel.monoComp - #[none, none, none, none, none, none, none, none, none, κ', none, η', none], lη) + #[none, none, none, none, none, none, none, none, none, κ', none, η', none], MonoOP::lη) | Expr.const ``Iso.hom _ => let args := e.getAppArgs let iso := args[args.size - 1]! @@ -385,6 +392,24 @@ def mkHomKernelEqProof (eqProofType : Expr) (eLevel : Level) evalTactic congr_tac catch _ => pure () + | .MonoidalComp sfinkerW ew sfinkerX ex sfinkerY ey sfinkerZ ez => + let sfinkerWStx ← Term.exprToSyntax sfinkerW + let ewStx ← Term.exprToSyntax ew + let sfinkerXStx ← Term.exprToSyntax sfinkerX + let exStx ← Term.exprToSyntax ex + let sfinkerYStx ← Term.exprToSyntax sfinkerY + let eyStx ← Term.exprToSyntax ey + let sfinkerZStx ← Term.exprToSyntax sfinkerZ + let ezStx ← Term.exprToSyntax ez + evalTactic (← `(tactic| nth_rw 1 [ + Kernel.hom_monoComp.{$eLevelStx} (W' := $sfinkerWStx) (X' := $sfinkerXStx) + (Y' := $sfinkerYStx) (Z' := $sfinkerZStx) + _ _ $ewStx $exStx $eyStx $ezStx + ] at h)) + try + evalTactic congr_tac + catch _ => + pure () | _ => pure () evalTactic (← `(tactic| rwa [Kernel.hom_congr.{$eLevelStx}] at h)) @@ -461,7 +486,6 @@ def mkHomKernelEqProof (eqProofType : Expr) (eLevel : Level) let eStx ← Term.exprToSyntax equiv evalTactic (← `(tactic| nth_rw 1 [Kernel.comul (X' := $sfinkerStx) (ex := $eStx)])) | _ => pure () - if !(← getGoals).isEmpty then let congr_tac ← `(tactic| simp only [ Kernel.hom_monoComp.{$eLevelStx}, @@ -493,6 +517,24 @@ def mkHomKernelEqProof (eqProofType : Expr) (eLevel : Level) evalTactic congr_tac catch _ => pure () + | .MonoidalComp sfinkerW ew sfinkerX ex sfinkerY ey sfinkerZ ez => + let sfinkerWStx ← Term.exprToSyntax sfinkerW + let ewStx ← Term.exprToSyntax ew + let sfinkerXStx ← Term.exprToSyntax sfinkerX + let exStx ← Term.exprToSyntax ex + let sfinkerYStx ← Term.exprToSyntax sfinkerY + let eyStx ← Term.exprToSyntax ey + let sfinkerZStx ← Term.exprToSyntax sfinkerZ + let ezStx ← Term.exprToSyntax ez + evalTactic (← `(tactic| nth_rw 1 [ + Kernel.hom_monoComp.{$eLevelStx} (W' := $sfinkerWStx) (X' := $sfinkerXStx) + (Y' := $sfinkerYStx) (Z' := $sfinkerZStx) + _ _ $ewStx $exStx $eyStx $ezStx + ])) + try + evalTactic congr_tac + catch _ => + pure () | _ => pure () evalTactic (← `(tactic| rwa [Kernel.hom_congr.{$eLevelStx}])) | _ => @@ -501,7 +543,6 @@ def mkHomKernelEqProof (eqProofType : Expr) (eLevel : Level) if !(← getGoals).isEmpty then setGoals savedGoals throwError "Failed to solve all goals while building kernel_hom equivalence proof" - setGoals savedGoals instantiateMVars mvar diff --git a/KernelHom/Tactic/Hom/KernelHom.lean b/KernelHom/Tactic/Hom/KernelHom.lean index 7b2ad994..06ab93e1 100644 --- a/KernelHom/Tactic/Hom/KernelHom.lean +++ b/KernelHom/Tactic/Hom/KernelHom.lean @@ -233,6 +233,26 @@ partial def transformKernelToHom (maxLvl : Level) (e : Expr) (op_data : List Cat let (η', lη) ← transformKernelToHom maxLvl η op_data let (κ', lκ) ← transformKernelToHom maxLvl κ lη return (← mkAppM ``CategoryStruct.comp #[η', κ'], lκ) + | Expr.const ``Kernel.monoComp _ => + let args := e.getAppArgs + let κ := args[args.size - 4]! + let η := args[args.size - 2]! + let (W, X, wLvl, xLvl) ← getTypesFromKernel κ + let (Y, Z, yLvl, zLvl) ← getTypesFromKernel η + let (κ', lκ) ← transformKernelToHom maxLvl κ op_data + let (η', lη) ← transformKernelToHom maxLvl η lκ + let (sfinkerOfX, ex) ← computeEquivAndSFinKerOf X xLvl maxLvl + let (sfinkerOfY, ey) ← computeEquivAndSFinKerOf Y yLvl maxLvl + let monoComp := Expr.const ``monoidalComp [maxLvl, maxLvl.succ] + let monoCoherenceConst := Expr.const `MeasurableCoherence.monoidalCoherence + [maxLvl, xLvl, yLvl] + let monoCoherence ← mkAppOptM' monoCoherenceConst + #[none, none, none, none, none, sfinkerOfX, sfinkerOfY, ex, ey] + let (sfinkerOfW, ew) ← computeEquivAndSFinKerOf W wLvl maxLvl + let (sfinkerOfZ, ez) ← computeEquivAndSFinKerOf Z zLvl maxLvl + let MonoOP := .MonoidalComp sfinkerOfW ew sfinkerOfX ex sfinkerOfY ey sfinkerOfZ ez + return (← mkAppOptM' monoComp + #[none, none, none, none, none, none, monoCoherence, κ', η'], MonoOP :: lη) | Expr.const ``Kernel.parallelComp _ => let (X, _, _, _) ← getTypesFromKernel e if ← checkWhiskerLeft e then @@ -383,7 +403,6 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level) evalTactic (← `(tactic| nth_rw 1 [Kernel.comul (X' := $sfinkerStx) (ex := $equivStx)])) | _ => pure () let congr_tac ← `(tactic| simp only [ - Kernel.hom_monoComp.{$maxLvlStx}, Kernel.hom_comp.{$maxLvlStx}, Kernel.tensorHom.{$maxLvlStx}, ] @@ -396,6 +415,7 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level) for e in op_data do match e with | .WhiskerLeft sfinker equiv => + logInfo m! "WhiskerLeft: {sfinker}, {equiv}" let sfinkerStx ← Term.exprToSyntax sfinker let equivStx ← Term.exprToSyntax equiv evalTactic (← `(tactic| nth_rw 1 [ @@ -405,6 +425,7 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level) catch _ => pure () | .WhiskerRight sfinker equiv => + logInfo m! "WhiskerRight: {sfinker}, {equiv}" let sfinkerStx ← Term.exprToSyntax sfinker let equivStx ← Term.exprToSyntax equiv evalTactic (← `(tactic| nth_rw 1 [ @@ -413,6 +434,25 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level) evalTactic congr_tac catch _ => pure () + | .MonoidalComp sfinkerW ew sfinkerX ex sfinkerY ey sfinkerZ ez => + logInfo m! "MonoidalComp: {sfinkerW}, {ew}, {sfinkerX}, {ex}, {sfinkerY}, {ey}, {sfinkerZ}, {ez}" + let sfinkerWStx ← Term.exprToSyntax sfinkerW + let ewStx ← Term.exprToSyntax ew + let sfinkerXStx ← Term.exprToSyntax sfinkerX + let exStx ← Term.exprToSyntax ex + let sfinkerYStx ← Term.exprToSyntax sfinkerY + let eyStx ← Term.exprToSyntax ey + let sfinkerZStx ← Term.exprToSyntax sfinkerZ + let ezStx ← Term.exprToSyntax ez + evalTactic (← `(tactic| nth_rw 1 [ + Kernel.hom_monoComp.{$maxLvlStx} (W' := $sfinkerWStx) (X' := $sfinkerXStx) + (Y' := $sfinkerYStx) (Z' := $sfinkerZStx) + _ _ $ewStx $exStx $eyStx $ezStx + ])) + try + evalTactic congr_tac + catch _ => + pure () | _ => pure () evalTactic (← `(tactic| rwa [Kernel.hom_congr.{$maxLvlStx} (κ₁ := $rhsStx) (κ₂ := $lhsStx)])) @@ -483,7 +523,6 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level) | _ => pure () if !(← getGoals).isEmpty then let congr_tac ← `(tactic| simp only [ - Kernel.hom_monoComp.{$maxLvlStx}, Kernel.hom_comp.{$maxLvlStx}, Kernel.tensorHom.{$maxLvlStx}, ] at h @@ -512,17 +551,60 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level) evalTactic congr_tac catch _ => pure () + | .MonoidalComp sfinkerW ew sfinkerX ex sfinkerY ey sfinkerZ ez => + let sfinkerWStx ← Term.exprToSyntax sfinkerW + let ewStx ← Term.exprToSyntax ew + let sfinkerXStx ← Term.exprToSyntax sfinkerX + let exStx ← Term.exprToSyntax ex + let sfinkerYStx ← Term.exprToSyntax sfinkerY + let eyStx ← Term.exprToSyntax ey + let sfinkerZStx ← Term.exprToSyntax sfinkerZ + let ezStx ← Term.exprToSyntax ez + evalTactic (← `(tactic| nth_rw 1 [ + Kernel.hom_monoComp.{$maxLvlStx} (W' := $sfinkerWStx) (X' := $sfinkerXStx) + (Y' := $sfinkerYStx) (Z' := $sfinkerZStx) + _ _ $ewStx $exStx $eyStx $ezStx + ] at h)) + try + evalTactic congr_tac + catch _ => + pure () | _ => pure () evalTactic (← `(tactic| rwa [Kernel.hom_congr.{$maxLvlStx} (κ₁ := $rhsStx) (κ₂ := $lhsStx)] at h)) | _ => setGoals savedGoals throwError "Expected exactly two goals after `constructor`" - if !(← getGoals).isEmpty then setGoals savedGoals throwError "Failed to solve all goals while building kernel_hom equivalence proof" + setGoals savedGoals + instantiateMVars mvar +/-- Construct the proof of equivalence between the original equality and the transformed one. -/ +def mkKernelHomEqProofSorry (eqProofType rhs lhs : Expr) (maxLvl : Level) + (op_data : List CategoryOP) : TacticM Expr := do + let maxLvlStx ← liftMacroM <| levelToSyntax maxLvl + let rhsStx ← Term.exprToSyntax rhs + let lhsStx ← Term.exprToSyntax lhs + let op_data := op_data.reverse + let savedGoals ← getGoals + let mvar ← mkFreshExprSyntheticOpaqueMVar eqProofType + let mvarId := mvar.mvarId! + setGoals [mvarId] + evalTactic (← `(tactic| apply propext)) + evalTactic (← `(tactic| constructor)) + let goalsAfterConstructor ← getGoals + match goalsAfterConstructor with + | [forwardGoal, backwardGoal] => + setGoals [forwardGoal] + evalTactic (← `(tactic| sorry)) + + setGoals [backwardGoal] + evalTactic (← `(tactic| sorry)) + | _ => + setGoals savedGoals + throwError "Expected exactly two goals after `constructor`" setGoals savedGoals instantiateMVars mvar @@ -576,12 +658,3 @@ syntax (name := kernelHom) "kernel_hom" (ppSpace location)? : tactic elab_rules : tactic | `(tactic| kernel_hom $[$loc]?) => expandOptLocation (Lean.mkOptionalNode loc) |> applyLocTactic <| ApplyKernelHom - -variable {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] - -open Kernel - -lemma discard_comp_deterministic {f : X → Y} (hf : Measurable f) : - discard Y ∘ₖ (deterministic f hf) = discard X := by - kernel_hom - simp only [IsComonHom.hom_counit] diff --git a/KernelHom/Tactic/Hom/Utils.lean b/KernelHom/Tactic/Hom/Utils.lean index 92928cb9..7071e31b 100644 --- a/KernelHom/Tactic/Hom/Utils.lean +++ b/KernelHom/Tactic/Hom/Utils.lean @@ -76,6 +76,7 @@ inductive CategoryOP | Braiding_hom (sfinker₁ equiv₁ sfinker₂ equiv₂ : Expr) | Counit (sfinker equiv : Expr) | Comul (sfinker equiv : Expr) + | MonoidalComp (sfinker₁ equiv₁ sfinker₂ equiv₂ sfinker₃ equiv₃ sfinker₄ equiv₄ : Expr) /-- Transform both sides of an equality and return the new equality plus metadata. -/ def transformEquality (maxLvl : Level) (e : Expr)