13
$\begingroup$

Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove

Theorem eta : forall (A : Type) (f : A -> A), (fun x => f x) = f?

Does this require functional extensionality?

Edit: I already accepted an answer, but a better (followup) question would be, if Coq supports eta-conversion, why does Eval compute in (fun x => f x). not reduce to f?

Improve this question
$\endgroup$
2
  • 3
    $\begingroup$ It should be noted that even if we have reduction rules related to eta-equality, we would usually do expansion instead of contraction, because it leads to better theoretic properties. $\endgroup$
    – Trebor ♦
    Commented Feb 10, 2022 at 7:53
  • $\begingroup$ @GuyCoder it should probably be a synonym $\endgroup$
    – Couchy
    Commented Feb 10, 2022 at 21:32

2 Answers 2

Reset to default
19
$\begingroup$

Yes, this is provable—indeed, it is provable by reflexivity. This is because Coq has eta-equality of functions built into its notion of definitional equality. Definitional equality also has a congruence rule for lambdas, which does look kind of like function extensionality, but which exists at the judgmental level, and is about definitional equality rather than propositional equality. This does not allow us to prove function extensionality, because the premise in function extensionality is a propositional equality and not a definitional one. In the presence of an equality reflection rule, this would furnish a proof of function extensionality, which is why type systems with equality reflection, eta for functions, and defeq congruence for lambdas validate function extensionality.

Improve this answer
$\endgroup$
10
$\begingroup$

As for your follow-up question: Coq implements η-conversion, but not η-reduction/expansion, because η really is treated at the level of the conversion test and not at that of reduction (which is a sub-routine thereof). Concretely, the conversion test works roughly as follows when comparing t and u:

  1. reduce t and u to weak head normal forms (using a bunch of reduction rules including β but not η)
  2. if one of the reducts is a neutral n and the other is an abstraction fun x : A => t, recursively compare n x and t (this corresponds to η-expanding the neutral followed by a congruence rule for abstraction)

The reasons to do things like this are a bit tricky, but the bottom line is that implementing η inside reduction (be it as expansion or reduction) would either break good properties or simply be unfeasable in current Coq.

I did a talk about this at WITS a few weeks ago, the video does not seem to be up on Youtube yet (it should be there at some point) but the slides and abstract are on my page.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.