# Is it possible to prove the theorem I created?

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.

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.``````

You could try to replace `pal ys` with `ys = rev ys` in the statement of `Theorem rev_pr`.

My theorems are mutual. Like mutual functions in Idris… I am running in a wheel like a hamster.

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

(* (x :: a :: x) *)
(*   x :: l *)
(*   l = rev l -> pal l *)

Theorem rev_pr : forall {X : Type} (x : X) (xs : list X),
x :: xs = rev (x :: xs) -> xs = [] \/ (exists ys, xs = ys ++ [x] /\ pal ys).
Proof. intros X x xs H.
apply rev_pal in H.
inversion H.
- left. reflexivity.
- right. exists xs0.
split. reflexivity.
apply H0.
Qed.

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.``````

Is that terminating? in rev_pr you apply rev_pal to `x :: xs`, but using the proof of palindrome_converse this would immediately apply rev_pr back.

BTW you don’t need to indent that much, just put a newline after `Proof.`

Have you tried the modified `rev_pr` statement by reversed induction over `xs`:

``````Theorem rev_pr : forall {X : Type} x (xs : list X),
x :: xs = rev (x :: xs) -> xs = [] \/ (exists ys, xs = ys ++ [x] /\ ys = rev ys).
Proof.
intros X x xs.
induction xs as [ | x' xs ] using rev_ind; simpl; intros Heq.
``````

The thing is : if I’ll change right part of conjunction from (pal ys) to (ys = rev ys), this will make this theorem useless for me. The goal of this theorem is to be used in the theorem palindrome_converse.

I suggest you use the modified version of `rev_pr` to prove `palindrome_converse` by induction on the length of the list.

Thank you, looks like I didn’t understand your idea. let me try…