The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

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