CODEWITHSUNDEEP
coqinduction
some1fromhell
some1fromhell

Reputation: 135

Prove "rev (rev l) = l" in Coq

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.

Upvotes: 1

Views: 482

Answers (2)

larsr
larsr

Reputation: 5811

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.

Upvotes: 4

Vinz
Vinz

Reputation: 6047

We won't do your homework for you, you should first prove it on pen & paper as @gallais said.

A tip: you might need to generalize your property a little (use an intermediate lemma) to be able to prove rev_rev. You should have a look at rev_append.

Upvotes: 1

Related Questions