Kernel Categorical Reasoning

8. Implementation of the translation🔗

The translation performed by kernel_hom traverses the kernel expression twice (once to lift it to a common universe level, once to translate it into SFinKer) and builds, at each node, an instance of a translation lemma such as comp_toHom_of_eq or comp_lift_of_eq. Three design choices keep this cheap and safe.

8.1. Proofs by congruence lemmas🔗

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. The translation lemmas are stated for this purpose with the translations of the subterms as hypotheses, so that each step of the translation is a single application of a lemma:

🔗theorem
ProbabilityTheory.Kernel.comp_toHom_of_eq.{x, y, z, u} {X : Type x}
  {Y : Type y} {Z : Type z} [MeasurableSpace X] [MeasurableSpace Y]
  [MeasurableSpace Z] {SX SY SZ : SFinKer} {ex : SX.carrier ≃ᵐ X}
  {ey : SY.carrier ≃ᵐ Y} {ez : SZ.carrier ≃ᵐ Z}
  {η : ProbabilityTheory.Kernel X Y} {κ : ProbabilityTheory.Kernel Z X}
  [ProbabilityTheory.IsSFiniteKernel η]
  [ProbabilityTheory.IsSFiniteKernel κ] {f : SZ ⟶ SX} {g : SX ⟶ SY}
  (hf : f = κ.toHom) (hg : g = η.toHom) :
  CategoryTheory.CategoryStruct.comp f g = (η.comp κ).toHom
ProbabilityTheory.Kernel.comp_toHom_of_eq.{x,
    y, z, u}
  {X : Type x} {Y : Type y} {Z : Type z}
  [MeasurableSpace X] [MeasurableSpace Y]
  [MeasurableSpace Z] {SX SY SZ : SFinKer}
  {ex : SX.carrier ≃ᵐ X}
  {ey : SY.carrier ≃ᵐ Y}
  {ez : SZ.carrier ≃ᵐ Z}
  {η : ProbabilityTheory.Kernel X Y}
  {κ : ProbabilityTheory.Kernel Z X}
  [ProbabilityTheory.IsSFiniteKernel η]
  [ProbabilityTheory.IsSFiniteKernel κ]
  {f : SZ ⟶ SX} {g : SX ⟶ SY}
  (hf : f = κ.toHom) (hg : g = η.toHom) :
  CategoryTheory.CategoryStruct.comp f g =
    (η.comp κ).toHom

The translation f ≫ g of a composition η ∘ₖ κ, from the translations f of κ and g of η (see comp_toHom).

The same lemmas serve both directions: kernelToHom and homToKernel both return a proof of f = κ.toHom, where f is the morphism and κ the kernel. The equality of propositions is then obtained from toHom_congr_of_eq (or lift_congr_of_eq for the lifting, which follows the same structure in Eq-Lift).

🔗theorem
ProbabilityTheory.Kernel.toHom_congr_of_eq.{x, y, u} {X : Type x}
  {Y : Type y} [MeasurableSpace X] [MeasurableSpace Y] {SX SY : SFinKer}
  {ex : SX.carrier ≃ᵐ X} {ey : SY.carrier ≃ᵐ Y}
  {κ η : ProbabilityTheory.Kernel X Y}
  [ProbabilityTheory.IsSFiniteKernel κ]
  [ProbabilityTheory.IsSFiniteKernel η] {f g : SX ⟶ SY}
  (hf : f = κ.toHom) (hg : g = η.toHom) : (κ = η) = (f = g)
ProbabilityTheory.Kernel.toHom_congr_of_eq.{x,
    y, u}
  {X : Type x} {Y : Type y}
  [MeasurableSpace X] [MeasurableSpace Y]
  {SX SY : SFinKer} {ex : SX.carrier ≃ᵐ X}
  {ey : SY.carrier ≃ᵐ Y}
  {κ η : ProbabilityTheory.Kernel X Y}
  [ProbabilityTheory.IsSFiniteKernel κ]
  [ProbabilityTheory.IsSFiniteKernel η]
  {f g : SX ⟶ SY} (hf : f = κ.toHom)
  (hg : g = η.toHom) : (κ = η) = (f = g)

The equivalence between an equality of kernels and the equality of their translations f and g, given by toHom_congr.

8.2. Terms built with Qq🔗

The terms and the lemma instances are built with the quotations q(...) of Qq. A quotation is elaborated when the tactic is compiled, and only instantiated at run time: the result is as cheap as an explicit application (mkAppN with explicit universe levels and instances), without the unification and instance synthesis of mkAppM, which dominated the cost of the translation. Moreover, the quotations are type-checked against the statements of the lemmas, so that an argument in the wrong position is a compilation error rather than an ill-typed proof at run time. The category-theoretic instances of SFinKer (Category, MonoidalCategory, ...) are synthesized at compilation as well.

The expressions are typed by the expressions of their types: Q(Kernel $X $Y) is the type of the expressions of a kernel from X to Y. The kernel and categorical expressions are matched syntactically, with match_expr, and their subterms are then given such types. The recursion itself works on untyped expressions: kernelToHomQ gives the typed view of the translation of a subterm, assuming that the carriers of its source and target are those of homCarrier.

🔗opaque
kernelToHomQ {u : Lean.Level} {X Y : Q(Type u)}
  {mX : Q(MeasurableSpace «$X»)} {mY : Q(MeasurableSpace «$Y»)}
  {SX SY : Q(SFinKer)} (ex : Q(«$SX».carrier ≃ᵐ «$X»))
  (ey : Q(«$SY».carrier ≃ᵐ «$Y»)) (κ : Lean.Expr) :
  Lean.MetaM
    ((κ : Q(ProbabilityTheory.Kernel «$X» «$Y»)) ×
      (x : Q(ProbabilityTheory.IsSFiniteKernel «$κ»)) ×
        (f : Q(«$SX» ⟶ «$SY»)) × Q(«$f» = «$κ».toHom))
kernelToHomQ {u : Lean.Level}
  {X Y : Q(Type u)}
  {mX : Q(MeasurableSpace «$X»)}
  {mY : Q(MeasurableSpace «$Y»)}
  {SX SY : Q(SFinKer)}
  (ex : Q(«$SX».carrier ≃ᵐ «$X»))
  (ey : Q(«$SY».carrier ≃ᵐ «$Y»))
  (κ : Lean.Expr) :
  Lean.MetaM
    ((κ :
      Q(ProbabilityTheory.Kernel «$X»
          «$Y»)) ×
      (x :
        Q(ProbabilityTheory.IsSFiniteKernel
            «$κ»)) ×
        (f : Q(«$SX» ⟶ «$SY»)) ×
          Q(«$f» = «$κ».toHom))

Typed version of kernelToHom, for a kernel κ : Kernel X Y and the carriers ex : SX ≃ᵐ X and ey : SY ≃ᵐ Y of X and Y given by homCarrier (as in kernelToHom): returns κ with its IsSFiniteKernel instance, its translation f : SX ⟶ SY and the proof of f = κ.toHom.

8.3. Memoization🔗

The instances (MeasurableSpace X, IsSFiniteKernel κ, ...) and the recursively built objects (measurable equivalences, objects of SFinKer) are memoized in a cache which is reset at the beginning of each transformation. The cache lives in Eq-Lift:

🔗structure
TransformCache : Type
TransformCache : Type

The cache of the lifting/unlifting transformations.

Constructor

TransformCache.mk

Fields

insts : Std.HashMap Lean.Expr Lean.Expr

Synthesized instances, keyed by the class application.

memo : Std.HashMap (Lean.Name × Lean.Expr) (Array Lean.Expr)

Memoized computations, keyed by a tag and an expression.

🔗def
resetTransformCache : Lean.MetaM Unit
resetTransformCache : Lean.MetaM Unit

Empties the cache. To be called at the beginning of each transformation.

🔗def
synthInstanceCached (type : Lean.Expr) : Lean.MetaM Lean.Expr
synthInstanceCached (type : Lean.Expr) :
  Lean.MetaM Lean.Expr

synthInstance with memoization.

🔗def
memoized (tag : Lean.Name) (key : Lean.Expr)
  (f : Lean.MetaM (Array Lean.Expr)) : Lean.MetaM (Array Lean.Expr)
memoized (tag : Lean.Name)
  (key : Lean.Expr)
  (f : Lean.MetaM (Array Lean.Expr)) :
  Lean.MetaM (Array Lean.Expr)

Memoizes the computation f, keyed by tag and key.

8.4. Carriers🔗

During the lifting, each measurable space comes with its lift to the common universe level and the measurable equivalence between them, computed once per carrier by liftCarrier, and recovered from the lifted space by unliftCarrier. Both live in Eq-Lift:

🔗opaque
liftCarrier (w : Lean.Level) (X : Lean.Expr) :
  Lean.MetaM
    ((x : Lean.Level) ×
      (X : Q(Type x)) ×
        (x_1 : Q(MeasurableSpace «$X»)) ×
          (X' : Q(Type w)) ×
            (x_2 : Q(MeasurableSpace «$X'»)) × Q(«$X'» ≃ᵐ «$X»))
liftCarrier (w : Lean.Level)
  (X : Lean.Expr) :
  Lean.MetaM
    ((x : Lean.Level) ×
      (X : Q(Type x)) ×
        (x_1 : Q(MeasurableSpace «$X»)) ×
          (X' : Q(Type w)) ×
            (x_2 :
              Q(MeasurableSpace «$X'»)) ×
              Q(«$X'» ≃ᵐ «$X»))

The lift X' of a measurable space X : Type x to the universe w, together with the MeasurableSpace instances of X and X' and the measurable equivalence X' ≃ᵐ X. Products are lifted componentwise, PUnit to PUnit and the other types to ULift.

🔗def
unliftCarrier (w : Lean.Level) (X' : Lean.Expr) :
  Lean.MetaM
    ((X' : Q(Type w)) ×
      (x : Q(MeasurableSpace «$X'»)) ×
        (x_1 : Lean.Level) ×
          (X : Q(Type x_1)) ×
            (x_2 : Q(MeasurableSpace «$X»)) × Q(«$X'» ≃ᵐ «$X»))
unliftCarrier (w : Lean.Level)
  (X' : Lean.Expr) :
  Lean.MetaM
    ((X' : Q(Type w)) ×
      (x : Q(MeasurableSpace «$X'»)) ×
        (x_1 : Lean.Level) ×
          (X : Q(Type x_1)) ×
            (x_2 :
              Q(MeasurableSpace «$X»)) ×
              Q(«$X'» ≃ᵐ «$X»))

A lifted measurable space X' : Type w with its original space X (see getOriginalType), their MeasurableSpace instances and the measurable equivalence X' ≃ᵐ X of liftCarrier.

After the lifting, all the carriers live in the same universe, in which the translation takes place.

🔗def
kernelLevel (κ : Lean.Expr) : Lean.MetaM Lean.Level
kernelLevel (κ : Lean.Expr) :
  Lean.MetaM Lean.Level

The universe level w of the carriers of a lifted kernel κ : Kernel X Y: all the carriers of a lifted equality live in Type w.

The translation to SFinKer needs more data about each carrier X: the object of 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 toHom and of the translation lemmas. They are computed once per carrier by homCarrier.

🔗opaque
homCarrier (u : Lean.Level) (X : Lean.Expr) :
  Lean.MetaM
    ((X : Q(Type u)) ×
      (x : Q(MeasurableSpace «$X»)) ×
        (SX : Q(SFinKer)) × Q(«$SX».carrier ≃ᵐ «$X»))
homCarrier (u : Lean.Level)
  (X : Lean.Expr) :
  Lean.MetaM
    ((X : Q(Type u)) ×
      (x : Q(MeasurableSpace «$X»)) ×
        (SX : Q(SFinKer)) ×
          Q(«$SX».carrier ≃ᵐ «$X»))

The object SX of SFinKer.{u} associated with a measurable space X : Type u, together with the MeasurableSpace instance of X and the measurable equivalence SX ≃ᵐ X. Products are decomposed into tensor products and PUnit into the monoidal unit, so that the monoidal tactics see the tensor structure (memoized).

🔗def
homCarrierOfEquiv (u : Lean.Level) (e₀ : Lean.Expr) :
  Lean.MetaM
    ((X : Q(Type u)) ×
      (x : Q(MeasurableSpace «$X»)) ×
        (SX : Q(SFinKer)) ×
          (_ : Q(«$SX».carrier ≃ᵐ «$X»)) ×
            (v : Lean.Level) ×
              (X₀ : Q(Type v)) ×
                (x_2 : Q(MeasurableSpace «$X₀»)) × Q(«$X» ≃ᵐ «$X₀»))
homCarrierOfEquiv (u : Lean.Level)
  (e₀ : Lean.Expr) :
  Lean.MetaM
    ((X : Q(Type u)) ×
      (x : Q(MeasurableSpace «$X»)) ×
        (SX : Q(SFinKer)) ×
          (_ : Q(«$SX».carrier ≃ᵐ «$X»)) ×
            (v : Lean.Level) ×
              (X₀ : Q(Type v)) ×
                (x_2 :
                  Q(MeasurableSpace
                      «$X₀»)) ×
                  Q(«$X» ≃ᵐ «$X₀»))

For a measurable equivalence e₀ : X ≃ᵐ X₀ from a lifted measurable space X : Type u to the original space X₀ : Type v (an equivalence of Kernel.lift, or a component of one): the data of homCarrier for X, then X₀ with its universe level and its MeasurableSpace instance, and e₀.

In the other direction, the carrier of an object is computed by typeOfObj, and its data by homCarrier again.

🔗def
objCarrier (u : Lean.Level) (SX : Lean.Expr) :
  Lean.MetaM
    ((SX : Q(SFinKer)) ×
      (X : Q(Type u)) ×
        (x : Q(MeasurableSpace «$X»)) × Q(«$SX».carrier ≃ᵐ «$X»))
objCarrier (u : Lean.Level)
  (SX : Lean.Expr) :
  Lean.MetaM
    ((SX : Q(SFinKer)) ×
      (X : Q(Type u)) ×
        (x : Q(MeasurableSpace «$X»)) ×
          Q(«$SX».carrier ≃ᵐ «$X»))

An object SX of SFinKer.{u} with its carrier X, the MeasurableSpace instance of X and the measurable equivalence SX ≃ᵐ X of homCarrier.