Why did this proof succeed without function extensionality?

Question

I'm very confused as to why a proof of a lemma succeeded without function extensionality.

---

I'm messing around with some trivial Coq proofs for manipulating pseudosequences of the form A -> B -> C -> D.

I'm interested in this way of using Coq because it lets me write functions in Gallina that act like tactics and use them by attaching hypotheses to my goal, firing off an apply my_gallina_term., and then intros-ing the new hypotheses back into the environment. I'm also hoping to understand basic SSReflect (i.e. just the goal management parts, not the reflection parts, which I don't understand yet).

Anyway, here's a swapper function, which swaps the two arguments of a two-argument function.

Lemma identity : forall A, A -> A.
Proof. easy. Qed.

Definition swapper : forall {A} {B} {C}, (A -> B -> C) -> (B -> A -> C) :=
  fun A B C f x y => f y x.

Lemma swapper_is_invertible : forall A B C f, f = @swapper B A C (swapper f).
Proof.
  intros.
  easy.
Qed.

I can't figure out why this lemma succeeded. I'm not assuming function extensionality.

Answer 1

To expand on @NaïmFavier's answer:

The key here is the difference between definitional and propositional equality.

Most times, when people talk about "function extensionality" they mean funext for propositional equality, which says that if you have a proof that two functions agree on every argument, then you can build a proof that the functions are equal. Indeed this cannot be proven in Coq without additional axioms.

However, the other kind of equality is definitional equality. This is the syntactic check that the type checker does when it's trying to answer the question "are these two types equal". For example, this happens whenever you have an application: you make sure that the type of the argument is equal to the domain of the function.

In a language with $\eta$, definitional equality is extensional: two functions are defined to be definitionally equal if their bodies are definitionally equal, when they are given the same fresh variable as an argument. This is almost like funext, but it's only checking if the functions produce syntactically identical output when given the same variable as input.

There is no general way to turn a propositional equality proof into a definitional equality proof, so if you have a proof that two functions agree on their arguments, you can't use this to build a definitional equality, and hence you can't derive functional extensionality.

There are languages with something called equality reflection where you can turn any propositional equality into a definitional equality, and in these languages, you can prove funext as a proof.

Answer 2

You don't need function extensionality to prove that, only the $\eta$-rule for functions: then both sides are equal to $\lambda x y.\ f x y$. I don't know if that's how Coq does it.