coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is it possible to rewrite under binders?

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is it possible to rewrite under binders?
Date: Wed, 27 Jan 2016 10:36:24 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f42.google.com
Ironport-phdr: 9a23:j9Iq1RYWFKY5Yq4UEagzVSD/LSx+4OfEezUN459isYplN5qZpc+zbnLW6fgltlLVR4KTs6sC0LqJ9fi6EjNfqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0o8eYPFoArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JcGIQmwZICg6NyBz7QJr3rmOutO172SqXOcD7Zb8xUDWmqaxsTUm72288Kzcl/TSP2YRLh6VBrUf5qg==

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.

Maybe this just indicates a difference in Coq usage between software developers and type theorists. Although Curry-Howard says we should correspond ;)

-- Jonathan

[Coq-Club] Is it possible to rewrite under binders?, Hugo Carvalho, 01/26/2016
- Re: [Coq-Club] Is it possible to rewrite under binders?, Jonathan Leivent, 01/26/2016
- Re: [Coq-Club] Is it possible to rewrite under binders?, Emilio Jesús Gallego Arias, 01/26/2016
  - Re: [Coq-Club] Is it possible to rewrite under binders?, Pierre-Yves Strub, 01/27/2016
- Re: [Coq-Club] Is it possible to rewrite under binders?, Thorsten Altenkirch, 01/27/2016
  - Re: [Coq-Club] Is it possible to rewrite under binders?, Jonathan Leivent, 01/27/2016
    - Re: [Coq-Club] Is it possible to rewrite under binders?, Thorsten Altenkirch, 01/27/2016
    - Re: [Coq-Club] Is it possible to rewrite under binders?, Guillaume Melquiond, 01/27/2016
      - Re: [Coq-Club] Is it possible to rewrite under binders?, Jonathan Leivent, 01/27/2016
        
        Re: [Coq-Club] Is it possible to rewrite under binders?, Guillaume Melquiond, 01/28/2016
        
        Re: [Coq-Club] Is it possible to rewrite under binders?, Pierre-Marie Pédrot, 01/28/2016
        
        Re: [Coq-Club] Is it possible to rewrite under binders?, Jonathan Leivent, 01/28/2016
        Re: [Coq-Club] Is it possible to rewrite under binders?, Guillaume Melquiond, 01/28/2016
        Re: [Coq-Club] Is it possible to rewrite under binders?, Jonathan Leivent, 01/28/2016
        Re: [Coq-Club] Is it possible to rewrite under binders?, Guillaume Brunerie, 01/28/2016