The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

The question is wether "RedSize M N p" doesn't depend on p, i.e. wether for 
p, q : Red M N we 
have RedSize M N p = RedSize M N q (assuming we move Red to Set temporarily). 
If yes, it
should be possible to define RedSize given your signature.

I have to admit that when I think of Prop then it is rather Voevodsky's hProp 
then Coq's builtin Prop.

Thorsten

On 4 Nov 2011, at 20:53, Randy Pollack wrote:

> I have some inductively defined set, say of terms
> 
>  Inductive Term : Set := ...
> 
> and some inductively defined relation, say of reduction
> 
> Inductive Red : Term -> Term -> Prop := ...
> 
> I want to do induction on the size of derivations of the Red relation.
> So I try to define
> 
> Fixpoint RedSize : (M N: Term) (r:Red M N) {struct r} : nat :=
>    match r with ...
>    end.
> 
> This fails, because Red is a Prop, not a Set.  How is this usually done?
> 
> One could index the relation Red with size, as is necessary in (simply
> typed) HOL, but it seems we should do better with dependent types.
> 
> Thanks,
> Randy