The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 07/19/2013 01:23 PM, Michiel Helvensteijn wrote:
> Take this simplified example of my own situation:
>
> Inductive Test1 := t1list : list Test2 ->  Test1
> with      Test2 := t2item : Test1 ->  Test2.
>
> Now I want to define a simple property on it, such as:
>
> Require Import Coq.Lists.List.
> Fixpoint short_lists1 t : Prop :=
>    match t with t1list lst =>
>      length lst<  10  /\
>      Forall (fun t2 =>  short_lists2 t2) lst
>    end
> with short_lists2 t : Prop :=
>    match t with t2item t1 =>  short_lists1 t1 end.
>
> Coq won't accept it, because I'm attempting structural reduction
> through both `Test1` and `list`.
>    

I think if you define a variant of [Forall] based on recursion instead 
of induction, this will just work, since the termination checking 
understands the former but not the latter.