unification hint

Stream: lean4

[Kenny Lau]

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

[Eric Wieser]

Also this question, but for lean3

[Adam Topaz]

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]

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

[Alexander Bentkamp]

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]

nice!

[Adam Topaz]

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

[Reid Barton]

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

[Alexander Bentkamp]

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

[Kenny Lau]

Well this sure is exciting to see.

[Kenny Lau]

but how well can this scale?

[Adam Topaz]

Yeah that's something we should experiment with.

[Kenny Lau]

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]

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

[Adam Topaz]

(Looks like adding the CoeSort instance doesn't break anything.)

[Adam Topaz]

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]

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]

looks like this works as-is

[Kenny Lau]

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

[Cyril Cohen]

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]

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