如何添加到 Coq 中相等的两边

Question

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

我有声明

n - x = n

并想证明

(n - x) + x = n + x

我没能找到什么定理允许这样做。

Answer 1

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

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

对于您的情况，解决方案要简单得多。

Answer 2

Coq 中有一个使用模式的强大搜索引擎。您可以尝试例如：

Search (_=_ -> _+_=_+_).

Answer 3

基于@gallais 关于使用 f_equal 的建议。我们从以下状态开始：

n : nat
x : nat
H : n - x = n
============================
 n - x + x = n + x

(1) 使用 f_equal 引理通过 "forward" 推理（将定理应用于假设）的第一个变体。

Check f_equal.
f_equal
 : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y

需要函数f，所以

apply f_equal with (f := fun t => t + x) in H.

这会给你：

H : n - x + x = n + x

这可以通过 apply H. 或 exact H. 或 assumption. 或 auto. 或其他最适合您的方式来解决。

(2) 或者您可以使用 "backward" 推理（将定理应用于目标）。还有 f_equal2 引理：

Check f_equal2.
f_equal2
 : forall (A1 A2 B : Type) (f : A1 -> A2 -> B) 
     (x1 y1 : A1) (x2 y2 : A2),
   x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2

我们只是将其应用于目标，这会产生两个微不足道的子目标。

apply f_equal2. assumption. reflexivity.

或者只是

apply f_equal2; trivial.

(3) 还有更专业的引理 f_equal2_plus:

Check f_equal2_plus.
(*
f_equal2_plus
  : forall x1 y1 x2 y2 : nat,
    x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
*)

使用这个引理，我们可以通过以下一行解决目标：

apply (f_equal2_plus _ _ _ _ H eq_refl).

How to add to both sides of an equality in Coq