1

这是我的问题的一个最小示例

Lemma arith: forall T (G: seq T), (size G + 1 + 1).+1 = (size G + 3).

我希望能够将其减少到 forall T (G: seq T), (size G + 2).+1 = (size G + 3).

用最简单的方法。立即尝试 simpl 或 auto 无济于事。

如果我先用关联性重写，也就是说，

intros. rewrite - addnA. simpl. auto.,

simpl 和 auto 仍然什么都不做。我的目标是

(size G + (1 + 1)).+1 = size G + 3

我猜 .+1 以某种方式在 (1+1) 上进行简单和自动工作的“方式”。看来我必须先删除 .+1 才能简化 1+1。

然而，在我的实际证明中，除了 .+1 之外，还有很多东西“挡道”，我真的很想先简化我大量的 +1。作为一个黑客，我在个别事件上使用“替换”，但这感觉非常笨拙（并且有很多不同的算术表达式要替换）。有没有更好的方法来做到这一点？

我正在使用 ssrnat 库。

谢谢。

4

2 回答 2

2

ssrnat关于加法的推理有很多引理。您的问题的一种可能解决方案如下：

From mathcomp Require Import all_ssreflect.

Lemma arith: forall T (G: seq T), (size G + 1 + 1).+1 = (size G + 3).
Proof. by move=> T G; rewrite !addn1 addn3. Qed.

在哪里

addn1 : forall n, n + 1 = n.+1
addn3 : forall n, n + 3 = n.+3 (* := n.+1.+1.+1 *)

您可以使用该Search命令查找与某些术语模式相关的引理。例如，Search (_ + 1)返回，除其他外，addn1.

于 2021-05-24T02:58:24.927 回答
2

Coq对这类工作有一套策略ring。ring_simplify对不起我的 ssreflect ignorant intros，但这有效：

From mathcomp Require Import all_ssreflect.

Lemma arith: forall T (G: seq T), (size G + 1 + 1).+1 = (size G + 3).
Proof.
  intros.
  ring.
Qed.

还有一个field和field_simplify。对于不等式，有liaand lra，但我不确定这些是否适用于 mathcomp - 因为lia你可能需要这个（https://github.com/math-comp/mczify）但它可能同时被集成。

于 2021-05-25T07:56:08.187 回答