陷入 Coq 中自然数证明的简单不等式

Question

我想用自然数证明不等式的反转：

forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j.

我尝试用归纳法来证明。我首先通过反射简单地证明了

w - i >= w - i

。然后我尝试证明

w - i >= w - S m

前提是

w - i >= w - m

，但我陷入了困境。看来如果我证明了

w - m >= w - S m

，那就完成了。但我也无法解决这个问题。有人可以帮忙吗？非常感谢！

为什么网络上没有简单的可用策略列表及其描述？

Answer 1

我不是这方面的专家，但你可以用一种方法来构造这个证明：

Coq

：

Require Import Arith.

Lemma le_minus : forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j.
Proof.
  intros i j H1 w H2 H3.
  (* Induction on j *)
  induction j as [| m IHm].
  - (* Base Case: j = 0 *)
    assert (i = 0) as Hi0 by lia.
    rewrite Hi0. simpl. auto.
  - (* Inductive Step: j = S m *)
    destruct (Nat.eq_dec i (S m)).
    + (* Case: i = S m *)
      subst. lia.
    + (* Case: i < S m *)
      assert (i <= m) as H4 by lia.
      specialize (IHm H4 w H2).
      apply le_trans with (w - m). 
      * apply IHm. lia.
      * simpl. lia.
Qed.

基本案例

如果

j = 0

，那么根据条件

i ≤ j

，我们有

i = 0

。目标是

w − 0 ≥ w − 0

，这是微不足道的。

归纳步骤

j = S m

• 我们假设假设

  i ≤ m

  （即

  w − i ≥ w − m

  ）成立。
• 现在，我们需要证明

  w − i ≥ w − S m

  。
• 我们对

  i = S m

  还是

  i < S m

  进行案例分析。
• 如果

  i = S m

  ，那么

  w − i ≥ w − j

  是微不足道的，因为

  w − S m ≥ w - S m

  。
• 如果

  i < S m

  ，我们使用归纳假设来降低目标，然后应用基本的算术推理。

战术

• intros

  ：介绍量化变量和假设。

• induction j as [| m IHm]

  ：对 jj 进行归纳。

• destruct (Nat.eq_dec i (S m))

  ：

  i = S m

  还是

  i < S m

  的案例分析。

• assert (i = 0) as Hi0 by lia

  ：使用 lia 策略引入并证明必要的相等性。

• lia

  ：解决线性算术目标的强大策略。

• apply le_trans

  ：使用 ≥≥ 的传递性来组合结果。

网络上一些有用的

Coq

战术资源

• https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tropics-cheatsheet.html
• https://coq.inria.fr/doc/V8.19.2/refman/proof-engine/tropics.html
• https://www.inf.ed.ac.uk/teaching/courses/tspl/cheatsheet.pdf
• https://julesjacobs.com/notes/coq-cheatsheet/coq-cheatsheet.pdf

不幸的是，网络上没有“简单”的

Coq

策略列表，并且确实需要在网上进行大量挖掘。

我希望这有帮助！