coq - 複数の引数を指定して、coq でネイティブ帰納法を適用する

Question

「Software Foundation」という本を読んでいます。「誘導の詳細」の章で、著者は、誘導型が定義されているときに coq によって生成される誘導原理について話します。

演習は次のとおりです。「+」の関連付けの概念を定義にカプセル化し、それに nat_ind を適用します。

定義の最初の推測は次のとおりです。

Definition P_plusassoc (n m o:nat) : Prop :=
  n + (m+ o) = (n+m) +o.

しかし、これを証明したいときに問題があります。

Theorem plus_assoct : forall o m n, P_plusassoc n m o.
Proof.
  apply nat_ind.

nat_ind動作しません。だから私はそれがP_plusassoc1つだけの整数ではなく3つに依存しているからだと思った。

だから私はこのように書き直しP_plusassocます：

Definition P_plusassoc (n:nat) : nat->nat->Prop :=
      fun (m o:nat) => n + (m+ o) = (n+m) +o.

しかし、それでもうまくいきません。問題はどこだ？P_plusassocを使用するように定義するにはどうすればよいnat_indですか?

score 1 · Accepted Answer

本は後で答えを出します。定義は次のようになります。

Definition P_plusassoc (n:nat) : Prop :=
      forall m o, n + (m+ o) = (n+m) +o.

score 0 · Accepted Answer

問題は補題を証明することです。ただし、関数を定義しています。あなたがすべきことは、タイプ Prop (のようなものDefinition P_plusassoc (n:nat) : Prop := forall m o, n + (m+ o) = (n+m) +o.) を定義することです。

個人的には、Lemma : forall m n o :nat, n+(m+o)=(n+m)+o.Coq を定義すると、この補題を証明できるようになります。intros. apply (nat_ind n).

2 に答える 2