The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Jul 19, 2013 at 10:42 AM, Michiel Helvensteijn
<mhelvens 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:

Definition forall_Forall {A:Type} {P:A->Prop}
  (H : forall x:A, P x) : forall l:list A, Forall P l :=
fix F (l:list A) : Forall P l :=
match l return Forall P l with
| nil => Forall_nil _
| cons h t => Forall_cons _ (H h) (F t)
end.

Definition Test1_ind' (P : Test1 -> Prop) (Q : Test2 -> Prop)
  (H : forall l:list Test2, Forall Q l -> P (t1list l))
  (H0 : forall t:Test1, P t -> Q (t2item t)) :
  forall t1:Test1, P t1 :=
fix F (t1:Test1) : P t1 :=
match t1 return P t1 with
| t1list l => H l (forall_Forall G l)
end with
G (t2:Test2) : Q t2 :=
match t2 return Q t2 with
| t2item t => H0 t (F t)
end for F.
Definition Test2_ind' (P : Test1 -> Prop) (Q : Test2 -> Prop)
  (H : forall l:list Test2, Forall Q l -> P (t1list l))
  (H0 : forall t:Test1, P t -> Q (t2item t)) :
  forall t2:Test2, Q t2 :=
fix F (t1:Test1) : P t1 :=
match t1 return P t1 with
| t1list l => H l (forall_Forall G l)
end with
G (t2:Test2) : Q t2 :=
match t2 return Q t2 with
| t2item t => H0 t (F t)
end for G.

And similarly, for a recursion principle with dependent types:

Inductive ForallT {A:Type} (P : A -> Type) : list A -> Type :=
| nil_dep : ForallT P nil
| cons_dep (h:A) (t:list A) : P h -> ForallT P t -> ForallT P (cons h t).
(* Fixpoint ForallT_R {A:Type} (P : A -> Type) (l : list A) : Type :=
match l with
| nil => unit
| cons h t => (P h * ForallT P t)%type
end. *)

Definition map_dep {A:Type} {P:A->Type} (f : forall x:A, P x) :=
fix m (l : list A) : ForallT P l :=
match l return ForallT P l with
| nil => nil_dep _
| cons h t => cons_dep _ _ _ (f h) (m t)
end.
(* Definition map_dep_R {A:Type} {P:A->Type} (f : forall x:A, P x) :=
fix m (l : list A) : forallT_R P l :=
match l return ForallT P l with
| nil => tt
| cons h t => (f h, m t)
end. *)

Require Import List.

Definition Test1_rect' (P : Test1 -> Type) (Q : Test2 -> Type)
  (rec_fun1 : forall l:list Test2, ForallT Q l -> P (t1list l))
  (rec_fun2 : forall t:Test1, P t -> Q (t2item t)) :
  forall t1:Test1, P t1 :=
fix F (t1:Test1) : P t1 :=
match t1 return P t1 with
| t1list l => rec_fun1 l (map_dep G l)
end with
G (t2:Test2) : Q t2 :=
match t2 return Q t2 with
| t2item t => rec_fun2 t (F t)
end for F.
Definition Test2_rect' (P : Test1 -> Type) (Q : Test2 -> Type)
  (rec_fun1 : forall l:list Test2, ForallT Q l -> P (t1list l))
  (rec_fun2 : forall t:Test1, P t -> Q (t2item t)) :
  forall t2:Test2, Q t2 :=
fix F (t1:Test1) : P t1 :=
match t1 return P t1 with
| t1list l => rec_fun1 l (map_dep G l)
end with
G (t2:Test2) : Q t2 :=
match t2 return Q t2 with
| t2item t => rec_fun2 t (F t)
end for G.
-- 
Daniel Schepler