如何证明Coq中的算术等式‘3*S (i + j) +1=S (3 *i+ 1) +S (3 *j+1)？

Question

如何证明平等

3 * S (i + j) + 1 = S (3 * i + 1) + S (3 * j + 1)`

在科克？

为了证明我在Coq中的归纳假设，我需要证明这些边是相等的(显然它们是相等的)。

但是，如果我在左边删除S，那么我就得到了自然数3。但是，我不知道如何将其分解为1 + 1 + 1。

此外，坐在和烦扰Nat.add_assoc和Nat.add_comm是非常耗时的，并使我疯狂。

对于初学者来说一定有一些“直截了当”的方法，如何用“基本”策略来证明这一点呢？

Answer 1

让我们先做一些自动证明。将它们与我想出的(更长的)人工证据进行比较。

Require Import
Arith      (* `ring` tactic on `nat` and lemmas *)
Omega      (* `omega` tactic *)
Psatz.     (* `lia`, `nia` tactics *)

Goal forall i j,
    3 * S (i + j) + 1 = S (3 * i + 1) + S (3 * j + 1).
Proof.

ring策略

Coq参考手册，§8.16.3：

ring策略利用环 (或半环)结构的多项式表达式求解方程。它通过正规化方程的两边(w.r.t )来进行。结合性、交换性和分布性、常量传播)，并对所得结果进行了句法比较。

  intros; ring.
  Undo.

omega策略

Coq参考手册，§8.16.2：

由于皮埃尔·克雷格特的战术omega是普雷布格算法的一种自动决策程序。它解决了用~，\/，/\，->建立在等式之上的无量词公式，解决了自然数的nat型和二进制整数的Z型上的不等式和不等式。此策略必须由命令Require Import Omega加载。请参阅有关omega的其他文档(请参阅第21章)。

  intros; omega.
  Undo.

lia策略

Coq参考手册，第22.5条：

策略lia提供了omega和romega策略的替代方案(见第21章)。粗略地说，lia的演绎能力是ring_simplify和omega的综合演绎能力。然而，它解决了omega和romega没有解决的线性目标，比如下面所谓的omega噩梦130。

  intros; lia.
  Undo.

nia策略

Coq参考手册，第22.6条：

nia策略是非线性整数算法的一个实验证明过程.该策略在运行lia的线性证明器之前，执行了有限的非线性推理.

  intros; nia.
  Undo.

人工证明

以上所有战术都自动解决了进球问题。Undo是一个普通的命令，“un- to”是一个步骤，它允许我们从一开始就重新启动验证，在这种情况下，使用Restart命令可以实现同样的效果。

现在，让我们做一个手动的证明。出于说教的原因，我没有删除用于查找必要引理的Search命令。坦白地说，我不经常使用它们，也不记得它们的名字--使用自动战术要容易得多。

主要的困难之一(至少对我来说)是“专注于”我想要重写的目标的子表达式。为此，我们可以使用replace ... with ...策略(见下面的示例)和symmetry (在某种程度上)。symmetry将表单a = b的目标转换为b = a --它允许您用b而不是a重写。

另外，rewrite !<lemma>也有很大的帮助--感叹号意味着“尽可能多地重写”。

  intros.
  Search (S (?n + ?m) = ?n + S ?m).
  rewrite !plus_n_Sm.
  rewrite <- Nat.add_assoc.
  Search (?n + (?m + ?p) = ?m + (?n + ?p)).
  rewrite Nat.add_shuffle3.
  symmetry.
  rewrite Nat.add_comm.
  rewrite Nat.add_assoc.
  Search (?k * ?x + ?k * ?y).
  rewrite <- Nat.mul_add_distr_l.
  replace (S j) with (j + 1) by now rewrite Nat.add_comm.
  rewrite Nat.add_assoc.
  symmetry.
  rewrite Nat.mul_add_distr_l.
  rewrite <- !Nat.add_assoc.
  reflexivity.
Qed.

上述手册证明可压缩成以下同等表格：

  intros.
  rewrite !plus_n_Sm, <- Nat.add_assoc, Nat.add_shuffle3.
  symmetry.
  rewrite Nat.add_comm, Nat.add_assoc, <- Nat.mul_add_distr_l.
  replace (S j) with (j + 1) by now rewrite Nat.add_comm.
  rewrite Nat.add_assoc. symmetry.
  now rewrite Nat.mul_add_distr_l, <- !Nat.add_assoc.

Answer 2

您可以使用自动策略之一的算术：

Require Import Coq.omega.Omega.

Lemma U i j : 3 * S (i + j) + 1 = S (3 * i + 1) + S (3 * j + 1).
now omega.
Qed.

事实上，这些证据中有一些是非常耗时的，请参阅Coq手册中关于现有战术的更多细节。如果您想手动进行验证，我将按以下方式进行：

simpl; rewrite !add_0_r, !add_1_r, !add_succ_r, !add_assoc; simpl.

在我的辅助库中加上几个交换引理。