Tactics and theorems related to casting

Stream: mathlib4

[Patrick Nicodemus]

I started a formalization in category theory using lots of dependent types and some of my definitions involve casting, then I have to reason about equalities between terms with casts inside.

An example theorem I'm trying to prove right now is:

⊢ comp (p1 ▸ q1 ▸ comp f g) h =
  comp f (p2 ▸ q2 ▸ comp g h)

where the p1, q1, p2, q2 are paths that relate terms in the type of f, g, h.

What tactics/theorems should I be aware of that can dispatch some of these obligations

[Yan Yablonovskiy 🇺🇦]

This could be helpful, if you didn't know about it yet:
docs#Mathlib.Tactic.convert

[Eric Wieser]

cases p1 is likely to make proress on that goal

[Eric Wieser]

But without a #mwe it's hard to say

[Aaron Liu]

I've found that grind worked surprisingly well at pure casting goals (maybe since it's an equality reasoning tactic)

[Patrick Nicodemus]

Eric Wieser said:

But without a #mwe it's hard to say

Hi Eric. I hope the following code is fairly straightforward.

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Bicategory.Basic

open CategoryTheory
section ParametricQuiver
set_option linter.unusedVariables false

class hzQuiver.{v1, u1} (O : Type u1) where
  HHom : O -> O -> Type v1

class ParametricQuiver.{v₁, u₁, v₂, u₂, v₃, u₃}
  (O₁ : Type u₁) [Quiver.{v₁} O₁] (O₂ : Type u₂) [Quiver.{v₂} O₂]
  (HHom : O₁ -> O₂ -> Type u₃) where
  two_cells : forall {o₁ o₁' : O₁} (f : Quiver.Hom o₁ o₁') {o₂ o₂' : O₂} (g : Quiver.Hom o₂ o₂'),
    HHom o₁ o₂ -> HHom o₁' o₂' -> Sort v₃

end ParametricQuiver

section ParametricCategory
universe u₁ v₁ u₂ v₂ w₁ w₂

open ParametricQuiver in

/--
A parametric CategoryStruct over two CategoryStructs C and D.
- For each pair of objects (c, d) in C × D, we have a type of objects Ob c d
- For each pair of morphisms (f : c → c') in C and (g : d → d') in D,
  and objects X : Ob c d and Y : Ob c' d', we have a type of morphisms Hom f g X Y
-/

local notation:50 "□(" f "," g ";" X "," Y ")" => two_cells f g X Y

class ParametricCategoryStruct (C : Type u₁) (D : Type u₂)
    [Ccat : CategoryStruct.{v₁, u₁} C] [Dcat: CategoryStruct.{v₂,u₂} D]
    (HHom : C -> D -> Type w₁) [ParametricQuiver.{v₁ + 1, u₁, v₂ + 1, u₂, w₂ + 1, w₁} C D HHom]
    : Type (max u₁ v₁ u₂ v₂ w₁ w₂ + 1) where
  /-- Identity morphism over the pair of identity morphisms -/
  id : ∀ {c : C} {d : D} (F : HHom c d), ParametricQuiver.two_cells (𝟙 c) (𝟙 d) F F
  /-- Composition of morphisms over composition of base morphisms -/
  comp : ∀ {c c' c'' : C} {d d' d'' : D}
    {f : c ⟶ c'} {f' : c' ⟶ c''} {g : d ⟶ d'} {g' : d' ⟶ d''}
    {X : HHom c d} {Y : HHom c' d'} {Z : HHom c'' d''},
    □(f,g; X, Y) → □(f', g'; Y, Z) → □( (f ≫ f'), (g ≫ g'); X, Z)

def special2cell {C: Type u₁} {D : Type u₂} [Category C] [Category D]
  (HHom : C -> D -> Type v₁)
  [ParametricQuiver _ _ HHom]
  [ParametricCategoryStruct C D HHom] {x : C} {y : D}
  (f g : HHom x y) :=
  □(𝟙 x, 𝟙 y; f, g)

/--
A parametric Category over two Categories C and D.
Extends ParametricCategoryStruct with identity and associativity axioms.
These axioms state that the parametric structure respects the categorical structure of C and D.
-/
class ParametricCategory (C : Type u₁) (D : Type u₂)
    [Category.{v₁} C] [Category.{v₂} D]
    (HHom : C -> D -> Type w₁)
    [ParametricQuiver _ _ HHom]
    extends ParametricCategoryStruct.{u₁, v₁, u₂, v₂, w₁, w₂} C D HHom where
  /-- Identity morphisms are left identities for composition,
      modulo the left identity laws in C and D -/
  id_comp : ∀ {c c' : C} {d d' : D} {f : c ⟶ c'} {g : d ⟶ d'}
    {X : HHom c d} {Y : HHom c' d'} (h : □(f, g; X, Y)),
    (Category.id_comp f) ▸ (Category.id_comp g) ▸ (comp (id X) h) = h
      -- ((Category.id_comp f).symm ▸ (Category.id_comp g).symm ▸ h : □((𝟙 c ≫ f), (𝟙 d ≫ g); X, Y))
  /-- Identity morphisms are right identities for composition,
      modulo the right identity laws in C and D -/
  comp_id : ∀ {c c' : C} {d d' : D} {f : c ⟶ c'} {g : d ⟶ d'}
    {X : HHom c d} {Y : HHom c' d'} (h : □(f, g; X, Y)),
    (Category.comp_id f) ▸ (Category.comp_id g) ▸ comp h (id Y) = h
  /-- Composition is associative, modulo the associativity laws in C and D -/
  assoc : ∀ {c₀ c₁ c₂ c₃ : C} {d₀ d₁ d₂ d₃ : D}
    {f₁ : c₀ ⟶ c₁} {f₂ : c₁ ⟶ c₂} {f₃ : c₂ ⟶ c₃}
    {g₁ : d₀ ⟶ d₁} {g₂ : d₁ ⟶ d₂} {g₃ : d₂ ⟶ d₃}
    {X : HHom c₀ d₀} {Y : HHom c₁ d₁} {Z : HHom c₂ d₂} {W : HHom c₃ d₃}
    (h₁ : □(f₁, g₁; X,Y)) (h₂ : □(f₂, g₂; Y, Z)) (h₃ : □(f₃, g₃; Z, W)),
    comp (comp h₁ h₂) h₃ =
      (Category.assoc f₁ f₂ f₃ ▸ Category.assoc g₁ g₂ g₃ ▸
        comp h₁ (comp h₂ h₃) : □((f₁ ≫ f₂) ≫ f₃, (g₁ ≫ g₂) ≫ g₃; X, W))

instance special2cellCatStruct.{u, v} (C : Type u) (D : Type v) [Category C] [Category D]
  (HHom : C -> D -> Type w₁)
  [ParametricQuiver C D HHom]
  [ParametricCategoryStruct C D HHom] {x : C} {y : D}
  : CategoryStruct (HHom x y) := {
    Hom := special2cell HHom
    id := ParametricCategoryStruct.id
    comp := fun {X Y Z} (f : special2cell HHom X Y) (g : special2cell HHom Y Z) =>
      (Category.comp_id (𝟙 x) ▸ Category.comp_id (𝟙 y) ▸
        ParametricCategoryStruct.comp f g :
        □(𝟙 x, 𝟙 y; X, Z))
  }

set_option pp.proofs true

open ParametricCategoryStruct in
instance special2cellCat.{u} (C : Type u) [Category C]
 (D : Type v) [Category D]
 (HHom : C -> D -> Type w₁)
 [ParametricQuiver _ _ HHom]
 [ParametricCategory C D HHom] {x : C} {y : D}
  : Category (HHom x y) := {
    id_comp := fun {X Y} f => by
      dsimp [CategoryStruct.comp, special2cellCatStruct]
      exact ParametricCategory.id_comp f
    comp_id := fun {X Y} f => by
      dsimp [CategoryStruct.comp, special2cellCatStruct]
      exact ParametricCategory.comp_id f
    assoc := fun {W X Y Z} f g h => by
      dsimp [CategoryStruct.comp, special2cellCatStruct]
      apply (congr_arg (fun z => (@Eq.rec
          (x ⟶ x) (𝟙 x ≫ 𝟙 x) (fun x_1 h ↦ □(x_1,𝟙 y;W,Z))
          z
          (𝟙 x) (special2cellCatStruct._proof_1 C) : □(𝟙 x,𝟙 y;W,Z))))
      apply (congr_arg (fun z => (@Eq.rec (y ⟶ y) (𝟙 y ≫ 𝟙 y) (fun x_1 h ↦ □(𝟙 x ≫ 𝟙 x,x_1;W,Z))
        z (𝟙 y) (special2cellCatStruct._proof_1 D) : □(𝟙 x ≫ 𝟙 x,𝟙 y;W,Z))))

      apply eq_of_heq
      sorry
  }

end ParametricCategory

[Eric Wieser]

This looks like you're stepping into "equality of categories is evil" territory, which perhaps @Joël Riou can advise on how to avoid

[Patrick Nicodemus]

Eric Wieser said:

This looks like you're stepping into "equality of categories is evil" territory, which perhaps - can advise on how to avoid

Okay. I'm not sure I follow. My motivation is that I can define a category of triples (R, S, M) where R, S are rings and M is an R-S bimodule; morphisms are triples (f,g, phi) where f,g are ring homomorphisms and phi is a module homomorphism. Given this, if I fix some R and S and hold them constant, I should have a category whose objects are R-S bimodules and whose morphisms are of the form (id, id, phi). I need casting along equality here to make use of id * id = id when defining composition, but I don't see how this is categorically evil

[Eric Wieser]

I think the usual pattern is to provide some kind of associator as a data field, instead of using things like Category.assoc f₁ f₂ f₃ ▸ Category.assoc g₁ g₂ g₃ ▸. But I'm not the expert here, hopefully someone who is can chime in

[Patrick Nicodemus]

Yan Yablonovskiy 🇺🇦 said:

This could be helpful, if you didn't know about it yet:
docs#Mathlib.Tactic.convert

This is helpful as I don't know any of the lean tactics yet. However congr 1 already results in some unprovable goals so I will need something a little weaker I think.

[Patrick Nicodemus]

Aaron Liu said:

I've found that grind worked surprisingly well at pure casting goals (maybe since it's an equality reasoning tactic)

When using grind should I be importing lots of modules that might contain relevant hints? Does grind have an associated hint database?

[Joël Riou]

In this situation, it could be convenient to use a trick that I have used for shifts docs#CategoryTheory.shiftFunctorAdd' and pseudofunctors docs#CategoryTheory.Pseudofunctor.mapComp' by allowing that the compositions in C and D are not "by definition", see assumptions hf'' and hg'' below:

def ParametricCategoryStruct.comp' {C : Type u₁} {D : Type u₂}
    [CategoryStruct.{v₁, u₁} C] [CategoryStruct.{v₂,u₂} D]
    {HHom : C -> D -> Type w₁} [ParametricQuiver C D HHom]
    [ParametricCategoryStruct C D HHom]
    {c c' c'' : C} {d d' d'' : D}
    {f : c ⟶ c'} {f' : c' ⟶ c''} {g : d ⟶ d'} {g' : d' ⟶ d''}
    {X : HHom c d} {Y : HHom c' d'} {Z : HHom c'' d''}
    (α : □(f,g; X, Y)) (β : □(f', g'; Y, Z))
    {f'' : c ⟶ c''} {g'' : d ⟶ d''} (hf'' : f ≫ f' = f'' := by cat_disch) (hg'' : g ≫ g' = g'' := by cat_disch) :
    □(f'', g''; X, Z) := by
  subst hf'' hg''
  exact comp α β

One way to phrase the associativity would be:

  assoc : ∀ {c₀ c₁ c₂ c₃ : C} {d₀ d₁ d₂ d₃ : D}
    {f₁ : c₀ ⟶ c₁} {f₂ : c₁ ⟶ c₂} {f₃ : c₂ ⟶ c₃}
    {g₁ : d₀ ⟶ d₁} {g₂ : d₁ ⟶ d₂} {g₃ : d₂ ⟶ d₃}
    {X : HHom c₀ d₀} {Y : HHom c₁ d₁} {Z : HHom c₂ d₂} {W : HHom c₃ d₃}
    (h₁ : □(f₁, g₁; X,Y)) (h₂ : □(f₂, g₂; Y, Z)) (h₃ : □(f₃, g₃; Z, W)),
    comp (comp h₁ h₂) h₃ = ParametricCategoryStruct.comp' h₁ (comp h₂ h₃)

(See docs#CategoryTheory.shiftFunctorAdd'_assoc_hom_app or docs#CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom for inspiration on how the associativity could be phrased more generally by introducing maps that are equal to compositions f₁ ≫ f₂ or f₂ ≫ f₃, etc.)

[Joël Riou]

(In a more general phrasing of the associativity, all the comp would be replaced by comp'.)

[Chris Henson]

Patrick Nicodemus said:

Aaron Liu said:

I've found that grind worked surprisingly well at pure casting goals (maybe since it's an equality reasoning tactic)

When using grind should I be importing lots of modules that might contain relevant hints? Does grind have an associated hint database?

Generally the grind attributes are annotating the definitions/theorems they are used with, so you don't usually have to search for any extra imports. Some rules are scoped to a namespace meaning that you have to open or open scoped for them to be used, but I don't believe the category theory modules use this feature.

[Patrick Nicodemus]

@Joël Riou Thanks, great answer.

(hf'' : f ≫ f' = f'' := by cat_disch)
Oh, that's cute. I don't think Rocq has this feature. I assume this means that we try to prove hf'' by cat_disch and this fails then the user should manually supply a tactic