Mathlib.Data.List.Palindrome

Module docstring

{"# 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 induction principle. Also provided are conversions to and from other equivalent definitions.

References

Pierre Castéran, On palindromes

Tags

palindrome, reverse, induction "}

List.Palindrome inductive

: List α → Prop

Full source

/-- `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.
-/
inductive Palindrome : List α → Prop
  | nil : Palindrome []
  | singleton : ∀ x, Palindrome [x]
  | cons_concat : ∀ (x) {l}, Palindrome l → Palindrome (x :: (l ++ [x]))

Palindrome predicate for lists

Informal description

The predicate `Palindrome l` asserts that a list `l` is a palindrome, meaning it reads the same forwards and backwards. This is defined inductively with three cases: 1. The empty list is a palindrome. 2. A list with a single element is a palindrome. 3. If a list `l` is a palindrome, then adding the same element to both ends of `l` results in a longer palindrome.

List.Palindrome.reverse_eq theorem

{l : List α} (p : Palindrome l) : reverse l = l

Full source

theorem reverse_eq {l : List α} (p : Palindrome l) : reverse l = l := by
  induction p <;> try (exact rfl)
  simpa

Palindrome Lists Satisfy $\mathrm{reverse}(l) = l$

Informal description

For any list $l$ of elements of type $\alpha$, if $l$ is a palindrome, then the reverse of $l$ is equal to $l$, i.e., $\mathrm{reverse}(l) = l$.

List.Palindrome.of_reverse_eq theorem

{l : List α} : reverse l = l → Palindrome l

Full source

theorem of_reverse_eq {l : List α} : reverse l = l → Palindrome l := by
  refine bidirectionalRecOn l (fun _ => Palindrome.nil) (fun a _ => Palindrome.singleton a) ?_
  intro x l y hp hr
  rw [reverse_cons, reverse_append] at hr
  rw [head_eq_of_cons_eq hr]
  have : Palindrome l := hp (append_inj_left' (tail_eq_of_cons_eq hr) rfl)
  exact Palindrome.cons_concat x this

Reverse Equality Implies Palindrome

Informal description

For any list $l$ of elements of type $\alpha$, if the reverse of $l$ is equal to $l$, then $l$ is a palindrome.

List.Palindrome.iff_reverse_eq theorem

{l : List α} : Palindrome l ↔ reverse l = l

Full source

theorem iff_reverse_eq {l : List α} : PalindromePalindrome l ↔ reverse l = l :=
  Iff.intro reverse_eq of_reverse_eq

Palindrome Characterization via Reverse Equality

Informal description

For any list $l$ of elements of type $\alpha$, $l$ is a palindrome if and only if the reverse of $l$ is equal to $l$, i.e., $\mathrm{reverse}(l) = l$.

List.Palindrome.append_reverse theorem

(l : List α) : Palindrome (l ++ reverse l)

Full source

theorem append_reverse (l : List α) : Palindrome (l ++ reverse l) := by
  apply of_reverse_eq
  rw [reverse_append, reverse_reverse]

Concatenation of List with its Reverse Forms a Palindrome

Informal description

For any list $l$ of elements of type $\alpha$, the concatenation of $l$ with its reverse, denoted as $l \mathbin{+\!\!+} \operatorname{reverse}(l)$, is a palindrome.

List.Palindrome.map theorem

(f : α → β) (p : Palindrome l) : Palindrome (map f l)

Full source

protected theorem map (f : α → β) (p : Palindrome l) : Palindrome (map f l) :=
  of_reverse_eq <| by rw [← map_reverse, p.reverse_eq]

Mapped Palindromes: $\mathrm{Palindrome}\,(\mathrm{map}\,f\,l)$ for $\mathrm{Palindrome}\,l$

Informal description

For any function $f : \alpha \to \beta$ and any palindrome $l$ over $\alpha$, the mapped list $\mathrm{map}\,f\,l$ is also a palindrome over $\beta$.

List.Palindrome.instDecidableOfDecidableEq instance

[DecidableEq α] (l : List α) : Decidable (Palindrome l)

Full source

instance [DecidableEq α] (l : List α) : Decidable (Palindrome l) :=
  decidable_of_iff' _ iff_reverse_eq

Decidability of Palindrome Property for Lists with Decidable Equality

Informal description

For any type $\alpha$ with decidable equality and any list $l$ of elements of type $\alpha$, the property of $l$ being a palindrome is decidable.