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

Я публикую решение в виде отдельного ответа, надеясь, что другие пользователи могут извлечь из него пользу. Вот оно:

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.

Answer 2

Проблема не в том, что 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.
  (* ...  *)