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

Goals accomplished! 🐙
α✝: Type u_1
as: List α
h: Palindrome as

Palindrome as.reverse

Goals accomplished! 🐙

Goals accomplished! 🐙

Goals accomplished! 🐙

Goals accomplished! 🐙

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

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

Goals accomplished! 🐙
α✝: Type u_1
as: List α
h: Palindrome as

as.reverse = as

Goals accomplished! 🐙

Goals accomplished! 🐙

Goals accomplished! 🐙

Goals accomplished! 🐙

Goals accomplished! 🐙

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

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.

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
(

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

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

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

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

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

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

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

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

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

(a₂ :: as).dropLast ++ [(a₂ :: as).last ] = a₂ :: as

Goals 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.

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 (a₂ :: as').dropLast
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
(

Goals accomplished! 🐙

Goals accomplished! 🐙
)] =
a₁: α
a₁
::
a₂: α
a₂
::
as': List α
as'
:=

Goals accomplished! 🐙

Goals 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').dropLast
ih
termination_by
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 α}, as.reverse = as → Palindrome as
List.palindrome_of_eq_reverse
(
h: as.reverse = as
h
:
as: List ?m.5832
as
.
reverse: {α : Type u_1} → List α → List α
reverse
=
as: List ?m.5832
as
) :
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List ?m.5832
as
:=

Goals accomplished! 🐙
α✝: Type u_1
h: [].reverse = []

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

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

Goals accomplished! 🐙
α✝: Type u_1
a✝: α
h: [a].reverse = [a]

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

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

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

Palindrome ([a] ++ as ++ [b])

Goals accomplished! 🐙

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

Palindrome ([a] ++ as ++ [a])
α✝: Type u_1
a: α
as: List α
ih: as.reverse = as Palindrome as
h: ([a] ++ as ++ [a]).reverse = [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 (max 0 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 α), as.isPalindrome = true ↔ Palindrome as
List.isPalindrome_correct
[
DecidableEq: Type u_1 → Type (max 0 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
:=

Goals accomplished! 🐙
α: Type u_1
inst✝: DecidableEq α
as: List α

as.reverse = 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: [1, 2, 1].isPalindrome = 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: [1, 2, 2, 1].isPalindrome = 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: (![1, 2, 3, 1].isPalindrome) = 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