The Coq mailing list

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

On 11/04/2011 09:53 PM, 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.

If you do not want to add the size as an extra index, I see two other 
possibilities:
        - define your Red relation in Set as well
	- depending on the way Red is defined, it might happen that the size 
can be computed by case analysis on M and N alone and that the Red 
relation is only useful to ensure termination of the fixoint construction.

This is the case if after case analysis on M and N you end up in a case 
where only one of the Red constructors is possible.

So you can write inversion lemmas Red_case1_inv of the form
      Red M N -> (discriminating condition on M and N) -> Red M0 N0

by case analysis on the proof of Red M N such that Red_case1_inv H is 
considered as a subterm of the proof H of Red M N
     the proof of the lemma has to be something like
      fun H : Red M N =>
      match H returns (discriminating condition on M and N) -> Red M0 N0
      with (c ..p ) => fun ... => p (* the only applicable constructor, 
with p a recursive argument)
          | _ => fun .... => match (p:False) with end (* all the non 
possible cases *)

so you can do your fixpoint construction using a recursive call which is 
structurally decreasing on the proof of Red which can stay in Prop.


I am not sure my explanations are clear enough - if not send me the full 
problem or I can try to post an example where we use this phenomenon.

Hope it helps, al the best.

Christine











> Thanks,
> Randy