Coq Beweis für Subtraktion pendelt nicht

Question

Ich möchte beweisen, dass die Subtraktion nicht in Coq pendeln, aber ich bin fest. Ich glaube, dass die Aussage, die ich in Coq beweisen möchte, geschrieben würde forall a b : nat, a <> b -> a - b <> b - a

Hier ist, was ich für den Beweis so weit habe.

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. 

Ich glaube, ich C : a <> b verwenden könnte a = b das Ziel, zu widersprechen.

Answer 1

Eine Möglichkeit, dies zu lösen, ist die Verwendung von Induktion auf a. Wenn Sie jedoch Ihr Nachweis mit

intros a b C; induction a. 

beginnen Sie nicht weiterkommen, weil der Kontext folgende Hypothesen haben:

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

Sie werden nicht in der Lage sein, die Induktionsvoraussetzung verwenden IHa weil man nicht folgern die Prämisse von IHa (a <> b) von S a <> b: eg 1 <> 0 bedeutet nicht 0 <> 0.

Aber wir können die Induktionsvoraussetzung stärker machen, indem nicht die Variablen in den Kontext vorzeitig Einführung:

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. 

Oder alternativ mit der omega Taktik, bekommen wir einen einzeiligen Beweis:

Require Import Omega. 

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