嵌套归纳类型的归纳原理

Question

我注意到我一直在为嵌套（有时是相互的）归纳类型重新定义非常相似的归纳原则，因为 Coq 自动生成的归纳原则太弱了。这是一个非常简单的例子：

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 自动生成 T_ind:

forall P : T -> Prop,
  P C1 ->
  (forall l : list T, P (C2 l)) ->
  forall t : T, P t

虽然我需要对列表中嵌套的元素进行归纳假设T_nested_ind:

forall P : T -> Prop,
  P C1 ->
  (forall l : list T, Forall P l -> P (C2 l)) ->
  forall t : T, P t

有没有办法自动执行此操作？
我是不是做错了什么，需要这样的归纳原理吗？
Coq 中的标准解是什么？
是否有关于该主题的一些孵化研究？

Answer 1

这是部分答案：

不，Coq 给了你一个归纳原理，它是正确的但不是很有用，你可以巧妙地使用你已经知道的 fix 来做得更好。
据我所知，定义并证明一个新的归纳原理是标准解决方案。

嵌套归纳类型的归纳原理

Induction principle for nested inductive types

coq

induction