CODEWITHSUNDEEP
applycoqcoq-tactic
OrenIshShalom
OrenIshShalom

Reputation: 7102

Coq fails an apply tactic

I am trying to prove the following simple theorem over natural numbers:

((i + j) = (i + k)) -> (j = k)

Here is what I have in 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.

And after that I have the sub-goal:

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

So I thought I'd apply eq_add_S which states that S m = S n -> m = n. However, when I try to do so with apply eq_add_S I get the following error:

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

So I guess it can't understand that I want is m = (add i j) and n = (add i k). How come Coq can't read my mind? or more seriously, how can I help him do so? thanks!

Upvotes: 0

Views: 839

Answers (2)

OrenIshShalom
OrenIshShalom

Reputation: 7102

I'm posting the solution as a separate answer hoping other users can benefit from it. Here it is:

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.

Upvotes: 0

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

The problem is not that Coq can't guess what value to use for m and n, but that your goal does not have the right shape for you to instantiate that theorem. When you write apply eq_add_S, Coq tries to unify S n = S m -> n = m with S (add i j) = S (add i k) -> j = k, which cannot be done.

What you need is to apply eq_add_S to the goal's premise, by introducing it into the context.

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.
  (* ...  *)

Upvotes: 2

Related Questions