[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