Is it possible to prove the theorem I created?

Using Coq
1

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

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

3

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. 
Proof. Admitted. 

         (* (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.
4

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.

5

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

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.

7

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

8

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