This is one of the exercise given to me, I got stuck almost immediately after doing an induction on l. I dont know what other assertion to make here.
I'm not allowed to use advanced tactics like auto, intuition etc.
Fixpoint snoc {A : Type} l a : list A :=
match l with
| nil => a :: nil
| h :: t => h :: (snoc t a)
end.
Fixpoint rev {A : Type} l : list A :=
match l with
| nil => nil
| h :: t => snoc (rev t) h
end.
(Prove the following)
Theorem rev_rev : forall A (l : list A),
rev (rev l) = l.
We have all been new to this, and in the beginning it is useful to get help to not get stuck an lose courage when trying to master a new subject. I'll try to give you a hint without giving away too much.
The reason why this is trickier than earlier exercises may be because this proof involves doing two inductive reasoning steps. You probably did the first one just fine and got the second goal like
...
IHl : rev (rev l) = l
============================
rev (snoc (rev l) a) = a :: l
Unfortunately you can't use your inductive hypothesis IHl immediately, because the argument to rev is not in the right shape.
So, here you could try to prove another lemma about rev (snoc l a) = ... that would turn the goal into something which you could rewrite with IHl.
If you can figure that out, and prove that in a lemma, then you should be fine.