The Coq mailing list

[Aaron Stump <aaron-stump AT uiowa.edu>]

Hi, Andreas.

On 01/08/2014 12:46 PM, Andreas Abel wrote:
> 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?

Sorry, you are right: this is the iterator, of course.

> 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?
I do not have a proposal for how to address the problem in Agda, since I 
do not know the exact formal system behind Agda well enough to comment.  
I just wanted to connect this problem with a simpler type theory, in 
case it sheds light on the more complex situation here.

Aaron

> 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