The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi Hugo!

Hugo Carvalho 
<hugoccomp AT gmail.com>
 writes:

> This other goal doesn't look as provable:
>
> Example e2: (fun x => x + 1) = (fun x => S x).
>
> Doesn't seem like you can rewrite "x+1" into "S x" (since you can't
> introduce "x" into the context, you can't refer to it in order to
> instantiate an equality you'd use to rewrite)... Is this the case? Is this
> goal unprovable without relying on axioms (functional extensionality does
> the trick, of course)?

Indeed, I think this goal is not probable in Coq, (beware that I'm not a
type theorist).

However, under certain restricted function spaces, "function
extensionality" can be made to hold in Coq.

For instance, if the domain of the function is finite (and decidable),
then you can represent the function as a canonically ordered list and
extensionality holds. This saved me from using the funext axiom in a
few occasions.

The best example I know is the finfun type provided by mathcomp:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/finfun.v

using this library, a (bounded) version of your lemma can be proven:

8<--------------------------------------------------------------------8<
From mathcomp.ssreflect
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype 
finfun.

Example e2 n : [ffun x : 'I_n => x + 1] = [ffun x : 'I_n => S x].
Proof. by apply/ffunP=> ?; rewrite !ffunE addn1. Qed.
8<--------------------------------------------------------------------8<

[I'm afraid I don't know if there's a similar machinery in the standard
 library of Coq]

For instance, this allows to carry environments as ffuns provided you
add a bit of dependently typed syntax bounding the number of variables,
etc...

Best regards,
Emilio