The Coq mailing list

[Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>]

On 07/01/2014 00:50, "Maxime Dénès" 
<mail AT maximedenes.fr>
 wrote:

>Well, my example does not typecheck with the --without-K flag.
>
>However, the same thing can be proven in Coq without K, so I am not sure
>if it is because the flag is too restrictive or because Agda's pattern
>matching is different.

Very good. Agda is right and Coq got it wrong. As I said previosuly the
definition of loop implicitely uses K.

T.

>
>I am also not sure how specific the problem is to univalence. As Cody
>said, I would expect to find some set-theoretical models where the
>equality holds. So being able to prove the negation is disturbing.
>
>Maxime.
>
>On 01/06/2014 07:23 PM, Abhishek Anand wrote:
>> It is known that UIP is inconsistent with univalence.
>> Does this typecheck even after disabling UIP(==K axiom?) ?
>> I might be wrong, but I think that UIP is baked into the typechecker
>> of Agda.
>> But, UIP can be disabled somehow?
>>
>>
>> -- Abhishek
>> http://www.cs.cornell.edu/~aa755/ <http://www.cs.cornell.edu/%7Eaa755/>
>>
>>
>> On Mon, Jan 6, 2014 at 3:42 PM, Maxime Dénès 
>> <mail AT maximedenes.fr
>> <mailto:mail AT maximedenes.fr>>
>>  wrote:
>>
>>     Bingo, Agda seems to have the same problem:
>>
>>     module Termination where
>>
>>     open import Relation.Binary.Core
>>
>>     data Empty : Set where
>>
>>     data Box : Set where
>>     wrap : (Empty → Box) → Box
>>
>>     postulate
>>     iso : (Empty → Box) ≡ Box
>>
>>     loop : Box -> Empty
>>     loop (wrap x) rewrite iso = loop x
>>
>>     gift : Empty → Box
>>     gift ()
>>
>>     bug : Empty
>>     bug = loop (wrap gift)
>>
>>     However, I may be missing something due to my ignorance of Agda.
>>     It may be well known that the axiom I introduced is inconsistent.
>>     Forgive me if it is the case.
>>
>>     Maxime.
>>
>>
>>     On 01/06/2014 01:15 PM, Maxime Dénès wrote:
>>
>>         The anti-extensionality bug is indeed related to termination.
>>         More precisely, it is the subterm relation used by the guard
>>         checker which is not defined quite the right way on dependent
>>         pattern matching.
>>
>>         It is not too hard to fix (we have a patch), but doing so
>>         without ruling out any interesting legitimate example (dealing
>>         with recursion on dependently typed data structures) is more
>>         challenging.
>>
>>         I am also curious as to whether Agda is impacted. Let's try it
>>:)
>>
>>         Maxime.
>>
>>         On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:
>>
>>             Which bug was this?
>>
>>             I only saw the one which allowed you to prove
>>             anti-extensionality? But
>>             this wasn't related to termination, or?
>>
>>             Thorsten
>>
>>             On 06/01/2014 16:54, "Cody Roux" 
>> <cody.roux AT andrew.cmu.edu
>>             
>> <mailto:cody.roux AT andrew.cmu.edu>>
>>  wrote:
>>
>>                 Nice summary!
>>
>>
>>                 On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
>>
>>                     Agda enforces termination via a termination
>>                     checker which is more
>>                     flexible but I think less principled than Coq's
>>                     approach.
>>
>>                 That's a bit scary given that there was an
>>                 inconsistency found in
>>                 the Coq termination checker just a couple of weeks ago
>>:)
>>
>>                 BTW, has anyone tried reproducing the bug in Agda?
>>
>>
>>                 Cody
>>
>>             This message and any attachment are intended solely for
>>             the addressee and may contain confidential information. If
>>             you have received this message in error, please send it
>>             back to me, and immediately delete it. Please do not use,
>>             copy or disclose the information contained in this message
>>             or in any attachment. Any views or opinions expressed by
>>             the author of this email do not necessarily reflect the
>>             views of the University of Nottingham.
>>
>>             This message has been checked for viruses but the contents
>>             of an attachment
>>             may still contain software viruses which could damage your
>>             computer system, you are advised to perform your own
>>             checks. Email communications with the University of
>>             Nottingham may be monitored as permitted by UK legislation.
>>
>>
>>
>>
>>
>>         _______________________________________________
>>         Agda mailing list
>>         
>> Agda AT lists.chalmers.se
>>  
>> <mailto:Agda AT lists.chalmers.se>
>>         https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>>     _______________________________________________
>>     Agda mailing list
>>     
>> Agda AT lists.chalmers.se
>>  
>> <mailto:Agda AT lists.chalmers.se>
>>     https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
>_______________________________________________
>Agda mailing list
>Agda AT lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda