Is Eta included in definitional equality?

[mtzguido]

In the following code, we try to automatically prove some eta-equivalences. The first two work, at different types, while the third (which is a particular case for the first) fails to be proved automatically. Instantiating e1 appropriately works to prove the goal, but it feels like this should be automatic.

module Eta

val e1 : f:(int -> Tot int) -> Lemma ((fun x -> f x) == f)
let e1 f = ()

val e2 : f:(int -> int -> Tot int) -> Lemma ((fun x -> f x) == f)
let e2 f = ()

val e3 : f:(int -> int -> Tot int) -> x:int -> Lemma ((fun y -> f x y) == f x)
let e3 f x = () // e1 (f x)

Output:

$ ./bin/fstar.exe Eta.fst 
./Eta.fst(9,59-9,84): (Error) could not prove post-condition
Verified module: Eta (519 milliseconds)
1 error was reported (see above)

[kyoDralliam]

I would say that it is rather surprising that you are even able to prove e1 and e2 without importing FStar.FunctionalExtensionality. Using that module you can prove the following

open FStar.FunctionalExtensionality

val e3' : f:(int -> int -> Tot int) -> x:int -> Lemma ((fun y -> f x y) `feq` f x)
let e3' f x = ()

Though I don't understand why the pattern does not kick in immediately (i.e. replacing feq with == did not work).

[mtzguido]

As far as I understand, eta-equivalence is different from functional extensionality. Specifically, eta-equivalence is about definitional equality, while the latter is about propositional equality.

Definitionally, if I have equivalent lambda terms M and N (M ≡ N), I can prove \x. M ≡ \x. N simply by a congruence. However given a propositional proof of \forall x. M = N, I cannot convert this into a proof for \x. M = \x. N (unless of course I assume functional extensionality). I think all of these three should be provable without assuming functional extensionality.

This is the case in Agda (probably in Coq too), where all three proofs go through without assuming it (Agda has eta-reductions).

module Eta where

open import Data.Nat
open import Relation.Binary.HeterogeneousEquality

e1 : (f : ℕ → ℕ) → (λ x → f x) ≅ f
e1 f = refl

e2 : (f : ℕ → ℕ → ℕ) → (λ x → f x) ≅ f
e2 f = refl

e3 : (f : ℕ → ℕ → ℕ) → (x : ℕ) → (λ y → f x y) ≅ f x
e3 f x = refl

[kyoDralliam]

Indeed, my comment was rather stupid... Moreover proving that (fun x y -> f x y) == f and (fun x y -> f x y) == (fun x -> f x) works just fine but (fun x y -> f x y) x == f x does not. It might be because we are not eta-reducing, but rather eta-expanding and we might not beta-reduce afterwards which seems to be needed here... I would expect the result of normalization to be beta-short eta-long form.

[nikswamy]

I don't see why this is a bug. None of our formal calculi include eta. Why should one expect this to be part of definitional equality. It is provable. I'm changing the label to a discussion / enhancement.

[mtzguido]

Randomly remembered this. I don't really mind the lack of eta, but it's not very consistent. The following code works, for instance:

module Eta

val refl : #a:Type -> (#x:a) -> squash (x == x)
let refl #a #x = ()

val e1 : f:(int -> Tot int) -> squash ((fun x -> f x) == f)
let e1 f = refl

val e2 : f:(int -> int -> Tot int) -> squash ((fun x -> f x) == f)
let e2 f = refl

val e3 : f:(int -> int -> Tot int) -> x:int -> squash ((fun y -> f x y) == f x)
let e3 f x = refl

[nikswamy]

Eta equivalence is specifically forbidden in F*. See #2294