뺄셈에 대한 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

이 문제를 해결하는 한 가지 방법은 a에서 유도를 사용하는 것입니다. 당신이

intros a b C; induction a. 

으로 증거를 시작하면 상황은 다음과 같은 가설 것입니다 때문에, 문제가 발생할 것입니다 :

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

당신은 유도 가설 IHa을 사용할 수 없습니다를 한 것이기 때문에 수 없어 IHa (a <> b)의 전제를 S a <> b에서 추론합니다. 예 : 1 <> 0은 0 <> 0을 의미하지 않습니다.

그러나 우리는 너무 빨리 상황에 변수를 도입하지 않음으로써 유도 가설을 강하게 만들 수 있습니다

또는 다른 방법으로, omega 전술을 사용하여, 우리는 증거 한 줄 수

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. 

:

Require Import Omega. 

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

을