coq - 如何在 Coq 中使用自定义归纳原理？

Question

我读到类型的归纳原理只是关于命题的定理 P .所以我为List构造了一个归纳原理基于正确(或反向)列表构造函数。

Definition rcons {X:Type} (l:list X) (x:X) : list X := 
  l ++ x::nil.

归纳原理本身是:

Definition true_for_nil {X:Type}(P:list X -> Prop) : Prop :=
  P nil.

Definition true_for_list {X:Type} (P:list X -> Prop) : Prop :=
  forall xs, P xs.

Definition preserved_by_rcons {X:Type} (P: list X -> Prop): Prop :=
  forall xs' x, P xs' -> P (rcons xs' x).

Theorem list_ind_rcons: 
  forall {X:Type} (P:list X -> Prop),
    true_for_nil P ->
    preserved_by_rcons P ->
    true_for_list P.
Proof. Admitted.

但是现在，我在使用该定理时遇到了麻烦。我不知道如何调用它来实现与 induction 相同的效果战术。

例如，我试过:

Theorem rev_app_dist: forall {X} (l1 l2:list X), rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof. intros X l1 l2. 
  induction l2 using list_ind_rcons.

但在最后一行，我得到:

Error: Cannot recognize an induction scheme.

定义和应用自定义归纳原理(如 list_ind_rcons)的正确步骤是什么？ ?

谢谢

Answer 1

你所做的大部分是正确的。问题是 Coq 在识别你写的是归纳原理时遇到了一些麻烦，因为中间定义。例如，这工作得很好:

Theorem list_ind_rcons:
  forall {X:Type} (P:list X -> Prop),
    P nil ->
    (forall x l, P l -> P (rcons l x)) ->
    forall l, P l.
Proof. Admitted.

Theorem rev_app_dist: forall {X} (l1 l2:list X), rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof. intros X l1 l2.
  induction l2 using @list_ind_rcons.

我不知道 Coq 无法自动展开中间定义是否应该被视为错误，但至少有一个解决方法。