coq - 如何证明 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:

The ring tactic solves equations upon polynomial expressions of a ring (or semi-ring) structure. It proceeds by normalizing both hand sides of the equation (w.r.t. associativity, commutativity and distributivity, constant propagation) and comparing syntactically the results.

  intros; ring.
  Undo.

omega战术

Coq 引用手册，§8.16.2:

The tactic omega, due to Pierre Crégut, is an automatic decision procedure for Presburger arithmetic. It solves quantifier-free formulas built with ~, \/, /\, -> on top of equalities, inequalities and disequalities on both the type nat of natural numbers and Z of binary integers. This tactic must be loaded by the command Require Import Omega. See the additional documentation about omega (see Chapter 21).

  intros; omega.
  Undo.

lia战术

Coq 引用手册，§22.5:

The tactic lia offers an alternative to the omega and romega tactic (see Chapter 21). Roughly speaking, the deductive power of lia is the combined deductive power of ring_simplify and omega. However, it solves linear goals that omega and romega do not solve, such as the following so-called omega nightmare [130].

  intros; lia.
  Undo.

nia战术

Coq 引用手册，§22.6:

The nia tactic is an experimental proof procedure for non-linear integer arithmetic. The tactic performs a limited amount of non-linear reasoning before running the linear prover of lia...

  intros; nia.
  Undo.

手动证明

以上所有策略自动解决目标。 Undo是一个“取消”一个步骤的白话命令，它允许我们从头开始重新开始证明，在这种情况下可以使用 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.