The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Jul 19, 2013 at 1:50 PM, Michiel Helvensteijn
<mhelvens AT gmail.com>
 wrote:
> On Fri, Jul 19, 2013 at 9:46 PM, Daniel Schepler 
> <dschepler AT gmail.com>
>  wrote:
>
>>> If possible, I'd still like a response to my question (1).
>>
>> This is something like what I'd expect a mutual induction principle to
>> look like:
>
> That looks like it took some effort. :-)
>
> I assure you it's not wasted, because I'll study it. But my primary
> question is more basic:
>
> How can those definitions be used to get Coq to accept the definitions
> of `short_lists1` and `short_lists2`?

First, here's a simplified version of the recursion principle where
the result types are constant:

Definition Test1_rect_nondep {P Q:Type}
  (rec_fun1 : list Test2 -> list Q -> P)
  (rec_fun2 : Test1 -> P -> Q) : Test1 -> P :=
fix F (t1 : Test1) : P :=
match t1 with
| t1list l => rec_fun1 l (map G l)
end with
G (t2 : Test2) : Q :=
match t2 with
| t2item t => rec_fun2 t (F t)
end for F.
Definition Test2_rect_nondep {P Q:Type}
  (rec_fun1 : list Test2 -> list Q -> P)
  (rec_fun2 : Test1 -> P -> Q) : Test2 -> Q :=
fix F (t1 : Test1) : P :=
match t1 with
| t1list l => rec_fun1 l (map G l)
end with
G (t2 : Test2) : Q :=
match t2 with
| t2item t => rec_fun2 t (F t)
end for G.

Then, to use these to define your short_lists{1,2}:
Definition short_lists1 : Test1 -> Prop :=
Test1_rect_nondep
 (fun (l : list Test2) (child_shortness : list Prop) =>
   length l < 10 /\
   Forall (fun P:Prop => P) child_shortness)
 (fun _ (P:Prop) => P).
Definition short_lists2 : Test2 -> Prop :=
Test2_rect_nondep
 (fun (l : list Test2) (child_shortness : list Prop) =>
   length l < 10 /\
   Forall (fun P:Prop => P) child_shortness)
 (fun _ (P:Prop) => P).
-- 
Daniel Schepler