The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/26/2016 01:56 PM, Hugo Carvalho wrote:
> Hi Club!
>
> Consider the following goal:
>
> Example e1 : (fun x => 1 + x) = (fun x => S x).
>
> This is provable, as computation occurs under binders normally, and
> addition in Coq happens to be defined recursively over the first argument.
>
> 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)?

It's my understanding that this is not provable in Coq's logic without 
the addition of the functional extensionality axiom.   Not being a type 
theorist, the way I think about this is to view Leibniz equality as 
being too strong - it not only says that the functions compute the same 
results, it says that they compute the same results using the same 
technique (modulo reduction - which allows 1 + x to reduce to S x).  The 
functional extensionality axiom basically adds "computational technique 
irrelevance" to Coq.  Coq's logic would otherwise allow you to keep 
computational techniques relevant (modulo reduction again).

But I will differ to the type theorists here - there are many on this list.

-- Jonathan