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

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

Last updated: Dec 20 2023 at 11:08 UTC