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_SCoq пытается объединиться 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.