Coqの "S"（succ）に "+ 1"（+ 1）を書き換えるにはどうすればよいですか？

Question

私は不完全な証拠で、次の補題があります

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

この証明は、これを証明する方法だろうeq_Sように思える

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

で失敗したが、私は（それを適用することはできませんn + 1をS n：Error: Unable to find an instance for the variable y.と認識しません。私もringを試しましたが、関係を見つけることができません。 rewriteを使用すると、最終目標は同じになります。

この証明はどのようにして完成できますか？

Answer 1

これは、(+)の定義に関連しています。あなたは表記(+)が機能Nat.addに対応して、Print Nat.addを呼び出すと、あなたを与えることを見て、（View > Display notations中だというCoqIDEで）表記をオフにすることで、(+)年代根本的な定義にアクセスすることができます

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

あなたはその(+)を見ることができますn + 1が変数nである最初の引数でマッチングすることによって定義されます。 nはOまたはS（「コンストラクタヘッダー」ではない）で始まらないため、matchは縮小できません。つまり、あなたは、2つのものが同じ普通の形（それはreflexivityが主張しているものです）を計算すると言って、平等を証明することはできません。

代わりに、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 + nではなくn + 1があった場合にのみ、マッチが発火することを意味していることに注意してくださいです。

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)を使用して、私たちが話しすべての定理を見つけることができます誰かがすでにNat.addがそう私達はちょうどそれを使用することができます可換であることを証明した標準ライブラリであるためまあ、我々は幸運ですいくつかの変数?nのパターン?n + 1（ここでは疑問符が重要です）。最初の結果は本当に関連補題です：

Nat.add_1_r: forall n : nat, n + 1 = S n