SemilatSup coercion

Stream: mathlib4

[Lars Ericson]

Looking at port of SemiLatSup. The original by @Yaël Dillies is here. I got up to here in the port (this typechecks up to but excluding the last line):

import Mathlib.Order.Category.PartOrdCat
import Mathlib.Order.Hom.Lattice
universe u
open CategoryTheory
variable {X: Type u}
structure SemilatSup : Type (u + 1) where
  pt : Type u
  [isSemilatticeSup : SemilatticeSup X]
  [isOrderBot : OrderBot X]
set_option linter.uppercaseLean3 false in
#align SemilatSup SemilatSup

structure SemilatInf : Type (u + 1) where
  pt : Type u
  [isSemilatticeInf : SemilatticeInf X]
  [isOrderTop : OrderTop X]
set_option linter.uppercaseLean3 false in
#align SemilatInf SemilatInf

namespace SemilatSup

instance : CoeSort SemilatSup (Type _) := ⟨SemilatSup.X⟩

The Lean 3 text of the last line is

instance : has_coe_to_sort SemilatSup Type* := ⟨SemilatSup.X⟩

Note I had to add this in the text above to get to line 52:

variable {X: Type u}

The instance fails in Lean 4 with this error:

Semilat.lean:52:19
don't know how to synthesize implicit argument
  @SemilatSup ?m.1223
context:
X: Type u
⊢ Type ?u.1222

when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
Semilat.lean:52:43
invalid field notation, type is not of the form (C ...) where C is a constant
  SemilatSup
has type
  Type (?u.1235 + 1)

I need a hint.

[Yaël Dillies]

Do instance : CoeSort SemilatSup.{u} (Type u) or something like that.

[Lars Ericson]

@Yaël Dillies the mathport script took

structure SemilatSup : Type.{u+1} :=
(X : Type.{u})
[is_semilattice_sup : semilattice_sup X]
[is_order_bot : order_bot X]

structure SemilatInf : Type.{u+1} :=
(X : Type.{u})
[is_semilattice_inf : semilattice_inf X]
[is_order_top : order_top X]

to

structure SemilatSup : Type (u + 1) where
  pt : Type u
  [isSemilatticeSup : SemilatticeSup X]
  [isOrderBot : OrderBot X]

structure SemilatInf : Type (u + 1) where
  pt : Type u
  [isSemilatticeInf : SemilatticeInf X]
  [isOrderTop : OrderTop X]

so (X : Type.{u}) becomes pt: Type u but other fields are still referring to X like [isOrderBot : OrderBot X]. If I change the port to

structure SemilatSup : Type (u + 1) where
  X : Type u
  [isSemilatticeSup : SemilatticeSup X]
  [isOrderBot : OrderBot X]
set_option linter.uppercaseLean3 false in
#align SemilatSup SemilatSup

/-- The category of inf-semilattices with a top element. -/
structure SemilatInf : Type (u + 1) where
  X : Type u
  [isSemilatticeInf : SemilatticeInf X]
  [isOrderTop : OrderTop X]
set_option linter.uppercaseLean3 false in
#align SemilatInf SemilatInf

then instance : CoeSort SemilatSup (Type _) := ⟨SemilatSup.X⟩ typechecks.

[Yaël Dillies]

So revert pt back to X?

[Lars Ericson]

Yes, that's the fix. I don't know why it change it to pt.

[Johan Commelin]

Where did you get that first codeblock?

[Yaël Dillies]

That's because X was renamed to pt in docs4#CategoryTheory.Cone, I believe?

[Lars Ericson]

@Johan Commelin follow this link:

https://github.com/leanprover-community/mathlib/blob/13b0d72fd8533ba459ac66e9a885e35ffabb32b2/src/order/category/Semilat.lean

[Lars Ericson]

@Yaël Dillies if there is a precedent for pt I can alternatively change all my X's to pts.

[Johan Commelin]

@Yaël Dillies Why did you write Type.{u} in that file? I guess it works, but I think we usually always write Type u...

[Yaël Dillies]

Uuuh. Looks like I autofixed a max universe issue the way I fixed all the other ones: by appending .{u}.

[Johan Commelin]

Never mind... the port seems to have an "autocorrect" feature :wink:

[Lars Ericson]

Which is more consistent with other files, pt or X?

[Lars Ericson]

In mathlib, category is defined as

class category (obj : Type u)
extends category_struct.{v} obj : Type (max u (v+1)) :=
(id_comp' : ∀ {X Y : obj} (f : hom X Y), 𝟙 X ≫ f = f . obviously)
(comp_id' : ∀ {X Y : obj} (f : hom X Y), f ≫ 𝟙 Y = f . obviously)
(assoc'   : ∀ {W X Y Z : obj} (f : hom W X) (g : hom X Y) (h : hom Y Z),
  (f ≫ g) ≫ h = f ≫ (g ≫ h) . obviously)

Note the use of ' character after id_comp and comp_id. In Mathlib4 Category is defined as

class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where
  /-- Identity morphisms are left identities for composition. -/
  id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f := by aesop_cat
  /-- Identity morphisms are right identities for composition. -/
  comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f := by aesop_cat
  /-- Composition in a category is associative. -/
  assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h :=
    by aesop_cat

Note that the ' character has been dropped in id_comp and comp_id. The mathlib3port of Semilat.lean keeps the ' characters, which I guess can be dropped

instance : LargeCategory.{u} SemilatSup
    where
  Hom X Y := SupBotHom X Y
  id X := SupBotHom.id X
  comp X Y Z f g := g.comp f
  id_comp' X Y := SupBotHom.comp_id
  comp_id' X Y := SupBotHom.id_comp
  assoc' W X Y Z _ _ _ := SupBotHom.comp_assoc _ _ _

Just curious if there is a style guide going one way another on the ' characters.

[Lars Ericson]

@Yaël Dillies I need help on line 49 of Semilat.lean. In Lean 3 this is

instance : large_category.{u} SemilatSup :=
{ hom := λ X Y, sup_bot_hom X Y,
  id := λ X, sup_bot_hom.id X,
  comp := λ X Y Z f g, g.comp f,
  id_comp' := λ X Y, sup_bot_hom.comp_id,
  comp_id' := λ X Y, sup_bot_hom.id_comp,
  assoc' := λ W X Y Z _ _ _, sup_bot_hom.comp_assoc _ _ _ }

In lean 4 port this is

instance : LargeCategory.{u} SemilatSup
    where
  Hom X Y := SupBotHom X Y
  id X := SupBotHom.id X
  comp X Y Z f g := g.comp f
  id_comp' X Y := SupBotHom.comp_id
  comp_id' X Y := SupBotHom.id_comp
  assoc' W X Y Z _ _ _ := SupBotHom.comp_assoc _ _ _

The comp X Y Z f g := g.comp f line doesn't work. I tried correcting this to

This gives me error

Type mismatch
  fun X Y Z f g ↦ comp f g
has type
  (X : X✝ ⟶ Y✝) →
    (Y : Y✝ ⟶ Z✝) →
      (Z : ?m.2915 X Y) →
        (f : SupBotHom (?m.2916 X Y Z) (?m.2917 X Y Z)) →
          SupBotHom (?m.2922 X Y Z f) (?m.2916 X Y Z) →
            SupBotHom (?m.2922 X Y Z f)
              (?m.2917 X Y Z) : Sort (max (max (max (max (u + 1) ?u.2747) (?u.2756 + 1)) (?u.2757 + 1)) (?u.2758 + 1))
but is expected to have type
  (X✝ ⟶ Y✝) → (Y✝ ⟶ Z✝) → (X✝ ⟶ Z✝) : Type u
the following variables have been introduced by the implicit lambda feature
  X✝ : SemilatSup
  Y✝ : SemilatSup
  Z✝ : SemilatSup
you can disable implicit lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.

I am stuck there.

[Yaël Dillies]

The answer is in the error message. Use @fun.

[Ruben Van de Velde]

Even better, use comp f g := g.comp f

[Lars Ericson]

Thank you @Yaël Dillies and @Ruben Van de Velde , the following typechecks. I'm not sure why I need the _ _ _ on the last one rather than eliding it on LHS and RHS, but it needs it to work:

instance : LargeCategory.{u} SemilatSup where
  Hom X Y := SupBotHom X Y
  id X := SupBotHom.id X
  comp f g := g.comp f
  id_comp f := SupBotHom.comp_id f
  comp_id f := SupBotHom.id_comp f
  assoc _ _ _ := SupBotHom.comp_assoc _ _ _

[Lars Ericson]

This Lean 3:

instance : concrete_category SemilatSup :=
{ forget := { obj := SemilatSup.X, map := λ X Y, coe_fn },
  forget_faithful := ⟨λ X Y, fun_like.coe_injective⟩ }

gets mathported to

instance : ConcreteCategory SemilatSup
    where
  forget :=
    { obj := SemilatSup.X
      map := fun X Y => coeFn }
  forget_faithful := ⟨fun X Y => FunLike.coe_injective⟩

The obj := SemilatSup.X gives a long error after what appears to be two invocations of tactic aesop:

Semilat.lean:80:4
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
⊢ ∀ (X : SemilatSup),
  { obj := SemilatSup.X, map := fun X Y ↦ sorryAx ((X ⟶ Y) → (X.X ⟶ Y.X)) true }.map (𝟙 X) =
    𝟙 ({ obj := SemilatSup.X, map := fun X Y ↦ sorryAx ((X ⟶ Y) → (X.X ⟶ Y.X)) true }.obj X)
Semilat.lean:80:4
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
⊢ ∀ {X Y Z : SemilatSup} (f : X ⟶ Y) (g : Y ⟶ Z),
  { obj := SemilatSup.X, map := fun X Y ↦ sorryAx ((X ⟶ Y) → (X.X ⟶ Y.X)) true }.map (f ≫ g) =
    { obj := SemilatSup.X, map := fun X Y ↦ sorryAx ((X ⟶ Y) → (X.X ⟶ Y.X)) true }.map f ≫
      { obj := SemilatSup.X, map := fun X Y ↦ sorryAx ((X ⟶ Y) → (X.X ⟶ Y.X)) true }.map g

The fun X Y => coeFn X fails with unknown identifier 'coeFn'. In the Lean 3 version, the coe_fn refers to line 83 of coe.lean:

@[reducible] def coe_fn {a : Sort u} {b : a → Sort v} [has_coe_to_fun a b] :
  Π x : a, b x :=
has_coe_to_fun.coe

I was unable to find a corresponding coe_fn or coeFn or CoeFn or CoeFN in Lean 4.

I would greatly appreciate two hints.

[Yakov Pechersky]

Part of the nice aspect of working with Lean + mathlib is the interactive theorem proving part. Usually, that is facilitated by an IDE like VSCode or emacs. It's really hard to debug these types of issues, like the ones you're posting, without that IDE, at least for me (I've been spoiled by it). I could venture a guess as to what's going wrong, but it's pretty hard without the goal state and other assistance from the IDE. It'd be much easier if you could also link to a branch that has these current states in a WIP state. Otherwise, asking for hints is like asking the people who have had experience solving Rubik's cubes to send the solution moves just based on a photo.

[Yakov Pechersky]

I'm sharing this thought not to stress anything, but to help find a way that makes it easier for you and for others to feel successful here

[Yakov Pechersky]

In your error, I see sorryAx, which looks like something is being provided which just isn't a term. In this case, what's going on mathematically is that the instance proving that SemilatSup is a concrete category is that you provide the data describing the functor of how the category can be interpreted as just a category over types.

[Yakov Pechersky]

In particular, that means how an object becomes a type, and how a hom becomes a function (I think). So, in mathlib3, the map is coe_fn, which, in a pointfree fashion, maps a hom to a function. Here, maybe you can write it in "pointfull" style: map := fun X Y f => f or \uparrow f.

[Yakov Pechersky]

This is purely my guess based on my very amateur understanding of category theory and the way it is formalized in mathlib

[Lars Ericson]

In this Lean 4 expression:

instance : ConcreteCategory SemilatSup where
  forget :=
    { obj := SemilatSup.X
      map := fun X Y  => coeFn
      }
  forget_faithful := ⟨fun X Y => FunLike.coe_injective⟩

the forget_faithful typechecks and the problem is in the forget. The forgetis declared as

universe w v u

class ConcreteCategory (C : Type u) [Category.{v} C] where
  protected forget : C ⥤ Type w
  [forget_faithful : Faithful forget]

So the forget is a structure of type C ⥤ Type w where C : Type u and ⥤ denotes a functor between categories defined as

infixr:26 " ⥤ " => Functor

where

structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
    extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where
  map_id : ∀ X : C, map (𝟙 X) = 𝟙 (obj X) := by aesop_cat
  map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g := by aesop_cat

map and obj are declared in Prefunctor:

structure Prefunctor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W] where
  obj : V → W
  map : ∀ {X Y : V}, (X ⟶ Y) → (obj X ⟶ obj Y)

Here is a self-contained fully reproducible snippet in Lean 4, from @Yaël Dillies file Semilat.lean:

import Mathlib.Order.Category.PartOrdCat
import Mathlib.Order.Hom.Lattice
universe u
open CategoryTheory SupBotHom

structure SemilatSup : Type (u + 1) where
  X : Type u
  [isSemilatticeSup : SemilatticeSup X]
  [isOrderBot : OrderBot X]

structure SemilatInf : Type (u + 1) where
  X : Type u
  [isSemilatticeInf : SemilatticeInf X]
  [isOrderTop : OrderTop X]

namespace SemilatSup

instance : CoeSort SemilatSup (Type _) := ⟨SemilatSup.X⟩
attribute [instance] isSemilatticeSup isOrderBot

instance : LargeCategory.{u} SemilatSup where
  Hom X Y := SupBotHom X Y
  id X := SupBotHom.id X
  comp f g := g.comp f
  id_comp f := SupBotHom.comp_id f
  comp_id f := SupBotHom.id_comp f
  assoc _ _ _ := SupBotHom.comp_assoc _ _ _

instance : ConcreteCategory SemilatSup where
  forget :=
    { obj := SemilatSup.X
      map := fun X Y  => coeFn
      }
  forget_faithful := ⟨fun X Y => FunLike.coe_injective⟩

The coe_fn in Lean 3 is defined as

@[reducible] def coe_fn {a : Sort u} {b : a → Sort v} [has_coe_to_fun a b] :
  Π x : a, b x :=
has_coe_to_fun.coe

I can't find the equivalent definition in Lean 4. The Lean 3 coe_fn definition above is not in mathlib, it is in an implementation layer below that. I don't know where that layer lives in Lean 4.

Question: what is the equivalent in Lean 4 for coe_fn in this context.