The Coq mailing list

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

Hi Maxime,

your postulate seems correct since certainly Empty → Box and Box are
isomorphic and hence equal as a consequence of univalence.

However, I think the definition of loop looks suspicious in the presence
of proof-relevant equality: if we replace rewrite by an explicit use of
subst, loop isn't structural recursive anymore. Hence my diagnosis would
be that rewrite is simply incompatible with univalence.

Cheers,
Thorsten

On 06/01/2014 20:42, "Maxime Dénès" 
<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>
>>>  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
>> https://lists.chalmers.se/mailman/listinfo/agda
>