[Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Andreas Abel]

Maxime, thanks for this nice example!  Find it on darcs Agda under

   test/succeed/HoTTAndStructuralOrderingIncompatibleMaximeDenes.agda

This is actually fuel on my fire.  It shows that the untyped structural 
termination order works only by accident.  It is not the first paradox 
found in the structural ordering, see e.g. Coquand, Pattern matching..., 
1992.

If you look at the Box through the lens of sized types, you cannot 
reproduce the loop.  Without sizes, your postulated isomorphism can fool 
the structural order.  Basically, to go from (Empty -> Box) to Box via 
the isomorphism would add another wrap constructor, but by going through 
propositional equality, you can hide this fact from Agda.  With sized 
types, the isomorphism is only between (Empty -> Box i) and (Box (i+1)), 
which exposes the increase in size when going in the 'to' direction. 
Here is the Agda code:

{-# OPTIONS --sized-types #-}

open import Common.Size
open import Common.Equality

data Empty : Set where

data Box : Size → Set where
   wrap : ∀ i → (Empty → Box i) → Box (↑ i)

-- Box is inhabited at each stage > 0:

gift : ∀ {i} → Empty → Box i
gift ()

box : ∀ {i} → Box (↑ i)
box {i} = wrap i gift

-- wrap has an inverse:

unwrap : ∀ i → Box (↑ i) → (Empty → Box i)
unwrap .i (wrap i f) = f

-- There is an isomorphism between (Empty → Box ∞) and (Box ∞)
-- but none between (Empty → Box i) and (Box i).
-- We only get the following, but it is not sufficient to
-- produce the loop.

postulate iso : ∀ i → (Empty → Box i) ≡ Box (↑ i)

-- Since Agda's termination checker uses the structural order
-- in addition to sized types, we need to conceal the subterm.

conceal : {A : Set} → A → A
conceal x = x

mutual
   loop : ∀ i → Box i → Empty
   loop .(↑ i) (wrap i x) = loop' (↑ i) (Empty → Box i) (iso i) (conceal x)

   -- We would like to write  loop' i  instead of  loop' (↑ i)
   -- but this is ill-typed.  Thus, we cannot achieve something
   -- well-founded wrt. to sized types.

   loop' : ∀ i A → A ≡ Box i → A → Empty
   loop' i .(Box i) refl x = loop i x

-- The termination checker complains here, rightfully!

Cheers,
Andreas

On 06.01.2014 21:42, Maxime Dénès 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/