減算のCoq証明書が通らない

Question

減算がCoqで通勤していないことを証明したいと思いますが、私は立ち往生しています。私は、Coqで証明したい声明が書かれていると信じています。forall a b : nat, a <> b -> a - b <> b - a

これまで私が証明しているものがあります。

Theorem subtraction_does_not_commute : 
    forall a b : nat, a <> b -> a - b <> b - a. 
Proof. 
    intros a b C. 
    unfold not; intro H. 
    apply C. 

私は目標a = bと矛盾するC : a <> bを使用できると思います。

Answer 1

これを解決する1つの方法は、aで誘導を使用することです。

C : S a <> b 
IHa : a <> b -> a - b <> b - a 

あなたは1ができませんので、帰納法の仮定IHaを使用することはできません：あなたは

intros a b C; induction a. 

であなたの証明を起動した場合ただし、コンテキストは、以下の仮説を持っていますので、はまりますIHa（a <> b）の前提をS a <> bから推測します。 1 <> 0は0 <> 0を意味しません。

しかし、私たちは途中でコンテキストに変数を導入しないことにより、帰納法の仮定を強くすることができます。

Require Import Coq.Arith.Arith. 

Lemma subtraction_does_not_commute : 
    forall a b : nat, a <> b -> a - b <> b - a. 
Proof. 
    induction a; intros b C. 
    - now rewrite Nat.sub_0_r. 
    - destruct b. 
    + trivial. 
    + repeat rewrite Nat.sub_succ. auto. 
Qed. 

または、代わりに、omega戦術を使用して、我々は、1行の証拠を得る：

Require Import Omega. 

Lemma subtraction_does_not_commute : 
    forall a b : nat, a <> b -> a - b <> b - a. 
Proof. intros; omega. Qed.