gpt4 book ai didi

coq - 如何证明 Coq 中的算术等式 `3 * S (i + j) + 1 = S (3 * i + 1) + S (3 * j + 1)`?

转载 作者:行者123 更新时间:2023-12-01 07:52:56 25 4
gpt4 key购买 nike

如何证明相等

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

在科克?

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

但是,如果我删除 S例如,在左侧,我得到自然数 3 .但是,我不知道如何将其分解为 1 + 1 + 1 .

还有,坐着摆弄 Nat.add_assocNat.add_comm非常耗时,让我发疯。

初学者必须有一些“直截了当”的方式如何使用“基本”策略来证明这一点?

最佳答案

我们先做一些自动证明。将它们与我想出的(长得多)手动证明进行比较。

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.

关于coq - 如何证明 Coq 中的算术等式 `3 * S (i + j) + 1 = S (3 * i + 1) + S (3 * j + 1)`?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/40695030/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com