Kernel Categorical Reasoning

6. Categorical tactics for kernels🔗

Two of the most powerful tactics for categories in Mathlib are monoidal and coherence. To facilitate the use of these tactics for kernel equalities, Kernel-Hom provides the kernel_disch, kernel_monoidal, kernel_coherence and aesop_kernel tactics which first apply kernel_hom to the goal to translate the kernel equality into a categorical equality in the SFinKer category, then apply, respectively, cat_disch and monoidal, monoidal, coherence, or aesop (with the CategoryTheory rule set) to solve or simplify the categorical equality. kernel_disch is the tactic to use by default: it tries both cat_disch and monoidal, and before giving up, it also normalizes the tensor products of morphisms, which allows it to use the exchange law and the comonoid laws of copy and discard, including for deterministic and Markov kernels.

🔗def
kernelDisch : Lean.ParserDescr
kernelDisch : Lean.ParserDescr

The kernel_disch tactic applies the kernel_hom transformation to the goal and then tries to solve the resulting goal with:

  1. cat_disch;

  2. monoidal;

  3. cat_disch, after merging the whiskers and the compositions of tensor products into single tensor products, together with the counit and comultiplication laws of the comonoid structure and of the deterministic and Markov kernels. This handles the exchange law and the laws hidden in tensor products;

  4. monoidal, after splitting the tensor products of compositions and applying the coassociativity of the comultiplication.

As it tries both cat_disch and monoidal, it is the tactic to use by default.

🔗def
kernelMonoidal : Lean.ParserDescr
kernelMonoidal : Lean.ParserDescr

The kernel_monoidal tactic applies the kernel_hom transformation to the goal and then invokes the monoidal tactic to solve or simplify the resulting goal.

🔗def
kernelCoherence : Lean.ParserDescr
kernelCoherence : Lean.ParserDescr

The kernel_coherence tactic applies the kernel_hom transformation to the goal and then invokes the coherence tactic to solve the resulting goal.

🔗def
aesopKernel : Lean.ParserDescr
aesopKernel : Lean.ParserDescr

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.

For more details on the implementation of the monoidal and coherence tactics, see the documentation made by @Yuma Mizuno.