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.

ところで、この誘導原理は標準ライブラリ ( Listmodule) に存在します:

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 に答える