The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Just a comment on this subject:

Until quite recently, the rule for an argument A to be a parameter of an 
inductive definition Ind was that any instance of Ind in the type of a 
constructor either as argument or in the conclusion should be applied to A.

The spirit was that the inductive definition was made in the context of 
the variable A and then discharged. Also for the induction principle, 
this is a condition for A to be treated as a parameter. This was the 
reason for mutual inductive definitions to share the same parameters.

Then, taking advantadge of the separation Fix/Match (versus a general 
induction principle) the condition for parameters was relaxed such that 
Ind in the arguments of constructors could be freely instantiated. Here 
the idea was that Ind could have been be defined as an indexed family 
and then the "parametric" pattern-matching is derivable (although we 
need to keep the indexed family view for the induction principle).
The derived principle is nice in principle but in order to use it you 
have to give up the pattern-matching notation.

So I do not see any major theoretical reason to reject mutual inductive 
definitions with different set of parameters. It is just a bit of work 
to change the implementation consistently.

Christine



roconnor AT theorem.ca
 wrote:
> On Sat, 17 Oct 2009, muad wrote:
>
> > I feel like I might still not understand exactly what is needed, but 
> > perhaps
> > this is a solution?
> >
> > Inductive SillyTreePair SillyTree (b:bool) : Type :=
> > | stp : SillyTree b -> SillyTree b -> SillyTreePair SillyTree b.
> >
> > Inductive SillyTree : bool -> Type :=
> > | leaf : SillyTree true
> > | node : forall b, SillyTreePair SillyTree b -> SillyTree false.
> >
> > Definition sillyFunction (st:SillyTree false) : bool :=
> >  match st with
> >    | node a (stp leaf leaf) => a
> >    | _ => false
> >  end.
> >
> > SillyTree is making use of the fact that SillyTreePair f b is a strictly
> > positive operator in f.
>
> Yes this works, and is a varient of what I had in mind for my very last 
> possible solution that I didn't write out in detail.  It is just a 
> little sad that SillyTreePair ends up being polymorphic in the SillyTree 
> parameter, which means another parameter needs to be passed everywhere.
>
> I would probably rename your SillyTreePair as preSillyTreePair and then 
> define (prehaps a notation) SillyTreePair := preSillyTreePair SillyTree.
>
> Perhaps this is the best compromise, but it still isn't as nice as what 
> you can express in Agda.