fixing a looping `unif_hint`

Stream: mathlib4

[Robert Maxton]

Is there any way to get the unification hint

unif_hint (X) [TopologicalSpace X] (Y : TopCat) where
  of X ≟ Y ⊢ X ≟ ↑Y

to work without sending simp etc into loops?

I've only played around with it a little, but I'm pretty sure it would solve a lot of annoying pain points when working with TopCat ... at the low, low cost of blocking simp from ever turning ↑(of X) back into X, meaning it loops basically everywhere.

This is unworkable as far as I can tell, but my knowledge of Lean's internals is still lacking, so maybe someone else can spot some other way of getting the same effect?

[Aaron Liu]

how does unif_hint work

[Robert Maxton]

(Right now, any time concrete and abstract defs in TopCat need to interact, neither defining things as C(X, Y)s nor defining them as X ⟶ Ys is entirely satisfactory; either way definitions break in odd places, hold up simp and fail unification and generally make a mess of things. Almost entirely, this is because ↑(of X) isn't sufficiently reducibly equivalent to X for the purposes of e.g. instance synthesis.

[Robert Maxton]

Aaron Liu said:

how does unif_hint work

Essentially, it's an apply rule that happens during unification. When unification encounters a unification problem that looks like the thing on the right of the tee, in this case trying to unify a type-with-a-topological-space-instance with a slot expecting a TopCat.carrier ?_, it will reduce the problem to the thing on the left, in this case trying to unify of X with Y instead.

To be honest, I'm not actually entirely sure how this process results in something that would send simp into a loop, but...

[Robert Maxton]

I guess because it reduces the problem to of X = Y and simp then promptly reduces that back to X = ↑Y?

[Anne Baanen]

For concrete categories like TopCat, of is an abbreviation for the constructor and ↑ for the first projection. So I would expect the type checker to be able to use its builtin eta and pi reduction to do this kind of unification automatically.

Do you have an example of a pain point you would like to fix with unification hints?

[Robin Arnez]

If I understand correctly, making of a constructor would already be enough, right? So

structure TopCat.{u} : Type (u + 1) where
  of ::
  carrier : Type u
  [str : TopologicalSpace carrier]

@[app_unexpander TopCat.of]
def TopCat.unexpand : Lean.PrettyPrinter.Unexpander := pure

Otherwise, the unification hint is bound to fail since unification will get from the left-hand side to the right-hand side automatically by structure eta expansion.

[Robert Maxton]

Anne Baanen said:

For concrete categories like TopCat, of is an abbreviation for the constructor and ↑ for the first projection. So I would expect the type checker to be able to use its builtin eta and pi reduction to do this kind of unification automatically.

Do you have an example of a pain point you would like to fix with unification hints?

The problem mostly concerns issues with simp lemmas not firing, though I do occasionally also get type checking errors when metavariables and instance synth get involved. I've had trouble with docs#TopCat.sigmaIsoSigma expecting an of ((i : ι) × ↑(α i)) and getting an of ((i : ι) × ↑(of (α i))), for example.

[Robert Maxton]

Here's a concrete example, though it needs some setup:

import Mathlib.Topology.Category.TopCat.Basic

open CategoryTheory Topology TopologicalSpace TopCat ContinuousMap
universe u

@[simps]
def ContinuousMap.uliftUp [TopologicalSpace α] : C(α, ULift α) where
  toFun := ULift.up

@[simps]
def ContinuousMap.uliftDown [TopologicalSpace α] : C(ULift α, α) where
  toFun := ULift.down

def UProp : TopCat.{u} := of (ULift Prop)

namespace UProp

@[simps -isSimp top] instance instTop : Top UProp := ⟨⟨True⟩⟩
@[simps -isSimp bot] instance instBot : Bot UProp := ⟨⟨False⟩⟩

open scoped Classical in
noncomputable def homOfSpecializes {X : TopCat} {x y : X} (hxy : x ⤳ y) : UProp ⟶ X :=
  ofHom <| .comp ⟨(if · then x else y), ⟨by
    intro s hs
    by_cases hy : y ∈ s
    · replace hxy := hxy.mem_open hs hy
      convert isOpen_univ
      simp only [Set.preimage_eq_univ_iff]
      rintro x ⟨p, rfl⟩
      dsimp only; split_ifs <;> assumption
    · by_cases hx : x ∈ s
      · convert isOpen_singleton_true
        ext p
        rcases em p with h | h <;> simp [h, hx, hy]
      · convert isOpen_empty
        ext p
        rcases em p with h | h <;> simp [h, hx, hy] ⟩⟩ .uliftDown

@[simp]
lemma homOfSpecializes_apply_top {X : TopCat} {x y : X} (hxy : x ⤳ y) :
    (homOfSpecializes hxy) ⊤ = x := by simp [homOfSpecializes, UProp]

@[simp]
lemma homOfSpecializes_apply_bot {X : TopCat} {x y : X} (hxy : x ⤳ y) :
    (homOfSpecializes hxy) ⊥ = y := by simp [homOfSpecializes, UProp]

end UProp

variable {X} [TopologicalSpace X] (x y : X) (hxy : x ⤳ y)

example : UProp.homOfSpecializes hxy ⊤ = x := by simp

[Robert Maxton]

The last example won't even typecheck without an explicit type ascription on the LHS, and even then homOfSpecializes_apply_top won't fire unless you match up the universe levels for simp, i.e. write

variable {X : Type u} [TopologicalSpace X] (x y : X) (hxy : x ⤳ y)
example : (UProp.homOfSpecializes hxy ⊤ : of X) = x := by
  simp [UProp.homOfSpecializes_apply_top.{u}]