coq - Coq証明戦術

Question

私はCoq証明システムの初心者です（約4日）。一生懸命やってみたのですが、以下のことを証明できませんでした。

forall a b c : nat, S (S (a + b)) = S (S (a + c)) -> b = c.

私の知る限り、+ の全単射性を証明する必要があるので、どうにかして を使用できますf(b) = f(c) -> b = c。これを行うにはどうすればよいですか?

Answer 1

Vinz の回答で指摘されているplusように、Coq 標準ライブラリで直接全単射性定理を見つけることができます。次のように、原始戦術と数学的帰納法を使用して直接証明することもできaます。

Theorem plus_l_bij: forall a b c : nat, a + b = a + c -> b = c.
Proof.
induction a as [|a'].
  intros b c H. apply H.
  intros b c H. simpl plus in H. inversion H. apply IHa' in H1. apply H1.
Qed.

の後induction a、基本ケースa = 0は自明です。

2 番目のケース の証明をa = S a'整理すると、

S a' + b = S a' + c 

に

S (a' + b) = S (a' + c)

S次に、その全単射性を使用してコンストラクターを削除します。最後に、帰納仮説を適用して証明を完成させることができます。