8

我读到类型的归纳原理只是关于命题的定理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什么？

谢谢

4

2 回答 2

5

你所做的大部分是正确的。问题是 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 不能自动展开中间定义是否应该被认为是一个错误，但至少有一个解决方法。

于 2015-10-12T02:25:24.937 回答
5

如果想保留中间定义，则可以使用该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
于 2016-10-28T21:31:53.227 回答