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.

theorem 
palindrome_reverse: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)
palindrome_reverse
(
h: Palindrome as
h
:
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List ?m.594
as
) :
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List ?m.594
as
.
reverse: {α : Type u_1} → List α → List α
reverse
:=
α✝: Type u_1
as: List α
h: Palindrome as

Palindrome (List.reverse as)
α✝: Type u_1
as: List α
h: Palindrome as

Palindrome (List.reverse as)
α✝: Type u_1
as: List α

nil
Palindrome (List.reverse [])

Goals accomplished! 🐙
α✝: Type u_1
as: List α
a: α

single
Palindrome (List.reverse [a])

Goals accomplished! 🐙
α✝: Type u_1
as, as✝: List α
a: α
h: Palindrome as
ih: Palindrome (List.reverse as)

sandwich
Palindrome (List.reverse ([a] ++ as ++ [a]))
α✝: Type u_1
as, as✝: List α
a: α
h: Palindrome as
ih: Palindrome (List.reverse as)

sandwich
Palindrome (a :: (List.reverse as ++ [a]))
;

Goals 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 = as
reverse_eq_of_palindrome
(
h: Palindrome as
h
:
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List ?m.919
as
) :
as: List ?m.919
as
.
reverse: {α : Type u_1} → List α → List α
reverse
=
as: List ?m.919
as
:=
α✝: Type u_1
as: List α
h: Palindrome as

List.reverse as = as
α✝: Type u_1
as: List α
h: Palindrome as

List.reverse as = as
α✝: Type u_1
as: List α

nil
List.reverse [] = []

Goals accomplished! 🐙
α✝: Type u_1
as: List α
a: α

single
List.reverse [a] = [a]

Goals accomplished! 🐙
α✝: Type u_1
as, as✝: List α
a: α
h: Palindrome as
ih: List.reverse as = as

sandwich
List.reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]
Warning: unused variable `h` [linter.unusedVariables]
α✝: Type u_1
as, as✝: List α
a: α
h: Palindrome as
ih: List.reverse as = as

sandwich
List.reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]
ih: List.reverse as✝ = as✝
α✝: Type u_1
as, as✝: List α
a: α
h: Palindrome as
ih: List.reverse as = as

sandwich
List.reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]

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 as
h
:
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List ?m.1195
as
) :
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List ?m.1195
as
.
reverse: {α : Type u_1} → List α → List α
reverse
:=
α✝: Type ?u.1191
as: List α
h: Palindrome as

Palindrome (List.reverse as)

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_1
List
α: 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
(
α: Type ?u.1243
head✝, a₂: α
as: List α
x✝: head :: a₂ :: as []

a₂ :: as []

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] theorem 
List.dropLast_append_last: ∀ {α : Type u_1} {as : List α} (h : as ≠ []), dropLast as ++ [last as h] = as
List.dropLast_append_last
(
h: as ≠ []
h
:
as: List ?m.1956
as
[]: List ?m.1956
[]
) :
as: List ?m.1956
as
.
dropLast: {α : Type u_1} → List α → List α
dropLast
++ [
as: List ?m.1956
as
.
last: {α : Type u_1} → (as : List α) → as ≠ [] → α
last
h: as ≠ []
h
] =
as: List ?m.1956
as
:=
α✝: Type u_1
as: List α
h: as []

dropLast as ++ [last as h] = as
α✝: Type u_1
as: List α
h: as []

dropLast as ++ [last as h] = as
α✝: Type u_1
as: List α
h: [] []

dropLast [] ++ [last [] h] = []

Goals accomplished! 🐙
α✝: Type u_1
as: List α
a: α
h: [a] []

dropLast [a] ++ [last [a] h] = [a]

Goals accomplished! 🐙
α✝: Type u_1
as✝: List α
a₁, a₂: α
as: List α
h: a₁ :: a₂ :: as []

dropLast (a₁ :: a₂ :: as) ++ [last (a₁ :: a₂ :: as) h] = a₁ :: a₂ :: as
α✝: Type u_1
as✝: List α
a₁, a₂: α
as: List α
h: a₁ :: a₂ :: as []

dropLast (a₂ :: as) ++ [last (a₂ :: as) (_ : ¬a₂ :: as = [])] = a₂ :: as
α✝: Type u_1
as✝: List α
a₁, a₂: α
as: List α
h: a₁ :: a₂ :: as []

dropLast (a₂ :: as) ++ [last (a₂ :: as) (_ : ¬a₂ :: as = [])] = a₂ :: as
α✝: Type u_1
as✝: List α
a₁, a₂: α
as: List α
h: a₁ :: a₂ :: as []

a₂ :: as []

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.

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 as
List.palindrome_ind
(
motive: List α → Prop
motive
:
List: Type u_1 → Type u_1
List
α: Type u_1
α
Prop: Type
Prop
) (
h₁: motive []
h₁
:
motive: List α → Prop
motive
[]: List α
[]
) (
h₂: ∀ (a : α), motive [a]
h₂
: (
a: α
a
:
α: Type u_1
α
)
motive: List α → Prop
motive
[
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_1
List
α: Type u_1
α
)
motive: List α → Prop
motive
as: List α
as
motive: List α → Prop
motive
([
a: α
a
] ++
as: List α
as
++ [
b: α
b
])) (
as: List α
as
:
List: Type u_1 → Type u_1
List
α: Type u_1
α
) :
motive: List α → Prop
motive
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 as
palindrome_ind
motive: List α → Prop
motive
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
(
α: Type u_1
motive: List α Prop
h₁: motive []
h₂: (a : α), motive [a]
h₃: (a b : α) (as : List α), motive as motive ([a] ++ as ++ [b])
as: List α
a₁, a₂: α
as': List α
ih: motive (dropLast (a₂ :: as'))

a₂ :: as' []

Goals accomplished! 🐙
)] =
a₁: α
a₁
::
a₂: α
a₂
::
as': List α
as'
:=
α: Type u_1
motive: List α Prop
h₁: motive []
h₂: (a : α), motive [a]
h₃: (a b : α) (as : List α), motive as motive ([a] ++ as ++ [b])
as: List α
a₁, a₂: α
as': List α
ih: motive (dropLast (a₂ :: as'))

[a₁] ++ dropLast (a₂ :: as') ++ [last (a₂ :: as') (_ : ¬a₂ :: as' = [])] = a₁ :: a₂ :: as'

Goals 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 α → Nat
length

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 as
List.palindrome_of_eq_reverse
(
h: reverse as = as
h
:
as: List ?m.9527
as
.
reverse: {α : Type u_1} → List α → List α
reverse
=
as: List ?m.9527
as
) :
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List ?m.9527
as
:=
α✝: Type u_1
as: List α
h: reverse as = as

Palindrome as
α✝: Type u_1
h: reverse [] = []

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

h₁
Palindrome []
α✝: Type u_1
a✝: α
h: reverse [a] = [a]
Palindrome [a]
α✝: Type u_1
a✝¹, 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_1
a✝: α
h: reverse [a] = [a]

h₂
Palindrome [a]
α✝: Type u_1
a✝¹, 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_1
a✝¹, b✝: α
as✝: List α
a✝: reverse as = as Palindrome as
h: reverse ([a✝¹] ++ as ++ [b]) = [a✝¹] ++ as ++ [b]

h₃
Palindrome ([a✝¹] ++ as ++ [b])
α✝: Type u_1
a, b: α
as: List α
ih: reverse as = as Palindrome as
h: reverse ([a] ++ as ++ [b]) = [a] ++ as ++ [b]

Palindrome ([a] ++ as ++ [b])
α✝: Type u_1
a, b: α
as: List α
ih: reverse as = as Palindrome as
h: reverse ([a] ++ as ++ [b]) = [a] ++ as ++ [b]

a = b

Goals accomplished! 🐙
α✝: Type u_1
a: α
as: List α
ih: reverse as = as Palindrome as
h: reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]

Palindrome ([a] ++ as ++ [a])
α✝: Type u_1
a: α
as: List α
ih: reverse as = as Palindrome as
h: reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]

Palindrome ([a] ++ as ++ [a])
α✝: Type u_1
a: α
as: List α
ih: reverse as = as Palindrome as
h: reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]

reverse as = as

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.

theorem 
List.isPalindrome_correct: ∀ {α : Type u_1} [inst : DecidableEq α] (as : List α), isPalindrome as = true ↔ Palindrome as
List.isPalindrome_correct
[
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
α
) :
as: List α
as
.
isPalindrome: {α : Type u_1} → [inst : DecidableEq α] → List α → Bool
isPalindrome
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List α
as
:=
α: Type u_1
inst✝: DecidableEq α
as: List α

isPalindrome as = true Palindrome as
α: Type u_1
inst✝: DecidableEq α
as: List α

reverse as = as Palindrome as

Goals accomplished! 🐙
true
[
1: Nat
1
,
2: Nat
2
,
1: Nat
1
].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome
false
[
1: Nat
1
,
2: Nat
2
,
3: Nat
3
,
1: Nat
1
].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome
example: List.isPalindrome [1, 2, 1] = true
example
: [
1: Nat
1
,
2: Nat
2
,
1: Nat
1
].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome
:=
rfl: ∀ {α : Type} {a : α}, a = a
rfl
example: List.isPalindrome [1, 2, 2, 1] = true
example
: [
1: Nat
1
,
2: Nat
2
,
2: Nat
2
,
1: Nat
1
].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome
:=
rfl: ∀ {α : Type} {a : α}, a = a
rfl
example: (!List.isPalindrome [1, 2, 3, 1]) = true
example
: ![
1: Nat
1
,
2: Nat
2
,
3: Nat
3
,
1: Nat
1
].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome
:=
rfl: ∀ {α : Type} {a : α}, a = a
rfl