6

Coq について学ぶために、オンライン ブックの「Software Foundations」を使用しています。

第 2 章では、「plus_assoc」定理を証明するよう求められます。

Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.

以前に証明された 2 つの定理を使用します。

Theorem plus_comm : forall n m : nat, n + m = m + n.
Theorem plus_n_Sm : forall n m : nat, S (n + m) = n + (S m).

n の帰納法を使用して plus_assoc 定理を証明します。

Proof.
  intros n m p.
  induction n as [ | n' ].
    reflexivity.

    rewrite plus_comm.
    rewrite <- plus_n_Sm.
    rewrite plus_comm.
    rewrite IHn'.
    symmetry.
    rewrite plus_comm.

この時点で、コンテキスト (*) は次のとおりです。

1 subgoals
case := "n = S n'" : String.string
n' : nat
m : nat
p : nat
IHn' : n' + (m + p) = n' + m + p
______________________________________(1/1)
p + (S n' + m) = S (n' + m + p)

plus_comm を使用して取得したい

p + (m + S n') = S (n' + m + p)

次に plus_n_sm

p + S (m + n') = S (n' + m + p)

そして再び plus_n_sm

S (p + (m + n')) = S (n' + m + p)

plus_comm を 2 回使用して証明を終了し、次に reflexivity を使用します。

S (p + (n' + m)) = S (n' + m + p)
S (n' + m + p) = S (n' + m + p)

ちょっとした質問は、plus_comm を (S n' + m) に適用する方法がわからないということです。

問題は、なぜ発行するのかということです。

apply plus_comm.

即座に証明を終了します (与えられた文脈 (*) において) ?

明確にしていただきありがとうございます。

ファビアン・パイケ

4

1 に答える 1

6

(S n') と m でインスタンス化することにより、plus_comm を (S n' + m) に適用できます。

    Check plus_comm.
    Check plus_comm (S n').
    Check plus_comm (S n') m.
    rewrite (plus_comm (S n') m).
    rewrite <- plus_n_Sm.
    rewrite <- plus_n_Sm.
    rewrite (plus_comm m n').
    rewrite plus_comm.
    reflexivity.
Qed.

Require Import Coq.Setoids.Setoid.使用してから使用しても同じ効果があると思いますrewrite plus_comm at 2.が、機能しません。

apply plus_comm目標を達成する理由は、applyユニファイド モジュロ変換を実行するためです。つまり、p + (S n' + m) = S (n' + m + p)は に変換可能 p + (S n' + m) = S n' + m + pであり、p + (S n' + m) = S n' + m + pで単一化 可能?1 + ?2 = ?2 + ?1です。

実際、simplタクティックを使用してリダクションを実行すると、証明が短くなります。

Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.
Proof.
induction n.
  reflexivity.

  intros.
  simpl.
  apply f_equal.
  apply IHn.
Qed.
于 2014-03-24T14:21:32.177 に答える