如何在更复杂的目标中简化基本算术

Question

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

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。作为 hack，我在个别事件上使用 'replace' 但这感觉非常笨拙（并且有很多不同的算术表达式可以替换）。有没有更好的方法来做到这一点？

我正在使用 ssrnat 库。

谢谢。

Answer 1

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) returns，除此之外，addn1.

Answer 2

Coq 对这种工作有 ring 和 ring_simplify 策略。抱歉我的 ssreflect 无知 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。对于不等式，有 lia 和 lra，但我不确定这些是否适用于 mathcomp - 对于 lia 你可能需要这个 (https://github.com/math-comp/mczify) 但它可能同时被整合.

如何在更复杂的目标中简化基本算术

how to simplify basic arithmetic in more complex goals

coq

ssreflect