## Stream: general

### Topic: unification

#### Kevin Buzzard (Jan 25 2019 at 08:51):

example (a : ℕ) : a ∈ {x : ℕ | x ≤ a} := le_refl _ -- fails
example (a : ℕ) : a ∈ {x : ℕ | x ≤ a} := le_refl a -- works
example (a : ℕ) : a ≤ a := le_refl _ -- works


How does unification work? I was in the middle of something else and I wrote the first line, confident that Lean should be able to figure it out, but it didn't: I got

type mismatch, term
le_refl ?m_3
has type
?m_3 ≤ ?m_3
but is expected to have type
a ∈ {x : ℕ | x ≤ a}


What is Lean's algorithm for attempting to solve for these metavariables, and how does adding the extra a actually help it? The moment Lean unfolds the definitions of has_mem.mem and set.mem it can see what's going on -- but why does adding a push it towards doing this? Is the algorithm easy to explain or is it some arcane thing which I should never be thinking about?

#### Kenny Lau (Jan 25 2019 at 08:53):

example (a : ℕ) : a ∈ {x : ℕ | x ≤ a} := @le_refl ℕ _ _ --works


#### Kenny Lau (Jan 25 2019 at 08:54):

Lean can't even figure out that we're talking about the natural numbers

#### Kevin Buzzard (Jan 25 2019 at 08:54):

Aah! I remember now. The @ changes Lean's strategy doesn't it.

#### Kenny Lau (Jan 25 2019 at 08:54):

but once we tell Lean that, Lean can figure it out by itself

does it?

#### Kevin Buzzard (Jan 25 2019 at 08:54):

I am not sure it's as simple as what you say

#### Kevin Buzzard (Jan 25 2019 at 08:54):

I think the @ changes Lean's elaboration procedure.

#### Kenny Lau (Jan 25 2019 at 08:54):

well Lean sees the head term being "has_mem.mem" and is like "what? where is has_le.le?"

#### Kevin Buzzard (Jan 25 2019 at 08:55):

Hey, look at us, mathematicians talking about head terms and elaboration procedures. This is progress, as far as I am concerned.

#### Kenny Lau (Jan 25 2019 at 08:55):

theorem le_refl' (α : Type*) [preorder α] (x : α) : x ≤ x := le_refl _
example (a : ℕ) : a ∈ {x : ℕ | x ≤ a} := le_refl' ℕ _ --works


#### Kenny Lau (Jan 25 2019 at 08:55):

no @

#### Kevin Buzzard (Jan 25 2019 at 08:55):

Right, but when I use a explicitly, it must say "OK! I can't see has_le.le -- let's go for the unfold option.

#### Kevin Buzzard (Jan 25 2019 at 08:56):

Oh so you are right.

#### Kevin Buzzard (Jan 25 2019 at 08:56):

It's not using a, it's using its type. How does this help things I wonder?

#### Kenny Lau (Jan 25 2019 at 08:57):

@Sebastian Ullrich might we plebs be honoured by your explanation?

#### Kevin Buzzard (Jan 25 2019 at 08:57):

ha ha, he logs on and within seconds he's being pestered by mathematicians :-)

aka plebs

#### Kevin Buzzard (Jan 25 2019 at 08:58):

I should re-read the bit in TPIL where it talks about elab_as_eliminator etc.

#### Kevin Buzzard (Jan 25 2019 at 09:00):

"Lean has to rely on heuristics to determine what to unfold or reduce, and when."

#### Sebastian Ullrich (Jan 25 2019 at 09:01):

arrives at university

How does unification work?

turns around and leaves

maybe it's hard?

#### Kevin Buzzard (Jan 25 2019 at 09:02):

"using the @ symbol in front of an identifier in an expression
instructs the elaborator to use the [elab_simple] strategy" -- that was what I was remembering

#### Kevin Buzzard (Jan 25 2019 at 09:03):

But

attribute [reducible] has_mem.mem
attribute [reducible] set.mem
attribute [elab_simple] le_refl
example (a : ℕ) : a ∈ {x : ℕ | x ≤ a} := le_refl _ -- fails


so it's not the @, as Kenny suspected.

#### Kevin Buzzard (Jan 25 2019 at 09:05):

example (a : ℕ) : a ∈ {x : ℕ | x ≤ a} := @@le_refl _ _ -- fails

#### Kevin Buzzard (Jan 25 2019 at 09:05):

not something you see very often, the @@

#### Kevin Buzzard (Jan 25 2019 at 09:07):

The first _ in the above is expecting preorder ?m_1 so again it seems to be a case of "I will unfold has_mem.mem iff you tell me we're talking about nats"

#### Kevin Buzzard (Jan 25 2019 at 09:10):

Computers are so stupid. Why are we even here? Maybe I should go back to writing references.

#### Kevin Buzzard (Jan 25 2019 at 09:11):

@Kenny Lau do you know if this is "higher order unification" or something else?

perhaps

#### Kevin Buzzard (Jan 25 2019 at 09:12):

I realise I am a bit unclear about what that term even means.

#### Kenny Lau (Jan 25 2019 at 09:12):

has_le.le is a function with > 0 inputs

#### Kevin Buzzard (Jan 25 2019 at 09:12):

i.e. what a mathematician would call "a function"

#### Kevin Buzzard (Jan 25 2019 at 09:14):

It has taken me a year to be proficient enough at Lean to be able to start formalising basic questions about what I don't understand, and because I have learnt type theory in some weird way (by trying to use it in a random context, i.e. mathematics) there are still, I'm sure, several important things which I don't understand yet.

#### Kevin Buzzard (Jan 25 2019 at 09:15):

It took me a year to understand what equality was, basically, and now I'm pressing on from there.

#### Kenny Lau (Jan 25 2019 at 09:16):

global sections of affine schemes are dependent functions

#### Kevin Buzzard (Jan 25 2019 at 09:23):

This I know. As is Fermat's Last Theorem.

#### Kevin Buzzard (Jan 25 2019 at 09:45):

example (a : ℕ) : has_mem.mem a {x : ℕ | x ≤ a} := le_refl _ -- fails
example (a : ℕ) : set.mem a {x : ℕ | x ≤ a} := le_refl _ -- works


#### Kenny Lau (Jan 25 2019 at 09:47):

theorem le_refl' (α : Type*) (h : preorder α) (x : α) : x ≤ x := le_refl _
example (a : ℕ) : @@has_mem.mem (@set.has_mem ℕ) a {x : ℕ | x ≤ a} := le_refl' _ _ _ --fails
example (a : ℕ) : set.mem a {x : ℕ | x ≤ a} := le_refl' _ _ _ --works


#### Kevin Buzzard (Jan 25 2019 at 09:49):

I think this must be a bug in has_mem.mem ;-)

#### Kevin Buzzard (Jan 25 2019 at 09:50):

but unfortunately I've now made it to work so need to do something serious.

#### Sebastian Ullrich (Jan 25 2019 at 09:57):

Yeah, this one is a bit involved. In your first example, you're asking Lean to figure out all parameters of le_refl by unifying its type with the expected type (the goal).

8:7: [type_context.is_def_eq_detail] : @has_mem.mem nat (set nat) (@set.has_mem nat) a (@set_of nat (λ (x : nat), @has_le.le nat nat.has_le x a)) =?= @has_le.le ?m_1 (@preorder.to_has_le ?m_1 ?m_2) ?m_3 ?m_3
[type_context.is_def_eq_detail] : @set.mem nat a (@set_of nat (λ (x : nat), @has_le.le nat nat.has_le x a)) =?= @preorder.le ?m_1 ?m_2 ?m_3 ?m_3
[type_context.is_def_eq_detail] unfold left: set.mem
[type_context.is_def_eq_detail] : @set_of nat (λ (x : nat), @has_le.le nat nat.has_le x a) a =?= @preorder.le ?m_1 ?m_2 ?m_3 ?m_3
[type_context.is_def_eq_detail] unfold left: set_of
[type_context.is_def_eq_detail] : (λ (x : nat), @has_le.le nat nat.has_le x a) a =?= @preorder.le ?m_1 ?m_2 ?m_3 ?m_3
[type_context.is_def_eq_detail] after whnf_core: @has_le.le nat nat.has_le a a =?= @preorder.le ?m_1 ?m_2 ?m_3 ?m_3
[type_context.is_def_eq_detail] : nat.less_than_or_equal a a =?= @preorder.le ?m_1 ?m_2 ?m_3 ?m_3
[type_context.is_def_eq_detail] : nat.less_than_or_equal =?= preorder.le
[type_context.is_def_eq_detail] on failure: nat.less_than_or_equal =?= preorder.le
[type_context.is_def_eq_detail] on failure: nat.less_than_or_equal a a =?= @preorder.le ?m_1 ?m_2 ?m_3 ?m_3


At different points during unification, Lean has unfolded the LHS has_le.le to nat.less_than_or_equal and the RHS's to preorder.le, but in the end fails to unify these two, because it doesn't know the RHS preorder yet and so can't unfold preorder.le.
If Lean can otherwise figure out the preorder (by specifying one of the arguments), it works. If you use set.mem, it works more or less coincidentally because Lean prefers unfolding the definition set.mem over the projection has_le.le.

#### Patrick Massot (Jan 25 2019 at 10:01):

Will this be easier with the Lean 4 non-monotonic elaboration?

#### Kenny Lau (Jan 25 2019 at 10:02):

@Sebastian Ullrich how did you get that output?

#### Sebastian Ullrich (Jan 25 2019 at 10:04):

set_option pp.implicit true
set_option pp.notation false
set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true


thanks

#### Sebastian Ullrich (Jan 25 2019 at 10:07):

@Patrick Massot No. The only thing the elaborator can do to figure out le_refl _'s arguments is to unify it with the expected type. Elaboration order doesn't matter if there's only a single way to proceed.

ok, thanks

#### Kevin Buzzard (Jan 25 2019 at 10:08):

I love it when those trace outputs turn from "incomprehensible debugging messages which I can't make any sense of and hence just ignore" to "something I can actually understand". Thanks Sebastian.

#### Kevin Buzzard (Jan 25 2019 at 10:11):

If you use set.mem, it works more or less coincidentally because Lean prefers unfolding the definition set.mem over the projection has_le.le.

One could imagine that rewriting Lean from scratch might change the coincidences that happen now to a completely different set of coincidences which may or may not happen. I wonder to what extent mathlib depends on such coincidences.

#### Kevin Buzzard (Jan 25 2019 at 10:14):

So the bug in has_mem.mem is that is that it is unfolded after has_le.le. Maybe someone should make a PR. How does one control unfolding power?

#### Sebastian Ullrich (Jan 25 2019 at 10:15):

No, they're both unfolded in the same step. You can't customize this.

#### Sebastian Ullrich (Jan 25 2019 at 10:16):

Unification isn't likely to change much, but heuristics in other parts of the elaborator may behave differently, yes.
I'm not an expert on unification, but I suppose one could argue that maybe Lean shouldn't unfold projections of stuck parent projections like @has_le.le ?m_1 (@preorder.to_has_le ?m_1 ?m_2). Not sure how other systems handle that.

#### Sebastian Ullrich (Jan 25 2019 at 10:22):

Uh... which is exactly what it would do when using new-style structures. If you copy the relevant code to a context where old_structure_cmd is not set, it just works.

namespace foo
class preorder (α : Type u) extends has_le α, has_lt α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b, a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)

@[refl] lemma le_refl {α} [preorder α] : ∀ a : α, a ≤ a :=
preorder.le_refl

instance : preorder nat := sorry
example (a : ℕ) : a ∈ {x : ℕ | x ≤ a} := le_refl _
end foo


#### Sebastian Ullrich (Jan 25 2019 at 10:25):

So depending on what preorder looks like in Lean 4 (where it may not be a part of core), this may just work. If it gets bundled, the unfication problems will look completely different anyway.

Last updated: May 08 2021 at 19:11 UTC