The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Dear Russell,
 We looked closely at this and you are right, the induction principle 
for the ``parametrized type'' is the same
as for an unparametrized type in the new case when n changes inside the 
constructors.
(Perhaps somebody could comment on why this change was made; apparently 
it is only for questions of universes?)
In particular this should give no benefit with respect to what you 
called your first option, and of course you would want
your second option so as to be able to specialize to specific values of n.
We didn't see any way of modifying the _rec statement to do better, 
because when n changes in the constructors, you need to
specify a dependent type P in the induction statement, over all possible 
values of n.
So finally we completely agree that Russell's contributions should be 
added to the standard library.
---Carlos, Marco




roconnor AT theorem.ca
 wrote:

> On Tue, 31 Jan 2006, Carlos.SIMPSON wrote:
>
>  
>
> > Inductive FinConditional (n : nat) : bool -> Set :=
> > | fin_prev : FinConditional (pred n) (non_zero n) -> Fin n true
> > | fin_next : FinConditional n true.
> >
> > Definition Fin n := FinConditional n true.
> >    
>
> I don't understand how this would be an improvement over either of my two
> proposals.  Perhaps you could explain.
>
> Also, Fin 0 ought to be empty, but this is (presumably) easy to fix.
>
>