Palindrome via an accumulator-based definition.

PalAcc.v

Require Import List.

Inductive PalAcc {A : Type} (acc : list A) : list A -> Type
  := Even : PalAcc acc acc
   | Odd  : forall x, PalAcc acc (x :: acc)
   | Step : forall x xs, PalAcc (x :: acc) xs -> PalAcc acc (x :: xs)
.

Definition Pal {A : Type} (xs : list A) : Type := PalAcc nil xs.

Theorem PalAccRevAcc {A : Type} (acc xs : list A) :
  PalAcc acc xs -> rev_append acc xs = rev_append xs acc.
Proof.
induction 1; trivial.
Qed.

Theorem PalRev {A : Type} (xs : list A) :
  Pal xs -> rev xs = xs.
Proof.
intro prf; rewrite rev_alt, <- (PalAccRevAcc _ _ prf); reflexivity.
Qed.