如何在 Coq 中证明算术等式 `3 * S (i + j) + 1 = S (3 * i + 1) + S (3 * j + 1)`？
How to prove the arithmetic equality `3 * S (i + j) + 1 = S (3 * i + 1) + S (3 * j + 1)` in Coq?
如何证明相等性
3 * S (i + j) + 1 = S (3 * i + 1) + S (3 * j + 1)`
在 Coq 中？
为了在 Coq 中证明我的归纳假设，我需要证明这些边是相等的（它们显然是相等的）。
但是，如果我删除左侧的 S，那么我会得到自然数 3。但是，我不知道如何将其分解为 1 + 1 + 1.
还有，坐着摆弄Nat.add_assoc和Nat.add_comm很费时间，让我抓狂。
初学者一定有一些"straightforward"方法如何使用"basic"策略证明这一点？
您可以使用一种自动算术策略：
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.
并向我的辅助库添加一些互换引理。
我们先做一些自动校样。将它们与我提出的（多）更长的手动证明进行比较。
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 是一个 "un-does" 步骤的白话命令，它允许我们从头开始重新开始证明，在这种情况下使用 Restart 命令可以达到相同的效果。
现在，让我们做一个手工证明。出于教学原因，我没有删除用于查找必要引理的 Search 命令。老实说，我用得不多，也不记得他们的名字了——使用自动战术要容易得多。
主要困难之一（至少对我而言）是 "focus" 我想重写的目标的子表达式。
为此，我们可以使用 replace ... with ... 策略（参见下面的示例）和 symmetry（在某种程度上）。 symmetry 将 a = b 形式的目标转换为 b = a -- 它允许您重写 b 而不是 a.
此外，rewrite !<lemma> 也有很大帮助 - 感叹号表示 "do rewrites as many times as possible"。
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.
如何证明相等性
3 * S (i + j) + 1 = S (3 * i + 1) + S (3 * j + 1)`
在 Coq 中？
为了在 Coq 中证明我的归纳假设，我需要证明这些边是相等的（它们显然是相等的）。
但是，如果我删除左侧的 S，那么我会得到自然数 3。但是，我不知道如何将其分解为 1 + 1 + 1.
还有，坐着摆弄Nat.add_assoc和Nat.add_comm很费时间，让我抓狂。
初学者一定有一些"straightforward"方法如何使用"basic"策略证明这一点？
您可以使用一种自动算术策略：
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.
并向我的辅助库添加一些互换引理。
我们先做一些自动校样。将它们与我提出的（多）更长的手动证明进行比较。
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
ringtactic 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 typenatof natural numbers andZof binary integers. This tactic must be loaded by the commandRequire Import Omega. See the additional documentation aboutomega(see Chapter 21).
intros; omega.
Undo.
lia战术
Coq 参考手册，§22.5:
The tactic
liaoffers an alternative to theomegaandromegatactic (see Chapter 21). Roughly speaking, the deductive power ofliais the combined deductive power ofring_simplifyandomega. However, it solves linear goals thatomegaandromegado not solve, such as the following so-called omega nightmare [130].
intros; lia.
Undo.
nia战术
Coq 参考手册，§22.6:
The
niatactic 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 oflia...
intros; nia.
Undo.
手动证明
以上所有战术自动解决目标。 Undo 是一个 "un-does" 步骤的白话命令，它允许我们从头开始重新开始证明，在这种情况下使用 Restart 命令可以达到相同的效果。
现在，让我们做一个手工证明。出于教学原因，我没有删除用于查找必要引理的 Search 命令。老实说，我用得不多，也不记得他们的名字了——使用自动战术要容易得多。
主要困难之一（至少对我而言）是 "focus" 我想重写的目标的子表达式。
为此，我们可以使用 replace ... with ... 策略（参见下面的示例）和 symmetry（在某种程度上）。 symmetry 将 a = b 形式的目标转换为 b = a -- 它允许您重写 b 而不是 a.
此外，rewrite !<lemma> 也有很大帮助 - 感叹号表示 "do rewrites as many times as possible"。
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.