Lemma about list and rev list

Main answer

Before you start proving your theorem, you should try to thoroughly understand what your theorem says. Your theorem is simply wrong.

Counterexample: 2 :: [1;2] = rev [1;2] ++ [2], but [1;2] is not a palindrome.

Full proof:

Require Import List.
Import ListNotations.

Lemma reverse_append_false :
  ~(forall (T : Type) (h : T) (t : list T),
       h :: t = rev t ++ [h] -> t = rev t).
~
(forall (T : Type) (h : T) (t : list T),
 h :: t = rev t ++ [h] -> t = rev t)
Proof.
~
(forall (T : Type) (h : T) (t : list T),
 h :: t = rev t ++ [h] -> t = rev t)
  intros H.
H: forall (T : Type) (h : T) (t : list T),
h :: t = rev t ++ [h] -> t = rev t
False specialize (H nat 2 [1;2] eq_refl).
H: [1; 2] = rev [1; 2]
False inversion H.
Qed.

Minor issues

rev(t) should be just rev t. Just an aesthetic point, but probably you should get yourself more familiar to writing in functional programming style.

Usually theorems about lists are proven using induction

This is a pretty naive statement, though technically correct. There are so many ways to do induction on a value, and choosing the induction that works best is a crucial skill. To name a few:

• Induction on the list

• Induction on the length of the list

  • arises quite frequently when dealing with rev and other functions that preserve length

  • Example

• If simple induction doesn't work, consider a custom induction scheme

  • nat_ind2