# 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 as.reversepalindrome_reverse (h: Palindrome ash : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.401as) : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.401as.reverse: {α : Type u_1} → List α → List αreverse := byGoals accomplished! 🐙
induction h: Palindrome ash withα✝: Type u_1as: List α✝h: Palindrome asPalindrome as.reverse
| nil: ∀ {α : Type u_1}, Palindrome []nil =>α✝: Type u_1as: List α✝nilPalindrome [].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 [a].reverse 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 as✝.reverseih =>α✝: Type u_1as, as✝: List α✝a: α✝h: Palindrome as✝ih: Palindrome as✝.reversesandwichPalindrome ([a] ++ as✝ ++ [a]).reverse simpα✝: Type u_1as, as✝: List α✝a: α✝h: Palindrome as✝ih: Palindrome as✝.reversesandwichPalindrome (a :: (as✝.reverse ++ [a])); exact Palindrome.sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])Palindrome.sandwich _: α✝_ ih: Palindrome as✝.reverseihGoals 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 → as.reverse = asreverse_eq_of_palindrome (h: Palindrome ash : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.667as) : as: List ?m.667as.reverse: {α : Type u_1} → List α → List αreverse = as: List ?m.667as := byGoals accomplished! 🐙
induction h: Palindrome ash withα✝: Type u_1as: List α✝h: Palindrome asas.reverse = as
| nil: ∀ {α : Type u_1}, Palindrome []nil =>α✝: Type u_1as: List α✝nil[].reverse = [] rflGoals accomplished! 🐙
| single: ∀ {α : Type u_1} (a : α), Palindrome [a]single a: α✝a =>α✝: Type u_1as: List α✝a: α✝single[a].reverse = [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: as✝.reverse = as✝sandwich([a] ++ as✝ ++ [a]).reverse = [a] ++ as✝ ++ [a] h: Palindrome as✝hWarning: unused variable `h`
note: this linter can be disabled with `set_option linter.unusedVariables false`α✝: Type u_1as, as✝: List α✝a: α✝h: Palindrome as✝ih: as✝.reverse = as✝sandwich([a] ++ as✝ ++ [a]).reverse = [a] ++ as✝ ++ [a] ih: as✝.reverse = as✝ih: as✝.reverse = as✝ih =>α✝: Type u_1as, as✝: List α✝a: α✝h: Palindrome as✝ih: as✝.reverse = as✝sandwich([a] ++ as✝ ++ [a]).reverse = [a] ++ as✝ ++ [a] simp [ih: as✝.reverse = 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 as.reverseexample (h: Palindrome ash : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.908as) : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.908as.reverse: {α : Type u_1} → List α → List αreverse := byGoals accomplished! 🐙
simp [reverse_eq_of_palindrome: ∀ {α : Type u_1} {as : List α}, Palindrome as → as.reverse = 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 ≠ []), as.dropLast ++ [as.last h] = asList.dropLast_append_last (h: as ≠ []h : as: List ?m.1461as ≠ []: List ?m.1461[]) : as: List ?m.1461as.dropLast: {α : Type u_1} → List α → List αdropLast ++ [as: List ?m.1461as.last: {α : Type u_1} → (as : List α) → as ≠ [] → αlast h: as ≠ []h] = as: List ?m.1461as := byGoals accomplished! 🐙
match as: List α✝as withα✝: Type u_1as: List α✝h: as ≠ []as.dropLast ++ [as.last h] = as
| [] =>α✝: Type u_1as: List α✝h: [] ≠ [][].dropLast ++ [[].last h] = [] contradictionGoals accomplished! 🐙
| [a: α✝a] =>α✝: Type u_1as: List α✝a: α✝h: [a] ≠ [][a].dropLast ++ [[a].last h] = [a] simp_all [last: {α : Type ?u.1760} → (as : List α) → as ≠ [] → αlast, dropLast: {α : Type ?u.2193} → List α → List αdropLast]Goals accomplished! 🐙
| a₁: α✝a₁ :: a₂: α✝a₂ :: as: List α✝as =>α✝: Type u_1as✝: List α✝a₁, a₂: α✝as: List α✝h: a₁ :: a₂ :: as ≠ [](a₁ :: a₂ :: as).dropLast ++ [(a₁ :: a₂ :: as).last h] = a₁ :: a₂ :: as
simp [last: {α : Type ?u.2271} → (as : List α) → as ≠ [] → αlast, dropLast: {α : Type ?u.2289} → List α → List αdropLast]α✝: Type u_1as✝: List α✝a₁, a₂: α✝as: List α✝h: a₁ :: a₂ :: as ≠ [](a₂ :: as).dropLast ++ [(a₂ :: as).last ⋯] = a₂ :: as
exact dropLast_append_last: ∀ {α : Type u_1} {as : List α} (h : as ≠ []), as.dropLast ++ [as.last h] = asdropLast_append_last (as := a₂: α✝a₂ :: as: List α✝as) (α✝: Type u_1as✝: List α✝a₁, a₂: α✝as: List α✝h: a₁ :: a₂ :: as ≠ [](a₂ :: as).dropLast ++ [(a₂ :: as).last ⋯] = 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 (a₂ :: as').dropLastih := 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₁] ++ (a₂ :: as').dropLast ++ [(a₂ :: as').last ⋯] = a₁ :: a₂ :: as'this ▸ h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])h₃ _: α_ _: α_ _: List α_ ih: motive (a₂ :: as').dropLastih
termination_by 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 α}, as.reverse = as → Palindrome asList.palindrome_of_eq_reverse (h: as.reverse = ash : as: List ?m.5484as.reverse: {α : Type u_1} → List α → List αreverse = as: List ?m.5484as) : Palindrome: {α : Type u_1} → List α → PropPalindrome as: List ?m.5484as := 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: [a✝].reverse = [a✝]h₂Palindrome [a✝]α✝: Type u_1a✝¹, b✝: α✝as✝: List α✝a✝: as✝.reverse = as✝ → Palindrome as✝h: ([a✝¹] ++ as✝ ++ [b✝]).reverse = [a✝¹] ++ as✝ ++ [b✝]h₃Palindrome ([a✝¹] ++ as✝ ++ [b✝])
next   =>α✝: Type u_1h: [].reverse = []h₁Palindrome []α✝: Type u_1a✝: α✝h: [a✝].reverse = [a✝]h₂Palindrome [a✝]α✝: Type u_1a✝¹, b✝: α✝as✝: List α✝a✝: as✝.reverse = as✝ → Palindrome as✝h: ([a✝¹] ++ as✝ ++ [b✝]).reverse = [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: [a✝].reverse = [a✝]h₂Palindrome [a✝]α✝: Type u_1a✝¹, b✝: α✝as✝: List α✝a✝: as✝.reverse = as✝ → Palindrome as✝h: ([a✝¹] ++ as✝ ++ [b✝]).reverse = [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: as.reverse = as → Palindrome asih =>α✝: Type u_1a✝¹, b✝: α✝as✝: List α✝a✝: as✝.reverse = as✝ → Palindrome as✝h: ([a✝¹] ++ as✝ ++ [b✝]).reverse = [a✝¹] ++ as✝ ++ [b✝]h₃Palindrome ([a✝¹] ++ as✝ ++ [b✝])
have : a: α✝a = b: α✝b :=α✝: Type u_1a, b: α✝as: List α✝ih: as.reverse = as → Palindrome ash: ([a] ++ as ++ [b]).reverse = [a] ++ as ++ [b]Palindrome ([a] ++ as ++ [b]) byGoals accomplished! 🐙 simp_allGoals accomplished! 🐙
subst this: a = bthisα✝: Type u_1a: α✝as: List α✝ih: as.reverse = as → Palindrome ash: ([a] ++ as ++ [a]).reverse = [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: as.reverse = as → Palindrome ash: ([a] ++ as ++ [a]).reverse = [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: as.reverse = as → Palindrome asih this: as.reverse = 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 α), as.isPalindrome = 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.6528} → [inst : DecidableEq α] → List α → BoolisPalindrome]α: Type u_1inst✝: DecidableEq αas: List αas.reverse = as ↔ Palindrome as
exact Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)Iff.intro (fun h: as.reverse = ash => palindrome_of_eq_reverse: ∀ {α : Type u_1} {as : List α}, as.reverse = as → Palindrome aspalindrome_of_eq_reverse h: as.reverse = ash) (fun h: Palindrome ash => reverse_eq_of_palindrome: ∀ {α : Type u_1} {as : List α}, Palindrome as → as.reverse = 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: [1, 2, 1].isPalindrome = trueexample : [1: Nat1, 2: Nat2, 1: Nat1].isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → BoolisPalindrome := rfl: ∀ {α : Type} {a : α}, a = arfl
example: [1, 2, 2, 1].isPalindrome = trueexample : [1: Nat1, 2: Nat2, 2: Nat2, 1: Nat1].isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → BoolisPalindrome := rfl: ∀ {α : Type} {a : α}, a = arfl
example: (![1, 2, 3, 1].isPalindrome) = trueexample : ![1: Nat1, 2: Nat2, 3: Nat3, 1: Nat1].isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → BoolisPalindrome := rfl: ∀ {α : Type} {a : α}, a = arfl```