So far I never had to state mutually recursive properties on both lang_ty and list lang_ty, so this induction principle was enough.

I am now facing a situation where I want to mutually prove something on them. Something like (∀ ty : lang_ty, P ty) /\ (∀ tys: list lang_ty, Q tys). With a mutual inductive family, I could use Lemma .. with to state this, but I don’t know how to do this for a nested inductive (or if that’s even possible).

Should I go back and change to a mutual inductive in the first place, or is there a way to state a mutual lemma when using nested inductive types ?

How do you expect to prove ∀ tys: list lang_ty, Q tys? If you can prove ∀ tys: list lang_ty, Forall P tys -> Q tys, then the following might suit you:

Variable P : lang_ty -> Prop.
Variable Q : list lang_ty -> Prop.
...
Hypothesis case_ClassT : forall cname targs, Q targs -> P (ClassT cname targs).
Hypothesis case_List : forall targs, Forall P targs -> Q targs.
...
Definition _lang_ty_list_ind (lang_ty_ind : forall t : lang_ty, P t) (l : list lang_ty) : Q l :=
let H := (fix fold (xs : list lang_ty) : Forall P xs :=
match xs with
| nil => List.Forall_nil _
| x :: xs => List.Forall_cons x (lang_ty_ind x) (fold xs)
end) l in
case_List _ H.
Fixpoint lang_ty_ind (t : lang_ty) : P t :=
match t with
...
| ClassT cname targs => case_ClassT cname targs (_lang_ty_list_ind lang_ty_ind targs)
...
end.
Definition lang_ty_list_ind : forall tys : list_lang_ty, Q tys := _lang_ty_list_ind (lang_ty_ind).

I’ll admit it’s probably not the nicest presentation, but it works.
This is the kind of induction principle we use for typing in MetaCoq (with a specific case going from a Forall over a list to the predicate we’re interested in), and it seems to work quite well there. The main difference is that we do not prove the induction principle directly by induction on the structure, but via an auxiliary definition of size.

Thank you for these suggestions, they are very interesting !
FYI I managed to get around this mutual induction by splitting the problem into smaller bits, that were no longer mutual.

Still I found all this feedback very valuable, thank you

My understanding is that Fixpoint…with is like Lemma…with and will only work with mutual inductive definitions, not nested ones. Am I missing something ?

For a nested, non-mutual inductive type, a single Fixpoint lemma can do the trick:

Section nested_ind.
Inductive tree :=
| Leaf : nat -> tree
| Single : tree -> tree
| Node : list tree -> tree.
Variable P : tree -> Prop.
Variable Q : list tree -> Prop.
Variable LeafCase : forall n, P (Leaf n).
Variable SingleCase : forall t, P t -> P (Single t).
Variable NodeCase : forall l, Q l -> P (Node l).
Variable NilCase : Q nil.
Variable ConsCase : forall t l, P t -> Q l -> Q (cons t l).
Definition ind_list (l : list tree) (IHt : forall t, P t) : Q l.
Proof.
induction l.
- apply NilCase.
- apply ConsCase.
+ apply IHt.
+ apply IHl.
Defined.
Fixpoint ind (t : tree) {struct t} : P t.
Proof.
destruct t.
- apply LeafCase.
- apply SingleCase.
apply ind.
- apply NodeCase.
apply ind_list.
apply ind.
Qed.
End nested_ind.