mathlib3 documentation

data.list.palindrome

Palindromes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

References #

Tags #

palindrome, reverse, induction

source
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.
Instances for list.palindrome
source
theorem list.palindrome.reverse_eq {α : Type u_1} {l : list α} (p : l.palindrome) :
l.reverse = l
source
theorem list.palindrome.of_reverse_eq {α : Type u_1} {l : list α} :
l.reverse = l → l.palindrome
source
theorem list.palindrome.iff_reverse_eq {α : Type u_1} {l : list α} :
l.palindrome ↔ l.reverse = l
source
theorem list.palindrome.append_reverse {α : Type u_1} (l : list α) :
(l ++ l.reverse).palindrome
source
@[protected]
theorem list.palindrome.map {α : Type u_1} {β : Type u_2} {l : list α} (f : α → β) (p : l.palindrome) :
(list.map f l).palindrome
source
@[protected, instance]
def list.palindrome.decidable {α : Type u_1} [decidable_eq α] (l : list α) :
decidable l.palindrome
Equations