The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/27/2016 05:22 PM, Guillaume Melquiond wrote:
> 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

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.

Certainly, it would be nice to have guarantees that use of certain 
axioms does not lead to inconsistency.  I suggested an enhanced version 
of something like Print Assumptions on coqdev once just to help with 
this purpose (assert that a development uses only certain axioms or 
combinations of axioms that are considered consistent together).

-- Jonathan