为什么我不能在这里执行重写策略？

Question

我已经有了定理

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

我想证明它的“逆形式”。所以我有

Theorem plus_n_n_injective : forall n m,
     n + n = m + m ->
     n = m.
Proof.
  intros n. induction n as [| n' IHn'].
  - intros [] eq. reflexivity. discriminate.
  - intros m eq.

然后目标是

1 goal
n' : nat
IHn' : forall m : nat, n' + n' = m + m -> n' = m
m : nat
eq : S n' + S n' = m + m
______________________________________(1/1)
S n' = m

所以在我看来，我想将目标改写为

S n' + S n' = m + m

plus_id_example

。但是，它失败了

rewrite <- plus_id_example

我不知道为什么。

也许是因为我们只能像

a = b

那样重写。但是，将其替换为

apply plus_id_example

不起作用。而且我不知道如何

apply ... with ...

进行多次替换。

唯一的方法就是

    pose proof plus_id_example as pp.
    specialize pp with (n := S n').
    specialize pp with (m := m).

我的问题是有什么方法可以通过 apply with 或 rewrite 来做到这一点吗？

同时，我想重写目标以匹配

eq

，有办法吗？

Answer 1

当您发送命令时

rewrite <- plus_id_example.

系统分析

plus_id_example

的陈述并检测其结论是否是等式（是），然后计算该等式右侧的模式，这里这个模式是：

(x + x)

其中

x

可以替换为任何值（因为

m

中的

plus_id_example

是通用量化的。

然后它在目标的结论中查找此模式的实例。

目标的结论是

S n' = m

因此，没有地方可以应用此重写，并且该命令失败。这就是为什么你无法执行这个精确的重写命令的原因。

不管怎样，定理

plus_id_example

其实对于证明定理

plus_n_n_injective

没有什么用处，你应该想想另外的证明方案。