About Unification Hints

Stream: lean4

[Julien Marquet]

Some experiments with unification hints

I was playing with category theory in Lean. At some point, I realised I had to use unification hints to solve a problem. I have spent a lot of time figuring this out, and I guess I gathered some valuable experience with this and I'd like to share it with you.
Basically, there are two points:

• I found a way to trigger infinite recursion using unification hints. I guess this is some valuable information for the core developers, and that's the main reason why I'm writing this post.
• I made some mistakes, and eventually found out why I was mistaken. I guess I'm not the only one who has made these mistakes, there have been other people doing the same things before, and most importantly there will be other people doing this after me. Therefore, I think my experience is valuable for the purpose of documentation, and I'm trying to make a discussion that is as clear as possible so that it could fit in Lean 4's documentation, or in some other resources, like tutorials on unification hints.

I intended on posting the whole thing here, but unfortunately the message would be way too long for Zulip. Therefore I posted the document on gist.github.com, here.
The file is runnable in Lean 4 (at the time of writing I'm using nightly:2023-04-20).

Please feel free to comment, I'd appreciate any feedback!
I think comments should preferably be posted here on Zulip for everyone to read, but if it makes sense to you to comment on github then feel free to do so :)

[Julien Marquet]

TL;DR: Here's a way to triger an infinite recursionusing unification hints.

Let's first set the stage (I'm trying to make this quick).

universe u v

class Hom (α : Type u) : Sort (max u v + 1) where
  hom : α → α → Sort v

infixr:10 " ⟶ " => Hom.hom -- \h

structure Quiver : Type (max u v + 1) where
  α : Type u
  hom : α → α → Sort v

instance : CoeSort Quiver (Type u) where
  coe Q := Q.α

instance (Q : Quiver.{u,v}) : Hom.{u,v} Q where
  hom := Q.hom

structure Prefunctor (Q R : Quiver.{u,v}) : Type (max u v) where
  obj : Q → R
  map {x y : Q} : (x ⟶ y) → (obj x ⟶ obj y)

infixr:26 "⥤" => Prefunctor

def product_quiver (Q R : Quiver) : Quiver where
  α := Q × R
  hom a b := (a.1 ⟶ b.1) × (a.2 ⟶ b.2)

infixr:70 "⊗" => product_quiver

Here's a troublesome expression:

def assoc (Q R S : Quiver) : (Q ⊗ R) ⊗ S ⥤ Q ⊗ (R ⊗ S) where
  obj := fun ((a, b), c) => (a, (b, c))
  map := fun ((f, g), h) => (f, (g, h))

Two problematic unification hints (I discuss how to fix them in the post).

local unif_hint (C D : Quiver) (c : C) (d : D) (x : C ⊗ D) where
  x =?= (c, d)
  ⊢ d =?= x.2

local unif_hint (C D : Quiver) (c : C) (d : D) (x : C ⊗ D) where
  x =?= (c, d)
  ⊢ c =?= x.1

Here we go:

maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

theorem assoc_map {Q R S : Quiver}
  {a a' : Q} {b b' : R} {c c' : S}
  (f : a ⟶ a') (g : b ⟶ b') (h : c ⟶ c') :
  (assoc Q R S).map ((f, g), h) = (f, (g, h)) := rfl

[Kevin Buzzard]

Rather bizarrely I had just been trying to understand these things myself. Thanks a lot for posting!

PS can't help but note that fancy unicode syntax

unif_hint (S : Magma) where
  S ≟ Nat.Magma ⊢ S.α ≟ Nat

also works