如何在 Coq 中添加到等式的两边

Question

这似乎是一个非常简单的问题，但我找不到任何有用的东西。

我有声明

n - x = n

并想证明

(n - x) + x = n + x

我一直无法找到什么定理允许这样做。

Answer 1

你应该看看这个rewrite策略（然后也许reflexivity）。

编辑：有关重写的更多信息：

• 你可以rewrite H rewrite -> H从左向右重写
• 您可以rewrite <- H从右向左重写

• 您可以使用该pattern策略仅选择要重写的目标的特定实例。例如，只重写第二个n，您可以执行以下步骤

  2 处的模式 n 重写 <- H.

就您而言，解决方案要简单得多。