Coq 简单意味着证明

Question

我正在尝试证明以下自然数的平凡抵消定理：

forall i, j, k in nat . ((i+j) = (i+k)) -> (j = k)

这是我在Coq中写的：

Theorem cancel : forall (i j k : nat),
  ((add i j) = (add i k)) -> (j = k).
Proof.
intros i j k.
induction i.
simpl.

之后 Coq 试图证明归纳法的基础是微不足道的：

j = k -> j = k

几乎所有 Coq 教程都从证明 A -> A 开始，但是当我尝试使用此类证明时，我被卡住了。例如，我正在使用：

Theorem my_first_proof : (forall A : Prop, A -> A).
Proof.
  intros A.
  intros proof_of_A.
  exact proof_of_A.
Qed.

然后当我尝试：

rewrite -> my_first_proof

我收到以下错误：

Error: Cannot find a relation to rewrite.

非常感谢任何帮助，谢谢！

Answer 1

在这种情况下正确的策略是apply。

apply my_first_proof.

rewrite 用于将目标的一个子项替换为另一个，通常带有一个引理，表明这些子项在某种意义上是相等或等价的。 my_first_proof 不是等式证明。

Coq simple implies proof