From 09232d77f5754dcb439ad35df41f1f5d1bfe28fa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Fri, 11 Sep 2026 15:07:06 +0200 Subject: [PATCH 1/3] docstring --- KernelHom/Kernel/MonoidalComp.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/KernelHom/Kernel/MonoidalComp.lean b/KernelHom/Kernel/MonoidalComp.lean index 5761c1d05..d0b7a3dde 100644 --- a/KernelHom/Kernel/MonoidalComp.lean +++ b/KernelHom/Kernel/MonoidalComp.lean @@ -17,8 +17,6 @@ This file introduces the monoidal composition for s-finite kernels (noted `⊗ * `MeasurableCoherence`: class witnessing measurable equivalences between types. * `monoComp`: monoidal composition of kernels using measurable equivalences to transport to `SFinKer`. -* `hom_monoComp`: the `SFinKer` morphism of the kernelized monoidal composition is the monoidal - composition of the morphisms in `SFinKer`. -/ @[expose] public section From 6dcf1d85424a79c2e698d90e5af1c7c2be1b6872 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Fri, 11 Sep 2026 18:00:32 +0200 Subject: [PATCH 2/3] Optimize tactics --- KernelHom/Tactic/HomKernel.lean | 101 ++++++++------------- KernelHom/Tactic/KernelCat.lean | 23 +++-- KernelHom/Tactic/KernelDiagram.lean | 4 +- KernelHom/Tactic/KernelHom.lean | 122 +++++++++++--------------- KernelHom/Tactic/Reassoc.lean | 19 ++-- KernelHom/Tactic/Utils.lean | 6 -- KernelHomManual/Front.lean | 2 +- KernelHomManual/Pages/CatTactics.lean | 4 +- KernelHomManual/Pages/Examples.lean | 4 +- KernelHomTests.lean | 1 + KernelHomTests/Tests.lean | 4 + KernelHomTests/Time.lean | 76 ++++++++++++++++ lake-manifest.json | 46 +++++----- lean-toolchain | 2 +- 14 files changed, 226 insertions(+), 188 deletions(-) create mode 100644 KernelHomTests/Time.lean diff --git a/KernelHom/Tactic/HomKernel.lean b/KernelHom/Tactic/HomKernel.lean index 42ea4c65b..61032c557 100644 --- a/KernelHom/Tactic/HomKernel.lean +++ b/KernelHom/Tactic/HomKernel.lean @@ -19,7 +19,7 @@ equivalent equalities of kernels. * `transformHomToKernel`: recursive translation from categorical morphism expressions to kernel expressions. -* `applyHomKernel`: core implementation on goals and hypotheses. +* `KernelEquality`: core implementation of `hom_kernel` on an equality. * `hom_kernel`: user-facing tactic (with location support). -/ @@ -123,9 +123,10 @@ def deconstructAssociator (e : Expr) (eLvl : Level) (hom : Bool) : MetaM (Expr #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, ex₀, ey₀, ez₀] return (← getKernelRHSEqProofType associator_proof_eq, associator_proof_eq) -/-- Recursive transformation from morphism expression in `SFinKer` to kernel expression. -/ -partial def transformHomToKernel (e : Expr) (proofs : List Expr) : - MetaM (Expr × List Expr) := do +/-- Recursive transformation from morphism expression in `SFinKer` to kernel expression. +Returns the kernel expression `e'` together with a proof of `e = e'.hom`, built by congruence from +the translation lemmas. -/ +partial def transformHomToKernel (e : Expr) : MetaM (Expr × Expr) := do match e.getAppFn with | Expr.const ``tensorHom _ => let args := e.getAppArgs @@ -135,13 +136,14 @@ partial def transformHomToKernel (e : Expr) (proofs : List Expr) : let SZ := args[args.size - 4]! let SY := args[args.size - 5]! let SX := args[args.size - 6]! - let (κ', proofs_κ) ← transformHomToKernel κ proofs - let (η', proofs_η) ← transformHomToKernel η proofs_κ + let (κ', pκ) ← transformHomToKernel κ + let (η', pη) ← transformHomToKernel η let (X, Y, _, _) ← getTypesFromKernel κ' let (Z, T, _, _) ← getTypesFromKernel η' let parallelComp_hom_proof ← mkAppMInst ``parallelComp_hom #[SX, SY, SZ, ST, ← idME X, ← idME Y, ← idME Z, ← idME T, κ', η'] 2 - return (← mkAppM ``Kernel.parallelComp #[κ', η'], parallelComp_hom_proof :: proofs_η) + let h ← mkCongr (← mkCongrArg e.appFn!.appFn! pκ) pη + return (← mkAppM ``Kernel.parallelComp #[κ', η'], ← mkEqTrans h parallelComp_hom_proof) | Expr.const ``CategoryStruct.comp _ => let args := e.getAppArgs let κ := args[args.size - 2]! @@ -149,111 +151,80 @@ partial def transformHomToKernel (e : Expr) (proofs : List Expr) : let SY := args[args.size - 3]! let SX := args[args.size - 4]! let SZ := args[args.size - 5]! - let (κ', proofs_κ) ← transformHomToKernel κ proofs - let (η', proofs_η) ← transformHomToKernel η proofs_κ + let (κ', pκ) ← transformHomToKernel κ + let (η', pη) ← transformHomToKernel η let (X, Y, _, _) ← getTypesFromKernel η' let (Z, _, _, _) ← getTypesFromKernel κ' let comp_hom_proof ← mkAppMInst ``comp_hom #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, η', κ'] 2 - return (← mkAppM ``Kernel.comp #[η', κ'], comp_hom_proof :: proofs_η) + let h ← mkCongr (← mkCongrArg e.appFn!.appFn! pκ) pη + return (← mkAppM ``Kernel.comp #[η', κ'], ← mkEqTrans h comp_hom_proof) | Expr.const ``CategoryStruct.id [xLvl, _] => let args := e.getAppArgs let SX := args[args.size - 1]! let X ← getTypeFromSFinKer SX let mX' ← synthInstance (mkApp (mkConst ``MeasurableSpace [xLvl]) X) let id ← mkAppOptM ``Kernel.id #[X, mX'] - let id_hom_proof ← mkAppM ``id_hom #[SX, ← idME X] - return (id, id_hom_proof :: proofs) + return (id, ← mkAppM ``id_hom #[SX, ← idME X]) | Expr.const ``ComonObj.counit [xLvl, _] => let args := e.getAppArgs let SX := args[args.size - 2]! let X ← getTypeFromSFinKer SX - let discard_kernel_const := mkConst ``Kernel.discard [xLvl, xLvl] - let discard_const := mkConst ``counit [xLvl, xLvl, xLvl] - let discard_hom_proof ← mkAppM' discard_const #[SX, ← idME X] - return (← mkAppOptM' discard_kernel_const #[X, none], discard_hom_proof :: proofs) + let discard_hom_proof ← mkAppM' (mkConst ``counit [xLvl, xLvl, xLvl]) #[SX, ← idME X] + return (← mkAppOptM' (mkConst ``Kernel.discard [xLvl, xLvl]) #[X, none], discard_hom_proof) | Expr.const ``ComonObj.comul [xLvl, _] => let args := e.getAppArgs let SX := args[args.size - 2]! let X ← getTypeFromSFinKer SX - let copy_kernel_const := mkConst ``Kernel.copy [xLvl] - let copy_hom_proof ← mkAppM ``comul #[SX, ← idME X] - return (← mkAppOptM' copy_kernel_const #[X, none], copy_hom_proof :: proofs) + return (← mkAppOptM' (mkConst ``Kernel.copy [xLvl]) #[X, none], + ← mkAppM ``comul #[SX, ← idME X]) | Expr.const ``Kernel.hom _ => let args := e.getAppArgs - let κ := args[args.size - 2]! - return (κ, proofs) + return (args[args.size - 2]!, ← mkEqRefl e) | Expr.const ``MonoidalCategory.whiskerLeft [eLvl, _] => let (κ, kernel_id, SX, SY, SZ, X, Y, Z) ← deconstructWhiskersHomArgs e eLvl true - let (κ', proofs_κ) ← transformHomToKernel κ proofs + let (κ', pκ) ← transformHomToKernel κ let whisker_left_hom_proof ← mkAppMInst ``Kernel.whiskerLeft #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ'] 1 - return (← mkAppM ``Kernel.parallelComp #[kernel_id, κ'], whisker_left_hom_proof :: proofs_κ) + let h ← mkCongrArg e.appFn! pκ + return (← mkAppM ``Kernel.parallelComp #[kernel_id, κ'], ← mkEqTrans h whisker_left_hom_proof) | Expr.const ``MonoidalCategory.whiskerRight [eLvl, _] => let (κ, kernel_id, SX, SY, SZ, X, Y, Z) ← deconstructWhiskersHomArgs e eLvl false - let (κ', proofs_κ) ← transformHomToKernel κ proofs + let (κ', pκ) ← transformHomToKernel κ let whisker_right_hom_proof ← mkAppMInst ``Kernel.whiskerRight #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ'] 1 - return (← mkAppM ``Kernel.parallelComp #[κ', kernel_id], whisker_right_hom_proof :: proofs_κ) + let h ← mkCongrFun (← mkCongrArg e.appFn!.appFn! pκ) SZ + return (← mkAppM ``Kernel.parallelComp #[κ', kernel_id], ← mkEqTrans h whisker_right_hom_proof) | Expr.const ``Iso.hom _ => let args := e.getAppArgs let iso := args[args.size - 1]! match iso.getAppFn with - | Expr.const ``BraidedCategory.braiding _ => - let (braiding_expr, swap_hom_proof) ← deconstructBraiding iso - return (braiding_expr, swap_hom_proof :: proofs) - | Expr.const ``leftUnitor [eLvl, _] => - let (left_unitor_expr, left_unitor_hom_proof) ← deconstructUnitors iso eLvl true true - return (left_unitor_expr, left_unitor_hom_proof :: proofs) - | Expr.const ``rightUnitor [eLvl, _] => - let (right_unitor_expr, right_unitor_hom_proof) ← deconstructUnitors iso eLvl false true - return (right_unitor_expr, right_unitor_hom_proof :: proofs) - | Expr.const ``MonoidalCategory.associator [eLvl, _] => - let (associator_expr, associator_hom_proof) ← deconstructAssociator iso eLvl true - return (associator_expr, associator_hom_proof :: proofs) + | Expr.const ``BraidedCategory.braiding _ => deconstructBraiding iso + | Expr.const ``leftUnitor [eLvl, _] => deconstructUnitors iso eLvl true true + | Expr.const ``rightUnitor [eLvl, _] => deconstructUnitors iso eLvl false true + | Expr.const ``MonoidalCategory.associator [eLvl, _] => deconstructAssociator iso eLvl true | _ => throwError "Unexpected isomorphism {iso}." | Expr.const ``Iso.inv _ => let args := e.getAppArgs let iso := args[args.size - 1]! match iso.getAppFn with - | Expr.const ``BraidedCategory.braiding _ => - let (braiding_expr, swap_hom_proof) ← deconstructBraiding iso - return (braiding_expr, swap_hom_proof :: proofs) - | Expr.const ``leftUnitor [eLvl, _] => - let (left_unitor_expr, left_unitor_inv_hom_proof) ← deconstructUnitors iso eLvl true false - return (left_unitor_expr, left_unitor_inv_hom_proof :: proofs) - | Expr.const ``rightUnitor [eLvl, _] => - let (right_unitor_expr, right_unitor_inv_hom_proof) ← deconstructUnitors iso eLvl false false - return (right_unitor_expr, right_unitor_inv_hom_proof :: proofs) - | Expr.const ``MonoidalCategory.associator [eLvl, _] => - let (associator_expr, associator_inv_hom_proof) ← deconstructAssociator iso eLvl false - return (associator_expr, associator_inv_hom_proof :: proofs) + | Expr.const ``BraidedCategory.braiding _ => deconstructBraiding iso + | Expr.const ``leftUnitor [eLvl, _] => deconstructUnitors iso eLvl true false + | Expr.const ``rightUnitor [eLvl, _] => deconstructUnitors iso eLvl false false + | Expr.const ``MonoidalCategory.associator [eLvl, _] => deconstructAssociator iso eLvl false | _ => throwError "Unexpected isomorphism {iso}." | _ => throwError "Expected a hom expression, got: {e}." -/-- Get the universe level from the left side of an equality expression. -/ -def getUniverseFromEq (eq : Expr) : MetaM Level := do - let eq ← instantiateMVars eq - let eq ← zetaReduce eq - let eq ← whnf eq - let eq := eq.consumeMData - let some (_, lhs, _) := eq.eq? | throwError "Expected an equality, got: {eq}." - let l ← getLevel (← inferType lhs) - match l with - | Level.succ l' => return l' - | _ => throwError "Expected a universe level ≥ 1, got: {l}" - /-- Transform a `SFinKer` equality into an equivalent equality of kernels, along with a proof of equivalence. -/ def KernelEquality (eq : Expr) : MetaM (Expr × Expr) := do let eq ← whnfR <| ← instantiateMVars eq let some (_, lhs_hom, rhs_hom) := eq.eq? | throwError "Expected an equality, got: {eq}." - let (lhs, proofs) ← transformHomToKernel lhs_hom [] - let (rhs, proofs) ← transformHomToKernel rhs_hom proofs + let (lhs, pl) ← transformHomToKernel lhs_hom + let (rhs, pr) ← transformHomToKernel rhs_hom let kernel_expr ← mkEq lhs rhs let (unlifted_expr, unlifted_proof) ← unliftEquality kernel_expr - let kernel_eq_proof_type ← mkEq kernel_expr eq - let kernel_eq_proof ← mkAppM ``Eq.symm #[← mkKernelHomEqProof kernel_eq_proof_type lhs rhs proofs] + let kernel_eq_proof ← mkEqSymm (← mkHomCongrProof lhs rhs pl pr) return (unlifted_expr, ← mkEqTrans kernel_eq_proof unlifted_proof) /-- The `hom_kernel` tactic is the inverse of `kernel_hom`: it transforms an diff --git a/KernelHom/Tactic/KernelCat.lean b/KernelHom/Tactic/KernelCat.lean index 238fa346c..431a3ec36 100644 --- a/KernelHom/Tactic/KernelCat.lean +++ b/KernelHom/Tactic/KernelCat.lean @@ -11,14 +11,16 @@ public import Mathlib.Tactic.CategoryTheory.Coherence /-! # Kernel category tactics -This file implements the `kernel_coherence` and `kernel_monoidal` tactics, which apply the -`kernel_hom` transformation and then use categorical `coherence` or `monoidal` tactics to solve the -resulting goal. +This file implements tactics which apply the `kernel_hom` transformation and then use a +categorical tactic to solve the resulting goal. ## Main declarations -* `kernel_coherence`: tactic combining kernel_hom and categorical coherence. -* `kernel_monoidal`: tactic combining kernel_hom and categorical monoidal coherence. +* `kernel_monoidal`: `kernel_hom` followed by `monoidal`. +* `kernel_coherence`: `kernel_hom` followed by `coherence`. +* `kernel_disch`: `kernel_hom` followed by `cat_disch`. +* `aesop_kernel`: `kernel_hom` followed by `aesop` with the `CategoryTheory` rule set, skipping the + `rfl_cat` attempt of `cat_disch`. -/ public meta section @@ -53,3 +55,14 @@ elab_rules : tactic | `(tactic| kernel_disch) => do evalTactic (← `(tactic| kernel_hom)) evalTactic (← `(tactic| cat_disch)) + +/-- The `aesop_kernel` tactic applies the `kernel_hom` transformation to the goal and then +invokes `aesop` with the `CategoryTheory` rule set, using the same configuration as `aesop_cat`. -/ +syntax (name := aesopKernel) "aesop_kernel" : tactic + +elab_rules : tactic + | `(tactic| aesop_kernel) => do + evalTactic (← `(tactic| kernel_hom)) + evalTactic (← `(tactic| aesop + (config := { introsTransparency? := some .default, terminal := true }) + (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))) diff --git a/KernelHom/Tactic/KernelDiagram.lean b/KernelHom/Tactic/KernelDiagram.lean index 02fcfce7b..01b3b8457 100644 --- a/KernelHom/Tactic/KernelDiagram.lean +++ b/KernelHom/Tactic/KernelDiagram.lean @@ -53,7 +53,7 @@ def Node.toPenroseVar_kernel (n : Node) : MetaM PenroseVar := do let res ← getTypeFromSFinKer n.e pure res | _ => do - let (expr, _) ← transformHomToKernel n.e [] + let (expr, _) ← transformHomToKernel n.e pure expr catch _ => pure n.e @@ -95,7 +95,7 @@ open scoped Jsx in def KernelM? (e : Expr) : MetaM (Option Html) := do let e ← instantiateMVars e try - let (e, _) ← transformKernelToHom e [] + let (e, _) ← transformKernelToHom e let k ← StringDiagram.mkKind e let x : Option (List (List StringDiagram.Node) × List (List StringDiagram.Strand)) ← (match k with diff --git a/KernelHom/Tactic/KernelHom.lean b/KernelHom/Tactic/KernelHom.lean index 772f93e4c..5673b57b1 100644 --- a/KernelHom/Tactic/KernelHom.lean +++ b/KernelHom/Tactic/KernelHom.lean @@ -20,9 +20,8 @@ kernels into equivalent equalities in the monoidal category. * `transformKernelToHom`: recursive translation from kernel expressions to categorical morphism expressions. -* `mkKernelHomEqProof`: construction of the equivalence proof used by the - tactic. -* `applyKernelHom`: core implementation of `kernel_hom` on goals and hypotheses. +* `mkHomCongrProof`: construction of the equivalence proof used by the tactic. +* `HomEquality`: core implementation of `kernel_hom` on an equality. * `kernel_hom`: user-facing tactic (with location support). -/ @@ -243,9 +242,9 @@ def constructAssociatorInv (left right ex₀ ey₀ ez₀ : Expr) := constructAssociator left right ex₀ ey₀ ez₀ false /-- Recursive transformation from kernel expressions to morphism expressions in the `SFinKer` -category. -/ -partial def transformKernelToHom (e : Expr) (proofs : List Expr) : - MetaM (Expr × List Expr) := do +category. Returns the morphism expression `e'` together with a proof of `e' = e.hom`, built by +congruence from the translation lemmas. -/ +partial def transformKernelToHom (e : Expr) : MetaM (Expr × Expr) := do match e.getAppFn with | Expr.const ``Kernel.comp _ => let args := e.getAppArgs @@ -257,26 +256,30 @@ partial def transformKernelToHom (e : Expr) (proofs : List Expr) : let SY ← computeSFinkerOf Y yLvl let SZ ← computeSFinkerOf Z tLvl let comp_hom_proof ← mkAppMInst ``comp_hom #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, η, κ] 2 - let (κ', proofs_κ) ← transformKernelToHom κ proofs - let (η', proofs_η) ← transformKernelToHom η proofs_κ - return (← mkAppM ``CategoryStruct.comp #[κ', η'], comp_hom_proof :: proofs_η) + let (κ', pκ) ← transformKernelToHom κ + let (η', pη) ← transformKernelToHom η + let e' ← mkAppM ``CategoryStruct.comp #[κ', η'] + let h ← mkCongr (← mkCongrArg e'.appFn!.appFn! pκ) pη + return (e', ← mkEqTrans h comp_hom_proof) | Expr.const ``Kernel.parallelComp _ => if ← checkWhiskerLeft e then let (X, Y, _, _) ← getTypesFromKernel e let (SZ, Z, SX, X, SY, Y, κ) ← constructWhiskersArgs e X Y false - let (κ', proofs_κ) ← transformKernelToHom κ proofs let whisker_left_hom_proof ← mkAppMInst ``Kernel.whiskerLeft #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ] 1 - let whiskerleft ← mkAppM ``MonoidalCategory.whiskerLeft #[SZ, κ'] - return (whiskerleft, whisker_left_hom_proof :: proofs_κ) + let (κ', pκ) ← transformKernelToHom κ + let e' ← mkAppM ``MonoidalCategory.whiskerLeft #[SZ, κ'] + let h ← mkCongrArg e'.appFn! pκ + return (e', ← mkEqTrans h whisker_left_hom_proof) else if ← checkWhiskerRight e then let (X, Y, _, _) ← getTypesFromKernel e let (SZ, Z, SX, X, SY, Y, κ) ← constructWhiskersArgs e X Y true - let (κ', proofs_κ) ← transformKernelToHom κ proofs - let whiskerright ← mkAppM ``MonoidalCategory.whiskerRight #[κ', SZ] let whiskerright_hom_proof ← mkAppMInst ``Kernel.whiskerRight #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ] 1 - return (whiskerright, whiskerright_hom_proof :: proofs_κ) + let (κ', pκ) ← transformKernelToHom κ + let e' ← mkAppM ``MonoidalCategory.whiskerRight #[κ', SZ] + let h ← mkCongrFun (← mkCongrArg e'.appFn!.appFn! pκ) SZ + return (e', ← mkEqTrans h whiskerright_hom_proof) else let args := e.getAppArgs let κ := args[args.size - 2]! @@ -289,34 +292,32 @@ partial def transformKernelToHom (e : Expr) (proofs : List Expr) : let ST ← computeSFinkerOf T tLvl let parallelComp_hom_proof ← mkAppMInst ``parallelComp_hom #[SX, SY, SZ, ST, ← idME X, ← idME Y, ← idME Z, ← idME T, κ, η] 2 - let (κ', proofs_κ) ← transformKernelToHom κ proofs - let (η', proofs_η) ← transformKernelToHom η proofs_κ - return (← mkAppM ``tensorHom #[κ', η'], parallelComp_hom_proof :: proofs_η) + let (κ', pκ) ← transformKernelToHom κ + let (η', pη) ← transformKernelToHom η + let e' ← mkAppM ``tensorHom #[κ', η'] + let h ← mkCongr (← mkCongrArg e'.appFn!.appFn! pκ) pη + return (e', ← mkEqTrans h parallelComp_hom_proof) | Expr.const ``Kernel.id [xLvl] => let X := e.getAppArgs[0]! let SX ← computeSFinkerOf X xLvl - let id_hom_proof ← mkAppM ``id_hom #[SX, ← idME X] - return (← mkAppM ``CategoryStruct.id #[SX], id_hom_proof :: proofs) + return (← mkAppM ``CategoryStruct.id #[SX], ← mkAppM ``id_hom #[SX, ← idME X]) | Expr.const ``Kernel.discard [xLvl, punitLvl] => let X := e.getAppArgs[0]! let SX ← computeSFinkerOf X xLvl - let discard_const := mkConst ``counit [xLvl, xLvl, punitLvl] - let discard_hom_proof ← mkAppM' discard_const #[SX, ← idME X] - return (← mkAppOptM ``ComonObj.counit #[none, none, none, SX, none], - discard_hom_proof :: proofs) + let discard_hom_proof ← mkAppM' (mkConst ``counit [xLvl, xLvl, punitLvl]) #[SX, ← idME X] + return (← mkAppOptM ``ComonObj.counit #[none, none, none, SX, none], discard_hom_proof) | Expr.const ``Kernel.copy [xLvl] => let X := e.getAppArgs[0]! let SX ← computeSFinkerOf X xLvl - let copy_hom_proof ← mkAppM ``comul #[SX, ← idME X] - return (← mkAppOptM ``ComonObj.comul #[none, none, none, SX, none], copy_hom_proof :: proofs) + return (← mkAppOptM ``ComonObj.comul #[none, none, none, SX, none], + ← mkAppM ``comul #[SX, ← idME X]) | Expr.const ``Kernel.swap [xLvl, yLvl] => let X := e.getAppArgs[0]! let Y := e.getAppArgs[1]! let SX ← computeSFinkerOf X xLvl let SY ← computeSFinkerOf Y yLvl - let swap_hom_proof ← mkAppM ``braiding_hom #[SX, SY, ← idME X, ← idME Y] let braiding ← mkAppM ``Iso.hom #[← mkAppM ``BraidedCategory.braiding #[SX, SY]] - return (braiding, swap_hom_proof :: proofs) + return (braiding, ← mkAppM ``braiding_hom #[SX, SY, ← idME X, ← idME Y]) | Expr.const ``Kernel.lift [_, y₀Lvl, _] => let (X, Y, xLvl, yLvl) ← getTypesFromKernel e let args := e.getAppArgs @@ -325,69 +326,52 @@ partial def transformKernelToHom (e : Expr) (proofs : List Expr) : let punitLvl ← match args[0]!.getAppFn with | Expr.const ``Prod [punitLvl, _] => pure punitLvl | _ => throwError "Expected a product with PUnit as the first component, got {args[0]!}." - let ey₀ := args[args.size - 2]! - let (leftUnitorExpr, left_unitor_hom_proof) ← constructUnitors Y ey₀ yLvl y₀Lvl punitLvl 0 - return (leftUnitorExpr, left_unitor_hom_proof :: proofs) + constructUnitors Y args[args.size - 2]! yLvl y₀Lvl punitLvl 0 else if ← checkRightUnitor κ then let punitLvl ← match args[0]!.getAppFn with | Expr.const ``Prod [_, punitLvl] => pure punitLvl - | _ => throwError "Expected a product with PUnit as the first component, got {args[0]!}." - let ey₀ := args[args.size - 2]! - let (rightUnitorExpr, right_unitor_hom_proof) ← constructUnitors Y ey₀ yLvl y₀Lvl punitLvl 1 - return (rightUnitorExpr, right_unitor_hom_proof :: proofs) + | _ => throwError "Expected a product with PUnit as the second component, got {args[0]!}." + constructUnitors Y args[args.size - 2]! yLvl y₀Lvl punitLvl 1 else if ← checkAssociatorHom κ then let (ex₀, ey₀, ez₀) ← getMEFromThreeProds args[args.size - 2]! - let (associatorExpr, associator_hom_proof) ← constructAssociatorHom X Y ex₀ ey₀ ez₀ - return (associatorExpr, associator_hom_proof :: proofs) + constructAssociatorHom X Y ex₀ ey₀ ez₀ else if ← checkAssociatorInv κ then let (ex₀, ey₀, ez₀) ← getMEFromThreeProds args[args.size - 3]! - let (associatorInvExpr, associator_inv_hom_proof) ← constructAssociatorInv X Y ex₀ ey₀ ez₀ - return (associatorInvExpr, associator_inv_hom_proof :: proofs) + constructAssociatorInv X Y ex₀ ey₀ ez₀ else let SX ← computeSFinkerOf X xLvl let SY ← computeSFinkerOf Y yLvl let homExpr ← mkAppOptM ``ProbabilityTheory.Kernel.hom #[X, Y, none, none, SX, SY, (← idME X), (← idME Y), e, none] - pure (homExpr, proofs) + return (homExpr, ← mkEqRefl homExpr) | _ => throwError "Expected a lifted kernel expression, got: {e}." -/-- Construct the proof of equivalence between the original equality and the transformed one. -/ -def mkKernelHomEqProof (eqProofType lhs rhs : Expr) (proofs : List Expr) : MetaM Expr := do - let mvar ← mkFreshExprSyntheticOpaqueMVar eqProofType - let mvarId := mvar.mvarId! - let propext := mkConst ``propext - match ← mvarId.apply propext with - | [mvarId] => - let proofs := proofs.reverse - let mut mvarId := mvarId - for proof in proofs do - mvarId ← mvarId.nthRewrite 1 proof - let (X, Y, xLvl, yLvl) ← getTypesFromKernel lhs - let SX ← computeSFinkerOf X xLvl - let SY ← computeSFinkerOf Y yLvl - let e ← mkAppMInst ``hom_congr #[SX, SY, ← idME X, ← idME Y, lhs, rhs] 2 - unless ← isDefEq (← mvarId.getType) (← inferType e) do - throwError "Type mismatch: expected {← mvarId.getType}, got {← inferType e}." - mvarId.assign e - instantiateMVars mvar - | _ => - throwError "Failed to apply propext while building kernel_hom equivalence proof for - {eqProofType}." +/-- Given lifted kernels `lhs rhs` and morphisms `lh rh` with proofs `pl : lh = lhs.hom` and +`pr : rh = rhs.hom`, construct a proof of `(lhs = rhs) = (lh = rh)`. -/ +def mkHomCongrProof (lhs rhs pl pr : Expr) : MetaM Expr := do + let (X, Y, xLvl, yLvl) ← getTypesFromKernel lhs + let SX ← computeSFinkerOf X xLvl + let SY ← computeSFinkerOf Y yLvl + let hom_congr_proof ← mkAppMInst ``hom_congr #[SX, SY, ← idME X, ← idME Y, lhs, rhs] 2 + mkEqTrans (← mkPropExt hom_congr_proof) (← mkEqSymm (← mkEqCongr pl pr)) /-- Transform a kernel equality into an equivalent equality in `SFinKer`, along with a proof of -equivalence. -/ -def HomEquality (eq : Expr) : MetaM (Expr × Expr) := do +equivalence. The equality is first lifted to a common universe level using `lift`. -/ +def HomEqualityWith (lift : Expr → MetaM (Expr × Expr)) (eq : Expr) : MetaM (Expr × Expr) := do let eq ← unfoldKernelOp eq - let (lifted_expr, lifted_proof) ← liftEquality eq + let (lifted_expr, lifted_proof) ← lift eq let some (_, lhs, rhs) := lifted_expr.eq? | throwError "Expected an equality, got: {lifted_expr}." - let (lhs_hom, proofs) ← transformKernelToHom lhs [] - let (rhs_hom, proofs) ← transformKernelToHom rhs proofs + let (lhs_hom, pl) ← transformKernelToHom lhs + let (rhs_hom, pr) ← transformKernelToHom rhs let hom_expr ← mkEq lhs_hom rhs_hom - let hom_eq_proof_type ← mkEq lifted_expr hom_expr - let hom_eq_proof ← mkKernelHomEqProof hom_eq_proof_type lhs rhs proofs + let hom_eq_proof ← mkHomCongrProof lhs rhs pl pr return (hom_expr, ← mkEqTrans lifted_proof hom_eq_proof) +/-- Transform a kernel equality into an equivalent equality in `SFinKer`, along with a proof of +equivalence. -/ +def HomEquality : Expr → MetaM (Expr × Expr) := HomEqualityWith liftEquality + /-- The `kernel_hom` tactic transforms a kernel equality to an equivalent equality in the category of measurable spaces and s-finite kernels. diff --git a/KernelHom/Tactic/Reassoc.lean b/KernelHom/Tactic/Reassoc.lean index 50d48c7aa..eb2de01f2 100644 --- a/KernelHom/Tactic/Reassoc.lean +++ b/KernelHom/Tactic/Reassoc.lean @@ -23,16 +23,8 @@ open Lean Meta Elab Tactic ProbabilityTheory Mathlib.Tactic Reassoc /-- Same as `HomEquality`, but allows specifying a universe level that will be taken into account when computing the maximum universe level. -/ -def HomEqualityToLvl (eq : Expr) (Lvl : Level) : MetaM (Expr × Expr) := do - let eq ← unfoldKernelOp eq - let (lifted_expr, lifted_proof) ← liftEqualityWithLevel Lvl eq - let some (_, lhs, rhs) := lifted_expr.eq? | throwError "Expected an equality, got: {lifted_expr}." - let (lhs_hom, proofs) ← transformKernelToHom lhs [] - let (rhs_hom, proofs) ← transformKernelToHom rhs proofs - let hom_expr ← mkEq lhs_hom rhs_hom - let hom_eq_proof_type ← mkEq lifted_expr hom_expr - let hom_eq_proof ← mkKernelHomEqProof hom_eq_proof_type lhs rhs proofs - return (hom_expr, ← mkEqTrans lifted_proof hom_eq_proof) +def HomEqualityToLvl (eq : Expr) (Lvl : Level) : MetaM (Expr × Expr) := + HomEqualityWith (liftEqualityWithLevel Lvl) eq /-- Replace all level metavariables appearing in an expression with named level parameters. -/ def freshenLevelParam (e : Expr) : MetaM Expr := do @@ -65,10 +57,9 @@ def kernelReassocHandler (h_eq : Expr) : MetaM (Expr × Array LMVarId) := do let (_, hom_proof) ← HomEqualityToLvl eq_type u let hom_proof ← mkAppM ``Eq.mp #[hom_proof, h_eq] let (hom_proof_reassoc, _) ← reassocExprHom hom_proof - let univs ← collectExprUniverses eq_type - let maxLvl ← computeMaxLevel <| u :: univs - let (ξ_lift, _) ← liftKernel ξ maxLvl [] - let (ξ_hom, _) ← transformKernelToHom ξ_lift [] + let maxLvl ← computeMaxLevel <| u :: (← collectEqUniverses eq_type) + let (ξ_lift, _) ← liftKernel ξ maxLvl + let (ξ_hom, _) ← transformKernelToHom ξ_lift let reassoc_body ← mkAppM' hom_proof_reassoc #[ξ_hom] let (_, kernel_reassoc_proof) ← KernelEquality <| ← inferType reassoc_body let kernel_reassoc_proof ← mkAppM ``Eq.mp #[kernel_reassoc_proof, reassoc_body] diff --git a/KernelHom/Tactic/Utils.lean b/KernelHom/Tactic/Utils.lean index 435015f48..f79dc20ac 100644 --- a/KernelHom/Tactic/Utils.lean +++ b/KernelHom/Tactic/Utils.lean @@ -29,9 +29,3 @@ def Lean.Meta.mkAppMInst (constName : Name) (xs : Array Expr) (n_impls : Nat) : let e ← mkAppM constName xs let nones : Array (Option Expr) := Array.replicate n_impls none mkAppOptM' e nones - -/-- Similar to `mkAppMInst`, but takes an `Expr` instead of a constant name. -/ -def Lean.Meta.mkAppMInst' (f : Expr) (xs : Array Expr) (n_insts : Nat) : MetaM Expr := do - let e ← mkAppM' f xs - let nones : Array (Option Expr) := Array.replicate n_insts none - mkAppOptM' e nones diff --git a/KernelHomManual/Front.lean b/KernelHomManual/Front.lean index db5018767..f1b759d2a 100644 --- a/KernelHomManual/Front.lean +++ b/KernelHomManual/Front.lean @@ -46,7 +46,7 @@ The library introduces two main tactics: - {name kernelHom}`kernel_hom` : transforms a kernel equality into an equality in the monoidal category. - {name homKernel}`kernel_hom` : performs the inverse transformation, bringing the categorical equality back to a kernel equality. -These tactics allow users to transform complex kernel equalities into categorical equalities, where powerful categorical tactics can be applied to simplify or prove them. To this end, the library provides built-in helpers like {name kernelMonoidal}`kernel_monoidal` and {name kernelCoherence}`kernel_coherence` to apply categorical tactics directly to kernels without needing to manually invoke the translation tactics. +These tactics allow users to transform complex kernel equalities into categorical equalities, where powerful categorical tactics can be applied to simplify or prove them. To this end, the library provides built-in helpers like {name kernelMonoidal}`kernel_monoidal`, {name kernelCoherence}`kernel_coherence`, {name kernelDisch}`kernel_disch` and {name aesopKernel}`aesop_kernel` to apply categorical tactics directly to kernels without needing to manually invoke the translation tactics. The library rests on {name SFinKer}`SFinKer`, the category of measurable spaces with s-finite kernels as morphisms, equipped with monoidal and symmetric structures. This category is also used to define {name Stoch}`Stoch`, the category of measurable spaces with Markov kernels as morphisms, which is a wide subcategory of {name SFinKer}`SFinKer` (see {citep fritz2020}[]). Both categories have been merged into Mathlib (PR [#36779](https://github.com/leanprover-community/mathlib4/pull/36779)). diff --git a/KernelHomManual/Pages/CatTactics.lean b/KernelHomManual/Pages/CatTactics.lean index c4982837a..2f652726f 100644 --- a/KernelHomManual/Pages/CatTactics.lean +++ b/KernelHomManual/Pages/CatTactics.lean @@ -20,7 +20,7 @@ set_option verso.code.warnLineLength 100 htmlSplit := .never %%% -Two of the most powerful tactics for categories is Mathlib are {name Monoidal.monoidal}`monoidal` and {name Coherence.coherence}`coherence`. To facilitate the use of these tactics for kernel equalities, *Kernel-Hom* provide the {name kernelMonoidal}`kernel_monoidal`, {name kernelCoherence}`kernel_coherence`, and the {name kernelDisch}`kernel_disch` tactics which first apply {name kernelHom}`kernel_hom` to the goal to translate the kernel equality into a categorical equality in the {name SFinKer}`SFinKer` category, then apply {name Monoidal.monoidal}`monoidal`, {name Coherence.coherence}`coherence`, or {name CategoryTheory.categoryTheoryDischarger}`cat_disch` to solve or simplify the categorical equality. +Two of the most powerful tactics for categories is Mathlib are {name Monoidal.monoidal}`monoidal` and {name Coherence.coherence}`coherence`. To facilitate the use of these tactics for kernel equalities, *Kernel-Hom* provide the {name kernelMonoidal}`kernel_monoidal`, {name kernelCoherence}`kernel_coherence`, {name kernelDisch}`kernel_disch` and {name aesopKernel}`aesop_kernel` tactics which first apply {name kernelHom}`kernel_hom` to the goal to translate the kernel equality into a categorical equality in the {name SFinKer}`SFinKer` category, then apply {name Monoidal.monoidal}`monoidal`, {name Coherence.coherence}`coherence`, {name CategoryTheory.categoryTheoryDischarger}`cat_disch` or `aesop` (with the `CategoryTheory` rule set) to solve or simplify the categorical equality. {docstring kernelMonoidal} @@ -28,4 +28,6 @@ Two of the most powerful tactics for categories is Mathlib are {name Monoidal.mo {docstring kernelDisch} +{docstring aesopKernel} + For more details on the implementation of the {name Monoidal.monoidal}`monoidal` and {name Coherence.coherence}`coherence` tactics, see the [documentation](https://yuma-mizuno.github.io/coherence-tactics/) made by [@Yuma Mizuno](https://yuma-mizuno.github.io/). diff --git a/KernelHomManual/Pages/Examples.lean b/KernelHomManual/Pages/Examples.lean index 97b396047..00e7c4c97 100644 --- a/KernelHomManual/Pages/Examples.lean +++ b/KernelHomManual/Pages/Examples.lean @@ -61,7 +61,9 @@ The library provides several tactics for working with s-finite kernels equalitie - {name kernelDisch}`kernel_disch`: Applies the {name CategoryTheory.categoryTheoryDischarger}`cat_disch` tactic to a s-finite kernel equality. -Basically, whenever you have a equality of s-finite kernels that you want to simplify, you can apply {name kernelHom}`kernel_hom` to transform it into a categorical equality, try applying categorical tactics, simps, or manually manipulate it, and then apply {name homKernel}`hom_kernel` to get back to a kernel equality if needed. The built-in helpers {name kernelMonoidal}`kernel_monoidal` and {name kernelCoherence}`kernel_coherence` directly apply categorical tactics to kernels without needing to manually invoke the translation tactic. +- {name aesopKernel}`aesop_kernel`: Applies `aesop` with the `CategoryTheory` rule set to a s-finite kernel equality, without the `rfl_cat` attempt of {name CategoryTheory.categoryTheoryDischarger}`cat_disch`. + +Basically, whenever you have a equality of s-finite kernels that you want to simplify, you can apply {name kernelHom}`kernel_hom` to transform it into a categorical equality, try applying categorical tactics, simps, or manually manipulate it, and then apply {name homKernel}`hom_kernel` to get back to a kernel equality if needed. The built-in helpers {name kernelMonoidal}`kernel_monoidal`, {name kernelCoherence}`kernel_coherence`, {name kernelDisch}`kernel_disch` and {name aesopKernel}`aesop_kernel` directly apply categorical tactics to kernels without needing to manually invoke the translation tactic. *Kernel diagrams* diff --git a/KernelHomTests.lean b/KernelHomTests.lean index 7828cbe54..eb22620c0 100644 --- a/KernelHomTests.lean +++ b/KernelHomTests.lean @@ -2,3 +2,4 @@ module -- shake: keep-all --deprecated_module: ignore public import KernelHomTests.Examples public import KernelHomTests.Tests +public import KernelHomTests.Time diff --git a/KernelHomTests/Tests.lean b/KernelHomTests/Tests.lean index 7c403e848..560a8c1d5 100644 --- a/KernelHomTests/Tests.lean +++ b/KernelHomTests/Tests.lean @@ -92,3 +92,7 @@ example (κ : Kernel Z Y) [IsSFiniteKernel κ] : simp only [ComonObj.counit_comul_hom] hom_kernel rfl + +example (κ : Kernel X Y) (η : Kernel Z W) [IsSFiniteKernel κ] [IsSFiniteKernel η] : + Kernel.swap Y W ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ Kernel.swap X Z := by + aesop_kernel diff --git a/KernelHomTests/Time.lean b/KernelHomTests/Time.lean new file mode 100644 index 000000000..305b4da4d --- /dev/null +++ b/KernelHomTests/Time.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2026 Gaëtan Serré. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gaëtan Serré +-/ +module + +public import KernelHom +public import Mathlib.Probability.Kernel.Composition.KernelLemmas + +/-! +# Timing of Kernel-Hom proofs + +Each lemma is proved twice: with its original Mathlib proof (`_orig`) and with Kernel-Hom (`_kh`). +Only lemmas whose Mathlib proof is a complete proof by integral manipulations are kept, so that the +comparison is meaningful. `trace.profiler` reports the elaboration time of each declaration. +-/ + +public section + +open MeasureTheory ProbabilityTheory Kernel CategoryTheory + +set_option trace.profiler true +set_option trace.profiler.threshold 10 + +variable {X Y Z T X' Y' Z' : Type*} [MeasurableSpace X] [MeasurableSpace Y] + [MeasurableSpace Z] [MeasurableSpace T] [MeasurableSpace X'] [MeasurableSpace Y'] + [MeasurableSpace Z'] + +variable {κ : Kernel X Y} {ξ : Kernel Z T} {η : Kernel Y Z} + +lemma swap_parallelComp_orig : swap Y T ∘ₖ (κ ∥ₖ ξ) = ξ ∥ₖ κ ∘ₖ swap X Z := by + by_cases hκ : IsSFiniteKernel κ + swap; · simp [hκ] + by_cases hη : IsSFiniteKernel ξ + swap; · simp [hη] + ext ac s hs + simp_rw [comp_apply, parallelComp_apply, Measure.bind_apply hs (Kernel.aemeasurable _), + swap_apply, lintegral_dirac' _ (Kernel.measurable_coe _ hs), parallelComp_apply' hs, + Prod.fst_swap, Prod.snd_swap] + rw [MeasureTheory.lintegral_prod_symm] + swap; · exact ((Kernel.id.measurable_coe hs).comp measurable_swap).aemeasurable + congr with d + simp_rw [Prod.swap_prod_mk, Measure.dirac_apply' _ hs, ← Set.indicator_comp_right, + lintegral_indicator (measurable_prodMk_left hs)] + simp + +lemma swap_parallelComp_kh : swap Y T ∘ₖ (κ ∥ₖ ξ) = ξ ∥ₖ κ ∘ₖ swap X Z := by + by_cases hκ : IsSFiniteKernel κ + swap; · simp [hκ] + by_cases hη : IsSFiniteKernel ξ + swap; · simp [hη] + kernel_hom + aesop_cat + +variable [IsSFiniteKernel η] [IsSFiniteKernel ξ] + +lemma parallelComp_id_left_comp_parallelComp_orig : + (Kernel.id ∥ₖ ξ) ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η) := by + by_cases hκ : IsSFiniteKernel κ + swap; · simp [hκ] + ext a s hs + rw [comp_apply' _ _ _ hs, parallelComp_apply, + MeasureTheory.lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable] + rw [parallelComp_apply, Measure.prod_apply hs] + congr with x + rw [comp_apply' _ _ _ (measurable_prodMk_left hs)] + congr with y + rw [parallelComp_apply' hs, Kernel.id_apply, + lintegral_dirac' _ (measurable_measure_prodMk_left hs)] + +lemma parallelComp_id_left_comp_parallelComp_kh : + (Kernel.id ∥ₖ ξ) ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η) := by + by_cases hκ : IsSFiniteKernel κ + swap; · simp [hκ] + kernel_monoidal diff --git a/lake-manifest.json b/lake-manifest.json index 566962f73..2c2cd68f7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "364b383469ab9c4e428a5325f0623acfdd41fd4c", + "rev": "63025c440a76f080d28ec38a8469e53d46809926", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d2ec8cf5cb72722a5c8b06661e900966a126a60d", + "rev": "e77bb5fe78158b37ba9907962055d8e5e5593782", "name": "eqlift", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "805cdb5a0feb2b2bf4d1d50963521f22660ec7ee", + "rev": "27444dfe4a89c26b4ca8a29d73939b536e347162", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669", + "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2bc7cf064315b26bc38dac2e9612fb581be9b75f", + "rev": "ba67e212be1197b84c1f1f6299488a10a3002713", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "978b7ec9fbbf9a535114f1de8fe5b3778b358870", + "rev": "1681d78dd6e65e38b143f9740d829c826673807c", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ebeca04ecd5ee2ba9740e13576d80d4ab6b5779c", + "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c1c4362a130f12e632d252180a6c2a31d8fd4726", + "rev": "18889deb9e83ea7420ef51c160d6f88552e744e3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3b55e9d00c6b0018e5d984eb011b6f93c09bd163", + "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,17 +95,27 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "36cc05ca2d0e469bfbeea9437f460e19238e885e", + "rev": "3b4ce082a2051785ac99f899a50c55d43b6d9c28", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.34.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/illuminate", "type": "git", "subDir": null, "scope": "", - "rev": "76f052847294d189dc9924a33466b4b677f47e67", + "rev": "6e558472c981dbee8cb9fcde92fa9593daf04228", "name": "illuminate", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -125,22 +135,12 @@ "type": "git", "subDir": null, "scope": "", - "rev": "847084e80500726e4331dded5f17007ddaf89c31", + "rev": "fda188f7329fa18ce4b2e8cc96c9b0a8f0c78c46", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "af8bc067a4cc6c6df472a68909a3f40b1c76c43e", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0-rc1", - "inherited": true, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.lean"}], "name": "KernelHom", "lakeDir": ".lake", "fixedToolchain": false} diff --git a/lean-toolchain b/lean-toolchain index e2a0e3569..d5ae4e312 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0-rc1 \ No newline at end of file +leanprover/lean4:v4.34.0-rc2 \ No newline at end of file From 9850f741e0d454a9f7f2d642ca9c346333276856 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Fri, 11 Sep 2026 19:32:12 +0200 Subject: [PATCH 3/3] Memoization --- .github/workflows/build-doc.yml | 2 +- .github/workflows/build-project.yml | 2 +- KernelHom/Kernel/Hom.lean | 15 +- KernelHom/Tactic/HomKernel.lean | 151 ++++++++---------- KernelHom/Tactic/KernelHom.lean | 211 +++++++++---------------- KernelHom/Tactic/Reassoc.lean | 2 +- KernelHom/Tactic/Utils.lean | 193 +++++++++++++++++++++- KernelHomManual/Front.lean | 7 + KernelHomManual/Pages/Performance.lean | 80 ++++++++++ KernelHomTests.lean | 2 +- KernelHomTests/Heartbeats.lean | 154 ++++++++++++++++++ KernelHomTests/Time.lean | 76 --------- README.md | 4 + lake-manifest.json | 4 +- lakefile.toml | 1 + 15 files changed, 594 insertions(+), 310 deletions(-) create mode 100644 KernelHomManual/Pages/Performance.lean create mode 100644 KernelHomTests/Heartbeats.lean delete mode 100644 KernelHomTests/Time.lean diff --git a/.github/workflows/build-doc.yml b/.github/workflows/build-doc.yml index 3d89533a0..215a011b3 100644 --- a/.github/workflows/build-doc.yml +++ b/.github/workflows/build-doc.yml @@ -49,7 +49,7 @@ jobs: uses: leanprover/lean-action@a811f12834a45345026c26b89eea877e0ddad406 # 2026-01-15 with: build: true - lint: false + lint: true mk_all-check: false - name: Lint project diff --git a/.github/workflows/build-project.yml b/.github/workflows/build-project.yml index 02c9e6c91..138286c09 100644 --- a/.github/workflows/build-project.yml +++ b/.github/workflows/build-project.yml @@ -40,7 +40,7 @@ jobs: uses: leanprover/lean-action@a811f12834a45345026c26b89eea877e0ddad406 # 2026-01-15 with: build: true - lint: false + lint: true mk_all-check: false - name: Lint project diff --git a/KernelHom/Kernel/Hom.lean b/KernelHom/Kernel/Hom.lean index 25823ee0f..af7180fa3 100644 --- a/KernelHom/Kernel/Hom.lean +++ b/KernelHom/Kernel/Hom.lean @@ -27,12 +27,14 @@ open scoped SFinKer CategoryTheory CategoryTheory.MonoidalCategory namespace ProbabilityTheory.Kernel -variable {X Y T Z : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace T] - [MeasurableSpace Z] +universe x y t z u x₀ y₀ z₀ + +variable {X : Type x} {Y : Type y} {T : Type t} {Z : Type z} [MeasurableSpace X] [MeasurableSpace Y] + [MeasurableSpace T] [MeasurableSpace Z] section -variable {SX SY ST SZ : SFinKer} {ex : SX ≃ᵐ X} {ey : SY ≃ᵐ Y} +variable {SX SY ST SZ : SFinKer.{u}} {ex : SX ≃ᵐ X} {ey : SY ≃ᵐ Y} /-- Transform a morphism in `SFinKer` into a kernel. -/ noncomputable def fromHom (κ : SX ⟶ SY) : Kernel X Y := (κ.1.comap ex.symm (by fun_prop)).map ey @@ -97,7 +99,7 @@ instance {κ : Kernel X Y} [IsDeterministic κ] [IsMarkovKernel κ] : end -lemma hom_congr (SX SY : SFinKer) (ex : SX ≃ᵐ X) (ey : SY ≃ᵐ Y) +lemma hom_congr (SX SY : SFinKer.{u}) (ex : SX ≃ᵐ X) (ey : SY ≃ᵐ Y) (κ η : Kernel X Y) [IsSFiniteKernel κ] [IsSFiniteKernel η] : κ = η ↔ κ.hom (ex := ex) (ey := ey) = η.hom (ex := ex) (ey := ey) := by constructor @@ -114,7 +116,7 @@ lemma hom_congr (SX SY : SFinKer) (ex : SX ≃ᵐ X) (ey : SY ≃ᵐ Y) section -variable (SX SY SZ ST : SFinKer) (ex : SX ≃ᵐ X) (ey : SY ≃ᵐ Y) (ez : SZ ≃ᵐ Z) (et : ST ≃ᵐ T) +variable (SX SY SZ ST : SFinKer.{u}) (ex : SX ≃ᵐ X) (ey : SY ≃ᵐ Y) (ez : SZ ≃ᵐ Z) (et : ST ≃ᵐ T) lemma comp_hom (η : Kernel X Y) (κ : Kernel Z X) [IsSFiniteKernel η] [IsSFiniteKernel κ] : κ.hom (ex := ez) (ey := ex) ≫ η.hom (ex := ex) (ey := ey) = @@ -196,7 +198,8 @@ lemma braiding_hom : (β_ SX SY).hom = congr with x all_goals simp [MeasurableEquiv.prodCongr] -variable {X₀ Y₀ Z₀ : Type*} [MeasurableSpace X₀] [MeasurableSpace Y₀] [MeasurableSpace Z₀] +variable {X₀ : Type x₀} {Y₀ : Type y₀} {Z₀ : Type z₀} [MeasurableSpace X₀] [MeasurableSpace Y₀] + [MeasurableSpace Z₀] (ex₀ : X ≃ᵐ X₀) (ey₀ : Y ≃ᵐ Y₀) (ez₀ : Z ≃ᵐ Z₀) lemma leftUnitor_hom : (λ_ SX).hom = hom (ex := punit.prodCongr ex) (ey := ex) diff --git a/KernelHom/Tactic/HomKernel.lean b/KernelHom/Tactic/HomKernel.lean index 61032c557..799b401e6 100644 --- a/KernelHom/Tactic/HomKernel.lean +++ b/KernelHom/Tactic/HomKernel.lean @@ -45,31 +45,6 @@ partial def getTypeFromSFinKer (e : Expr) : MetaM Expr := do mkAppOptM ``Prod #[X, Y] | _ => throwError "Expected a SFinKer.of expression, got: {e}." -/-- Deconstruct a left or right whisker. -/ -def deconstructWhiskersHomArgs (e : Expr) (eLvl : Level) (left : Bool) : - MetaM (Expr × Expr × Expr × Expr × Expr × Expr × Expr × Expr) := do - let args := e.getAppArgs - let SZ := if left then args[args.size - 4]! else args[args.size - 1]! - let SY := if left then args[args.size - 2]! else args[args.size - 3]! - let SX := if left then args[args.size - 3]! else args[args.size - 4]! - let κ := if left then args[args.size - 1]! else args[args.size - 2]! - let Z ← getTypeFromSFinKer SZ - let Y ← getTypeFromSFinKer SY - let X ← getTypeFromSFinKer SX - let mXUnit ← synthInstance (mkApp (mkConst ``MeasurableSpace [eLvl]) Z) - let kernel_id ← mkAppOptM ``Kernel.id #[Z, mXUnit] - return (κ, kernel_id, SX, SY, SZ, X, Y, Z) - -/-- Deconstruct a braiding morphism. -/ -def deconstructBraiding (e : Expr) : MetaM (Expr × Expr) := do - let args := e.getAppArgs - let SY := args[args.size - 1]! - let SX := args[args.size - 2]! - let Y ← getTypeFromSFinKer SY - let X ← getTypeFromSFinKer SX - let swap_hom_proof ← mkAppM ``braiding_hom #[SX, SY, ← idME X, ← idME Y] - return (← mkAppOptM ``Kernel.swap #[X, Y, none, none], swap_hom_proof) - /-- Given an equality between a categorical morphism (left) and a "morphized" kernel (right), get the kernel on the right side of the equality. -/ def getKernelRHSEqProofType (e : Expr) : MetaM Expr := do @@ -86,10 +61,10 @@ def deconstructUnitors (e : Expr) (eLvl : Level) (left hom : Bool) : let args := e.getAppArgs let SX := args[args.size - 1]! let X ← getTypeFromSFinKer SX - let ex ← idME X + let ex ← idME X eLvl let (X₀, x₀Lvl) ← getOriginalType X - let ex₀ ← constructMeasurableEquiv X₀ x₀Lvl eLvl - let const_args := [eLvl, x₀Lvl, eLvl, Level.zero] + let (ex₀, _) ← constructMeasurableEquiv X₀ x₀Lvl eLvl + let const_args := [eLvl, eLvl, x₀Lvl, Level.zero] let const_name := if left then if hom then ``leftUnitor_hom @@ -113,93 +88,105 @@ def deconstructAssociator (e : Expr) (eLvl : Level) (hom : Bool) : MetaM (Expr let (Z₀, z₀Lvl) ← getOriginalType Z let (Y₀, y₀Lvl) ← getOriginalType Y let (X₀, x₀Lvl) ← getOriginalType X - let ez₀ ← constructMeasurableEquiv Z₀ z₀Lvl eLvl - let ey₀ ← constructMeasurableEquiv Y₀ y₀Lvl eLvl - let ex₀ ← constructMeasurableEquiv X₀ x₀Lvl eLvl + let (ez₀, _) ← constructMeasurableEquiv Z₀ z₀Lvl eLvl + let (ey₀, _) ← constructMeasurableEquiv Y₀ y₀Lvl eLvl + let (ex₀, _) ← constructMeasurableEquiv X₀ x₀Lvl eLvl let associator_const := mkConst (if hom then ``Kernel.associator_hom else ``Kernel.associator_inv) - [eLvl, eLvl, eLvl, x₀Lvl, y₀Lvl, z₀Lvl, eLvl] + [eLvl, eLvl, eLvl, eLvl, x₀Lvl, y₀Lvl, z₀Lvl] let associator_proof_eq ← mkAppM' associator_const - #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, ex₀, ey₀, ez₀] + #[SX, SY, SZ, ← idME X eLvl, ← idME Y eLvl, ← idME Z eLvl, ex₀, ey₀, ez₀] return (← getKernelRHSEqProofType associator_proof_eq, associator_proof_eq) +/-- The `HomCarrier` of the carrier of an object of `SFinKer` living in universe `u`. -/ +def homCarrierOfObj (SX : Expr) (u : Level) : MetaM HomCarrier := do + HomCarrier.mk' ⟨← getTypeFromSFinKer SX, u⟩ + /-- Recursive transformation from morphism expression in `SFinKer` to kernel expression. Returns the kernel expression `e'` together with a proof of `e = e'.hom`, built by congruence from -the translation lemmas. -/ +the translation lemmas (`comp_hom`, `parallelComp_hom`, ...). -/ partial def transformHomToKernel (e : Expr) : MetaM (Expr × Expr) := do match e.getAppFn with | Expr.const ``tensorHom _ => let args := e.getAppArgs let κ := args[args.size - 2]! let η := args[args.size - 1]! - let ST := args[args.size - 3]! - let SZ := args[args.size - 4]! - let SY := args[args.size - 5]! - let SX := args[args.size - 6]! let (κ', pκ) ← transformHomToKernel κ let (η', pη) ← transformHomToKernel η - let (X, Y, _, _) ← getTypesFromKernel κ' - let (Z, T, _, _) ← getTypesFromKernel η' - let parallelComp_hom_proof ← mkAppMInst ``parallelComp_hom - #[SX, SY, SZ, ST, ← idME X, ← idME Y, ← idME Z, ← idME T, κ', η'] 2 + let (X, Y) ← getCarriersFromKernel κ' + let (Z, T) ← getCarriersFromKernel η' + let (X, Y, Z, T) := + (← HomCarrier.mk' X, ← HomCarrier.mk' Y, ← HomCarrier.mk' Z, ← HomCarrier.mk' T) + let pf := mkAppN (mkConst ``parallelComp_hom [X.lvl, Y.lvl, T.lvl, Z.lvl, X.lvl]) + (typeInstArgs #[X, Y, T, Z] ++ objEquivArgs #[X, Y, Z, T] ++ + #[κ', η', ← Z.sfinite T η', ← X.sfinite Y κ']) let h ← mkCongr (← mkCongrArg e.appFn!.appFn! pκ) pη - return (← mkAppM ``Kernel.parallelComp #[κ', η'], ← mkEqTrans h parallelComp_hom_proof) + let e' ← mkKernelParallelComp X Y Z T κ' η' + return (e', ← mkEqTrans h pf) | Expr.const ``CategoryStruct.comp _ => let args := e.getAppArgs let κ := args[args.size - 2]! let η := args[args.size - 1]! - let SY := args[args.size - 3]! - let SX := args[args.size - 4]! - let SZ := args[args.size - 5]! let (κ', pκ) ← transformHomToKernel κ let (η', pη) ← transformHomToKernel η - let (X, Y, _, _) ← getTypesFromKernel η' - let (Z, _, _, _) ← getTypesFromKernel κ' - let comp_hom_proof ← mkAppMInst ``comp_hom - #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, η', κ'] 2 + let (X, Y) ← getCarriersFromKernel η' + let (Z, _) ← getCarriersFromKernel κ' + let (X, Y, Z) := (← HomCarrier.mk' X, ← HomCarrier.mk' Y, ← HomCarrier.mk' Z) + let pf := mkAppN (mkConst ``comp_hom [X.lvl, Y.lvl, Z.lvl, X.lvl]) + (homLemmaArgs #[X, Y, Z] ++ + #[η', κ', ← X.sfinite Y η', ← Z.sfinite X κ']) let h ← mkCongr (← mkCongrArg e.appFn!.appFn! pκ) pη - return (← mkAppM ``Kernel.comp #[η', κ'], ← mkEqTrans h comp_hom_proof) - | Expr.const ``CategoryStruct.id [xLvl, _] => + return (← mkKernelComp Z X Y η' κ', ← mkEqTrans h pf) + | Expr.const ``CategoryStruct.id [u, _] => let args := e.getAppArgs - let SX := args[args.size - 1]! - let X ← getTypeFromSFinKer SX - let mX' ← synthInstance (mkApp (mkConst ``MeasurableSpace [xLvl]) X) - let id ← mkAppOptM ``Kernel.id #[X, mX'] - return (id, ← mkAppM ``id_hom #[SX, ← idME X]) - | Expr.const ``ComonObj.counit [xLvl, _] => + let X ← homCarrierOfObj args[args.size - 1]! u + return (← mkKernelId X, mkAppN (mkConst ``id_hom [u, u]) (homLemmaArgs #[X])) + | Expr.const ``ComonObj.counit [u, _] => let args := e.getAppArgs - let SX := args[args.size - 2]! - let X ← getTypeFromSFinKer SX - let discard_hom_proof ← mkAppM' (mkConst ``counit [xLvl, xLvl, xLvl]) #[SX, ← idME X] - return (← mkAppOptM' (mkConst ``Kernel.discard [xLvl, xLvl]) #[X, none], discard_hom_proof) - | Expr.const ``ComonObj.comul [xLvl, _] => + let X ← homCarrierOfObj args[args.size - 2]! u + return (← mkKernelDiscard X u, + mkAppN (mkConst ``counit [u, u, u]) (homLemmaArgs #[X])) + | Expr.const ``ComonObj.comul [u, _] => let args := e.getAppArgs - let SX := args[args.size - 2]! - let X ← getTypeFromSFinKer SX - return (← mkAppOptM' (mkConst ``Kernel.copy [xLvl]) #[X, none], - ← mkAppM ``comul #[SX, ← idME X]) + let X ← homCarrierOfObj args[args.size - 2]! u + return (← mkKernelCopy X, mkAppN (mkConst ``comul [u, u]) (homLemmaArgs #[X])) | Expr.const ``Kernel.hom _ => let args := e.getAppArgs return (args[args.size - 2]!, ← mkEqRefl e) - | Expr.const ``MonoidalCategory.whiskerLeft [eLvl, _] => - let (κ, kernel_id, SX, SY, SZ, X, Y, Z) ← deconstructWhiskersHomArgs e eLvl true - let (κ', pκ) ← transformHomToKernel κ - let whisker_left_hom_proof ← mkAppMInst ``Kernel.whiskerLeft - #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ'] 1 + | Expr.const ``MonoidalCategory.whiskerLeft [u, _] => + let args := e.getAppArgs + let Z ← homCarrierOfObj args[args.size - 4]! u + let X ← homCarrierOfObj args[args.size - 3]! u + let Y ← homCarrierOfObj args[args.size - 2]! u + let (κ', pκ) ← transformHomToKernel args[args.size - 1]! + let pf := mkAppN (mkConst ``Kernel.whiskerLeft [u, u, u, u]) + (homLemmaArgs #[X, Y, Z] ++ #[κ', ← X.sfinite Y κ']) let h ← mkCongrArg e.appFn! pκ - return (← mkAppM ``Kernel.parallelComp #[kernel_id, κ'], ← mkEqTrans h whisker_left_hom_proof) - | Expr.const ``MonoidalCategory.whiskerRight [eLvl, _] => - let (κ, kernel_id, SX, SY, SZ, X, Y, Z) ← deconstructWhiskersHomArgs e eLvl false - let (κ', pκ) ← transformHomToKernel κ - let whisker_right_hom_proof ← mkAppMInst ``Kernel.whiskerRight - #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ'] 1 - let h ← mkCongrFun (← mkCongrArg e.appFn!.appFn! pκ) SZ - return (← mkAppM ``Kernel.parallelComp #[κ', kernel_id], ← mkEqTrans h whisker_right_hom_proof) + let e' ← mkKernelParallelComp Z Z X Y + (← mkKernelId Z) κ' + return (e', ← mkEqTrans h pf) + | Expr.const ``MonoidalCategory.whiskerRight [u, _] => + let args := e.getAppArgs + let X ← homCarrierOfObj args[args.size - 4]! u + let Y ← homCarrierOfObj args[args.size - 3]! u + let Z ← homCarrierOfObj args[args.size - 1]! u + let (κ', pκ) ← transformHomToKernel args[args.size - 2]! + let pf := mkAppN (mkConst ``Kernel.whiskerRight [u, u, u, u]) + (homLemmaArgs #[X, Y, Z] ++ #[κ', ← X.sfinite Y κ']) + let h ← mkCongrFun (← mkCongrArg e.appFn!.appFn! pκ) Z.obj + let e' ← mkKernelParallelComp X Y Z Z κ' + (← mkKernelId Z) + return (e', ← mkEqTrans h pf) | Expr.const ``Iso.hom _ => let args := e.getAppArgs let iso := args[args.size - 1]! match iso.getAppFn with - | Expr.const ``BraidedCategory.braiding _ => deconstructBraiding iso + | Expr.const ``BraidedCategory.braiding [u, _] => + let args := iso.getAppArgs + let X ← homCarrierOfObj args[args.size - 2]! u + let Y ← homCarrierOfObj args[args.size - 1]! u + return (← mkKernelSwap X Y, + mkAppN (mkConst ``braiding_hom [u, u, u]) (homLemmaArgs #[X, Y])) | Expr.const ``leftUnitor [eLvl, _] => deconstructUnitors iso eLvl true true | Expr.const ``rightUnitor [eLvl, _] => deconstructUnitors iso eLvl false true | Expr.const ``MonoidalCategory.associator [eLvl, _] => deconstructAssociator iso eLvl true @@ -208,7 +195,6 @@ partial def transformHomToKernel (e : Expr) : MetaM (Expr × Expr) := do let args := e.getAppArgs let iso := args[args.size - 1]! match iso.getAppFn with - | Expr.const ``BraidedCategory.braiding _ => deconstructBraiding iso | Expr.const ``leftUnitor [eLvl, _] => deconstructUnitors iso eLvl true false | Expr.const ``rightUnitor [eLvl, _] => deconstructUnitors iso eLvl false false | Expr.const ``MonoidalCategory.associator [eLvl, _] => deconstructAssociator iso eLvl false @@ -218,6 +204,7 @@ partial def transformHomToKernel (e : Expr) : MetaM (Expr × Expr) := do /-- Transform a `SFinKer` equality into an equivalent equality of kernels, along with a proof of equivalence. -/ def KernelEquality (eq : Expr) : MetaM (Expr × Expr) := do + resetTransformCache let eq ← whnfR <| ← instantiateMVars eq let some (_, lhs_hom, rhs_hom) := eq.eq? | throwError "Expected an equality, got: {eq}." let (lhs, pl) ← transformHomToKernel lhs_hom diff --git a/KernelHom/Tactic/KernelHom.lean b/KernelHom/Tactic/KernelHom.lean index 5673b57b1..589ff53ac 100644 --- a/KernelHom/Tactic/KernelHom.lean +++ b/KernelHom/Tactic/KernelHom.lean @@ -30,45 +30,6 @@ public meta section open Lean Elab Tactic Meta CategoryTheory Parser.Tactic ProbabilityTheory MonoidalCategory open ProbabilityTheory.Kernel -/-- Recursively decompose a product type into `SFinKer` objects with monoidal tensor structure. -/ -partial def decomposeProductToSFinker (X : Expr) (xLvl : Level) : MetaM Expr := do - match X.getAppFn with - | Expr.const ``Prod _ => - let args := X.getAppArgs - let t1 ← decomposeProductToSFinker args[0]! xLvl - let t2 ← decomposeProductToSFinker args[1]! xLvl - mkAppM ``tensorObj #[t1, t2] - | _ => - mkAppOptM ``SFinKer.of #[X, none] - -/-- Compute the `SFinKer` object corresponding to a measurable space. -/ -def computeSFinkerOf (X : Expr) (xLvl : Level) : MetaM Expr := do - match X with - | Expr.const ``PUnit _ | Expr.const ``Unit _ => - let tensorunit := mkConst ``tensorUnit [xLvl, xLvl.succ] - let sfinker := mkConst ``SFinKer [xLvl] - mkAppOptM' tensorunit #[sfinker, none, none] - | _ => - decomposeProductToSFinker X xLvl - -/-- Compute a measurable equivalence between a type and itself by recursively decomposing -products. -/ -partial def idME (X : Expr) : MetaM Expr := do - match X.getAppFn with - | Expr.const ``Prod _ => - let args := X.getAppArgs - let id1 ← idME args[0]! - let id2 ← idME args[1]! - mkAppM ``MeasurableEquiv.prodCongr #[id1, id2] - | Expr.const ``PUnit [xLvl] | Expr.const ``Unit [xLvl] => - let xLvl ← match xLvl with - | Level.succ l => pure l - | _ => throwError "Expected a successor level for PUnit/Unit, got: {xLvl}." - let punitME := mkConst ``MeasurableEquiv.punit [xLvl, xLvl] - mkAppM' punitME #[] - | _ => - mkAppOptM ``MeasurableEquiv.refl #[X, none] - /-- Check if a kernel expression corresponds to a left or right whisker. -/ def checkWhiskers (κ : Expr) (offset : Nat) : MetaM Bool := do let κ := κ.consumeMData @@ -84,35 +45,23 @@ def checkWhiskerLeft (κ : Expr) : MetaM Bool := checkWhiskers κ 2 /-- Check if a kernel expression corresponds to a right whisker. -/ def checkWhiskerRight (κ : Expr) : MetaM Bool := checkWhiskers κ 1 -/-- Construct the relevant data for converting a kernel expression to its whisker morphism -representation. -/ -def constructWhiskersArgs (e X Y : Expr) (left : Bool) : - MetaM (Expr × Expr × Expr × Expr × Expr × Expr × Expr) := do - let (Z, zLvl, X, xLvl) ← match X.getAppFn with - | Expr.const ``Prod univs => - let args := X.getAppArgs - pure (args[left.toNat]!, univs[left.toNat]!, args[1 - left.toNat]!, univs[1 - left.toNat]!) - | _ => - if left then throwError "Expected left whisker with source Z × X, got: {X}." - else throwError "Expected right whisker with source X × Z, got: {X}." - let (Y, yLvl) ← match Y.getAppFn with - | Expr.const ``Prod univs => - let args := Y.getAppArgs - pure (args[1 - left.toNat]!, univs[1 - left.toNat]!) - | _ => - if left then throwError "Expected left whisker with target Z × Y, got: {Y}." - else throwError "Expected right whisker with target Y × Z, got: {Y}." - let κ ← match e.getAppFn with - | Expr.const ``Kernel.parallelComp _ => - let args := e.getAppArgs - pure args[args.size - (left.toNat + 1)]! - | _ => - if left then throwError "Expected left whisker with parallelComp, got: {e}." - else throwError "Expected right whisker with parallelComp, got: {e}." - let SZ ← computeSFinkerOf Z zLvl - let SX ← computeSFinkerOf X xLvl - let SY ← computeSFinkerOf Y yLvl - return (SZ, Z, SX, X, SY, Y, κ) +/-- Given a whisker `e = Kernel.id ∥ₖ κ` (left) or `e = κ ∥ₖ Kernel.id` (right) with +`κ : Kernel X Y` and `Kernel.id : Kernel Z Z`, return the carriers `Z X Y` and `κ`. -/ +def whiskerData (e : Expr) (left : Bool) : MetaM (Carrier × Carrier × Carrier × Expr) := do + let (src, tgt, _, _) ← getTypesFromKernel e + let prodArgs (P : Expr) : MetaM (Carrier × Carrier) := do + match P.getAppFn with + | Expr.const ``Prod [l₁, l₂] => + let args := P.getAppArgs + return (⟨args[0]!, l₁⟩, ⟨args[1]!, l₂⟩) + | _ => throwError "Expected a product type, got: {P}." + let (s₁, s₂) ← prodArgs src + let (t₁, t₂) ← prodArgs tgt + let args := e.getAppArgs + if left then + return (s₁, s₂, t₂, args[args.size - 1]!) + else + return (s₂, s₁, t₁, args[args.size - 2]!) /-- Check if a kernel expression corresponds to a left or right unitor. -/ def checkUnitors (κ : Expr) (offset : Nat) (prod : Name) : MetaM Bool := do @@ -154,11 +103,11 @@ def constructUnitors (X ex₀ : Expr) (xLvl y₀Lvl punitLvl : Level) (offset : let unitor ← if left then mkAppM ``leftUnitor #[SX] else mkAppM ``rightUnitor #[SX] let unitor_hom_const := - if left then mkConst ``leftUnitor_hom [xLvl, y₀Lvl, xLvl, punitLvl] - else mkConst ``rightUnitor_hom [xLvl, y₀Lvl, xLvl, punitLvl] + if left then mkConst ``leftUnitor_hom [xLvl, xLvl, y₀Lvl, punitLvl] + else mkConst ``rightUnitor_hom [xLvl, xLvl, y₀Lvl, punitLvl] let unitor_hom_proof ← - if left then mkAppM' unitor_hom_const #[SX, ← idME X, ex₀] - else mkAppM' unitor_hom_const #[SX, ← idME X, ex₀] + if left then mkAppM' unitor_hom_const #[SX, ← idME X xLvl, ex₀] + else mkAppM' unitor_hom_const #[SX, ← idME X xLvl, ex₀] return (← mkAppM ``Iso.hom #[unitor], unitor_hom_proof) /-- Check if a kernel expression corresponds to an associator morphism or its inverse. -/ @@ -228,9 +177,8 @@ def constructAssociator (left right ex₀ ey₀ ez₀ : Expr) (hom : Bool) : let SY ← computeSFinkerOf Y yLvl let SZ ← computeSFinkerOf Z zLvl let associator ← mkAppM ``MonoidalCategory.associator #[SX, SY, SZ] - let associator_hom_proof ← - if hom then mkAppM ``associator_hom #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, ex₀, ey₀, ez₀] - else mkAppM ``associator_inv #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, ex₀, ey₀, ez₀] + let lemmaArgs := #[SX, SY, SZ, ← idME X xLvl, ← idME Y yLvl, ← idME Z zLvl, ex₀, ey₀, ez₀] + let associator_hom_proof ← mkAppM (if hom then ``associator_hom else ``associator_inv) lemmaArgs return (← mkAppM (if hom then ``Iso.hom else ``Iso.inv) #[associator], associator_hom_proof) /-- Construct the associator morphism. -/ @@ -243,81 +191,82 @@ def constructAssociatorInv (left right ex₀ ey₀ ez₀ : Expr) := /-- Recursive transformation from kernel expressions to morphism expressions in the `SFinKer` category. Returns the morphism expression `e'` together with a proof of `e' = e.hom`, built by -congruence from the translation lemmas. -/ +congruence from the translation lemmas (`comp_hom`, `parallelComp_hom`, ...). -/ partial def transformKernelToHom (e : Expr) : MetaM (Expr × Expr) := do match e.getAppFn with | Expr.const ``Kernel.comp _ => let args := e.getAppArgs let η := args[args.size - 2]! let κ := args[args.size - 1]! - let (X, Y, xLvl, yLvl) ← getTypesFromKernel η - let (Z, _, tLvl, _) ← getTypesFromKernel κ - let SX ← computeSFinkerOf X xLvl - let SY ← computeSFinkerOf Y yLvl - let SZ ← computeSFinkerOf Z tLvl - let comp_hom_proof ← mkAppMInst ``comp_hom #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, η, κ] 2 + let (X, Y) ← getCarriersFromKernel η + let (Z, _) ← getCarriersFromKernel κ + let (X, Y, Z) := (← HomCarrier.mk' X, ← HomCarrier.mk' Y, ← HomCarrier.mk' Z) + let I ← sfinkerInsts X.lvl + let pf := mkAppN (mkConst ``comp_hom [X.lvl, Y.lvl, Z.lvl, I.u]) + (homLemmaArgs #[X, Y, Z] ++ + #[η, κ, ← X.sfinite Y η, ← Z.sfinite X κ]) let (κ', pκ) ← transformKernelToHom κ let (η', pη) ← transformKernelToHom η - let e' ← mkAppM ``CategoryStruct.comp #[κ', η'] + let e' := I.comp Z.obj X.obj Y.obj κ' η' let h ← mkCongr (← mkCongrArg e'.appFn!.appFn! pκ) pη - return (e', ← mkEqTrans h comp_hom_proof) + return (e', ← mkEqTrans h pf) | Expr.const ``Kernel.parallelComp _ => if ← checkWhiskerLeft e then - let (X, Y, _, _) ← getTypesFromKernel e - let (SZ, Z, SX, X, SY, Y, κ) ← constructWhiskersArgs e X Y false - let whisker_left_hom_proof ← mkAppMInst ``Kernel.whiskerLeft - #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ] 1 + let (Z, X, Y, κ) ← whiskerData e true + let (X, Y, Z) := (← HomCarrier.mk' X, ← HomCarrier.mk' Y, ← HomCarrier.mk' Z) + let I ← sfinkerInsts X.lvl + let pf := mkAppN (mkConst ``Kernel.whiskerLeft [X.lvl, Y.lvl, Z.lvl, I.u]) + (homLemmaArgs #[X, Y, Z] ++ #[κ, ← X.sfinite Y κ]) let (κ', pκ) ← transformKernelToHom κ - let e' ← mkAppM ``MonoidalCategory.whiskerLeft #[SZ, κ'] + let e' := I.whiskerLeft Z.obj X.obj Y.obj κ' let h ← mkCongrArg e'.appFn! pκ - return (e', ← mkEqTrans h whisker_left_hom_proof) + return (e', ← mkEqTrans h pf) else if ← checkWhiskerRight e then - let (X, Y, _, _) ← getTypesFromKernel e - let (SZ, Z, SX, X, SY, Y, κ) ← constructWhiskersArgs e X Y true - let whiskerright_hom_proof ← mkAppMInst ``Kernel.whiskerRight - #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ] 1 + let (Z, X, Y, κ) ← whiskerData e false + let (X, Y, Z) := (← HomCarrier.mk' X, ← HomCarrier.mk' Y, ← HomCarrier.mk' Z) + let I ← sfinkerInsts X.lvl + let pf := mkAppN (mkConst ``Kernel.whiskerRight [X.lvl, Y.lvl, Z.lvl, I.u]) + (homLemmaArgs #[X, Y, Z] ++ #[κ, ← X.sfinite Y κ]) let (κ', pκ) ← transformKernelToHom κ - let e' ← mkAppM ``MonoidalCategory.whiskerRight #[κ', SZ] - let h ← mkCongrFun (← mkCongrArg e'.appFn!.appFn! pκ) SZ - return (e', ← mkEqTrans h whiskerright_hom_proof) + let e' := I.whiskerRight X.obj Y.obj κ' Z.obj + let h ← mkCongrFun (← mkCongrArg e'.appFn!.appFn! pκ) Z.obj + return (e', ← mkEqTrans h pf) else let args := e.getAppArgs let κ := args[args.size - 2]! let η := args[args.size - 1]! - let (X, Y, xLvl, yLvl) ← getTypesFromKernel κ - let (Z, T, zLvl, tLvl) ← getTypesFromKernel η - let SX ← computeSFinkerOf X xLvl - let SY ← computeSFinkerOf Y yLvl - let SZ ← computeSFinkerOf Z zLvl - let ST ← computeSFinkerOf T tLvl - let parallelComp_hom_proof ← mkAppMInst ``parallelComp_hom - #[SX, SY, SZ, ST, ← idME X, ← idME Y, ← idME Z, ← idME T, κ, η] 2 + let (X, Y) ← getCarriersFromKernel κ + let (Z, T) ← getCarriersFromKernel η + let (X, Y, Z, T) := + (← HomCarrier.mk' X, ← HomCarrier.mk' Y, ← HomCarrier.mk' Z, ← HomCarrier.mk' T) + let I ← sfinkerInsts X.lvl + let pf := mkAppN (mkConst ``parallelComp_hom [X.lvl, Y.lvl, T.lvl, Z.lvl, I.u]) + (typeInstArgs #[X, Y, T, Z] ++ objEquivArgs #[X, Y, Z, T] ++ + #[κ, η, ← Z.sfinite T η, ← X.sfinite Y κ]) let (κ', pκ) ← transformKernelToHom κ let (η', pη) ← transformKernelToHom η - let e' ← mkAppM ``tensorHom #[κ', η'] + let e' := I.tensorHom X.obj Y.obj Z.obj T.obj κ' η' let h ← mkCongr (← mkCongrArg e'.appFn!.appFn! pκ) pη - return (e', ← mkEqTrans h parallelComp_hom_proof) + return (e', ← mkEqTrans h pf) | Expr.const ``Kernel.id [xLvl] => - let X := e.getAppArgs[0]! - let SX ← computeSFinkerOf X xLvl - return (← mkAppM ``CategoryStruct.id #[SX], ← mkAppM ``id_hom #[SX, ← idME X]) + let X ← HomCarrier.mk' ⟨e.getAppArgs[0]!, xLvl⟩ + let I ← sfinkerInsts xLvl + return (I.id X.obj, mkAppN (mkConst ``id_hom [xLvl, I.u]) (homLemmaArgs #[X])) | Expr.const ``Kernel.discard [xLvl, punitLvl] => - let X := e.getAppArgs[0]! - let SX ← computeSFinkerOf X xLvl - let discard_hom_proof ← mkAppM' (mkConst ``counit [xLvl, xLvl, punitLvl]) #[SX, ← idME X] - return (← mkAppOptM ``ComonObj.counit #[none, none, none, SX, none], discard_hom_proof) + let X ← HomCarrier.mk' ⟨e.getAppArgs[0]!, xLvl⟩ + let I ← sfinkerInsts xLvl + return (← I.counit X.obj, + mkAppN (mkConst ``counit [xLvl, I.u, punitLvl]) (homLemmaArgs #[X])) | Expr.const ``Kernel.copy [xLvl] => - let X := e.getAppArgs[0]! - let SX ← computeSFinkerOf X xLvl - return (← mkAppOptM ``ComonObj.comul #[none, none, none, SX, none], - ← mkAppM ``comul #[SX, ← idME X]) + let X ← HomCarrier.mk' ⟨e.getAppArgs[0]!, xLvl⟩ + let I ← sfinkerInsts xLvl + return (← I.comul X.obj, mkAppN (mkConst ``comul [xLvl, I.u]) (homLemmaArgs #[X])) | Expr.const ``Kernel.swap [xLvl, yLvl] => - let X := e.getAppArgs[0]! - let Y := e.getAppArgs[1]! - let SX ← computeSFinkerOf X xLvl - let SY ← computeSFinkerOf Y yLvl - let braiding ← mkAppM ``Iso.hom #[← mkAppM ``BraidedCategory.braiding #[SX, SY]] - return (braiding, ← mkAppM ``braiding_hom #[SX, SY, ← idME X, ← idME Y]) + let X ← HomCarrier.mk' ⟨e.getAppArgs[0]!, xLvl⟩ + let Y ← HomCarrier.mk' ⟨e.getAppArgs[1]!, yLvl⟩ + let I ← sfinkerInsts xLvl + return (← I.braidingHom X.obj Y.obj, + mkAppN (mkConst ``braiding_hom [xLvl, yLvl, I.u]) (homLemmaArgs #[X, Y])) | Expr.const ``Kernel.lift [_, y₀Lvl, _] => let (X, Y, xLvl, yLvl) ← getTypesFromKernel e let args := e.getAppArgs @@ -339,10 +288,7 @@ partial def transformKernelToHom (e : Expr) : MetaM (Expr × Expr) := do let (ex₀, ey₀, ez₀) ← getMEFromThreeProds args[args.size - 3]! constructAssociatorInv X Y ex₀ ey₀ ez₀ else - let SX ← computeSFinkerOf X xLvl - let SY ← computeSFinkerOf Y yLvl - let homExpr ← mkAppOptM ``ProbabilityTheory.Kernel.hom - #[X, Y, none, none, SX, SY, (← idME X), (← idME Y), e, none] + let homExpr ← mkHom (← HomCarrier.mk' ⟨X, xLvl⟩) (← HomCarrier.mk' ⟨Y, yLvl⟩) e return (homExpr, ← mkEqRefl homExpr) | _ => throwError "Expected a lifted kernel expression, got: {e}." @@ -350,10 +296,11 @@ partial def transformKernelToHom (e : Expr) : MetaM (Expr × Expr) := do /-- Given lifted kernels `lhs rhs` and morphisms `lh rh` with proofs `pl : lh = lhs.hom` and `pr : rh = rhs.hom`, construct a proof of `(lhs = rhs) = (lh = rh)`. -/ def mkHomCongrProof (lhs rhs pl pr : Expr) : MetaM Expr := do - let (X, Y, xLvl, yLvl) ← getTypesFromKernel lhs - let SX ← computeSFinkerOf X xLvl - let SY ← computeSFinkerOf Y yLvl - let hom_congr_proof ← mkAppMInst ``hom_congr #[SX, SY, ← idME X, ← idME Y, lhs, rhs] 2 + let (X, Y) ← getCarriersFromKernel lhs + let (X, Y) := (← HomCarrier.mk' X, ← HomCarrier.mk' Y) + let hom_congr_proof := mkAppN (mkConst ``hom_congr [X.lvl, Y.lvl, X.lvl]) <| + homLemmaArgs #[X, Y] ++ + #[lhs, rhs, ← X.sfinite Y lhs, ← X.sfinite Y rhs] mkEqTrans (← mkPropExt hom_congr_proof) (← mkEqSymm (← mkEqCongr pl pr)) /-- Transform a kernel equality into an equivalent equality in `SFinKer`, along with a proof of diff --git a/KernelHom/Tactic/Reassoc.lean b/KernelHom/Tactic/Reassoc.lean index eb2de01f2..d6f81b09e 100644 --- a/KernelHom/Tactic/Reassoc.lean +++ b/KernelHom/Tactic/Reassoc.lean @@ -50,7 +50,7 @@ def kernelReassocHandler (h_eq : Expr) : MetaM (Expr × Array LMVarId) := do withLocalDecl `Z .implicit (mkSort (mkLevelSucc u)) fun Z => do let mspaceType ← mkAppM ``MeasurableSpace #[Z] withLocalDecl `inst .instImplicit mspaceType fun _inst => do - let kernelType ← mkAppMInst ``Kernel #[Y, Z] 2 + let kernelType ← mkAppOptM ``Kernel #[Y, Z, none, none] withLocalDeclD `ξ kernelType fun ξ => do let sfiniteType ← mkAppM ``IsSFiniteKernel #[ξ] withLocalDecl `inst_1 BinderInfo.instImplicit sfiniteType fun _inst_1 => do diff --git a/KernelHom/Tactic/Utils.lean b/KernelHom/Tactic/Utils.lean index f79dc20ac..29d2f160c 100644 --- a/KernelHom/Tactic/Utils.lean +++ b/KernelHom/Tactic/Utils.lean @@ -5,16 +5,28 @@ Authors: Gaëtan Serré -/ module -public import Mathlib.Probability.Kernel.Composition.Prod -public import Mathlib.Probability.Kernel.Composition.CompProd +public import EqLift.Tactic.Kernel.Utils +public import KernelHom.Kernel.Hom /-! # Kernel transformation utilities + +Explicit constructors for the objects and morphisms of `SFinKer` used by the `kernel_hom` and +`hom_kernel` tactics. The applications are built directly (`mkAppN` with explicit universe levels +and cached instances) instead of going through `mkAppM`. + +## Main declarations + +* `unfoldKernelOp`: unfolds `Kernel.prod` and `Kernel.compProd`. +* `SFinKerInsts`: the category-theoretic instances of `SFinKer.{u}`. +* `computeSFinkerOf`, `idME`: the object of `SFinKer` associated with a measurable space, and the + identity measurable equivalence, recursively on products (memoized). +* `mkCatComp`, `mkTensorHom`, ...: explicit constructors of morphisms. -/ public meta section -open Lean Meta ProbabilityTheory +open Lean Meta ProbabilityTheory CategoryTheory /-- Unfold kernel operations in an expression. -/ def unfoldKernelOp (e : Expr) : MetaM Expr := do @@ -24,8 +36,173 @@ def unfoldKernelOp (e : Expr) : MetaM Expr := do let e' ← Core.betaReduce e' return .done e') -/-- Returns the application `constName` `xs` with `n_impls` last arguments as implicit. -/ -def Lean.Meta.mkAppMInst (constName : Name) (xs : Array Expr) (n_impls : Nat) : MetaM Expr := do - let e ← mkAppM constName xs - let nones : Array (Option Expr) := Array.replicate n_impls none - mkAppOptM' e nones +/-- The `IsSFiniteKernel` instance of a kernel (cached). -/ +def sfiniteInst (X Y : Carrier) (κ : Expr) : MetaM Expr := do + synthInstanceCached <| mkAppN (mkConst ``IsSFiniteKernel [X.lvl, Y.lvl]) + #[X.type, Y.type, ← X.inst, ← Y.inst, κ] + +/-- The category-theoretic instances of `SFinKer.{u}`. -/ +structure SFinKerInsts where + /-- The universe level. -/ + u : Level + /-- `SFinKer.{u}`. -/ + C : Expr + /-- `Category SFinKer`. -/ + cat : Expr + /-- `CategoryStruct SFinKer`. -/ + catStruct : Expr + /-- `MonoidalCategory SFinKer`. -/ + monoidal : Expr + /-- `MonoidalCategoryStruct SFinKer`. -/ + monStruct : Expr + +/-- The category-theoretic instances of `SFinKer.{u}` (cached). -/ +def sfinkerInsts (u : Level) : MetaM SFinKerInsts := do + let C := mkConst ``SFinKer [u] + let lvls := [u, u.succ] + let cat ← synthInstanceCached (mkApp (mkConst ``Category lvls) C) + return { + u, C, cat + catStruct := ← synthInstanceCached (mkApp (mkConst ``CategoryStruct lvls) C) + monoidal := ← synthInstanceCached (mkApp2 (mkConst ``MonoidalCategory lvls) C cat) + monStruct := ← synthInstanceCached (mkApp2 (mkConst ``MonoidalCategoryStruct lvls) C cat) } + +namespace SFinKerInsts + +/-- `SFinKer.of X`. -/ +def of (X : Carrier) : MetaM Expr := do + return mkApp2 (mkConst ``SFinKer.of [X.lvl]) X.type (← X.inst) + +/-- `A ⊗ B`. -/ +def tensorObj (I : SFinKerInsts) (A B : Expr) : Expr := + mkAppN (mkConst ``MonoidalCategoryStruct.tensorObj [I.u, I.u.succ]) + #[I.C, I.cat, I.monStruct, A, B] + +/-- `𝟙_ SFinKer`. -/ +def tensorUnit (I : SFinKerInsts) : Expr := + mkAppN (mkConst ``MonoidalCategoryStruct.tensorUnit [I.u, I.u.succ]) #[I.C, I.cat, I.monStruct] + +/-- `f ≫ g` with `f : X ⟶ Y` and `g : Y ⟶ Z`. -/ +def comp (I : SFinKerInsts) (X Y Z f g : Expr) : Expr := + mkAppN (mkConst ``CategoryStruct.comp [I.u, I.u.succ]) #[I.C, I.catStruct, X, Y, Z, f, g] + +/-- `𝟙 X`. -/ +def id (I : SFinKerInsts) (X : Expr) : Expr := + mkAppN (mkConst ``CategoryStruct.id [I.u, I.u.succ]) #[I.C, I.catStruct, X] + +/-- `f ⊗ₘ g` with `f : X₁ ⟶ Y₁` and `g : X₂ ⟶ Y₂`. -/ +def tensorHom (I : SFinKerInsts) (X₁ Y₁ X₂ Y₂ f g : Expr) : Expr := + mkAppN (mkConst ``MonoidalCategoryStruct.tensorHom [I.u, I.u.succ]) + #[I.C, I.cat, I.monStruct, X₁, Y₁, X₂, Y₂, f, g] + +/-- `X ◁ f` with `f : Y₁ ⟶ Y₂`. -/ +def whiskerLeft (I : SFinKerInsts) (X Y₁ Y₂ f : Expr) : Expr := + mkAppN (mkConst ``MonoidalCategoryStruct.whiskerLeft [I.u, I.u.succ]) + #[I.C, I.cat, I.monStruct, X, Y₁, Y₂, f] + +/-- `f ▷ Y` with `f : X₁ ⟶ X₂`. -/ +def whiskerRight (I : SFinKerInsts) (X₁ X₂ f Y : Expr) : Expr := + mkAppN (mkConst ``MonoidalCategoryStruct.whiskerRight [I.u, I.u.succ]) + #[I.C, I.cat, I.monStruct, X₁, X₂, f, Y] + +/-- The `ComonObj X` instance (cached). -/ +def comonInst (I : SFinKerInsts) (X : Expr) : MetaM Expr := + synthInstanceCached (mkAppN (mkConst ``ComonObj [I.u, I.u.succ]) #[I.C, I.cat, I.monoidal, X]) + +/-- `ε[X]`. -/ +def counit (I : SFinKerInsts) (X : Expr) : MetaM Expr := do + return mkAppN (mkConst ``ComonObj.counit [I.u, I.u.succ]) + #[I.C, I.cat, I.monoidal, X, ← I.comonInst X] + +/-- `Δ[X]`. -/ +def comul (I : SFinKerInsts) (X : Expr) : MetaM Expr := do + return mkAppN (mkConst ``ComonObj.comul [I.u, I.u.succ]) + #[I.C, I.cat, I.monoidal, X, ← I.comonInst X] + +/-- `(β_ X Y).hom`. -/ +def braidingHom (I : SFinKerInsts) (X Y : Expr) : MetaM Expr := do + let braided ← synthInstanceCached + (mkAppN (mkConst ``BraidedCategory [I.u, I.u.succ]) #[I.C, I.cat, I.monoidal]) + let iso := mkAppN (mkConst ``BraidedCategory.braiding [I.u, I.u.succ]) + #[I.C, I.cat, I.monoidal, braided, X, Y] + return mkAppN (mkConst ``Iso.hom [I.u, I.u.succ]) + #[I.C, I.cat, I.tensorObj X Y, I.tensorObj Y X, iso] + +end SFinKerInsts + +/-- Compute the `SFinKer` object corresponding to a measurable space `X : Type xLvl`, decomposing +products into tensor products and `PUnit` into the monoidal unit (memoized). -/ +partial def computeSFinkerOf (X : Expr) (xLvl : Level) : MetaM Expr := do + let res ← memoized `computeSFinkerOf X do + match X.getAppFn with + | Expr.const ``PUnit _ | Expr.const ``Unit _ => return #[(← sfinkerInsts xLvl).tensorUnit] + | Expr.const ``Prod [xLvl, yLvl] => + let args := X.getAppArgs + let I ← sfinkerInsts xLvl + return #[I.tensorObj (← computeSFinkerOf args[0]! xLvl) (← computeSFinkerOf args[1]! yLvl)] + | _ => return #[← SFinKerInsts.of ⟨X, xLvl⟩] + return res[0]! + +/-- The measurable equivalence `X ≃ᵐ X`, built recursively on products so that it matches the +decomposition of `computeSFinkerOf` (memoized). -/ +partial def idME (X : Expr) (xLvl : Level) : MetaM Expr := do + let res ← memoized `idME X do + match X.getAppFn with + | Expr.const ``Prod [xLvl, yLvl] => + let args := X.getAppArgs + let X₁ := args[0]! + let X₂ := args[1]! + return #[mkAppN (mkConst ``MeasurableEquiv.prodCongr [xLvl, xLvl, yLvl, yLvl]) + #[X₁, X₁, X₂, X₂, ← Carrier.inst ⟨X₁, xLvl⟩, ← Carrier.inst ⟨X₁, xLvl⟩, + ← Carrier.inst ⟨X₂, yLvl⟩, ← Carrier.inst ⟨X₂, yLvl⟩, + ← idME X₁ xLvl, ← idME X₂ yLvl]] + | Expr.const ``PUnit [l] | Expr.const ``Unit [l] => + let l ← match l with + | Level.succ l => pure l + | _ => throwError "Expected a successor level for PUnit/Unit, got: {l}." + return #[mkConst ``MeasurableEquiv.punit [l, l]] + | _ => return #[mkApp2 (mkConst ``MeasurableEquiv.refl [xLvl]) X (← Carrier.inst ⟨X, xLvl⟩)] + return res[0]! + +/-- A carrier `X` together with its `MeasurableSpace` instance, its object `obj` in `SFinKer` and +the measurable equivalence `equiv : obj ≃ᵐ X`. -/ +structure HomCarrier extends Carrier where + /-- The `MeasurableSpace` instance. -/ + inst : Expr + /-- The object of `SFinKer`. -/ + obj : Expr + /-- The measurable equivalence `obj ≃ᵐ X`. -/ + equiv : Expr + +/-- Build the `HomCarrier` of a carrier. -/ +def HomCarrier.mk' (X : Carrier) : MetaM HomCarrier := do + let inst ← X.inst + let obj ← computeSFinkerOf X.type X.lvl + let equiv ← idME X.type X.lvl + return { X with inst, obj, equiv } + +instance : Coe HomCarrier Carrier := ⟨HomCarrier.toCarrier⟩ + +/-- The `IsSFiniteKernel` instance of `κ : Kernel X Y` (cached). -/ +def HomCarrier.sfinite (X Y : HomCarrier) (κ : Expr) : MetaM Expr := + sfiniteInst X Y κ + +/-- The carriers and their `MeasurableSpace` instances: `X Y ... [mX] [mY] ...`. -/ +def typeInstArgs (cs : Array HomCarrier) : Array Expr := + cs.map (·.type) ++ cs.map (·.inst) + +/-- The objects of `SFinKer` and the measurable equivalences: `SX SY ... ex ey ...`. -/ +def objEquivArgs (cs : Array HomCarrier) : Array Expr := + cs.map (·.obj) ++ cs.map (·.equiv) + +/-- The arguments shared by the translation lemmas for carriers `X Y ...`: +`X Y ... [mX] [mY] ... SX SY ... ex ey ...`. -/ +def homLemmaArgs (cs : Array HomCarrier) : Array Expr := + typeInstArgs cs ++ objEquivArgs cs + +/-- `κ.hom (ex := ex) (ey := ey) : SX ⟶ SY`. -/ +def mkHom (X Y : HomCarrier) (κ : Expr) : MetaM Expr := do + return mkAppN (mkConst ``Kernel.hom [X.lvl, Y.lvl, X.lvl]) + (homLemmaArgs #[X, Y] ++ #[κ, ← X.sfinite Y κ]) + +end diff --git a/KernelHomManual/Front.lean b/KernelHomManual/Front.lean index f1b759d2a..eded042d0 100644 --- a/KernelHomManual/Front.lean +++ b/KernelHomManual/Front.lean @@ -13,6 +13,7 @@ import KernelHomManual.Pages.HomKernel import KernelHomManual.Pages.CatTactics import KernelHomManual.Pages.Reassoc import KernelHomManual.Pages.MonoidalComp +import KernelHomManual.Pages.Performance import KernelHom.Tactic.KernelDiagram import EqLift.Tactic.Lift import Mathlib.Probability.Kernel.Category.Stoch @@ -66,6 +67,10 @@ The library also provides the `@[kernel_reassoc]` attribute, which is a variant An additional consequence of the translation to {name SFinKer}`SFinKer` is that one can adapt the categorical monoidal composition “{name CategoryTheory.monoidalComp}`⊗≫`” to kernels, resulting in a kernelized monoidal composition “{name ProbabilityTheory.Kernel.monoComp}`⊗≫ₖ`”. This composition automatically handles measurable equivalences, allowing for seamless composition of kernels while maintaining s-finiteness. +*Performance* + +The translation builds its terms and proofs directly rather than through `mkAppM` and rewriting: the equivalence between the original and the translated equalities is proved by congruence from the translation lemmas, and the instances, inferred types and recursively built objects (measurable equivalences, objects of {name SFinKer}`SFinKer`) are memoized in a cache that is reset at each call. See the {ref "performance"}[Performance] page for the underlying structures. + *About* This library is under active development and is under the [Apache 2.0 license](https://www.apache.org/licenses/LICENSE-2.0). Contributions and feedback are welcome! @@ -83,3 +88,5 @@ This library is under active development and is under the [Apache 2.0 license](h {include 0 KernelHomManual.Pages.Reassoc} {include 0 KernelHomManual.Pages.MonoidalComp} + +{include 0 KernelHomManual.Pages.Performance} diff --git a/KernelHomManual/Pages/Performance.lean b/KernelHomManual/Pages/Performance.lean new file mode 100644 index 000000000..9df472584 --- /dev/null +++ b/KernelHomManual/Pages/Performance.lean @@ -0,0 +1,80 @@ +/- +Copyright (c) 2026 Gaëtan Serré. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gaëtan Serré +-/ + +import KernelHom.Tactic.KernelHom +import EqLift.Tactic.Cache +import EqLift.Tactic.Kernel.Utils +import VersoManual + +open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External + +set_option linter.style.setOption false +set_option linter.hashCommand false +set_option linter.style.longLine false +set_option pp.rawOnError true +set_option verso.code.warnLineLength 100 + +#doc (Manual) "Performance" => +%%% +htmlSplit := .never +tag := "performance" +%%% + +The translation performed by {name kernelHom}`kernel_hom` traverses the kernel expression twice (once to lift it to a common universe level, once to translate it into {name SFinKer}`SFinKer`) and builds, at each node, an instance of a translation lemma such as {name ProbabilityTheory.Kernel.comp_hom}`comp_hom` or {name ProbabilityTheory.Kernel.comp_lift}`comp_lift`. Two design choices keep this cheap. + +# Proofs by congruence + +The proof of equivalence between the original equality and the translated one is not obtained by rewriting the goal with the translation lemmas (which requires abstracting a pattern and type-checking a motive at each step), but by congruence: each translation function returns the translated expression together with a proof that it is the translation of the original one, built from the proofs of its subterms with {name Lean.Meta.mkCongr}`mkCongr`, {name Lean.Meta.mkCongrArg}`mkCongrArg` and {name Lean.Meta.mkEqTrans}`mkEqTrans`. The equality of propositions is then obtained from {name ProbabilityTheory.Kernel.hom_congr}`hom_congr` (or {name ProbabilityTheory.Kernel.lift_congr}`lift_congr`) and `propext`, see {name mkHomCongrProof}`mkHomCongrProof`. + +{docstring mkHomCongrProof} + +# Explicit constructors and memoization + +The terms and lemma instances are built directly with `mkAppN`, with explicit universe levels and instances, instead of `mkAppM`, whose unification and instance synthesis dominated the cost of the translation. This requires a fixed order of the universe parameters of the translation lemmas, which is why the universes of `KernelHom.Kernel.Hom` are declared explicitly (`x y t z u x₀ y₀ z₀`). + +The instances (`MeasurableSpace X`, `IsSFiniteKernel κ`, the category-theoretic instances of {name SFinKer}`SFinKer`, ...), the inferred types of kernels and the recursively built objects (measurable equivalences, objects of {name SFinKer}`SFinKer`) are memoized in a cache which is reset at the beginning of each transformation. The cache lives in *Eq-Lift*: + +{docstring TransformCache} + +{docstring resetTransformCache} + +{docstring synthInstanceCached} + +{docstring inferTypeCached} + +{docstring memoized} + +# Carriers + +A measurable space is represented during the transformations by its carrier type and universe level, from which the `MeasurableSpace` instance is obtained through the cache. + +{docstring Carrier} + +{docstring Carrier.inst} + +{docstring Carrier.lift} + +{docstring getCarriersFromKernel} + +{docstring constructMeasurableEquiv} + +The translation to {name SFinKer}`SFinKer` needs more data about each carrier `X`: the object of {name SFinKer}`SFinKer` it is translated to (`SFinKer.of X`, or a tensor product of such objects when `X` is a product, so that the monoidal tactics see the tensor structure) and the measurable equivalence between the carrier of this object and `X`, which is the argument `ex` of {name ProbabilityTheory.Kernel.hom}`hom` and of the translation lemmas. These are computed once per carrier by {name computeSFinkerOf}`computeSFinkerOf` and {name idME}`idME`, and gathered in a {name HomCarrier}`HomCarrier`. + +{docstring HomCarrier} + +{docstring HomCarrier.mk'} + +{docstring HomCarrier.sfinite} + +{docstring computeSFinkerOf} + +{docstring idME} + +Finally, every morphism built during the translation (`≫`, `⊗ₘ`, whiskers, `𝟙`, `ε`, `Δ`, braiding) takes as implicit arguments the category-theoretic instances of {name SFinKer}`SFinKer` (`Category`, `MonoidalCategory`, ...). Since the constructors are explicit, these instances have to be provided, and they are synthesized once per universe level and gathered in a {name SFinKerInsts}`SFinKerInsts`, which also provides the constructors of the morphisms. + +{docstring SFinKerInsts} + +{docstring sfinkerInsts} diff --git a/KernelHomTests.lean b/KernelHomTests.lean index eb22620c0..c13387637 100644 --- a/KernelHomTests.lean +++ b/KernelHomTests.lean @@ -2,4 +2,4 @@ module -- shake: keep-all --deprecated_module: ignore public import KernelHomTests.Examples public import KernelHomTests.Tests -public import KernelHomTests.Time +public import KernelHomTests.Heartbeats diff --git a/KernelHomTests/Heartbeats.lean b/KernelHomTests/Heartbeats.lean new file mode 100644 index 000000000..849ab783a --- /dev/null +++ b/KernelHomTests/Heartbeats.lean @@ -0,0 +1,154 @@ +/- +Copyright (c) 2026 Gaëtan Serré. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gaëtan Serré +-/ +module + +public import KernelHom +public import Mathlib.Probability.Kernel.Composition.KernelLemmas +public import Mathlib.Util.CountHeartbeats + +/-! +# Heartbeats of Kernel-Hom proofs + +Each lemma of `KernelHomTests.Examples` is reproduced here together with its Mathlib proof +(`_orig`), and `#count_heartbeats!` reports the number of heartbeats used by each proof, a +deterministic measure of the work done by the elaborator. +-/ + +public section + +open MeasureTheory ProbabilityTheory CategoryTheory BraidedCategory + +open scoped MonoidalCategory ComonObj KernelHom + +variable {X Y Z T X' Y' Z' : Type*} [MeasurableSpace X] [MeasurableSpace Y] + [MeasurableSpace Z] [MeasurableSpace T] [MeasurableSpace X'] [MeasurableSpace Y'] + [MeasurableSpace Z'] + +namespace ProbabilityTheory.Kernel + +variable {κ : Kernel X Y} {ξ : Kernel Z T} {η : Kernel Y Z} + +#count_heartbeats! in +lemma swap_parallelComp_orig : swap Y T ∘ₖ (κ ∥ₖ ξ) = ξ ∥ₖ κ ∘ₖ swap X Z := by + by_cases hκ : IsSFiniteKernel κ + swap; · simp [hκ] + by_cases hη : IsSFiniteKernel ξ + swap; · simp [hη] + ext ac s hs + simp_rw [comp_apply, parallelComp_apply, Measure.bind_apply hs (Kernel.aemeasurable _), + swap_apply, lintegral_dirac' _ (Kernel.measurable_coe _ hs), parallelComp_apply' hs, + Prod.fst_swap, Prod.snd_swap] + rw [MeasureTheory.lintegral_prod_symm] + swap; · exact ((Kernel.id.measurable_coe hs).comp measurable_swap).aemeasurable + congr with d + simp_rw [Prod.swap_prod_mk, Measure.dirac_apply' _ hs, ← Set.indicator_comp_right, + lintegral_indicator (measurable_prodMk_left hs)] + simp + +#count_heartbeats! in +lemma swap_parallelComp₀ : swap Y T ∘ₖ (κ ∥ₖ ξ) = ξ ∥ₖ κ ∘ₖ swap X Z := by + by_cases hκ : IsSFiniteKernel κ + swap; · simp [hκ] + by_cases hη : IsSFiniteKernel ξ + swap; · simp [hη] + kernel_hom + cat_disch + +variable [IsSFiniteKernel η] [IsSFiniteKernel ξ] + +#count_heartbeats! in +lemma parallelComp_id_left_comp_parallelComp_orig : + (Kernel.id ∥ₖ ξ) ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η) := by + by_cases hκ : IsSFiniteKernel κ + swap; · simp [hκ] + ext a s hs + rw [comp_apply' _ _ _ hs, parallelComp_apply, + MeasureTheory.lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable] + rw [parallelComp_apply, Measure.prod_apply hs] + congr with x + rw [comp_apply' _ _ _ (measurable_prodMk_left hs)] + congr with y + rw [parallelComp_apply' hs, Kernel.id_apply, + lintegral_dirac' _ (measurable_measure_prodMk_left hs)] + +#count_heartbeats! in +lemma parallelComp_id_left_comp_parallelComp₀ : + (Kernel.id ∥ₖ ξ) ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η) := by + by_cases hκ : IsSFiniteKernel κ + swap; · simp [hκ] + kernel_monoidal + +#count_heartbeats! in +lemma parallelComp_id_right_comp_parallelComp_orig : + (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = (ξ ∘ₖ η) ∥ₖ κ := by + suffices swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ ((ξ ∘ₖ η) ∥ₖ κ) by + calc ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) + _ = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) := by + simp_rw [← comp_assoc, swap_swap, id_comp] + _ = swap Y T ∘ₖ (swap T Y ∘ₖ ((ξ ∘ₖ η) ∥ₖ κ)) := by rw [this] + _ = ξ ∘ₖ η ∥ₖ κ := by simp_rw [← comp_assoc, swap_swap, id_comp] + simp_rw [swap_parallelComp, comp_assoc, swap_parallelComp, ← comp_assoc, + parallelComp_id_left_comp_parallelComp] + +#count_heartbeats! in +lemma parallelComp_id_right_comp_parallelComp₀ : + (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = (ξ ∘ₖ η) ∥ₖ κ := by + by_cases hκ : IsSFiniteKernel κ + swap; · simp [hκ] + kernel_monoidal + +variable [IsSFiniteKernel κ] + +variable {κ' : Kernel X Y'} {η' : Kernel Y' Z'} [IsSFiniteKernel κ'] [IsSFiniteKernel η'] + +#count_heartbeats! in +lemma parallelComp_comp_parallelComp_orig : + (η ∥ₖ η') ∘ₖ (κ ∥ₖ κ') = (η ∘ₖ κ) ∥ₖ (η' ∘ₖ κ') := by + rw [← parallelComp_id_left_comp_parallelComp, ← parallelComp_id_right_comp_parallelComp, + ← comp_assoc, parallelComp_id_left_comp_parallelComp, comp_id] + +#count_heartbeats! in +lemma parallelComp_comp_parallelComp₀ : + (η ∥ₖ η') ∘ₖ (κ ∥ₖ κ') = (η ∘ₖ κ) ∥ₖ (η' ∘ₖ κ') := by + kernel_monoidal + +#count_heartbeats! in +lemma parallelComp_comp_prod_orig : + (η ∥ₖ η') ∘ₖ (κ ×ₖ κ') = (η ∘ₖ κ) ×ₖ (η' ∘ₖ κ') := by + rw [← parallelComp_comp_copy, ← comp_assoc, parallelComp_comp_parallelComp, + ← parallelComp_comp_copy] + +#count_heartbeats! in +lemma parallelComp_comp_prod₀ : + (η ∥ₖ η') ∘ₖ (κ ×ₖ κ') = (η ∘ₖ κ) ×ₖ (η' ∘ₖ κ') := by + kernel_monoidal + +#count_heartbeats! in +lemma discard_comp_deterministic_orig {f : X → Y} (hf : Measurable f) : + discard Y ∘ₖ (deterministic f hf) = discard X := + comp_discard _ + +#count_heartbeats! in +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] + +variable (κ : Kernel (X × Y) Z) + +#count_heartbeats! in +lemma parallelComp_self_comp_copy_orig [IsMarkovKernel κ] [IsDeterministic κ] : + (κ ∥ₖ κ) ∘ₖ copy (X × Y) = copy Z ∘ₖ κ := + parallelComp_self_comp_copy + +#count_heartbeats! in +lemma parallelComp_self_comp_copy₀ [IsMarkovKernel κ] [IsDeterministic κ] : + (κ ∥ₖ κ) ∘ₖ copy (X × Y) = copy Z ∘ₖ κ := by + kernel_disch + +end ProbabilityTheory.Kernel + +end diff --git a/KernelHomTests/Time.lean b/KernelHomTests/Time.lean deleted file mode 100644 index 305b4da4d..000000000 --- a/KernelHomTests/Time.lean +++ /dev/null @@ -1,76 +0,0 @@ -/- -Copyright (c) 2026 Gaëtan Serré. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Gaëtan Serré --/ -module - -public import KernelHom -public import Mathlib.Probability.Kernel.Composition.KernelLemmas - -/-! -# Timing of Kernel-Hom proofs - -Each lemma is proved twice: with its original Mathlib proof (`_orig`) and with Kernel-Hom (`_kh`). -Only lemmas whose Mathlib proof is a complete proof by integral manipulations are kept, so that the -comparison is meaningful. `trace.profiler` reports the elaboration time of each declaration. --/ - -public section - -open MeasureTheory ProbabilityTheory Kernel CategoryTheory - -set_option trace.profiler true -set_option trace.profiler.threshold 10 - -variable {X Y Z T X' Y' Z' : Type*} [MeasurableSpace X] [MeasurableSpace Y] - [MeasurableSpace Z] [MeasurableSpace T] [MeasurableSpace X'] [MeasurableSpace Y'] - [MeasurableSpace Z'] - -variable {κ : Kernel X Y} {ξ : Kernel Z T} {η : Kernel Y Z} - -lemma swap_parallelComp_orig : swap Y T ∘ₖ (κ ∥ₖ ξ) = ξ ∥ₖ κ ∘ₖ swap X Z := by - by_cases hκ : IsSFiniteKernel κ - swap; · simp [hκ] - by_cases hη : IsSFiniteKernel ξ - swap; · simp [hη] - ext ac s hs - simp_rw [comp_apply, parallelComp_apply, Measure.bind_apply hs (Kernel.aemeasurable _), - swap_apply, lintegral_dirac' _ (Kernel.measurable_coe _ hs), parallelComp_apply' hs, - Prod.fst_swap, Prod.snd_swap] - rw [MeasureTheory.lintegral_prod_symm] - swap; · exact ((Kernel.id.measurable_coe hs).comp measurable_swap).aemeasurable - congr with d - simp_rw [Prod.swap_prod_mk, Measure.dirac_apply' _ hs, ← Set.indicator_comp_right, - lintegral_indicator (measurable_prodMk_left hs)] - simp - -lemma swap_parallelComp_kh : swap Y T ∘ₖ (κ ∥ₖ ξ) = ξ ∥ₖ κ ∘ₖ swap X Z := by - by_cases hκ : IsSFiniteKernel κ - swap; · simp [hκ] - by_cases hη : IsSFiniteKernel ξ - swap; · simp [hη] - kernel_hom - aesop_cat - -variable [IsSFiniteKernel η] [IsSFiniteKernel ξ] - -lemma parallelComp_id_left_comp_parallelComp_orig : - (Kernel.id ∥ₖ ξ) ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η) := by - by_cases hκ : IsSFiniteKernel κ - swap; · simp [hκ] - ext a s hs - rw [comp_apply' _ _ _ hs, parallelComp_apply, - MeasureTheory.lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable] - rw [parallelComp_apply, Measure.prod_apply hs] - congr with x - rw [comp_apply' _ _ _ (measurable_prodMk_left hs)] - congr with y - rw [parallelComp_apply' hs, Kernel.id_apply, - lintegral_dirac' _ (measurable_measure_prodMk_left hs)] - -lemma parallelComp_id_left_comp_parallelComp_kh : - (Kernel.id ∥ₖ ξ) ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η) := by - by_cases hκ : IsSFiniteKernel κ - swap; · simp [hκ] - kernel_monoidal diff --git a/README.md b/README.md index 5223447da..ca65fea32 100644 --- a/README.md +++ b/README.md @@ -54,6 +54,10 @@ It first transforms the kernel equality into a categorical equality in `SFinKer` An additional consequence of the translation to `SFinKer` is that one can adapt the categorical monoidal composition `⊗≫` to kernels, resulting in a kernelized monoidal composition `⊗≫ₖ`. This composition automatically handles measurable equivalences, allowing for seamless composition of kernels while maintaining s-finiteness. +## Performance + +The translation is designed to be cheap: the equivalence between the original kernel equality and its categorical counterpart is proved by congruence from the translation lemmas (`comp_hom`, `parallelComp_hom`, ...) rather than by rewriting, and the terms are built directly with explicit universe levels and instances. Instances (`MeasurableSpace`, `IsSFiniteKernel`, the categorical instances of `SFinKer`), inferred types and recursively built objects (measurable equivalences, objects of `SFinKer`) are memoized in a cache reset at each call of the tactics. On the lemmas of `KernelHomTests/Heartbeats.lean`, the heartbeat count of the Kernel-Hom proofs is below that of the corresponding Mathlib proofs by integral manipulations. + ## Usage Add this in your `lakefile.toml`: diff --git a/lake-manifest.json b/lake-manifest.json index 2c2cd68f7..8679c22cb 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "63025c440a76f080d28ec38a8469e53d46809926", + "rev": "ac3d0c9671540e5ea16ebbbf0699e4f62f4e9f96", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e77bb5fe78158b37ba9907962055d8e5e5593782", + "rev": "e91fd45bf2bf9e9677b9257b3f8f2fd5cced2b31", "name": "eqlift", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lakefile.toml b/lakefile.toml index c9e72ae2d..4a00ff2ed 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -3,6 +3,7 @@ version = "0.1.0" keywords = ["math"] defaultTargets = ["KernelHom"] testDriver = "KernelHomTests" +lintDriver = "batteries/runLinter" [leanOptions] pp.unicode.fun = true # pretty-prints `fun a ↦ b`