The Coq mailing list

[roconnor AT theorem.ca]

According to the Coq manual, mutually defined inductive types must have 
the same parameters for all inductive definitions.  Is this restriction 
fundamental, or is there only to simplify the implemenation?

I'll try to give a simplified example of where I want to have mutually 
defined inductive definitions with different parameters below.  I have a 
real example in mind for the definion of a type for the syntax of a 
moderately complex language.

Consider the type family of silly trees:

Inductive SillyTree : bool -> Type :=
 | leaf : SillyTree true
 | node : forall b, SillyTree b -> SillyTree b -> SillyTree false.

I want to be able to pattern match on my silly trees like in the 
following:

Definition sillyFunction (st:SillyTree false) : bool :=
match st with
| node a leaf leaf => a
| _ => false
end.

The above works all fine.  But now I want to capture the pair of 
SillyTrees occuring in the node constructor as its own type, because I 
want to reuse this notion in many places.  I try to make a mutual 
inductive type:

Inductive SillyTree : bool -> Type :=
 | leaf : SillyTree true
 | node : forall b, SillyTreePair b -> SillyTree false
with SillyTreePair (b:bool) : Type :=
 | stp : SillyTree b -> SillyTree b -> SillyTreePair b.

but this fails because the type parameters are not all the same in the 
different defintions.

One attempted solution is to make SillyTreePair a family:

Inductive SillyTree : bool -> Type :=
 | leaf : SillyTree true
 | node : forall b, SillyTreePair b -> SillyTree false
with SillyTreePair : bool -> Type :=
 | stp : forall b, SillyTree b -> SillyTree b -> SillyTreePair b.

however, there is a problem.  When pattern matting we get a new pattern 
variable bound:

Definition isMyTree (st:SillyTree false) : bool :=
match st with
| node a (stp b leaf leaf) => a (* a must equal b,
                              but pattern matching forces us to
                              provide a new pattern variable b *)
| _ => false
end.

This new variable b must always be equal to a; however we do not get such 
a proof when doing normal pattern matching.

Another attempt is to use the existing product type to capture this pair 
as one object.

Inductive SillyTree : bool -> Type :=
 | leaf : SillyTree true
 | node : forall b, (SillyTree b * SillyTree b) -> SillyTree false.

Definition isMyTree (st:SillyTree false) : bool :=
match st with
| node a (pair leaf leaf) => a
| _ => false
end.

This works, but we no longer get our own type for (SillyTree b * SillyTree 
b).  In particular, I want to define coercions from SillyTreePairs, but 
now I cannot do it because I'm using the general prod type.

I could define my own pair type:

Inductive TreePair (A : Type) : Type := treePair : A -> A -> TreePair A.

but I have to make it polymorphic.  I have no way to make it only hold 
SillyTrees like I want it to be restricted to.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''