Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Authors: Chris Wong

! This file was ported from Lean 3 source module data.list.palindrome
! leanprover-community/mathlib commit 5a3e819569b0f12cbec59d740a2613018e7b8eec
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.Basic

/-!
# 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*][casteran]

[casteran]: https://www.labri.fr/perso/casteran/CoqArt/inductive-prop-chap/palindrome.html

## Tags

palindrome, reverse, induction
-/

variable {
α: Type ?u.670
α
β: Type ?u.5
β
:
Type _: Type (?u.261+1)
Type _
} namespace List /-- `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: {α : Type u_1} → List αProp
Palindrome
:
List: Type ?u.15 → Type ?u.15
List
α: Type ?u.8
α
Prop: Type
Prop
|
nil: ∀ {α : Type u_1},
nil
:
Palindrome: List αProp
Palindrome
[]: List ?m.21
[]
|
singleton: ∀ {α : Type u_1} (x : α), Palindrome [x]
singleton
: ∀
x: ?m.25
x
,
Palindrome: List αProp
Palindrome
[
x: ?m.25
x
] |
cons_concat: ∀ {α : Type u_1} (x : α) {l : List α}, Palindrome (x :: (l ++ [x]))
cons_concat
: ∀ (
x: ?m.37
x
) {
l: ?m.40
l
},
Palindrome: List αProp
Palindrome
l: ?m.40
l
Palindrome: List αProp
Palindrome
(
x: ?m.37
x
:: (
l: ?m.40
l
++ [
x: ?m.37
x
])) #align list.palindrome
List.Palindrome: {α : Type u_1} → List αProp
List.Palindrome
namespace Palindrome variable {
l: List α
l
:
List: Type ?u.1077 → Type ?u.1077
List
α: Type ?u.670
α
} theorem
reverse_eq: ∀ {l : List α}, = l
reverse_eq
{
l: List α
l
:
List: Type ?u.279 → Type ?u.279
List
α: Type ?u.270
α
} (
p:
p
:
Palindrome: {α : Type ?u.282} → List αProp
Palindrome
l: List α
l
) :
reverse: {α : Type ?u.289} → List αList α
reverse
l: List α
l
=
l: List α
l
:=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.273

l✝, l: List α

p:

= l
α: Type u_1

β: Type ?u.273

l✝, l: List α

nil
reverse [] = []
α: Type u_1

β: Type ?u.273

l✝, l: List α

x✝: α

singleton
reverse [x✝] = [x✝]
α: Type u_1

β: Type ?u.273

l✝¹, l: List α

x✝: α

l✝: List α

a✝:

a_ih✝: reverse l✝ = l✝

cons_concat
reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
α: Type u_1

β: Type ?u.273

l✝, l: List α

p:

= l
α: Type u_1

β: Type ?u.273

l✝, l: List α

nil
reverse [] = []
α: Type u_1

β: Type ?u.273

l✝, l: List α

x✝: α

singleton
reverse [x✝] = [x✝]
α: Type u_1

β: Type ?u.273

l✝¹, l: List α

x✝: α

l✝: List α

a✝:

a_ih✝: reverse l✝ = l✝

cons_concat
reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
α: Type u_1

β: Type ?u.273

l✝, l: List α

p:

= l
α: Type u_1

β: Type ?u.273

l✝, l: List α

x✝: α

singleton
reverse [x✝] = [x✝]
α: Type u_1

β: Type ?u.273

l✝, l: List α

nil
reverse [] = []

Goals accomplished! 🐙

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.273

l✝, l: List α

p:

= l
α: Type u_1

β: Type ?u.273

l✝¹, l: List α

x✝: α

l✝: List α

a✝:

a_ih✝: reverse l✝ = l✝

cons_concat
reverse l✝ = l✝
α: Type u_1

β: Type ?u.273

l✝¹, l: List α

x✝: α

l✝: List α

a✝:

a_ih✝: reverse l✝ = l✝

cons_concat
reverse l✝ = l✝
α: Type u_1

β: Type ?u.273

l✝, l: List α

p:

= l

Goals accomplished! 🐙
#align list.palindrome.reverse_eq
List.Palindrome.reverse_eq: ∀ {α : Type u_1} {l : List α}, = l
List.Palindrome.reverse_eq
theorem
of_reverse_eq: ∀ {l : List α}, = l
of_reverse_eq
{
l: List α
l
:
List: Type ?u.679 → Type ?u.679
List
α: Type ?u.670
α
} :
reverse: {α : Type ?u.684} → List αList α
reverse
l: List α
l
=
l: List α
l
Palindrome: {α : Type ?u.690} → List αProp
Palindrome
l: List α
l
:=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.673

l✝, l: List α

= l
α: Type u_1

β: Type ?u.673

l✝, l: List α

∀ (a : α) (l : List α) (b : α), ( = l) → reverse (a :: (l ++ [b])) = a :: (l ++ [b])Palindrome (a :: (l ++ [b]))
α: Type u_1

β: Type ?u.673

l✝, l: List α

= l
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse (x :: (l ++ [y])) = x :: (l ++ [y])

Palindrome (x :: (l ++ [y]))
α: Type u_1

β: Type ?u.673

l✝, l: List α

= l
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse (x :: (l ++ [y])) = x :: (l ++ [y])

Palindrome (x :: (l ++ [y]))
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse (l ++ [y]) ++ [x] = x :: (l ++ [y])

Palindrome (x :: (l ++ [y]))
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse (x :: (l ++ [y])) = x :: (l ++ [y])

Palindrome (x :: (l ++ [y]))
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse [y] ++ ++ [x] = x :: (l ++ [y])

Palindrome (x :: (l ++ [y]))
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse [y] ++ ++ [x] = x :: (l ++ [y])

Palindrome (x :: (l ++ [y]))
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse [y] ++ ++ [x] = x :: (l ++ [y])

Palindrome (x :: (l ++ [y]))
α: Type u_1

β: Type ?u.673

l✝, l: List α

= l
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse [y] ++ ++ [x] = x :: (l ++ [y])

Palindrome (x :: (l ++ [y]))
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse [y] ++ ++ [x] = x :: (l ++ [y])

Palindrome (x :: (l ++ [x]))
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse [y] ++ ++ [x] = x :: (l ++ [y])

Palindrome (x :: (l ++ [x]))
α: Type u_1

β: Type ?u.673

l✝, l: List α

= l
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: = l

hr: reverse [y] ++ ++ [x] = x :: (l ++ [y])

this:

Palindrome (x :: (l ++ [x]))
α: Type u_1

β: Type ?u.673

l✝, l: List α

= l

Goals accomplished! 🐙
#align list.palindrome.of_reverse_eq
List.Palindrome.of_reverse_eq: ∀ {α : Type u_1} {l : List α}, = l
List.Palindrome.of_reverse_eq
theorem
iff_reverse_eq: ∀ {α : Type u_1} {l : List α}, = l
iff_reverse_eq
{
l: List α
l
:
List: Type ?u.1030 → Type ?u.1030
List
α: Type ?u.1021
α
} :
Palindrome: {α : Type ?u.1033} → List αProp
Palindrome
l: List α
l
reverse: {α : Type ?u.1038} → List αList α
reverse
l: List α
l
=
l: List α
l
:=
Iff.intro: ∀ {a b : Prop}, (ab) → (ba) → (a b)
Iff.intro
reverse_eq: ∀ {α : Type ?u.1048} {l : List α}, = l
reverse_eq
of_reverse_eq: ∀ {α : Type ?u.1060} {l : List α}, = l
of_reverse_eq
#align list.palindrome.iff_reverse_eq
List.Palindrome.iff_reverse_eq: ∀ {α : Type u_1} {l : List α}, = l
List.Palindrome.iff_reverse_eq
theorem
append_reverse: ∀ (l : List α), Palindrome (l ++ )
append_reverse
(
l: List α
l
:
List: Type ?u.1080 → Type ?u.1080
List
α: Type ?u.1071
α
) :
Palindrome: {α : Type ?u.1083} → List αProp
Palindrome
(
l: List α
l
++
reverse: {α : Type ?u.1088} → List αList α
reverse
l: List α
l
) :=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.1074

l✝, l: List α

α: Type u_1

β: Type ?u.1074

l✝, l: List α

a
reverse (l ++ ) = l ++
α: Type u_1

β: Type ?u.1074

l✝, l: List α

α: Type u_1

β: Type ?u.1074

l✝, l: List α

a
reverse (l ++ ) = l ++
α: Type u_1

β: Type ?u.1074

l✝, l: List α

a
reverse () ++ = l ++
α: Type u_1

β: Type ?u.1074

l✝, l: List α

a
reverse (l ++ ) = l ++
α: Type u_1

β: Type ?u.1074

l✝, l: List α

a
l ++ = l ++

Goals accomplished! 🐙
#align list.palindrome.append_reverse
List.Palindrome.append_reverse: ∀ {α : Type u_1} (l : List α), Palindrome (l ++ )
List.Palindrome.append_reverse
protected theorem
map: ∀ (f : αβ), Palindrome (map f l)
map
(
f: αβ
f
:
α: Type ?u.1189
α
β: Type ?u.1192
β
) (
p:
p
:
Palindrome: {α : Type ?u.1202} → List αProp
Palindrome
l: List α
l
) :
Palindrome: {α : Type ?u.1208} → List αProp
Palindrome
(
map: {α : Type ?u.1211} → {β : Type ?u.1210} → (αβ) → List αList β
map
f: αβ
f
l: List α
l
) :=
of_reverse_eq: ∀ {α : Type ?u.1222} {l : List α}, = l
of_reverse_eq
<|

Goals accomplished! 🐙
α: Type u_1

β: Type u_2

l: List α

f: αβ

p:

reverse (map f l) = map f l
α: Type u_1

β: Type u_2

l: List α

f: αβ

p:

reverse (map f l) = map f l
α: Type u_1

β: Type u_2

l: List α

f: αβ

p:

map f () = map f l
α: Type u_1

β: Type u_2

l: List α

f: αβ

p:

reverse (map f l) = map f l
α: Type u_1

β: Type u_2

l: List α

f: αβ

p:

map f l = map f l

Goals accomplished! 🐙
#align list.palindrome.map
List.Palindrome.map: ∀ {α : Type u_1} {β : Type u_2} {l : List α} (f : αβ), Palindrome (map f l)
List.Palindrome.map
instance: {α : Type u_1} → [inst : ] → (l : List α) →
instance
[
DecidableEq: Sort ?u.1284 → Sort (max1?u.1284)
DecidableEq
α: Type ?u.1275
α
] (
l: List α
l
:
List: Type ?u.1293 → Type ?u.1293
List
α: Type ?u.1275
α
) :
Decidable:
Decidable
(
Palindrome: {α : Type ?u.1296} → List αProp
Palindrome
l: List α
l
) :=
decidable_of_iff': {a : Prop} → (b : Prop) → (a b) → [inst : ] →
decidable_of_iff'
_: Prop
_
iff_reverse_eq: ∀ {α : Type ?u.1308} {l : List α}, = l
iff_reverse_eq
end Palindrome end List