# Palindromes

Palindromes are lists that read the same from left to right and from right to left. For example, `[a, b, b, a]` and `[a, h, a]` are palindromes.

We use an inductive predicate to specify whether a list is a palindrome or not. Recall that inductive predicates, or inductively defined propositions, are a convenient way to specify functions of type `... → Prop`.

This example is a based on an example from the book "The Hitchhiker's Guide to Logical Verification".

```inductive Palindrome: {α : Type u_1} → List α → PropPalindrome : List: Type u_1 → Type u_1List α: Type u_1α → Prop: TypeProp where
| nil: ∀ {α : Type u_1}, Palindrome []nil      : Palindrome: {α : Type u_1} → List α → PropPalindrome []: List ?m.17[]
| single: ∀ {α : Type u_1} (a : α), Palindrome [a]single   : (a: αa : α: Type u_1α) → Palindrome: {α : Type u_1} → List α → PropPalindrome [a: αa]
| sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])sandwich : (a: αa : α: Type u_1α) → Palindrome: {α : Type u_1} → List α → PropPalindrome as: List αas → Palindrome: {α : Type u_1} → List α → PropPalindrome ([a: αa] ++ as: List αas ++ [a: αa])```

The definition distinguishes three cases: (1) `[]` is a palindrome; (2) for any element `a`, the singleton list `[a]` is a palindrome; (3) for any element `a` and any palindrome `[b₁, . . ., bₙ]`, the list `[a, b₁, . . ., bₙ, a]` is a palindrome.

We now prove that the reverse of a palindrome is a palindrome using induction on the inductive predicate `h : Palindrome as`.

```theorem palindrome_reverse: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)palindrome_reverse (h: Palindrome ash : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.394as) : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.394as.reverse: {α : Type u_1} → List α → List αreverse := byGoals accomplished! 🐙
induction h: Palindrome ash withα✝: Type u_1as: List α✝h: Palindrome asPalindrome (List.reverse as)
| nil: ∀ {α : Type u_1}, Palindrome []nil =>α✝: Type u_1as: List α✝nilPalindrome (List.reverse []) exact Palindrome.nil: ∀ {α : Type u_1}, Palindrome []Palindrome.nilGoals accomplished! 🐙
| single: ∀ {α : Type u_1} (a : α), Palindrome [a]single a: α✝a =>α✝: Type u_1as: List α✝a: α✝singlePalindrome (List.reverse [a]) exact Palindrome.single: ∀ {α : Type u_1} (a : α), Palindrome [a]Palindrome.single a: α✝aGoals accomplished! 🐙
| sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])sandwich a: α✝a h: Palindrome as✝h ih: Palindrome (List.reverse as✝)ih =>α✝: Type u_1as, as✝: List α✝a: α✝h: Palindrome as✝ih: Palindrome (List.reverse as✝)sandwichPalindrome (List.reverse ([a] ++ as✝ ++ [a])) simpα✝: Type u_1as, as✝: List α✝a: α✝h: Palindrome as✝ih: Palindrome (List.reverse as✝)sandwichPalindrome (a :: (List.reverse as✝ ++ [a])); exact Palindrome.sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])Palindrome.sandwich _: α✝_ ih: Palindrome (List.reverse as✝)ihGoals accomplished! 🐙```

If a list `as` is a palindrome, then the reverse of `as` is equal to itself.

```theorem reverse_eq_of_palindrome: ∀ {α : Type u_1} {as : List α}, Palindrome as → List.reverse as = asreverse_eq_of_palindrome (h: Palindrome ash : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.707as) : as: List ?m.707as.reverse: {α : Type u_1} → List α → List αreverse = as: List ?m.707as := byGoals accomplished! 🐙
induction h: Palindrome ash withα✝: Type u_1as: List α✝h: Palindrome asList.reverse as = as
| nil: ∀ {α : Type u_1}, Palindrome []nil =>α✝: Type u_1as: List α✝nilList.reverse [] = [] rflGoals accomplished! 🐙
| single: ∀ {α : Type u_1} (a : α), Palindrome [a]single a: α✝a =>α✝: Type u_1as: List α✝a: α✝singleList.reverse [a] = [a] rflGoals accomplished! 🐙
| sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])sandwich a: α✝aα✝: Type u_1as, as✝: List α✝a: α✝h: Palindrome as✝ih: List.reverse as✝ = as✝sandwichList.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a] h: Palindrome as✝hWarning: unused variable `h` [linter.unusedVariables]α✝: Type u_1as, as✝: List α✝a: α✝h: Palindrome as✝ih: List.reverse as✝ = as✝sandwichList.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a] ih: List.reverse as✝ = as✝ih: List.reverse as✝ = as✝ih =>α✝: Type u_1as, as✝: List α✝a: α✝h: Palindrome as✝ih: List.reverse as✝ = as✝sandwichList.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a] simp [ih: List.reverse as✝ = as✝ih]Goals accomplished! 🐙```

Note that you can also easily prove `palindrome_reverse` using `reverse_eq_of_palindrome`.

```example: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)example (h: Palindrome ash : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.969as) : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.969as.reverse: {α : Type u_1} → List α → List αreverse := byGoals accomplished! 🐙
simp [reverse_eq_of_palindrome: ∀ {α : Type ?u.965} {as : List α}, Palindrome as → List.reverse as = asreverse_eq_of_palindrome h: Palindrome ash, h: Palindrome ash]Goals accomplished! 🐙```

Given a nonempty list, the function `List.last` returns its element. Note that we use `(by simp)` to prove that `a₂ :: as ≠ []` in the recursive application.

```def List.last: {α : Type u_1} → (as : List α) → as ≠ [] → αList.last : (as: List αas : List: Type u_1 → Type u_1List α: Type u_1α) → as: List αas ≠ []: List α[] → α: Type u_1α
| [a: αa],         _ => a: αa
| _::a₂: αa₂:: as: List αas, _ => (a₂: αa₂::as: List αas).last: {α : Type u_1} → (as : List α) → as ≠ [] → αlast (byGoals accomplished! 🐙 simpGoals accomplished! 🐙)```

We use the function `List.last` to prove the following theorem that says that if a list `as` is not empty, then removing the last element from `as` and appending it back is equal to `as`. We use the attribute `@[simp]` to instruct the `simp` tactic to use this theorem as a simplification rule.

```@[simp] theorem List.dropLast_append_last: ∀ {α : Type u_1} {as : List α} (h : as ≠ []), dropLast as ++ [last as h] = asList.dropLast_append_last (h: as ≠ []h : as: List ?m.1701as ≠ []: List ?m.1701[]) : as: List ?m.1701as.dropLast: {α : Type u_1} → List α → List αdropLast ++ [as: List ?m.1701as.last: {α : Type u_1} → (as : List α) → as ≠ [] → αlast h: as ≠ []h] = as: List ?m.1701as := byGoals accomplished! 🐙
match as: List α✝as withα✝: Type u_1as: List α✝h: as ≠ []dropLast as ++ [last as h] = as
| [] =>α✝: Type u_1as: List α✝h: [] ≠ []dropLast [] ++ [last [] h] = [] contradictionGoals accomplished! 🐙
| [a: α✝a] =>α✝: Type u_1as: List α✝a: α✝h: [a] ≠ []dropLast [a] ++ [last [a] h] = [a] simp_all [last: {α : Type ?u.2017} → (as : List α) → as ≠ [] → αlast, dropLast: {α : Type ?u.2674} → List α → List αdropLast]Goals accomplished! 🐙
| a₁: α✝a₁ :: a₂: α✝a₂ :: as: List α✝as =>α✝: Type u_1as✝: List α✝a₁, a₂: α✝as: List α✝h: a₁ :: a₂ :: as ≠ []dropLast (a₁ :: a₂ :: as) ++ [last (a₁ :: a₂ :: as) h] = a₁ :: a₂ :: as
simp [last: {α : Type ?u.3836} → (as : List α) → as ≠ [] → αlast, dropLast: {α : Type ?u.3861} → List α → List αdropLast]α✝: Type u_1as✝: List α✝a₁, a₂: α✝as: List α✝h: a₁ :: a₂ :: as ≠ []dropLast (a₂ :: as) ++ [last (a₂ :: as) (_ : ¬a₂ :: as = [])] = a₂ :: as
exact dropLast_append_last: ∀ {α : Type u_1} {as : List α} (h : as ≠ []), dropLast as ++ [last as h] = asdropLast_append_last (as := a₂: α✝a₂ :: as: List α✝as) (α✝: Type u_1as✝: List α✝a₁, a₂: α✝as: List α✝h: a₁ :: a₂ :: as ≠ []dropLast (a₂ :: as) ++ [last (a₂ :: as) (_ : ¬a₂ :: as = [])] = a₂ :: asbyGoals accomplished! 🐙 simpGoals accomplished! 🐙)Goals accomplished! 🐙```

We now define the following auxiliary induction principle for lists using well-founded recursion on `as.length`. We can read it as follows, to prove `motive as`, it suffices to show that: (1) `motive []`; (2) `motive [a]` for any `a`; (3) if `motive as` holds, then `motive ([a] ++ as ++ [b])` also holds for any `a`, `b`, and `as`. Note that the structure of this induction principle is very similar to the `Palindrome` inductive predicate.

```theorem List.palindrome_ind: ∀ {α : Type u_1} (motive : List α → Prop),
motive [] →
(∀ (a : α), motive [a]) →
(∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive asList.palindrome_ind (motive: List α → Propmotive : List: Type u_1 → Type u_1List α: Type u_1α → Prop: TypeProp)
(h₁: motive []h₁ : motive: List α → Propmotive []: List α[])
(h₂: ∀ (a : α), motive [a]h₂ : (a: αa : α: Type u_1α) → motive: List α → Propmotive [a: αa])
(h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])h₃ : (a: αa b: αb : α: Type u_1α) → (as: List αas : List: Type u_1 → Type u_1List α: Type u_1α) → motive: List α → Propmotive as: List αas → motive: List α → Propmotive ([a: αa] ++ as: List αas ++ [b: αb]))
(as: List αas : List: Type u_1 → Type u_1List α: Type u_1α)
: motive: List α → Propmotive as: List αas :=
match as: List αas with
| []  => h₁: motive []h₁
| [a: αa] => h₂: ∀ (a : α), motive [a]h₂ a: αa
| a₁: αa₁::a₂: αa₂::as': List αas' =>
have ih: motive (dropLast (a₂ :: as'))ih := palindrome_ind: ∀ {α : Type u_1} (motive : List α → Prop),
motive [] →
(∀ (a : α), motive [a]) →
(∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive aspalindrome_ind motive: List α → Propmotive h₁: motive []h₁ h₂: ∀ (a : α), motive [a]h₂ h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])h₃ (a₂: αa₂::as': List αas').dropLast: {α : Type u_1} → List α → List αdropLast
have : [a₁: αa₁] ++ (a₂: αa₂::as': List αas').dropLast: {α : Type u_1} → List α → List αdropLast ++ [(a₂: αa₂::as': List αas').last: {α : Type u_1} → (as : List α) → as ≠ [] → αlast (byGoals accomplished! 🐙 simpGoals accomplished! 🐙)] = a₁: αa₁::a₂: αa₂::as': List αas' := byGoals accomplished! 🐙 simpGoals accomplished! 🐙
this: [a₁] ++ dropLast (a₂ :: as') ++ [last (a₂ :: as') (_ : ¬a₂ :: as' = [])] = a₁ :: a₂ :: as'this ▸ h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])h₃ _: α_ _: α_ _: List α_ ih: motive (dropLast (a₂ :: as'))ih
termination_by _ as => as: List αas.length: {α : Type u_1} → List α → Natlength```

We use our new induction principle to prove that if `as.reverse = as`, then `Palindrome as` holds. Note that we use the `using` modifier to instruct the `induction` tactic to use this induction principle instead of the default one for lists.

```theorem List.palindrome_of_eq_reverse: ∀ {α : Type u_1} {as : List α}, reverse as = as → Palindrome asList.palindrome_of_eq_reverse (h: reverse as = ash : as: List ?m.9541as.reverse: {α : Type u_1} → List α → List αreverse = as: List ?m.9541as) : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.9541as := byGoals accomplished! 🐙
induction as: List α✝as using palindrome_ind: ∀ {α : Type u_1} (motive : List α → Prop),
motive [] →
(∀ (a : α), motive [a]) →
(∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive aspalindrome_indα✝: Type u_1h: reverse [] = []h₁Palindrome []α✝: Type u_1a✝: α✝h: reverse [a✝] = [a✝]h₂Palindrome [a✝]α✝: Type u_1a✝¹, b✝: α✝as✝: List α✝a✝: reverse as✝ = as✝ → Palindrome as✝h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]h₃Palindrome ([a✝¹] ++ as✝ ++ [b✝])
next   =>α✝: Type u_1h: reverse [] = []h₁Palindrome []α✝: Type u_1a✝: α✝h: reverse [a✝] = [a✝]h₂Palindrome [a✝]α✝: Type u_1a✝¹, b✝: α✝as✝: List α✝a✝: reverse as✝ = as✝ → Palindrome as✝h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]h₃Palindrome ([a✝¹] ++ as✝ ++ [b✝]) exact Palindrome.nil: ∀ {α : Type u_1}, Palindrome []Palindrome.nilGoals accomplished! 🐙
next a: α✝a =>α✝: Type u_1a✝: α✝h: reverse [a✝] = [a✝]h₂Palindrome [a✝]α✝: Type u_1a✝¹, b✝: α✝as✝: List α✝a✝: reverse as✝ = as✝ → Palindrome as✝h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]h₃Palindrome ([a✝¹] ++ as✝ ++ [b✝]) exact Palindrome.single: ∀ {α : Type u_1} (a : α), Palindrome [a]Palindrome.single a: α✝aGoals accomplished! 🐙
next a: α✝a b: α✝b as: List α✝as ih: reverse as = as → Palindrome asih =>α✝: Type u_1a✝¹, b✝: α✝as✝: List α✝a✝: reverse as✝ = as✝ → Palindrome as✝h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]h₃Palindrome ([a✝¹] ++ as✝ ++ [b✝])
have : a: α✝a = b: α✝b :=α✝: Type u_1a, b: α✝as: List α✝ih: reverse as = as → Palindrome ash: reverse ([a] ++ as ++ [b]) = [a] ++ as ++ [b]Palindrome ([a] ++ as ++ [b]) byGoals accomplished! 🐙 simp_allGoals accomplished! 🐙
subst this: a = bthisα✝: Type u_1a: α✝as: List α✝ih: reverse as = as → Palindrome ash: reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]Palindrome ([a] ++ as ++ [a])
have : as: List α✝as.reverse: {α : Type u_1} → List α → List αreverse = as: List α✝as :=α✝: Type u_1a: α✝as: List α✝ih: reverse as = as → Palindrome ash: reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]Palindrome ([a] ++ as ++ [a]) byGoals accomplished! 🐙 simp_allGoals accomplished! 🐙
exact Palindrome.sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])Palindrome.sandwich a: α✝a (ih: reverse as = as → Palindrome asih this: reverse as = asthis)Goals accomplished! 🐙```

We now define a function that returns `true` iff `as` is a palindrome. The function assumes that the type `α` has decidable equality. We need this assumption because we need to compare the list elements.

```def List.isPalindrome: {α : Type u_1} → [inst : DecidableEq α] → List α → BoolList.isPalindrome [DecidableEq: Type u_1 → Type u_1DecidableEq α: Type u_1α] (as: List αas : List: Type u_1 → Type u_1List α: Type u_1α) : Bool: TypeBool :=
as: List αas.reverse: {α : Type u_1} → List α → List αreverse = as: List αas```

It is straightforward to prove that `isPalindrome` is correct using the previously proved theorems.

```theorem List.isPalindrome_correct: ∀ {α : Type u_1} [inst : DecidableEq α] (as : List α), isPalindrome as = true ↔ Palindrome asList.isPalindrome_correct [DecidableEq: Type u_1 → Type u_1DecidableEq α: Type u_1α] (as: List αas : List: Type u_1 → Type u_1List α: Type u_1α) : as: List αas.isPalindrome: {α : Type u_1} → [inst : DecidableEq α] → List α → BoolisPalindrome ↔ Palindrome: {α : Type u_1} → List α → PropPalindrome as: List αas := byGoals accomplished! 🐙
simp [isPalindrome: {α : Type ?u.10468} → [inst : DecidableEq α] → List α → BoolisPalindrome]α: Type u_1inst✝: DecidableEq αas: List αreverse as = as ↔ Palindrome as
exact Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)Iff.intro (fun h: reverse as = ash => palindrome_of_eq_reverse: ∀ {α : Type u_1} {as : List α}, reverse as = as → Palindrome aspalindrome_of_eq_reverse h: reverse as = ash) (fun h: Palindrome ash => reverse_eq_of_palindrome: ∀ {α : Type u_1} {as : List α}, Palindrome as → reverse as = asreverse_eq_of_palindrome h: Palindrome ash)Goals accomplished! 🐙

#evaltrue
[1: Nat1, 2: Nat2, 1: Nat1].isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → BoolisPalindrome
#evalfalse
[1: Nat1, 2: Nat2, 3: Nat3, 1: Nat1].isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → BoolisPalindrome

example: List.isPalindrome [1, 2, 1] = trueexample : [1: Nat1, 2: Nat2, 1: Nat1].isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → BoolisPalindrome := rfl: ∀ {α : Type} {a : α}, a = arfl
example: List.isPalindrome [1, 2, 2, 1] = trueexample : [1: Nat1, 2: Nat2, 2: Nat2, 1: Nat1].isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → BoolisPalindrome := rfl: ∀ {α : Type} {a : α}, a = arfl
example: (!List.isPalindrome [1, 2, 3, 1]) = trueexample : ![1: Nat1, 2: Nat2, 3: Nat3, 1: Nat1].isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → BoolisPalindrome := rfl: ∀ {α : Type} {a : α}, a = arfl```