unif_hints_post.lean

/-
# 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](https://gist.github.com/thejohncrafter/7425065ab9007a7eb668b946270d035e).
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 :)
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/About.20Unification.20Hints
-/

universe u v

/-
## Introduction

Let's define some categorical notions.
I don't any fully fledged notion of categories,
so let's stick with quivers, which already contain all the
combinarorics that are relevant to my discussion.
-/

-- I introduce this notation because there is a point
-- I want to make about it later.
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

-- This is the object that is going to cause me trouble.
-- Morally, the difficulty is to know the difference
-- between `(a, b) ⟶ (a', b')` and `(a ⟶ a') × (b ⟶ b')`.
-- This is difficult, because these types are *definitionally equal*!
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

-- Symmetry and Associativity of the product.
-- The difficulty is going to be to guess
-- the types of `(symm Q R).map` and `(assoc Q R S).map`
def symm (Q R : Quiver) : Q ⊗ R ⥤ R ⊗ Q where
  obj := fun (a, b) => (b, a)
  map := fun (f, g) => (g, f)

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))

-- These two theorems are easy. In the code I extracted these
-- examples from, they are `simp` lemmas.
theorem symm_obj {A B : Quiver} (a : A) (b : B) :
  (symm A B).obj (a, b) = (b, a) := rfl

theorem assoc_obj {Q R S : Quiver} (a : Q) (b : R) (c : S) :
  (assoc Q R S).obj ((a, b), c) = (a, (b, c)) := rfl

/-
Here's where I get a problem:

```
application type mismatch
  Prod.mk f
argument
  f
has type
  a ⟶ a' : Type ?u.25348
but is expected to have type
  ?m.25356.fst ⟶ ?m.25357.fst : Type ?u.25348

error: type mismatch
  (g, f)
has type
  (b ⟶ b') × (a ⟶ a') : Type (max ?u.25346 ?u.25348)
but is expected to have type
  Prefunctor.obj (symm A B) ?m.25356 ⟶ Prefunctor.obj (symm A B) ?m.25357 : Type (max ?u.25346 ?u.25348)
```

Let's try unification hints to solve this!

-/

theorem symm_map {A B : Quiver}
  {a a' : A} {b b' : B}
  (f : a ⟶ a') (g : b ⟶ b') : (symm A B).map (f, g) = (g, f) := rfl

section

/-
Here's the solution. This Just Works™
-/

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

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

theorem symm_map₁ {A B : Quiver}
  {a a' : A} {b b' : B}
  (f : a ⟶ a') (g : b ⟶ b') : (symm A B).map (f, g) = (g, f) := rfl

end

section

/-
## Infinite Recursion, powered by Unification Hints

An earlier version of the UH above was
-/

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

/-
This still works for `symm`:
-/

theorem symm_map₂ {A B : Quiver}
  {a a' : A} {b b' : B}
  (f : a ⟶ a') (g : b ⟶ b') : (symm A B).map (f, g) = (g, f) := rfl

/-
But now, it triggers an unexpected behavior with the similar
theorem for `assoc`:

```
maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
```
Well, that's surprising!
-/

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

/-
What happened? Let's `set_option trace.Meta.isDefEq true`.

```
[Meta.isDefEq] 💥 ?m.30399.fst.fst ⟶ ?m.30400.fst.fst =?= a ⟶ a'
  [Meta.isDefEq] 💥 ?m.30399.fst.fst ⟶ ?m.30400.fst.fst =?= a ⟶ a'
    [Meta.isDefEq] 💥 ?m.30399.fst.fst =?= a
      [Meta.isDefEq] 💥 ?m.30399.fst.1 =?= a
        [Meta.isDefEq.onFailure] 💥 ?m.30399.fst.1 =?= a
          [Meta.isDefEq.stuckMVar] found stuck MVar ?m.30399 : ((Q⊗R)⊗S).α
          [Meta.isDefEq] ✅ ?m.30424 =?= ?m.30399.fst.1
          [Meta.isDefEq] ❌ ?m.30425.snd =?= a
          [Meta.isDefEq] ✅ ?m.30433 =?= ?m.30399.fst.1
          [Meta.isDefEq] ❌ ?m.30435.fst =?= a
          [Meta.isDefEq] ✅ ?m.30444 =?= a
          [Meta.isDefEq] ❌ ?m.30445.snd =?= ?m.30399.fst.1
          [Meta.isDefEq] ✅ ?m.30453 =?= a
          [Meta.isDefEq] ✅ ?m.30455.fst =?= ?m.30399.fst.1
          [Meta.isDefEq] 💥 ?m.30399.fst =?= (a, ?m.30454)
            [Meta.isDefEq] 💥 ?m.30399.fst =?= (a, ?m.30454)
              [Meta.isDefEq] ✅ (Q⊗R).α =?= Q.α × R.α
              [Meta.isDefEq] 💥 ?m.30399.fst.fst =?= a
                [Meta.isDefEq] 💥 ?m.30399.fst.1 =?= a
                  [Meta.isDefEq.onFailure] 💥 ?m.30399.fst.1 =?= a
                    [Meta.isDefEq.stuckMVar] found stuck MVar ?m.30399 : ((Q⊗R)⊗S).α
                    [Meta.isDefEq] ✅ ?m.30467 =?= ?m.30399.fst.1
                    [Meta.isDefEq] ❌ ?m.30468.snd =?= a
                    [Meta.isDefEq] ✅ ?m.30476 =?= ?m.30399.fst.1
                    [Meta.isDefEq] ❌ ?m.30478.fst =?= a
                    [Meta.isDefEq] ✅ ?m.30487 =?= a
                    [Meta.isDefEq] ❌ ?m.30488.snd =?= ?m.30399.fst.1
                    [Meta.isDefEq] ✅ ?m.30496 =?= a
                    [Meta.isDefEq] ✅ ?m.30498.fst =?= ?m.30399.fst.1
                    [Meta.isDefEq] 💥 ?m.30399.fst =?= (a, ?m.30497)
                      [Meta.isDefEq] 💥 ?m.30399.fst =?= (a, ?m.30497)
                        [Meta.isDefEq] ✅ (Q⊗R).α =?= Q.α × R.α
                        [Meta.isDefEq] 💥 ?m.30399.fst.fst =?= a
                          [Meta.isDefEq] 💥 ?m.30399.fst.1 =?= a
                            [Meta.isDefEq.onFailure] 💥 ?m.30399.fst.1 =?= a
```

Lean repeatedly tries `[Meta.isDefEq.onFailure] 💥 ?m.30399.fst.1 =?= a`!

Look at my unification hint:
-/

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

/-
When Lean chooses to use this UH, it has to check `x =?= (c, d)`,
which reduces to `x.1 =?= c` and `x.2 =?= d`, which in turns triggers
the same UH again...

That's why the right UH is
-/

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

/-
which introduces a new metavariable.

Basically, this one just says that the elements of `C ⊗ D` are pairs
directly formed by a the constructor `Prod.mk`.

I'm not sure what the takeaway of this discussion is, but basically
> Be careful with your unification hints!
I guess the real takeaway is that *if I want to use a unification
hint to "guess" the structure of an object, I should introduce
new variables for the memebers of this object, rather than using
already existing variables, to avoid circular computations.*
-/

end

section

/-
Now, if we use the solution I showed at the beginning, we get:
-/

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

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

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

/-
This works, yay!
-/

end

section

/-
--
## A mistake

Let me show another issue I encountered while I was figuring this out.

I first thought what I wanted was for Lean to guess that `Quiver.hom` is injective.
Well, Lean *already does that*:

with (Q R : Quiver) (a b : Q) (c d : R), let's look at the
following unification:
  a ⟶ b =?= c ⟶ d
this reduces to
  Quiver.hom Q a b =?= Quiver.hom R c d
then
  Q.2 a b =?= R.2 c d
which gives
  Q =?= R  <- And that's where "injectivity" is checked!
  a =?= c  <- But these two checks are also extremely important
  b =?= d     I encountered a bug which was caused by *me* not
              getting Lean to forget about these.
              Let's look at that!

(Well, this is not really injectivity, but let's call it that anyway
because I guess this makes it easier to understand.)

Here was my first shot at the UH: if the arrows are equal,
then the categories are equal too.

-/

local unif_hint (Q R : Quiver.{u,v}) (c c' : Q) (d d' : R) where
  Q =?= R
  ⊢ Q.hom c c' =?= R.hom d d'

/-
But uh-oh!
(For some reason I tried to place this UH before
the definition of Prefunctor.)

```
error: application type mismatch
  map✝ = map
argument has type
  {x y : Q.α} → (x ⟶ y) → (obj x ⟶ obj y)
but function has type
  ({x y : Q.α} → (x ⟶ y) → (obj✝ x ⟶ obj✝ y)) → Prop
./././Catlib4/mwe.lean:134:48: error: function expected at
  m
term has type
  ?m.27808
```
-/

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)

/-
What happened? Let's `set_option trace.Meta.isDefEq true`
and `set_option trace.Meta.isDefEq.hint true`.

[Meta.isDefEq] ✅ {x y : Q.α} → (x ⟶ y) → (obj✝ x ⟶ obj✝ y) =?= {x y : Q.α} → (x ⟶ y) → (obj x ⟶ obj y)
  [Meta.isDefEq] ✅ Q.α =?= Q.α
  [Meta.isDefEq] ✅ Q.α =?= Q.α
  [Meta.isDefEq] ✅ x ⟶ y =?= x ⟶ y
  [Meta.isDefEq] ✅ obj✝ x ⟶ obj✝ y =?= obj x ⟶ obj y
    [Meta.isDefEq] ✅ (instHasHomα R).1 (obj✝ x) (obj✝ y) =?= (instHasHomα R).1 (obj x) (obj y)
      [Meta.isDefEq] ✅ Quiver.hom R (obj✝ x) (obj✝ y) =?= Quiver.hom R (obj x) (obj y)
        [Meta.isDefEq] ✅ R.2 (obj✝ x) (obj✝ y) =?= R.2 (obj x) (obj y)
          [Meta.isDefEq] ✅ R.2 =?= R.2
          [Meta.isDefEq] ❌ obj✝ x =?= obj x
          [Meta.isDefEq.onFailure] ✅ R.2 (obj✝ x) (obj✝ y) =?= R.2 (obj x) (obj y)
            [Meta.isDefEq.hint] R.2 (obj✝ x) (obj✝ y) =?= R.2 (obj x) (obj y)
            [Meta.isDefEq.hint] ✅ hint hint._@.Catlib4.mwe._hyg.2029 at R.2 (obj✝ x) (obj✝ y) =?= R.2 (obj x) (obj y)
              [Meta.isDefEq] ✅ Quiver.hom ?m.27662 ?m.27664 ?m.27665 =?= R.2 (obj✝ x) (obj✝ y)
              [Meta.isDefEq] ✅ Quiver.hom ?m.27663 ?m.27666 ?m.27667 =?= R.2 (obj x) (obj y)
              [Meta.isDefEq.hint] hint._@.Catlib4.mwe._hyg.2029 succeeded, applying constraints
              [Meta.isDefEq] ✅ R =?= R
------------> I made Lean forget about `❌ obj✝ x =?= obj x`!

Here's the first thing:
> It is possible to write an ill-formed unification hint
> that makes Lean believe the constraints are coherent
> while they aren't!

Well, here's the zeroth thing:
> Unification hints "for injectivity" don't make sense.

I wonder how much I can make `isDefEq` lie with wrong unification hints.
I tried
-/

def add : Nat → Nat → Nat := λ a b => a + b

unif_hint (a b c d : Nat) where
  a =?= c
  ⊢ add a b =?= add c d

example : add 0 1 = add 0 2 := rfl

/-
but fortunately this doesn't work, even though it does trigger my
evil unification hint.
-/

end

section

/-
I gave another shot at this UH, which made me realize one important
behavior of the unification hints
-/

local unif_hint (Q R : Quiver.{u,v}) (c c' : Q) (d d' : R) where
  Q =?= R
  ⊢ c ⟶ c' =?= d ⟶ d'

/-
This looks fine, as the following code is accepted by Lean.
-/

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)

/-
But this UH *actually doesn't do anything*:
`set_option trace.Meta.isDefEq.hint true` reveals that
it is never even called.

The reason is (seems to be) that the sides of `c ⟶ c' =?= d ⟶ d'`
aren't in weak head normal form, which means the UH is never even called.

Therefore, here's another takeaway:
> Make sure the expressions in the "output" (for lack of a better name)
> constraint are in weak head normal form.
-/

end

section

/-
## What made me stick with my injectivity mistake

Recall the theorem `assoc_map`.

I actually got some progress with my "injectivity unification hint":
-/

local unif_hint (Q R : Quiver.{u,v}) (c c' : Q) (d d' : R) where
  Q =?= R
  ⊢ Q.hom c c' =?= R.hom d d'

set_option trace.Meta.isDefEq.hint true
theorem symm_map₃ {A B : Quiver}
  {a a' : A} {b b' : B}
  (f : a ⟶ a') (g : b ⟶ b') : (symm A B).map (f, g) = (g, f) := rfl

/-
```
error: don't know how to synthesize implicit argument
  @Prefunctor.map (A⊗B) (B⊗A) (symm A B) (?m.54128 f g) (?m.54129 f g) (f, g)
context:
A : Quiver
B : Quiver
a a' : A.α
b b' : B.α
f : a ⟶ a'
g : b ⟶ b'
⊢ (A⊗B).α
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
```

Well, since the error message has changed, I thought I made some progress!
But, as I discussed it earlier, my UH doesn't really make sense, therefore
this is a case where I "lied to Lean" with my UH and this made the resulting
messages look like I was on the right track.

I'm not sure what the takeaway of this last point is.
I guess once again here lies something relevant to say about "lying to Lean".
Rather, my guess is that with such mistaken unification hints it would be possible
to abuse some parts of Lean to produce unexpected behavior, like here where
I made argument synthesis fail, or like above where I made the unifier believe
two terms were equal when they really weren't.
-/

end

/-

# Final words

This is a very long post, thanks for sticking with me until the end!

Hopefully I've shared some valuable information with you.
I hope that the examples I discuss here can be useful for documentation
and for teaching Lean.

I think that cateory theory can be a great source of tests for Lean,
in that they put the whole system to a test. The difficulty is to make Lean
understand statements that are humanly understandable, but that contain
subtleties that are actually difficult, even for mathematicians.

Let me open this disucssion further.

Category theory is actually difficult to understand even -- well, especially --
for humans, because there is a lot of implicit information the expressions
that are classically written in a category paper or book. My personal
experience with Category Theory For The Working Mathematician was that I
struggled a lot to find the type of the many different expressions that
lied in diagrams, but I've found that, with exprience, it becomes easier
and easier to understand, or guess, what expressions really mean and how
they behave. I think formalizing category theory in Lean can serve two purposes:

* *Putting Lean to a test.* Here, I discussed some difficulties I encountered,
  but I've found some other pain points while I was working. I may write some other
  posts about them. I've also found that writing category theory, or writing
  code that uses category theory, is a very efficient way of discovering bugs
  or unexpected behavior in Lean (here, I've told about infinite recursion
  with unification hints, but I have posted before about some other issues
  I encountered while I was trying to formalize category theory).
* *Heping mathematicians understand category theory.* As I said, I believe
  it is difficult, especially for beginners, to understand category theory
  because there is so much implicit information lying in every expression.
  To me, this is pretty similar to how difficult it is to understand Haskell
  programs for a beginner. I'd actually like to make a pretty bold statement:
  *cagegory theory is actually about programming, rather than math*. To me,
  category theory is a way to formalize arguments about data flowing between
  objects, even (especially) in the contexts where it is use in mathematics.
  I believe it would make sense to use Lean to formalize difficult
  categorical theories, because then it would enable us to generate documentation
  for expessions, much like a Hoogle for category theory, following the idea
  that knowing the type of an expression can really help understanding what
  the expression does, without any need for looking at its details.
-/