Proving that a reversible list is a palindrome in Coq without exists tactic

Question

For an exercise in software foundation I want to prove the following theorem :

Theorem rev_pal {X:Type} : forall (l:list X), l = rev l -> pal l.

pal is defined as follow :

Inductive pal {X:Type} : list X -> Prop :=
| pal_nil : pal []
| pal_one : forall x, pal [x]
| pal_rec : forall x l, pal l -> pal (snoc(x:: l) x).

However to proove this I want to use a lemma using exists to say for exemple something like :

foral (l l':list X) (a b:X), a::l = l' ++[b] -> (a=b /\ l=[]) \/ exists k, l = k ++ [b].

In fact, I want to mention something little than l. But using the destruct tactic doesn't seems to help.

Why I don't want to use exists is because during the reading of the book software foundation, we don't have seen yet exists. Of course, one could tell me that exists can be seen as a forall, but it's hard to use in this form.

So how to prove this theorem without a such lemma ? I'm stuck.

How is `pal` defined? Please provide all definitions so that we can type your theorem on our machine and work with it. — Gilles 'SO- stop being evil', Mar 04 '15 at 22:02
Vinz : thanks for the typo. @Gilles : I added a definition for pal. We can also define pal with rev. I don't know if one definition is better than an other. — Saroupille, Mar 05 '15 at 09:34

score 3 · Answer 1 · answered Mar 07 '15 at 14:11

You can't prove your theorem by direct induction on l.

For the inductive step, the induction hypothesis is pal l (after clearing the antecedent) and you're trying to prove pal (x :: l). But the induction hypothesis clearly contradicts the conclusion (unless repeat x n = l), and so it's unusable.

Seeing that until this point in the book there's been no mention of fancier kinds of induction and that this is a 5 star exercise, I think it's safe to conclude that you have more freedom with this exercise.

Take a look at this other question.

Thanks ! I already seen this before posting here. But it's so frustrating to do an exercice and realize after that you need tools not mentionned in the book. Because even with an induction on n, I still need something like "exists" I guess. — Saroupille, Mar 07 '15 at 21:36

score 2 · Accepted Answer · answered Mar 09 '15 at 10:46

As it has been said before, It is easier to prove this theorem using the length of the list :

Theorem rev_pal_aux {X:Type} : forall (l:list X) (n:nat) , length l<= n -> l = rev l -> pal l.

Then you can start an induction on n.

The key point to avoid something with exists is to use an inversion. For this proof it is possible to use an inversion on something like x::l=rev x::l and then a destruct on rev l (for some l). This way, you will get x :: l = snoc (x0 :: l0) x (l0 is new).

(l0) is the key. It is on l0 that you need to use the induction hypothesis.

Finally, I used the following lemma (not so easy to proof) :

Lemma length_snoc_aux {X:Type} : forall (l m:list X) (n:nat) (x:X), length l <= n -> l = snoc m x -> length m <= n.

Proving that a reversible list is a palindrome in Coq without exists tactic

2 Answers2