# Zulip Chat Archive

## Stream: general

### Topic: Missing η

#### Gabriel Ebner (Mar 04 2020 at 13:53):

@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 (Mar 04 2020 at 13:55):

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 (Mar 04 2020 at 13:58):

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

#### Johan Commelin (Mar 04 2020 at 14:20):

Gabriel Ebner said:

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

example : (λ a b, a + b) = ((+) : ℕ → ℕ → ℕ) := rfl -- failsWhat 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 (Mar 04 2020 at 14:20):

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 (Mar 04 2020 at 14:22):

This looks like the same issue.

#### Anne Baanen (Mar 04 2020 at 16:33):

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 (Mar 04 2020 at 16:43):

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 (Mar 04 2020 at 16:49):

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

Last updated: May 09 2021 at 19:11 UTC