如何在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 无法自动展开中间定义是否应该被视为错误，但至少有一个解决方法。

Answer 2

如果想保留中间定义，则可以使用该Section机制，如下所示：

Require Import Coq.Lists.List. Import ListNotations.

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

Section custom_induction_principle.    
  Variable X : Type.
  Variable P : list X -> Prop.

  Hypothesis true_for_nil : P nil.
  Hypothesis true_for_list : forall xs, P xs.
  Hypothesis preserved_by_rcons : forall xs' x, P xs' -> P (rcons xs' x).

  Fixpoint list_ind_rcons (xs : list X) : P xs. Admitted.
End custom_induction_principle.

Coq 替换定义并list_ind_rcons具有所需的类型并induction ... using ...工作：

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.
Abort.

顺便说一下，这个归纳原理存在于标准库（List模块）中：

Coq < Check rev_ind.
rev_ind
     : forall (A : Type) (P : list A -> Prop),
       P [] ->
       (forall (x : A) (l : list A), P l -> P (l ++ [x])) ->
       forall l : list A, P l