unification

Stream: general

[Kevin Buzzard]

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]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

does it?

[Kevin Buzzard]

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

[Kevin Buzzard]

I think the @ changes Lean's elaboration procedure.

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

no @

[Kevin Buzzard]

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]

Oh so you are right.

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

aka plebs

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sebastian Ullrich]

arrives at university

How does unification work?

turns around and leaves

[Kevin Buzzard]

maybe it's hard?

[Kevin Buzzard]

"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]

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]

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

[Kevin Buzzard]

not something you see very often, the @@

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kenny Lau]

perhaps

[Kevin Buzzard]

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

[Kenny Lau]

has_le.le is a function with > 0 inputs

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kenny Lau]

global sections of affine schemes are dependent functions

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Sebastian Ullrich]

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] [1]: @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] [2]: @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] [3]: @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] [4]: (λ (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] [5]: nat.less_than_or_equal a a =?= @preorder.le ?m_1 ?m_2 ?m_3 ?m_3
[type_context.is_def_eq_detail] [6]: 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]

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

[Kenny Lau]

@Sebastian Ullrich how did you get that output?

[Sebastian Ullrich]

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

[Kenny Lau]

thanks

[Sebastian Ullrich]

@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.

[Patrick Massot]

ok, thanks

[Kevin Buzzard]

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]

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]

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]

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

[Sebastian Ullrich]

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]

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]

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.