This is the coq version I'm using:
sibi { ~ }-> coqc --version
The Coq Proof Assistant, version 8.4pl4 (November 2015)
compiled on Nov 04 2015 12:56:53 with OCaml 4.02.3
This is the theorem I'm trying to prove:
Require Import Coq.Lists.List.
Import ListNotations.
Theorem rev_app_distr: forall l1 l2 : list nat,
rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
Note that I will use this theorem in the proof (which has already been proved by me):
Theorem app_nil_r : forall l : list nat,
l ++ [] = l.
Ok, now this is my attempt to prove the theorem via the usual induction way:
Theorem rev_app_distr: forall l1 l2 : list nat,
rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
intros l1 l2.
induction l1 as [| n l1'].
- simpl.
rewrite -> app_nil_r with (l := rev l2) at 2.
But on executing the rewrite tactic, it gives me the following error:
Error: Tactic failure:Nothing to rewrite.
But If I use symmetry tactic, I can actually prove it via the same code:
Theorem rev_app_distr: forall l1 l2 : list nat,
rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
intros l1 l2.
induction l1 as [| n l1'].
- simpl.
symmetry.
rewrite -> app_nil_r with (l := rev l2) at 1.
So, why does rewriting it without symmetry doesn't work ?
The problem is not that you were missing the symmetry call, but that you added the at 2 modifier when invoking the tactic. Since the goal at that point has only one occurrence of the left-hand side of app_nil_r (that is, rev l2 ++ []), the rewrite tactic gets confused and does not do anything. If you replace at 2 by at 1, or simply delete it, the problem goes away. You can learn more about the at modifier in the Coq manual.