减法的 Coq 证明不通勤答案

【问题标题】：Coq proof for subtraction does not commute减法的 Coq 证明不通勤
【发布时间】：2017-05-18 00:13:07
【问题描述】：

我想证明减法不会在 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。

【问题讨论】：

我建议你首先证明 WLOG 的 a < b -> a - b <> b -a 的引理。您将需要使用归纳法。
但是直接证明没有什么特别的困难。

标签： coq coq-tactic

【解决方案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.

【讨论】：

有了omega，你就不再需要induction了。
好的，谢谢！忘记了我们在这种情况下属于 Presburger 算术领域。
非常感谢，效果很好。总的菜鸟问题我如何找到像 Nat.sub_succ 和 Nat.sub_0_r 这样可用的定义和定理列表？
@MikeHarris Require Import Coq.Arith.Arith.，然后分别是 Search (S _ - S _). 或 Search (_ - 0).。除了通配符_，Coq 的搜索还理解Search (?a + ?b = ?b + ?a).——这应该找到Nat.add_comm。请参阅here 了解更多信息。