Search code examples
coqcoq-tactic

Coq simple implies proof

I am trying to prove the following trivial cancellation theorem for natural numbers:

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

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

After which Coq tries to prove the basis of the induction which is trivial:

j = k -> j = k

Almost all Coq tutorials start with proving A -> A, but when I try to use such proofs I get stuck. For example, I'm using:

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

And then when I try to:

rewrite -> my_first_proof

I get the following error:

Error: Cannot find a relation to rewrite.

Any help is very much appreciated, thanks!

Solution

  • The right tactic in this case is apply.

    apply my_first_proof.

    rewrite is used to replace one subterm of the goal with another, usually with a lemma showing that these subterms are equal or equivalent in some sense. my_first_proof is not an equality proof.