[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy
theory & advantage of UF/Coq
=?GB2312?B?TWF4aW1lIESopm6oqHM=?=
mail at maximedenes.fr
Tue Jan 7 17:56:40 CET 2014
Very nice :)
I was pretty sure that the example was not using K intrinsically, since
it was typable in Coq.
If I understand correctly, what makes it syntactically go through
--without-K is that when noo eliminates the equality proof, the argument
is a variable.
Still, I don't understand why replacing the pattern matching in my
example by a call to subst makes the termination check fail.
Maxime.
On 01/07/2014 11:42 AM, Conor McBride wrote:
> On 7 Jan 2014, at 09:28, Altenkirch Thorsten <psztxa at exmail.nottingham.ac.uk> wrote:
>
>>
>> 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.
> Not so fast! The code below is accepted using the --without-K flag, and
> the elimination that noo does is a based path induction, IIUC.
>
> Conor
>
> {-# OPTIONS --without-K #-}
>
> module BadWithoutK where
>
> data Zero : Set where
>
> data WOne : Set where
> wrap : (Zero -> WOne) -> WOne
>
> data _<->_ (X : Set) : Set -> Set where
> Refl : X <-> X
>
> postulate
> myIso : WOne <-> (Zero -> WOne)
>
> moo : WOne -> Zero
> noo : (X : Set) -> (WOne <-> X) -> X -> Zero
>
> moo (wrap f) = noo (Zero -> WOne) myIso f
> noo .WOne Refl x = moo x
>
> bad : Zero
> bad = moo (wrap \ ())
>
>
>
>> 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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list