0

Trying to prove the following lemma I got stuck. Usully theorems about lists are proven using induction, but I don't know where to move next.

Lemma reverse_append : forall (T : Type) (h : T) (t : list T), h::t = rev(t) ++ [h] -> t = rev(t).
Proof.
  intros. induction t.
  - simpl. reflexivity.
  - simpl. simpl in H.

Result:

1 subgoal (ID 522)

T : Type
h, x : T
t : list T
H : h :: x :: t = (rev t ++ [x]) ++ [h]
IHt : h :: t = rev t ++ [h] -> t = rev t
============================
x :: t = rev t ++ [x]
user4035
  • 22,508
  • 11
  • 59
  • 94

2 Answers2

2

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)).
Proof. intros H. specialize (H nat 2 [1;2] eq_refl). 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
Bubbler
  • 940
  • 6
  • 15
1

The lemma isn't true as stated. Before proving anything, you should make sure it makes sense. The hypothesis is essentially saying that h::t = rev (h::t). But why would that mean that t = rev t? If you remove an element from the start of a palindromic list, it probably won't be a palindrome anymore. For example, deified is palindrome ('deified' = rev 'deified'), but eified isn't a palindrome.

For an example in this particular situation, 1::[2; 1] = (rev [2; 1]) ++ [1], since both are [1; 2; 1]. But [2; 1] is not equal to rev [2; 1] = [1; 2].

SCappella
  • 9,534
  • 1
  • 26
  • 35