如何在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？

试图在Coq中证明我的归纳假设,我需要证明这些方面是平等的(他们显然是这样).

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

此外,坐在与fidling 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策略在环(或半环)结构的多项式表达式上求解方程.它通过对等式的两个手边进行归一化(相关性,交换性和分布性,恒定传播)并在语法上比较结果.

  intros; ring.
  Undo.

该omega策略

Coq参考手册,§8.16.2:

omega由皮埃尔·克雷古特(PierreCrégut)提出的策略是普锐伯算术的自动决策程序.它解决了内置免费量词公式~,\/,/\,->对双方的类型平等,不平等和disequalities顶部nat自然数的和Z二进制整数.这个策略必须由命令加载Require Import Omega.请参阅其他文档omega(参见第21章).

  intros; omega.
  Undo.

该lia策略

Coq参考手册,§22.5:

这个策略lia提供给替代omega和romega策略(参见第21章).粗略地说,的演绎力量lia是联合演绎的功率ring_simplify和omega.然而,它解决了线性目标,omega而romega不是解决,例如下面所谓的欧米茄噩梦[130].

  intros; lia.
  Undo.

该nia策略

Coq参考手册,§22.6:

该nia策略是非线性整数算法的实验证明程序.在运行...的线性证明器之前,该策略执行有限量的非线性推理lia.

  intros; nia.
  Undo.

手动证明

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