The Coq mailing list

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

On 27/01/2016 23:51, 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.

> I am not saying that they cannot be equal, I am instead saying that it
> shouldn't be considered a Coq bug that they are not forced to be equal
> (or forced to be not equal).  Just as it should not be considered a Coq
> bug that proofs are not forced to be irrelevant (or forced to be
> relevant).  Or that excluded middle is not part of the logic.  In other
> words, it is a feature of Coq that its logic is weak enough to encompass
> many useful additions by axioms, yet permit usage without those axioms. 
> I honestly did not think this was the least bit controversial.

Since you are mentioning proof irrelevance and excluded middle, you seem
to have missed the point of my email. If it is impossible to build a
model of Coq's logic that invalidates a given axiom, the lack of this
axiom is not controversial, it is just a "bug", as Thorsten calls it.
(There might be technical reasons for not having such an axiom, so I
would rather call it a misfeature though.)

Now I am not saying that there are no models that invalidate functional
extensionality. What I am saying is that there are no models of coq's
logic that invalidate functional extensionality because of time
complexity of functions (that is impossible). So people should just
refrain from talking about time complexity whenever the topic of
functional extensionality comes around. It is just irrelevant.

As for proof irrelevance, there are models for both relevance and
irrelevance, so this is indeed controversial which one is better (if
any). Same for excluded middle, and so on. Note that that does not mean
that there exist models for every combination of such axioms; for
instance, it is well-known that there are no models of Coq's logic
mixing both excluded middle and proof relevance. This makes it a
relevant argument when people wonder about such axioms.

Best regards,

Guillaume