The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 27/01/2016 16:36, Jonathan Leivent wrote:

> On 01/27/2016 03:39 AM, Thorsten Altenkirch wrote:
>> Indeed you need functional extensionality which isn’t provable in coq.
>> Imho this is a bug, but one which isn’t easy to fix.
> 
> Why would it be considered a bug?  It is always possible to add the
> functional extensionality axiom to Coq when needed.  And, without it,
> one can express concepts such as that two functions of the same type
> where one sorts lists in O(N^2) time and the other in O(NlogN) time are
> not identical.

I have always found this argument to be far-fetched. Indeed, complexity
and convertibility are two orthogonal concepts. So saying that two
functions with different complexity cannot be equal is nonsensical,
since they might well be convertible and thus trivially equal.

Best regards,

Guillaume