Coq 应用策略失败

Question

我正在尝试证明以下关于自然数的简单定理：

((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.
apply A_IMPLIES_A.
simpl.

然后我有了子目标：

S (add i j) = S (add i k) -> j = k

所以我想我会申请 eq_add_S，其中说明 S m = S n -> m = n。但是，当我尝试使用 apply eq_add_S 这样做时，出现以下错误：

Error:
In environment
i, j, k : nat
IHi : add i j = add i k -> j = k
Unable to unify "k" with "add i k".

所以我猜它无法理解我想要的是m = (add i j)和n = (add i k)。为什么 Coq 看不懂我的想法？或者更严重的是，我怎样才能帮助他这样做？谢谢！

Answer 1

问题不在于 Coq 无法猜测 m 和 n 使用什么值，而是您的目标没有正确的形状来实例化该定理。当你写 apply eq_add_S 时，Coq 试图统一 S n = S m -> n = m 和 S (add i j) = S (add i k) -> j = k，这是做不到的。

您需要将 eq_add_S 应用到目标的前提，方法是将其引入上下文。

Proof.
intros i j k H. (* H : add i j = add i k *)
induction i as [|i IH].
- apply H.
- apply eq_add_S in H.
  (* ...  *)

Answer 2

我将解决方案作为单独的答案发布，希望其他用户可以从中受益。这是：

Theorem cancel : forall (i j k : nat),
  ((add i j) = (add i k)) -> (j = k).
Proof.
intros i j k H.
induction i.
apply H.
simpl in H.
apply eq_add_S in H.
apply IHi in H.
assumption.
Qed.

Coq 应用策略失败

Coq fails an apply tactic

apply

coq

coq-tactic