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

inductive List.Palindrome {α : Type u_1} : List α → Prop

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.

• nil: ∀ {α : Type u_1}, List.Palindrome []
• singleton: ∀ {α : Type u_1} (x : α), List.Palindrome [x]
• cons_concat: ∀ {α : Type u_1} (x : α) {l : List α}, List.Palindrome l → List.Palindrome (x :: (l ++ [x]))

theorem List.Palindrome.reverse_eq {α : Type u_1} {l : List α} (p : List.Palindrome l) : List.reverse l = l

theorem List.Palindrome.of_reverse_eq {α : Type u_1} {l : List α} : List.reverse l = l → List.Palindrome l

theorem List.Palindrome.iff_reverse_eq {α : Type u_1} {l : List α} : List.Palindrome l ↔ List.reverse l = l

theorem List.Palindrome.append_reverse {α : Type u_1} (l : List α) : List.Palindrome (l ++ List.reverse l)

theorem List.Palindrome.map {α : Type u_1} {β : Type u_2} {l : List α} (f : α → β) (p : List.Palindrome l) : List.Palindrome (List.map f l)

instance List.Palindrome.instDecidablePalindrome {α : Type u_1} [DecidableEq α] (l : List α) : Decidable (List.Palindrome l)

Equations

• List.Palindrome.instDecidablePalindrome l = decidable_of_iff' (List.reverse l = l) ⋯