The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Laurent,

Thank you for reply!  The problem was related to associativity of list and rewrite app_assoc. worked.

-Mukesh Tiwari

On Fri, Oct 31, 2014 at 5:19 PM, Laurent Théry <Laurent.Thery AT inria.fr> wrote:

> 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]).
>

With this definition you capture only palindromes with a length that is even
>
> Theorem reverseonlist : forall { X : Type } ( l : list X ), pal ( l >
> ++ rev
> l).> Proof.
> intros X l. induction l as [ | v' l'].
>   simpl. apply emptyC.
> simpl.


With assert you can see that both term does not match there is an
associativity problem

Try

 rewrite app_assoc.


--
Laurent