7

証明が不完全な次のレンマがあります。

Lemma (s_is_plus_one : forall n:nat, S n = n + 1).
Proof.
  intros.
  reflexivity.
Qed.

この証明は失敗します

Unable to unify "n + 1" with "S n".

これeq_Sを証明する方法のようですが、適用できません（:n + 1として認識されません）。も試しましたが、関係が見つかりません。を使用すると、同じ最終目標になります。S nError: Unable to find an instance for the variable y.ringrewrite

どうすればこの証明を完成させることができますか?

4

1 に答える 1

13

これは、(+)定義方法に関連しています。(+)表記をオフにすることで ( にある CoqIDE でView > Display notations)の基になる定義にアクセスできます。表記(+)が関数に対応していることを確認してから、 which をNat.add呼び出すと、次の結果Print Nat.addが得られます。

Nat.add = 
fix add (n m : nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => S (add p m)
  end

変数(+)である最初の引数で一致することによって定義されていることがわかります。orで始まらないため(「コンストラクター ヘッド」ではない)、 は還元できません。つまり、2 つのものが同じ正規形に計算されると言うだけでは、等しいことを証明することはできません (これが主張されていることです)。n + 1nnOSmatchreflexivity

n代わりに、coq に、どのような場合でも等式が成り立つ理由を説明する必要があります。のような再帰関数の場合の古典的な動きは、Nat.addによる証明を進めることinductionです。そして、それは実際にここで仕事をします:

Lemma s_is_plus_one : forall n:nat, S n = n + 1.
Proof.
intros. induction n.
 - reflexivity.
 - simpl. rewrite <- IHn. reflexivity.
Qed.

1あなたができるもう1つのことは、一方、コンストラクターが先頭にあることに注意することです。つまり1 + n、n + 1. 運が良かったのは、標準ライブラリで誰かNat.addが可換であることをすでに証明しているので、それをそのまま使用できるからです。

Lemma s_is_plus_one : forall n:nat, S n = n + 1.
Proof.
intros.
rewrite (Nat.add_comm n 1).
reflexivity.
Qed.

最後の選択肢: を使用すると、ある変数SearchAbout (?n + 1)のパターンについて話しているすべての定理を見つけることができます(ここでは疑問符が重要です)。最初の結果は、本当に関連のある補題です。?n + 1?n

Nat.add_1_r: forall n : nat, n + 1 = S n
于 2016-10-28T23:02:18.650 に答える