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.
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.
你应该看看rewrite
战术(然后也许reflexivity
)。
编辑:有关重写的更多信息:
rewrite H
rewrite -> H
从左到右重写rewrite <- H
从右到左重写您可以使用该pattern
策略仅选择要重写的目标的特定实例。例如,只重写第二个n
,您可以执行以下步骤
模式 n 在 2。重写 <- H。
在您的情况下,解决方案要简单得多。
基于@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).
Coq 中有一个使用模式的强大搜索引擎。您可以尝试例如:
Search (_=_ -> _+_=_+_).