The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

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

-- 
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/
{-# OPTIONS --without-K #-}

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