如何在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. 

我不知道勒柯克不能夠自動展開中間定義應被認爲是錯誤或沒有，但至少有一種變通方法。

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. 

勒柯克替代的定義和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