The Coq mailing list

[Aaron Stump <aaron.stump AT gmail.com>]

Related (I hope) to the discussion of eliminators, I want to point out that if we were working in a type theory based on positive recursive types rather than primitive datatypes, this example would not go through (of course).

Empty := mu X.X

Box := mu X. (Empty -> X)

Note that X occurs positively in the body of the mu-type for Box.  The theory gives us a recursor R with this typing rule

b : Box
f : (Empty -> T) -> T
---------------------
R(b,f) : T

We certainly have the isomorphism Box = (Empty -> Box) -- it is even a definitional equality! -- but we cannot use this recursor to write a term of type Box -> Empty.  The best we could do would be to start like this, where g has type Empty -> Empty, and hence is useless for deriving Empty.

loop = \ b . R(b, \ g . (g ?))

So I think the wrap constructor being used in Maxime's code is just an explicit witness of the above implicit isomorphism.  Removing it should not count for structural decrease (obviously).

Cheers,
Aaron

On 01/08/2014 11:53 AM, Andreas Abel wrote:

Conor,

that's on the latest darcs version of Agda, I guess?

At least my own version of --without-K rejects your match on Refl:

The indices
  WOne
  X
are not constructors (or literals) applied to variables (note that
parameters count as constructor arguments)
when checking that the pattern Refl has type WOne <-> X

But you say it is justified, is it?

Cheers,
Andreas

On 07.01.2014 17:42, Conor McBride wrote:

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 \ ())

_______________________________________________
Agda mailing list
Agda AT lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda