# 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 α → Prop

Palindrome : `List`**: **Type u_1 → Type u_1

List `α`**: **Type u_1

α → `Prop`**: **Type

Prop where
| `nil`**: **∀ {α : Type u_1}, Palindrome []

nil : `Palindrome`**: **{α : Type u_1} → List α → Prop

Palindrome `[]`**: **List ?m.17

[]
| `single`**: **∀ {α : Type u_1} (a : α), Palindrome [a]

single : (`a`**: **α

a : `α`**: **Type u_1

α) → `Palindrome`**: **{α : Type u_1} → List α → Prop

Palindrome [`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 α → Prop

Palindrome `as`**: **List α

as → `Palindrome`**: **{α : Type u_1} → List α → Prop

Palindrome ([`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`

.

theorempalindrome_reverse (palindrome_reverse:∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)h :h:Palindrome asPalindromePalindrome:{α : Type u_1} → List α → Propas) :as:List ?m.394PalindromePalindrome:{α : Type u_1} → List α → Propas.as:List ?m.394reverse :=reverse:{α : Type u_1} → List α → List αGoals accomplished! 🐙α✝:Type u_1as:List α✝h:Palindrome asPalindrome (List.reverse as)α✝:Type u_1as:List α✝

nilPalindrome (List.reverse [])Goals accomplished! 🐙α✝:Type u_1as:List α✝a:α✝

singlePalindrome (List.reverse [a])Goals accomplished! 🐙α✝:Type u_1as, as✝:List α✝a:α✝h:Palindrome as✝ih:Palindrome (List.reverse as✝)

sandwichPalindrome (List.reverse ([a] ++ as✝ ++ [a]));α✝:Type u_1as, as✝:List α✝a:α✝h:Palindrome as✝ih:Palindrome (List.reverse as✝)

sandwichPalindrome (a :: (List.reverse as✝ ++ [a]))Goals accomplished! 🐙

If a list `as`

is a palindrome, then the reverse of `as`

is equal to itself.

theoremreverse_eq_of_palindrome (reverse_eq_of_palindrome:∀ {α : Type u_1} {as : List α}, Palindrome as → List.reverse as = ash :h:Palindrome asPalindromePalindrome:{α : Type u_1} → List α → Propas) :as:List ?m.707as.as:List ?m.707reverse =reverse:{α : Type u_1} → List α → List αas :=as:List ?m.707Goals accomplished! 🐙α✝:Type u_1as:List α✝h:Palindrome asList.reverse as = asα✝:Type u_1as:List α✝

nilList.reverse [] = []Goals accomplished! 🐙α✝:Type u_1as:List α✝a:α✝

singleList.reverse [a] = [a]Goals accomplished! 🐙α✝:Type u_1as, as✝:List α✝a:α✝h:Palindrome as✝ih:List.reverse as✝ = as✝

sandwichList.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a]α✝: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✝α✝:Type u_1as, as✝:List α✝a:α✝h:Palindrome as✝ih:List.reverse as✝ = as✝

sandwichList.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a]Goals accomplished! 🐙

Note that you can also easily prove `palindrome_reverse`

using `reverse_eq_of_palindrome`

.

example (example:∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)h :h:Palindrome asPalindromePalindrome:{α : Type u_1} → List α → Propas) :as:List ?m.985PalindromePalindrome:{α : Type u_1} → List α → Propas.as:List ?m.985reverse :=reverse:{α : Type u_1} → List α → List αGoals accomplished! 🐙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.

defList.last : (List.last:{α : Type u_1} → (as : List α) → as ≠ [] → αas :as:List αListList:Type u_1 → Type u_1α) →α:Type u_1as ≠as:List α[] →[]:List αα | [α:Type u_1a], _ =>a:αa | _::a:αa₂::a₂:αas, _ => (as:List αa₂::a₂:αas).as:List αlast (last:{α : Type u_1} → (as : List α) → as ≠ [] → αGoals accomplished! 🐙)Goals 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] theoremList.dropLast_append_last (List.dropLast_append_last:∀ {α : Type u_1} {as : List α} (h : as ≠ []), dropLast as ++ [last as h] = ash :h:as ≠ []as ≠as:List ?m.1537[]) :[]:List ?m.1537as.as:List ?m.1537dropLast ++ [dropLast:{α : Type u_1} → List α → List αas.as:List ?m.1537lastlast:{α : Type u_1} → (as : List α) → as ≠ [] → αh] =h:as ≠ []as :=as:List ?m.1537Goals accomplished! 🐙α✝:Type u_1as:List α✝h:as ≠ []dropLast as ++ [last as h] = asα✝:Type u_1as:List α✝h:[] ≠ []dropLast [] ++ [last [] h] = []Goals accomplished! 🐙α✝:Type u_1as:List α✝a:α✝h:[a] ≠ []dropLast [a] ++ [last [a] h] = [a]Goals accomplished! 🐙α✝:Type u_1as✝:List α✝a₁, a₂:α✝as:List α✝h:a₁ :: a₂ :: as ≠ []dropLast (a₁ :: a₂ :: as) ++ [last (a₁ :: a₂ :: as) h] = a₁ :: a₂ :: asα✝:Type u_1as✝:List α✝a₁, a₂:α✝as:List α✝h:a₁ :: a₂ :: as ≠ []dropLast (a₂ :: as) ++ [last (a₂ :: as) ⋯] = a₂ :: asα✝:Type u_1as✝:List α✝a₁, a₂:α✝as:List α✝h:a₁ :: a₂ :: as ≠ []dropLast (a₂ :: as) ++ [last (a₂ :: as) ⋯] = a₂ :: asGoals accomplished! 🐙Goals 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.

theoremList.palindrome_ind (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 asmotive :motive:List α → PropListList:Type u_1 → Type u_1α →α:Type u_1Prop) (Prop:Typeh₁ :h₁:motive []motivemotive:List α → Prop[]) ([]:List αh₂ : (h₂:∀ (a : α), motive [a]a :a:αα) →α:Type u_1motive [motive:List α → Propa]) (a:αh₃ : (h₃:∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])aa:αb :b:αα) → (α:Type u_1as :as:List αListList:Type u_1 → Type u_1α) →α:Type u_1motivemotive:List α → Propas →as:List αmotive ([motive:List α → Propa] ++a:αas ++ [as:List αb])) (b:αas :as:List αListList:Type u_1 → Type u_1α) :α:Type u_1motivemotive:List α → Propas := matchas:List αas with | [] =>as:List αh₁ | [h₁:motive []a] =>a:αh₂h₂:∀ (a : α), motive [a]a |a:αa₁::a₁:αa₂::a₂:αas' => haveas':List αih :=ih:motive (dropLast (a₂ :: as'))palindrome_indpalindrome_ind:∀ {α : Type u_1} (motive : List α → Prop), motive [] → (∀ (a : α), motive [a]) → (∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive asmotivemotive:List α → Proph₁h₁:motive []h₂h₂:∀ (a : α), motive [a]h₃ (h₃:∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])a₂::a₂:αas').as':List αdropLast have : [dropLast:{α : Type u_1} → List α → List αa₁] ++ (a₁:αa₂::a₂:αas').as':List αdropLast ++ [(dropLast:{α : Type u_1} → List α → List αa₂::a₂:αas').as':List αlast (last:{α : Type u_1} → (as : List α) → as ≠ [] → αGoals accomplished! 🐙)] =Goals accomplished! 🐙a₁::a₁:αa₂::a₂:αas' :=as':List αGoals accomplished! 🐙Goals accomplished! 🐙this ▸this:[a₁] ++ dropLast (a₂ :: as') ++ [last (a₂ :: as') ⋯] = a₁ :: a₂ :: as'h₃h₃:∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])__:α__:α__:List αih termination_byih:motive (dropLast (a₂ :: as'))as.as:List αlengthlength:{α : Type u_1} → List α → Nat

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.

theoremList.palindrome_of_eq_reverse (List.palindrome_of_eq_reverse:∀ {α : Type u_1} {as : List α}, reverse as = as → Palindrome ash :h:reverse as = asas.as:List ?m.10234reverse =reverse:{α : Type u_1} → List α → List αas) :as:List ?m.10234PalindromePalindrome:{α : Type u_1} → List α → Propas :=as:List ?m.10234Goals accomplished! 🐙α✝:Type u_1h:reverse [] = []

h₁Palindrome []α✝:Type u_1a✝:α✝h:reverse [a✝] = [a✝]Palindrome [a✝]α✝:Type u_1a✝¹, b✝:α✝as✝:List α✝a✝:reverse as✝ = as✝ → Palindrome as✝h:reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]Palindrome ([a✝¹] ++ as✝ ++ [b✝])α✝:Type u_1h:reverse [] = []

h₁Palindrome []α✝:Type u_1a✝:α✝h:reverse [a✝] = [a✝]Palindrome [a✝]α✝:Type u_1a✝¹, b✝:α✝as✝:List α✝a✝:reverse as✝ = as✝ → Palindrome as✝h:reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]Palindrome ([a✝¹] ++ as✝ ++ [b✝])Goals accomplished! 🐙α✝: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✝]Palindrome ([a✝¹] ++ as✝ ++ [b✝])Goals accomplished! 🐙α✝: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✝])α✝:Type u_1a, b:α✝as:List α✝ih:reverse as = as → Palindrome ash:reverse ([a] ++ as ++ [b]) = [a] ++ as ++ [b]Palindrome ([a] ++ as ++ [b])Goals accomplished! 🐙Goals accomplished! 🐙α✝:Type u_1a:α✝as:List α✝ih:reverse as = as → Palindrome ash:reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]Palindrome ([a] ++ as ++ [a])α✝:Type u_1a:α✝as:List α✝ih:reverse as = as → Palindrome ash:reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]Palindrome ([a] ++ as ++ [a])Goals accomplished! 🐙Goals accomplished! 🐙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 α → Bool

List.isPalindrome [`DecidableEq`**: **Type u_1 → Type u_1

DecidableEq `α`**: **Type u_1

α] (`as`**: **List α

as : `List`**: **Type u_1 → Type u_1

List `α`**: **Type u_1

α) : `Bool`**: **Type

Bool :=
`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.

theoremList.isPalindrome_correct [List.isPalindrome_correct:∀ {α : Type u_1} [inst : DecidableEq α] (as : List α), isPalindrome as = true ↔ Palindrome asDecidableEqDecidableEq:Type u_1 → Type u_1α] (α:Type u_1as :as:List αListList:Type u_1 → Type u_1α) :α:Type u_1as.as:List αisPalindrome ↔isPalindrome:{α : Type u_1} → [inst : DecidableEq α] → List α → BoolPalindromePalindrome:{α : Type u_1} → List α → Propas :=as:List αGoals accomplished! 🐙α:Type u_1inst✝:DecidableEq αas:List αreverse as = as ↔ Palindrome asGoals accomplished! 🐙[1,1:Nat2,2:Nat1].1:NatisPalindromeisPalindrome:{α : Type} → [inst : DecidableEq α] → List α → Bool[1,1:Nat2,2:Nat3,3:Nat1].1:NatisPalindromeisPalindrome:{α : Type} → [inst : DecidableEq α] → List α → Boolexample : [example:List.isPalindrome [1, 2, 1] = true1,1:Nat2,2:Nat1].1:NatisPalindrome :=isPalindrome:{α : Type} → [inst : DecidableEq α] → List α → Boolrflrfl:∀ {α : Type} {a : α}, a = aexample : [example:List.isPalindrome [1, 2, 2, 1] = true1,1:Nat2,2:Nat2,2:Nat1].1:NatisPalindrome :=isPalindrome:{α : Type} → [inst : DecidableEq α] → List α → Boolrflrfl:∀ {α : Type} {a : α}, a = aexample : ![example:(!List.isPalindrome [1, 2, 3, 1]) = true1,1:Nat2,2:Nat3,3:Nat1].1:NatisPalindrome :=isPalindrome:{α : Type} → [inst : DecidableEq α] → List α → Boolrflrfl:∀ {α : Type} {a : α}, a = a