The Coq mailing list

[Andreas Abel <abela AT chalmers.se>]

On 08.01.14 7:37 PM, Aaron Stump wrote:
> 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

Mmh, why is this the recursor?  Should not T depend on (b : Box) or 
something similar?

This looks like the iterator to me...  Maybe that's what you meant...

> 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).

Where would you locate the structural decrease instead?

Cheers,
Andreas

> 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