## 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 -- 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 (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)