subsingleton simp failure in presence of instance

Stream: mathlib4

[Yakov Pechersky]

I am experimenting with definitions in category theory, based on what we have in mathlib. I found that importing Mathlib.CategoryTheory.Category.Preorder broke some of my simple simp proofs. Specifically, it seems the Preorder.subsingleton_hom instance gets in the way. Yet explicit reference to eq_iff_true_of_subsingleton works.

Here is my repro:

section Std

theorem subsingleton_of_forall_eq (x : α) (h : ∀ y, y = x) : Subsingleton α :=
  ⟨fun a b => h a ▸ h b ▸ rfl⟩

theorem iff_of_true (ha : a) (hb : b) : a ↔ b := ⟨fun _ => hb, fun _ => ha⟩
theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h ⟨⟩

theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
  iff_true_intro (Subsingleton.elim ..)

end Std

section Unique

structure Unique (α : Sort u) extends Inhabited α where
  uniq : ∀ a : α, a = default

attribute [class] Unique

namespace Unique

open Function

variable [Unique α]

instance (priority := 100) : Inhabited α :=
  toInhabited ‹Unique α›

theorem eq_default (a : α) : a = default :=
  uniq _ a

instance (priority := 100) : Subsingleton α :=
  subsingleton_of_forall_eq _ eq_default

-- turning this `attribute [simp] ... in` off breaks the first `Initial.Iso`
attribute [simp] eq_iff_true_of_subsingleton in
theorem Unique.bijective {A B} [Unique A] [Unique B] {f : A → B} : True := trivial

end Unique

universe v u

class Quiver (V : Type u) where
  Hom : V → V → Sort v

infixr:10 " ⟶ " => Quiver.Hom

class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
  id : ∀ X : obj, Hom X X
  comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)

notation "𝟙" => CategoryStruct.id  -- type as \b1
infixr:80 " ≫ " => CategoryStruct.comp -- type as \gg

abbrev SmallCategory (C : Type u) := CategoryStruct.{u} C

theorem ULift.ext (x y : ULift α) (h : x.down = y.down) : x = y :=
  congrArg up h

instance [Subsingleton α] : Subsingleton (PLift α) := sorry

class Preorder (α : Type u) extends LE α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c

structure Iso {C : Type u} [CategoryStruct.{v} C] (X Y : C) where
  hom : X ⟶ Y
  inv : Y ⟶ X
  hom_inv_id : hom ≫ inv = 𝟙 X
  inv_hom_id : inv ≫ hom = 𝟙 Y

infixr:10 " ≅ " => Iso

def Initial {C : Type u} [CategoryStruct C] (I : C) :=
    ∀ A : C, Unique (I ⟶ A)

set_option trace.Meta.synthInstance true

def Initial.Iso {C : Type u} [CategoryStruct C] {X Y : C} (hX : Initial X) (hY : Initial Y) : X ≅ Y where
  hom := (hX Y).default
  inv := (hY X).default
  hom_inv_id := by have := hX X; simp -- uses eq_iff_true_of_subsingleton
  inv_hom_id := by have := hY Y; simp

/-
[Meta.synthInstance] ✅ Subsingleton (X ⟶ X) ▼
  [] new goal Subsingleton (X ⟶ X) ▼
    [instances] #[@Unique.instSubsingleton, instSubsingleton]
  [] ❌ apply instSubsingleton to Subsingleton (X ⟶ X) ▼
    [tryResolve] ❌ Subsingleton (X ⟶ X) ≟ Subsingleton ?m.31237
  [] ✅ apply @Unique.instSubsingleton to Subsingleton (X ⟶ X) ▼
    [tryResolve] ✅ Subsingleton (X ⟶ X) ≟ Subsingleton (X ⟶ X)
    [] new goal Unique (X ⟶ X) ▶
  [] ✅ apply this to Unique (X ⟶ X) ▼
    [tryResolve] ✅ Unique (X ⟶ X) ≟ Unique (X ⟶ X)
  [resume] propagating Unique (X ⟶ X) to subgoal Unique (X ⟶ X) of Subsingleton (X ⟶ X) ▼
    [] size: 1
  [] result Unique.instSubsingleton
-/

section Mathlib.CategoryTheory.Category.Preorder

instance (priority := 100) Preorder.smallCategory (α : Type u) [Preorder α] : CategoryStruct.{u} α where
  Hom U V := ULift (PLift (U ≤ V))
  id X := ⟨⟨Preorder.le_refl X⟩⟩
  comp f g := ⟨⟨Preorder.le_trans _ _ _ f.down.down g.down.down⟩⟩

-- porting note: added to ease the port of `CategoryTheory.Subobject.Basic`
instance Preorder.subsingleton_hom {α : Type u} [Preorder α] (U V : α) :
  Subsingleton (U ⟶ V) := ⟨fun _ _ => ULift.ext _ _ (Subsingleton.elim _ _ )⟩

end Mathlib.CategoryTheory.Category.Preorder

def Initial.Iso' {C : Type u} [CategoryStruct C] {X Y : C} (hX : Initial X) (hY : Initial Y) : X ≅ Y where
  hom := (hX Y).default
  inv := (hY X).default
  hom_inv_id := by have := hX X; simp -- now it breaks
  inv_hom_id := by have := hY Y; simp -- now it breaks

/-
[Meta.synthInstance] 💥 Subsingleton (X ⟶ X) ▼
  [] new goal Subsingleton (X ⟶ X) ▼
    [instances] #[@Unique.instSubsingleton, instSubsingleton, @Preorder.subsingleton_hom]
  [] 💥 apply @Preorder.subsingleton_hom to Subsingleton (X ⟶ X) ▼
    [tryResolve] 💥 Subsingleton (X ⟶ X) ≟ Subsingleton (?m.31875 ⟶ ?m.31876)

[Meta.synthInstance] 💥 Subsingleton (X ⟶ X) ▼
  [] new goal Subsingleton (X ⟶ X) ▼
    [instances] #[@Unique.instSubsingleton, instSubsingleton, @Preorder.subsingleton_hom]
  [] 💥 apply @Preorder.subsingleton_hom to Subsingleton (X ⟶ X) ▼
    [tryResolve] 💥 Subsingleton (X ⟶ X) ≟ Subsingleton (?m.31905 ⟶ ?m.31906)
-/

def Initial.Iso'' {C : Type u} [CategoryStruct C] {X Y : C} (hX : Initial X) (hY : Initial Y) : X ≅ Y where
  hom := (hX Y).default
  inv := (hY X).default
  hom_inv_id := by have := hX X; exact (eq_iff_true_of_subsingleton _ _).mpr trivial
  inv_hom_id := by have := hY Y; exact (eq_iff_true_of_subsingleton _ _).mpr trivial

/-
[Meta.synthInstance] 💥 Subsingleton ?m.32133 ▼
  [] new goal Subsingleton ?m.32133 ▼
    [instances] #[@Unique.instSubsingleton, instSubsingleton, @instSubsingletonForAll, @Preorder.subsingleton_hom, instSubsingletonDecidable, @instSubsingletonSquash, @instSubsingletonPLift, instSubsingletonPUnit, @instSubsingletonStateM]
  [] 💥 apply @instSubsingletonStateM to Subsingleton ?m.32133 ▼
    [tryResolve] 💥 Subsingleton ?m.32133 ≟ Subsingleton (StateM ?m.32146 ?m.32147)

[Meta.synthInstance] ✅ Subsingleton (X ⟶ X) ▼
  [] new goal Subsingleton (X ⟶ X) ▼
    [instances] #[@Unique.instSubsingleton, instSubsingleton, @Preorder.subsingleton_hom]
  [] ❌ apply @Preorder.subsingleton_hom to Subsingleton (X ⟶ X) ▼
    [tryResolve] ❌ Subsingleton (X ⟶ X) ≟ Subsingleton (?m.32163 ⟶ ?m.32164)
  [] ❌ apply instSubsingleton to Subsingleton (X ⟶ X) ▼
    [tryResolve] ❌ Subsingleton (X ⟶ X) ≟ Subsingleton ?m.32181
  [] ✅ apply @Unique.instSubsingleton to Subsingleton (X ⟶ X) ▼
    [tryResolve] ✅ Subsingleton (X ⟶ X) ≟ Subsingleton (X ⟶ X)
    [] new goal Unique (X ⟶ X) ▼
      [instances] #[this]
  [] ✅ apply this to Unique (X ⟶ X) ▼
    [tryResolve] ✅ Unique (X ⟶ X) ≟ Unique (X ⟶ X)
  [resume] propagating Unique (X ⟶ X) to subgoal Unique (X ⟶ X) of Subsingleton (X ⟶ X) ▼
    [] size: 1
  [] result Unique.instSubsingleton
-/

[Yakov Pechersky]

Ah, this was explored in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Failure.20of.20TC.20search.20in.20.60simp.60.20with.20.60etaExperiment.60.2E

[Yakov Pechersky]

So setting explicit universes on Category.{v, u} makes simp work again.

[Kevin Buzzard]

Or [CategoryStruct.{v} C] (you only need to give v, that's the one it's not synthesizing). Without it and with universes on you get

                [] 💥 CategoryStruct.{?u.31729, u} C =?= CategoryStruct.{u, u} C ▼
                  [] ✅ C =?= C

and for some reason it won't solve that universe problem.

[Scott Morrison]

The other solution is to rely on Subsingleton.elim instead, which is what aesop_cat now does.

[Yakov Pechersky]

How would/does Subsingleton.elim work still, if one hits a failure to synthesize a Subsingleton here?

[Meta.synthInstance] 💥 Subsingleton (X ⟶ X) ▼
  [] new goal Subsingleton (X ⟶ X) ▼
    [instances] #[@Unique.instSubsingleton, instSubsingleton, @Preorder.subsingleton_hom]
  [] 💥 apply @Preorder.subsingleton_hom to Subsingleton (X ⟶ X) ▼
    [tryResolve] 💥 Subsingleton (X ⟶ X) ≟ Subsingleton (?m.31875 ⟶ ?m.31876)

[Meta.synthInstance] 💥 Subsingleton (X ⟶ X) ▼
  [] new goal Subsingleton (X ⟶ X) ▼
    [instances] #[@Unique.instSubsingleton, instSubsingleton, @Preorder.subsingleton_hom]
  [] 💥 apply @Preorder.subsingleton_hom to Subsingleton (X ⟶ X) ▼
    [tryResolve] 💥 Subsingleton (X ⟶ X) ≟ Subsingleton (?m.31905 ⟶ ?m.31906)

[Scott Morrison]

There are apparently different behaviours here inside simp vs just with apply (presumably also exact, etc).