Missing η

Stream: general

[Gabriel Ebner]

@Anne Baanen just showed me an interesting example, where you would expect η-reduction:

example : (λ a b, a + b) = ((+) : ℕ → ℕ → ℕ) := rfl -- fails

What is going wrong here?

[Anne Baanen]

Other fun examples:

example (f : nat → nat → nat) : (λ (a b : nat), f a b) = f := rfl -- works
example : let f : nat → nat → nat := (+) in (λ (a b : nat), f a b) = f := rfl -- fails
example (g : nat → nat → nat) : let f : nat → nat → nat := g in (λ (a b : nat), f a b) = f := rfl -- works

[Anne Baanen]

example : (λ (a b : nat), a + b) = (λ (a b : nat), a + b) := rfl -- works

[Johan Commelin]

Gabriel Ebner said:

Anne Baanen just showed me an interesting example, where you would expect η-reduction:

example : (λ a b, a + b) = ((+) : ℕ → ℕ → ℕ) := rfl -- fails

What is going wrong here?

Does it work if you switch the two sides? How/when does Lean figure out that the + on the LHS is addition for ℕ?

[Chris Hughes]

Is it something to do with this? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unify.20fails.20in.20the.20presence.20of.20binders

[Gabriel Ebner]

This looks like the same issue.

[Anne Baanen]

My current understanding of the issue: type_context_old::unfold_definition(e) (used in is_def_eq_delta) only unfolds nat.add if it is not applied to any arguments. Thus (+) gets unfolded to nat.brec_on ... and λ a b, nat.add a b doesn't get unfolded anymore. And reduce_aux_recursor is not invoked in time to do the unfolding anyway.

[Anne Baanen]

And so I guess the question is: do we want to stop unfolding of nat.add or start unfolding nat.add a b?

[Anne Baanen]

Here is a test case with less unification:

constants (p : (nat → nat → nat) → Prop) (p_add : p nat.add)

example : p (λ a b, nat.add a b) := p_add