Hello,

I am trying to solve an exercise from Software Foundations, Chapter IndProp.

Exercise: 5 stars, standard, optional (palindrome_converse). To prove suggested theorem I created “helper” theorem, but failed to prove it.

Please tell me… is there any beautiful and short way to prove palindrome_converse? Is my helper theorem having hole in logic? I feel like it’s not provable.

I successfully solved previous one where inductive proposition pal was defined and a couple of theorems, here is the code:

Exercise: 4 stars, standard, optional (palindromes)

```
Inductive pal {X : Type} : list X -> Prop :=
| EmptyPal : pal []
| OnePal x : pal [x]
| IndPal (x : X)
(xs : list X)
(H2 : pal xs) : pal ((x :: xs) ++ [x]).
Example test_pal1 : pal [1;2;1].
Proof. apply (IndPal 1 [2]). apply OnePal.
Qed.
Theorem pal_app_rev : forall {X : Type} (l : list X),
pal (l ++ rev l).
Proof. intros X l.
induction l as [| x l' IHl'].
- simpl. apply EmptyPal.
- simpl. rewrite app_assoc.
apply (IndPal x). apply IHl'.
Qed.
Theorem pal_rev : forall {X : Type} (l : list X) , pal l -> l = rev l.
Proof. intros X l H.
induction H as [| x' | x' xs' H1 IH1].
- simpl. reflexivity.
- simpl. reflexivity.
- rewrite rev_app_distr.
simpl. rewrite <- IH1. reflexivity.
Qed. ```
Exercise: 5 stars, standard, optional (palindrome_converse)
To make this proof I created this theorem but failed to prove it
Theorem rev_pr : forall {X : Type} (x : X) (xs ys : list X),
x :: xs = rev (x :: xs) -> xs = [] \/ (exists ys, xs = ys ++ [x] /\ pal ys).
Proof. intros X x xs ys H.
destruct xs as [| y xs'].
- left. reflexivity.
- right. exists ys.
split. (* dead end? *)
Theorem palindrome_converse : forall {X : Type} (l : list X), l = rev l -> pal l.
Proof. intros X l H.
destruct l as [| x l'] eqn:E.
- apply EmptyPal.
- apply rev_pr in H.
destruct H as [H1 | H2].
+ rewrite H1. apply OnePal.
+ destruct H2 as [ys' H0].
destruct H0 as [H1 H2].
rewrite H1.
apply (IndPal x ys'). apply H2.
+ apply l'.
Qed.
```