/-
Copyright (c) 2020 Google LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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}, Palindrome []
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 l → 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 α}, Palindrome l → reverse l = l
reverse_eq {
l: List α
l : 
List: Type ?u.279 → Type ?u.279
List 
α: Type ?u.270
α} (
p: Palindrome l
p : 
Palindrome: {α : Type ?u.282} → List α → Prop
Palindrome 
l: List α
l) : 
reverse: {α : Type ?u.289} → List α → List α
reverse 
l: List α
l = 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.273

l✝, l: List α

p: Palindrome l

reverse l = linduction 
p: Palindrome l
p
α: 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✝: Palindrome l✝

a_ih✝: reverse l✝ = l✝

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

β: Type ?u.273

l✝, l: List α

p: Palindrome l

reverse l = 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✝: Palindrome l✝

a_ih✝: reverse l✝ = l✝

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

β: Type ?u.273

l✝, l: List α

p: Palindrome l

reverse l = ltry 
α: 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 [] = []exact 
rfl: ∀ {α : Sort ?u.362} {a : α}, a = a
rfl
Goals accomplished! 🐙)
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.273

l✝, l: List α

p: Palindrome l

reverse l = lsimp
α: Type u_1

β: Type ?u.273

l✝¹, l: List α

x✝: α

l✝: List α

a✝: Palindrome l✝

a_ih✝: reverse l✝ = l✝

cons_concat
reverse l✝ = l✝;
α: Type u_1

β: Type ?u.273

l✝¹, l: List α

x✝: α

l✝: List α

a✝: Palindrome l✝

a_ih✝: reverse l✝ = l✝

cons_concat
reverse l✝ = l✝ 
α: Type u_1

β: Type ?u.273

l✝, l: List α

p: Palindrome l

reverse l = lassumption
Goals accomplished! 🐙
#align list.palindrome.reverse_eq 
List.Palindrome.reverse_eq: ∀ {α : Type u_1} {l : List α}, Palindrome l → reverse l = l
List.Palindrome.reverse_eq

theorem 
of_reverse_eq: ∀ {l : List α}, reverse l = l → Palindrome 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 := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.673

l✝, l: List α

reverse l = l → Palindrome lrefine' 
bidirectionalRecOn: ∀ {α : Type ?u.698} {C : List α → Sort ?u.697} (l : List α),
  C [] → (∀ (a : α), C [a]) → (∀ (a : α) (l : List α) (b : α), C l → C (a :: (l ++ [b]))) → C l
bidirectionalRecOn 
l: List α
l (fun 
_: ?m.734
_ => 
Palindrome.nil: ∀ {α : Type ?u.736}, Palindrome []
Palindrome.nil) (fun 
a: ?m.744
a 
_: ?m.747
_ => 
Palindrome.singleton: ∀ {α : Type ?u.749} (x : α), Palindrome [x]
Palindrome.singleton 
a: ?m.744
a) 
_: ∀ (a : α) (l : List α) (b : α),
  (reverse l = l → Palindrome l) → reverse (a :: (l ++ [b])) = a :: (l ++ [b]) → Palindrome (a :: (l ++ [b]))
_
α: Type u_1

β: Type ?u.673

l✝, l: List α

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

β: Type ?u.673

l✝, l: List α

reverse l = l → Palindrome lintro 
x: α
x 
l: List α
l 
y: α
y 
hp: reverse l = l → Palindrome l
hp 
hr: reverse (x :: (l ++ [y])) = x :: (l ++ [y])
hr
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: reverse l = l → Palindrome l

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

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

β: Type ?u.673

l✝, l: List α

reverse l = l → Palindrome lrw [
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: reverse l = l → Palindrome l

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

Palindrome (x :: (l ++ [y]))
reverse_cons: ∀ {α : Type ?u.771} (a : α) (as : List α), reverse (a :: as) = reverse as ++ [a]
reverse_cons,
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: reverse l = l → Palindrome 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: reverse l = l → Palindrome l

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

Palindrome (x :: (l ++ [y]))
reverse_append: ∀ {α : Type ?u.796} (as bs : List α), reverse (as ++ bs) = reverse bs ++ reverse as
reverse_append
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: reverse l = l → Palindrome l

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

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

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: reverse l = l → Palindrome l

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

Palindrome (x :: (l ++ [y])) at 
hr: reverse (x :: (l ++ [y])) = x :: (l ++ [y])
hr
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: reverse l = l → Palindrome l

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

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

β: Type ?u.673

l✝, l: List α

reverse l = l → Palindrome lrw [
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: reverse l = l → Palindrome l

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

Palindrome (x :: (l ++ [y]))
head_eq_of_cons_eq: ∀ {α : Type ?u.825} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → h₁ = h₂
head_eq_of_cons_eq 
hr: reverse [y] ++ reverse l ++ [x] = x :: (l ++ [y])
hr
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: reverse l = l → Palindrome l

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

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

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: reverse l = l → Palindrome l

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

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

β: Type ?u.673

l✝, l: List α

reverse l = l → Palindrome lhave : 
Palindrome: {α : Type ?u.901} → List α → Prop
Palindrome 
l: List α
l := 
hp: reverse l = l → Palindrome l
hp (
append_inj_left': ∀ {α : Type ?u.904} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → length t₁ = length t₂ → s₁ = s₂
append_inj_left' (
tail_eq_of_cons_eq: ∀ {α : Type ?u.911} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → t₁ = t₂
tail_eq_of_cons_eq 
hr: reverse [y] ++ reverse l ++ [x] = x :: (l ++ [y])
hr) 
rfl: ∀ {α : Sort ?u.975} {a : α}, a = a
rfl)
α: Type u_1

β: Type ?u.673

l✝¹, l✝: List α

x: α

l: List α

y: α

hp: reverse l = l → Palindrome l

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

this: Palindrome l

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

β: Type ?u.673

l✝, l: List α

reverse l = l → Palindrome lexact 
Palindrome.cons_concat: ∀ {α : Type ?u.1000} (x : α) {l : List α}, Palindrome l → Palindrome (x :: (l ++ [x]))
Palindrome.cons_concat 
x: α
x 
this: Palindrome l
this
Goals accomplished! 🐙
#align list.palindrome.of_reverse_eq 
List.Palindrome.of_reverse_eq: ∀ {α : Type u_1} {l : List α}, reverse l = l → Palindrome l
List.Palindrome.of_reverse_eq

theorem 
iff_reverse_eq: ∀ {α : Type u_1} {l : List α}, Palindrome l ↔ reverse l = 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}, (a → b) → (b → a) → (a ↔ b)
Iff.intro 
reverse_eq: ∀ {α : Type ?u.1048} {l : List α}, Palindrome l → reverse l = l
reverse_eq 
of_reverse_eq: ∀ {α : Type ?u.1060} {l : List α}, reverse l = l → Palindrome l
of_reverse_eq
#align list.palindrome.iff_reverse_eq 
List.Palindrome.iff_reverse_eq: ∀ {α : Type u_1} {l : List α}, Palindrome l ↔ reverse l = l
List.Palindrome.iff_reverse_eq

theorem 
append_reverse: ∀ (l : List α), Palindrome (l ++ reverse 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) := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.1074

l✝, l: List α

Palindrome (l ++ reverse l)apply 
of_reverse_eq: ∀ {α : Type ?u.1145} {l : List α}, reverse l = l → Palindrome l
of_reverse_eq
α: Type u_1

β: Type ?u.1074

l✝, l: List α

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

β: Type ?u.1074

l✝, l: List α

Palindrome (l ++ reverse l)rw [
α: Type u_1

β: Type ?u.1074

l✝, l: List α

a
reverse (l ++ reverse l) = l ++ reverse l
reverse_append: ∀ {α : Type ?u.1155} (as bs : List α), reverse (as ++ bs) = reverse bs ++ reverse as
reverse_append,
α: Type u_1

β: Type ?u.1074

l✝, l: List α

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

β: Type ?u.1074

l✝, l: List α

a
reverse (l ++ reverse l) = l ++ reverse l
reverse_reverse: ∀ {α : Type ?u.1173} (as : List α), reverse (reverse as) = as
reverse_reverse
α: Type u_1

β: Type ?u.1074

l✝, l: List α

a
l ++ reverse l = l ++ reverse l]
Goals accomplished! 🐙
#align list.palindrome.append_reverse 
List.Palindrome.append_reverse: ∀ {α : Type u_1} (l : List α), Palindrome (l ++ reverse l)
List.Palindrome.append_reverse

protected theorem 
map: ∀ (f : α → β), Palindrome l → Palindrome (map f l)
map (
f: α → β
f : 
α: Type ?u.1189
α → 
β: Type ?u.1192
β) (
p: Palindrome l
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 α}, reverse l = l → Palindrome l
of_reverse_eq <| by
Goals accomplished! 🐙 
α: Type u_1

β: Type u_2

l: List α

f: α → β

p: Palindrome l

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

β: Type u_2

l: List α

f: α → β

p: Palindrome l

reverse (map f l) = map f l← 
map_reverse: ∀ {α : Type ?u.1231} {β : Type ?u.1230} (f : α → β) (l : List α), map f (reverse l) = reverse (map f l)
map_reverse,
α: Type u_1

β: Type u_2

l: List α

f: α → β

p: Palindrome l

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

β: Type u_2

l: List α

f: α → β

p: Palindrome l

reverse (map f l) = map f l
p: Palindrome l
p.
reverse_eq: ∀ {α : Type ?u.1251} {l : List α}, Palindrome l → reverse l = l
reverse_eq
α: Type u_1

β: Type u_2

l: List α

f: α → β

p: Palindrome l

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 l → Palindrome (map f l)
List.Palindrome.map

instance: {α : Type u_1} → [inst : DecidableEq α] → (l : List α) → Decidable (Palindrome l)
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: Prop → Type
Decidable (
Palindrome: {α : Type ?u.1296} → List α → Prop
Palindrome 
l: List α
l) :=
  
decidable_of_iff': {a : Prop} → (b : Prop) → (a ↔ b) → [inst : Decidable b] → Decidable a
decidable_of_iff' 
_: Prop
_ 
iff_reverse_eq: ∀ {α : Type ?u.1308} {l : List α}, Palindrome l ↔ reverse l = l
iff_reverse_eq

end Palindrome

end List