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

ので、同様に1は、その後、1は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