The Coq mailing list

[Dan Licata <drl AT cs.cmu.edu>]

On Mar24, Adam Chlipala wrote:
> Ruddy Hahn wrote:
> >Inductive snatlist : Set :=
> >  | snil : snatlist
> >  | scons : forall (n : nat) (l : snatlist), ~ (occur n l) -> snatlist
> >with occur (n : nat) (l : snatlist) : Prop :=
> >  | ocHead : forall (n : nat) (l : snatlist) (p : ~ (occur n l)), 
> >occur n (scons n l p)
> >  | ocCons : forall (m  : nat) (l : snatlist) (p: ~ (occur n l)),
> >      (occur m l) -> occur m (scons n l p)
> >

> Even switching this won't help you.  When defining mutually inductive 
> types, none of the types being defined may appear in the type of 
> another.  Here you have [snatlist] appearing in the type of [occur], 
> despite the fact that these types are mutually inductive.  You will need 
> to use some less direct encoding to achieve what you're looking for.

By the way, in Agda, you can define mutally inductive types where one is
indexed by the other.  So in addition to defining this type with
induction-recursion, you can define it with two datatypes.  However,
there is still a positivity restriction, so you can do your example by
defining "DoesntOccur" instead of negating "Occur":

  data Nat : Set where
    Z : Nat
    S : Nat -> Nat

  data Void : Set where

  data Id {A : Set} (x : A) : A -> Set where
    Refl : Id x x

  mutual
    data SNatList : Set where
      SNil  : SNatList 
      SCons : (n : Nat) -> (l : SNatList) 
            -> (DoesntOccur n l) 
            -> SNatList

    data DoesntOccur (n : Nat) : (l : SNatList) -> Set where
      ONil  : DoesntOccur n SNil
      OCons : forall {n' l p}
            -> (Id n n' -> Void)
            -> DoesntOccur n l
            -> DoesntOccur n (SCons n' l p)

I'm not sure how well worked-out the theory of these mutually-indexed
inductive types is, though.

-Dan