减法的 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.

我想我可以使用 C : a <> b 与目标 a = b 相矛盾。

Answer 1

解决这个问题的一种方法是在 a 上使用归纳法。但是，如果您以

开始证明

intros a b C; induction a.

你会卡住，因为上下文会有以下假设：

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

您将无法使用归纳假设 IHa，因为无法从 S a <> b 推断出 IHa (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 策略，我们得到一个单行证明：

Require Import Omega.

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

减法的 Coq 证明不通勤

Coq proof for subtraction does not commute

coq

coq-tactic