Zulip Chat Archive

Stream: general

Topic: unification


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jan 25 2019 at 08:53):

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

view this post on Zulip Kenny Lau (Jan 25 2019 at 08:54):

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

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 08:54):

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

view this post on Zulip Kenny Lau (Jan 25 2019 at 08:54):

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

view this post on Zulip Kenny Lau (Jan 25 2019 at 08:54):

does it?

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 08:54):

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

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 08:54):

I think the @ changes Lean's elaboration procedure.

view this post on Zulip 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?"

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jan 25 2019 at 08:55):

no @

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 08:56):

Oh so you are right.

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jan 25 2019 at 08:57):

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

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 08:57):

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

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 08:57):

aka plebs

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 08:58):

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

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 09:00):

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

view this post on Zulip Sebastian Ullrich (Jan 25 2019 at 09:01):

arrives at university

How does unification work?

turns around and leaves

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 09:02):

maybe it's hard?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 09:05):

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

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 09:05):

not something you see very often, the @@

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 09:11):

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

view this post on Zulip Kenny Lau (Jan 25 2019 at 09:11):

perhaps

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 09:12):

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

view this post on Zulip Kenny Lau (Jan 25 2019 at 09:12):

has_le.le is a function with > 0 inputs

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 09:12):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jan 25 2019 at 09:16):

global sections of affine schemes are dependent functions

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 09:23):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 09:49):

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

view this post on Zulip Kevin Buzzard (Jan 25 2019 at 09:50):

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

view this post on Zulip 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] [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.

view this post on Zulip Patrick Massot (Jan 25 2019 at 10:01):

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

view this post on Zulip Kenny Lau (Jan 25 2019 at 10:02):

@Sebastian Ullrich how did you get that output?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jan 25 2019 at 10:04):

thanks

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 25 2019 at 10:08):

ok, thanks

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Sebastian Ullrich (Jan 25 2019 at 10:15):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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