# Zulip Chat Archive

## Stream: lean4

### Topic: unification hint

#### Kenny Lau (Jan 06 2021 at 09:09):

What is unification hint and where can I learn more about it?

#### Eric Wieser (Jan 06 2021 at 09:23):

Also this question, but for lean3

#### Adam Topaz (Jan 08 2021 at 19:03):

Is there a way to make the following code work?

```
structure Magma where
α : Type
mul : α → α → α
instance : CoeSort Magma Type where
coe M := M.α
infixl:70 (priority := high) "**" => Magma.mul
def Nat.Magma : Magma where
α := Nat
mul a b := Nat.mul a b
unif_hint (S : Magma) where
S.α =?= Nat
|-
S =?= Nat.Magma
#check (3 : Nat) ** 3
```

#### Adam Topaz (Jan 08 2021 at 19:26):

https://leanprover.github.io/lean4/doc/unifhint.html

:sad:

#### Alexander Bentkamp (Jan 08 2021 at 19:42):

```
structure Magma where
α : Type
mul : α → α → α
-- instance : CoeSort Magma Type where
-- coe M := M.α
infixl:70 (priority := high) "**" => Magma.mul _ -- added underscore
def Nat.Magma : Magma where
α := Nat
mul a b := Nat.mul a b
unif_hint (S : Magma) where
S =?= Nat.Magma
|-
S.α =?= Nat
--swapped
#check (3 : Nat) ** (3 : Nat) -- added type hint
```

#### Adam Topaz (Jan 08 2021 at 19:43):

nice!

#### Adam Topaz (Jan 08 2021 at 19:45):

The underscore and type hint I completely understand, but what's going on with the swapped syntax in the unification hint itself?

#### Reid Barton (Jan 08 2021 at 19:47):

I guess because normally one would try to check a typing judgment by matching it against the conclusions of inference rules

#### Alexander Bentkamp (Jan 08 2021 at 19:48):

In the unification hint paper https://www.cs.unibo.it/~sacerdot/PAPERS/tphol09.pdf they also use this order.

#### Kenny Lau (Jan 08 2021 at 19:48):

Well this sure is exciting to see.

#### Kenny Lau (Jan 08 2021 at 19:48):

but how well can this scale?

#### Adam Topaz (Jan 08 2021 at 19:49):

Yeah that's something we should experiment with.

#### Kenny Lau (Jan 08 2021 at 19:50):

I mean, what if I want to reason with an arbitrary Magma? Do I need to keep writing `S.\a`

all the time?

#### Adam Topaz (Jan 08 2021 at 19:51):

Yeah good question. Why can't we have the CoeSort as well?

#### Adam Topaz (Jan 08 2021 at 19:51):

(Looks like adding the `CoeSort`

instance doesn't break anything.)

#### Adam Topaz (Jan 08 2021 at 19:52):

```
structure Magma where
α : Type
mul : α → α → α
instance : CoeSort Magma Type where
coe M := M.α
infixl:70 (priority := high) "**" => Magma.mul _ -- added underscore
def Nat.Magma : Magma where
α := Nat
mul a b := Nat.mul a b
unif_hint (S : Magma) where
S =?= Nat.Magma
|-
S.α =?= Nat
#check (3 : Nat) ** (3 : Nat) -- added type hint
variables (M : Magma) (m : M)
```

#### Kenny Lau (Jan 08 2021 at 19:57):

```
structure Magma where
α : Type
mul : α → α → α
instance : CoeSort Magma Type where
coe M := M.α
infixl:70 (priority := high) "**" => Magma.mul _
def mul_assoc (S : Magma) : Prop :=
∀ x y z : S, (x ** y) ** z = x ** (y ** z)
```

#### Kenny Lau (Jan 08 2021 at 19:57):

looks like this works as-is

#### Kenny Lau (Jan 08 2021 at 20:00):

ok but can we build a bundled algberaic hierarchy without having to write every lemma 37 times?

#### Cyril Cohen (Jan 10 2021 at 03:51):

The answer is yes and the solution is in the literature: the "Packaging mathematical structures", "Competing inheritance paths in dependent type theory [...]" and "Hierarchy builder" papers are a good start to explain how to do so with Canonical structures which are a strict subset of unification hints. An extensive use case on a large hierarchy can be found in the Coq mathematical components library. I also wrote a short demo in lean3, for a lean meeting that someone found in the zulip archives and posted again in the topic of the same name but for lean3. Please have a look.

#### Alex Peattie (Jan 10 2021 at 15:48):

I think this is the post/demo in question: https://leanprover-community.github.io/archive/stream/113488-general/topic/unification.20hints.html#158613068

Last updated: May 18 2021 at 23:14 UTC