# mathlibdocumentation

data.list.palindrome

# Palindromes

This module defines palindromes, lists which are equal to their reverse.

The main result is the palindrome inductive type, and its associated palindrome.rec_on induction principle. Also provided are conversions to and from other equivalent definitions.

## Tags

palindrome, reverse, induction

inductive palindrome {α : Type u_1} :
list α → Prop
• nil : ∀ {α : Type u_1},
• singleton : ∀ {α : Type u_1} (x : α), palindrome [x]
• cons_concat : ∀ {α : Type u_1} (x : α) {l : list α}, palindrome (x :: (l ++ [x]))

palindrome l asserts that l is a palindrome. This is defined inductively:

• The empty list is a palindrome;
• A list with one element is a palindrome;
• Adding the same element to both ends of a palindrome results in a bigger palindrome.
theorem palindrome.reverse_eq {α : Type u_1} {l : list α} (p : palindrome l) :

theorem palindrome.of_reverse_eq {α : Type u_1} {l : list α} :
l.reverse = l

theorem palindrome.iff_reverse_eq {α : Type u_1} {l : list α} :

theorem palindrome.append_reverse {α : Type u_1} (l : list α) :

@[instance]
def palindrome.decidable {α : Type u_1} [decidable_eq α] (l : list α) :

Equations