1
$\begingroup$

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.

$\endgroup$

2 Answers 2

3
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Indeed, eta-expansion holds as a definitional rule in Coq. $\endgroup$ Commented Jun 21 at 18:00
  • $\begingroup$ Is the Coq built-in notion of function equality just $\alpha\beta\eta$-equivalence? That would make a lot of sense. $\endgroup$ Commented Jun 21 at 18:30
  • 3
    $\begingroup$ @GregNisbet Coq decides definitional equality (i.e.: when eq_refl works) by its "convertibility" relation, which is documented in the manual. (Most of Coq's core language is specified in great detail by the manual.) Convertibility is essentially $\alpha\beta\delta\iota\zeta\eta$-equivalence. ($\delta$ is Coq's rule for expanding definitions, $\iota$ reduces match, fix, and cofix, $\zeta$ removes lets. These rules are necessary as the core language is a bit more than just lambda calculus.) $\endgroup$
    – HTNW
    Commented Jun 21 at 19:12
  • $\begingroup$ Note that while propositional equality without funext is quite restricted, it is still more complicated than definitional equality. For instance, if you define an iter : forall A : Type, nat -> (A -> A) -> A -> A (such that iter A n f is $f^n$), you can prove propositionally (for instance, by induction over the natural) that iter A (n + 0) f = iter A n f, but this equality does not hold definitionally. More generally, if you manage to show m = n then iter A m f = iter A n f is also provable, again without funext. $\endgroup$ Commented Jun 24 at 9:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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