The Coq mailing list

[Cody Roux <cody.roux AT andrew.cmu.edu>]

The thing about Coq is that it's very disturbing not to have a
Set-theoretic interpretation where Prop is the set of Booleans {True,
False}. Agda of course doesn't have these qualms, but the fact that this
issue appears in Coq without use of anything fancy (impredicativity,
etc) makes me still a bit worried. In particular there should be a
Set-theoretic model for Agda where Empty -> Box and Box -are- equal:
with a sufficiently clever interpretation of inductives, I believe I can
get [[Empty -> Box ]] = [[Box]] = { {} } (where {} is just the empty
set). Can someone with more Agda knowledge try to type the original
problematic term?


Hypothesis Heq : (False -> False) = True.

Fixpoint contradiction (u : True) : False :=
contradiction (
match Heq in (_ = T) return T with
| eq_refl => fun f:False => match f with end
end
).



On 01/06/2014 06:12 PM, Altenkirch Thorsten wrote:
> 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