I noticed that I keep redefining very similar induction principles for nested (and sometime mutually) inductive types because the one generated automatically by Coq is too weak. Here is a very simplified example:
Require Import Coq.Lists.List.
Inductive T : Set :=
| C1 : T
| C2 : list T -> T.
Section T_nested_ind.
Variable P : T -> Prop.
Hypothesis C1_case : P C1.
Hypothesis C2_case : forall l : list T, Forall P l -> P (C2 l).
Fixpoint T_nested_ind (t : T) :=
match t with
| C1 => C1_case
| C2 xs =>
let H := (fix fold (xs : list T) : Forall P xs :=
match xs with
| nil => Forall_nil _
| x :: xs => Forall_cons _ (T_nested_ind x) (fold xs)
end) xs in
C2_case xs H
end.
End T_nested_ind.
Coq generates automatically T_ind
:
forall P : T -> Prop,
P C1 ->
(forall l : list T, P (C2 l)) ->
forall t : T, P t
While I need an induction hypothesis for the elements nested in the list T_nested_ind
:
forall P : T -> Prop,
P C1 ->
(forall l : list T, Forall P l -> P (C2 l)) ->
forall t : T, P t
Here's a partial answer:
fix
as you already know.