The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

(* find '--' patterns for my replies *)

(* 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? *)

(*-- It is fundamental, but as you did below, we can have dependent types,
  which accepts different parameters,
 and dealing is not as easy as with non dependent types *)

(* 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.
*)
(*-- And what about: *)
Inductive SillyTree : bool -> Type :=
 | leaf : SillyTree true
 | node : SillyTreePair -> SillyTree false
with SillyTreePair : Type :=
 | stp : forall b, SillyTree b -> SillyTree b -> SillyTreePair.
(*
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. *)
Definition isMyTree (st:SillyTree false) : bool :=
match st with
| node (stp b leaf leaf) => b (* a must equal b,
                              but pattern matching forces us to
                              provide a new pattern variable b *)
| _ => false
end.

(* 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.
*)
(*-- that is what I did upper but in a non embedded structure, so you can  
use it
 separetely *)

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

(* Hope it helped,

Cedric *)