The Coq mailing list

[Jakob Vidmar <jakob AT vidmar.be>]

Hi Mukesh,

Hint: Is [a] not a palindrome ?

Cheers,

Jakob

On 31 Oct 2014, at 11:37, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Hello Everyone,
I am trying to solve this problem from Software Foundations[1].

Exercise: 4 stars (palindromes)

A palindrome is a sequence that reads the same backwards as forwards.

Define an inductive proposition pal on list X that captures what it means to be a palindrome. (Hint: You'll need three cases. Your definition should be based on the structure of the list; just having a single constructor
c : ∀l, l = rev l → pal l
may seem obvious, but will not work very well.)
Prove that
 ∀l, pal (l ++ rev l).
Prove that
 ∀l, pal l → l = rev l.

Inductive data type for palindrome.

Inductive pal { X : Type } : list X -> Prop :=
 | emptyC : pal nil
 | consC : forall ( a : X ) ( l : list X ) , pal l -> pal ( a :: l ++ [a]).

The hint says that we need three case which I am not able to follow. I came up with following reasoning. Empty list is palindrome ( emptyC constructor ).
If you give me any element a of type X and a palindrome list l of type list X,  I can construct another palindrome list ( a :: l ++ [a] ) ( consC constructor ).

I tried to prove following theorem 

Theorem reverseonlist : forall { X : Type } ( l : list X ), pal ( l ++ rev l).
Proof.
 intros X l. induction l as [ | v' l'].
 Case "l = nil".
   simpl. apply emptyC.
 Case "l = Cons v' l'".
   simpl. 

(* This is my goal after apply the simplification.
Case := "l = Cons v' l'" : String.string
  X : Type
  v' : X
  l' : list X
  IHl' : pal (l' ++ rev l')
  ============================
   pal (v' :: l' ++ snoc (rev l') v')
*)
   rewrite -> snoc_list.

(* After this goal changes to
Case := "l = Cons v' l'" : String.string
  X : Type
  v' : X
  l' : list X
  IHl' : pal (l' ++ rev l')
  ============================
   pal (v' :: l' ++ rev l' ++ [v'])
*)

   apply consC with ( a := v' ) ( l := l' ++ rev l' ).

and getting this error
Toplevel input, characters 6-50:
Error: Impossible to unify "pal (v' :: (l' ++ rev l') ++ [v'])" with
 "pal (v' :: l' ++ rev l' ++ [v'])".

snoc_list: forall (X : Type) (v : X) (s : list X), snoc s v = s ++ [v].

I have little bit of Coq experience so it may be related to associativity of ++. Could some one please tell me how to solve this problem. ( A hint would be great ).

-Mukesh Tiwari

[1] http://www.cis.upenn.edu/~bcpierce/sf/current/Prop.html