coq - How to add to both sides of an equality in Coq

Question

This seems like a really simple question, but I wasn't able to find anything useful.

I have the statement

n - x = n

and would like to prove

(n - x) + x = n + x

I haven't been able to find what theorem allows for this.

Answer 1

你应该看看rewrite战术（然后也许reflexivity）。

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

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

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

  模式 n 在 2。重写 <- H。

在您的情况下，解决方案要简单得多。

Answer 2

基于@gallais 关于使用f_equal. 我们从以下状态开始：

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

(1)第一个变体通过“前向”推理（将定理应用于假设）使用f_equal引理。

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.or exact H.or or assumption.or auto.... 或其他最适合您的方式来解决。

(2)或者您可以使用“向后”推理（将定理应用于目标）。还有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).

Answer 3

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

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