1

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

4

1 回答 1

2

解决这个问题的一种方法是对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。

但是我们可以通过不将变量过早地引入上下文来使归纳假设更强：

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.
于 2017-05-18T06:18:49.107 回答