The Coq mailing list

[Pierre-Yves Strub <pierre-yves AT strub.nu>]

You should also look at section 27.3.1 of the reference manual -
although it doesn't help for your unprovable goal.

Best,
-- Pierre-Yves.

2016-01-26 23:42 GMT+01:00 Emilio Jesús Gallego Arias 
<e+coq-club AT x80.org>:
> 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