Kernel Categorical Reasoning

9.Β 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_hom or comp_lift. Two design choices keep this cheap.

9.1.Β 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 mkCongr, mkCongrArg and mkEqTrans. The equality of propositions is then obtained from hom_congr (or lift_congr) and propext, see mkHomCongrProof.

πŸ”—def
mkHomCongrProof (lhs rhs pl pr : Lean.Expr) : Lean.MetaM Lean.Expr
mkHomCongrProof
  (lhs rhs pl pr : Lean.Expr) :
  Lean.MetaM Lean.Expr

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).

9.2.Β 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 SFinKer, ...), the inferred types of kernels 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.

types : Std.HashMap Lean.Expr Lean.Expr

Inferred types, keyed by the expression.

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
inferTypeCached (e : Lean.Expr) : Lean.MetaM Lean.Expr
inferTypeCached (e : Lean.Expr) :
  Lean.MetaM Lean.Expr

inferType 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.

9.3.Β 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.

πŸ”—structure
Carrier : Type
Carrier : Type

A measurable space: the carrier type and its universe level.

Constructor

Carrier.mk

Fields

type : Lean.Expr

The carrier type.

lvl : Lean.Level

The universe level of the carrier type.

πŸ”—def
Carrier.inst (c : Carrier) : Lean.MetaM Lean.Expr
Carrier.inst (c : Carrier) :
  Lean.MetaM Lean.Expr

The MeasurableSpace instance of a carrier (cached).

πŸ”—def
Carrier.lift (c : Carrier) (maxLvl : Lean.Level) :
  Lean.MetaM (Lean.Expr Γ— Carrier)
Carrier.lift (c : Carrier)
  (maxLvl : Lean.Level) :
  Lean.MetaM (Lean.Expr Γ— Carrier)

Same as constructMeasurableEquiv, for a carrier.

πŸ”—def
getCarriersFromKernel (ΞΊ : Lean.Expr) : Lean.MetaM (Carrier Γ— Carrier)
getCarriersFromKernel (ΞΊ : Lean.Expr) :
  Lean.MetaM (Carrier Γ— Carrier)

Extract the source and target carriers of a kernel.

πŸ”—opaque
constructMeasurableEquiv (e : Lean.Expr) (eLevel maxLvl : Lean.Level) :
  Lean.MetaM (Lean.Expr Γ— Lean.Expr)
constructMeasurableEquiv (e : Lean.Expr)
  (eLevel maxLvl : Lean.Level) :
  Lean.MetaM (Lean.Expr Γ— Lean.Expr)

Build the measurable equivalence X' ≃ᡐ X between the lift X' of e to the universe maxLvl and e itself, recursively on products. Returns the equivalence and X'.

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 hom and of the translation lemmas. These are computed once per carrier by computeSFinkerOf and idME, and gathered in a HomCarrier.

πŸ”—structure
HomCarrier : Type
HomCarrier : Type

A carrier X together with its MeasurableSpace instance, its object obj in SFinKer and the measurable equivalence equiv : obj ≃ᡐ X.

Constructor

HomCarrier.mk

Extends

Fields

type : Lean.Expr
Inherited from
  1. Carrier
lvl : Lean.Level
Inherited from
  1. Carrier
inst : Lean.Expr

The MeasurableSpace instance.

obj : Lean.Expr

The object of SFinKer.

equiv : Lean.Expr

The measurable equivalence obj ≃ᡐ X.

πŸ”—def
HomCarrier.mk' (X : Carrier) : Lean.MetaM HomCarrier
HomCarrier.mk' (X : Carrier) :
  Lean.MetaM HomCarrier

Build the HomCarrier of a carrier.

πŸ”—def
HomCarrier.sfinite (X Y : HomCarrier) (ΞΊ : Lean.Expr) :
  Lean.MetaM Lean.Expr
HomCarrier.sfinite (X Y : HomCarrier)
  (ΞΊ : Lean.Expr) : Lean.MetaM Lean.Expr

The IsSFiniteKernel instance of ΞΊ : Kernel X Y (cached).

πŸ”—opaque
computeSFinkerOf (X : Lean.Expr) (xLvl : Lean.Level) :
  Lean.MetaM Lean.Expr
computeSFinkerOf (X : Lean.Expr)
  (xLvl : Lean.Level) :
  Lean.MetaM Lean.Expr

Compute the SFinKer object corresponding to a measurable space X : Type xLvl, decomposing products into tensor products and PUnit into the monoidal unit (memoized).

πŸ”—opaque
idME (X : Lean.Expr) (xLvl : Lean.Level) : Lean.MetaM Lean.Expr
idME (X : Lean.Expr) (xLvl : Lean.Level) :
  Lean.MetaM Lean.Expr

The measurable equivalence X ≃ᡐ X, built recursively on products so that it matches the decomposition of computeSFinkerOf (memoized).

Finally, every morphism built during the translation (≫, βŠ—β‚˜, whiskers, πŸ™, Ξ΅, Ξ”, braiding) takes as implicit arguments the category-theoretic instances of 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 SFinKerInsts, which also provides the constructors of the morphisms.

πŸ”—structure
SFinKerInsts : Type
SFinKerInsts : Type

The category-theoretic instances of SFinKer.{u}.

Constructor

SFinKerInsts.mk

Fields

u : Lean.Level

The universe level.

C : Lean.Expr

SFinKer.{u}.

cat : Lean.Expr

Category SFinKer.

catStruct : Lean.Expr

CategoryStruct SFinKer.

monoidal : Lean.Expr

MonoidalCategory SFinKer.

monStruct : Lean.Expr

MonoidalCategoryStruct SFinKer.

πŸ”—def
sfinkerInsts (u : Lean.Level) : Lean.MetaM SFinKerInsts
sfinkerInsts (u : Lean.Level) :
  Lean.MetaM SFinKerInsts

The category-theoretic instances of SFinKer.{u} (cached).