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.394
as) : Palindrome: {α : Type u_1} → List α → Prop
Palindrome as: List ?m.394
as.reverse: {α : Type u_1} → List α → List α
reverse := byGoals accomplished! 🐙
  induction h: Palindrome as
h withα✝: Type u_1
as: List α✝
h: Palindrome as
Palindrome as.reverse
  | nil: ∀ {α : Type u_1}, Palindrome []
nil =>α✝: Type u_1
as: 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_1
as: 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✝.reverse
ih =>α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: Palindrome as✝.reverse
sandwichPalindrome ([a] ++ as✝ ++ [a]).reverse simpα✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: Palindrome as✝.reverse
sandwichPalindrome (a :: (as✝.reverse ++ [a])); exact Palindrome.sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])
Palindrome.sandwich _: α✝
_ ih: Palindrome as✝.reverse
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 → as.reverse = as
reverse_eq_of_palindrome (h: Palindrome as
h : Palindrome: {α : Type u_1} → List α → Prop
Palindrome as: List ?m.661
as) : as: List ?m.661
as.reverse: {α : Type u_1} → List α → List α
reverse = as: List ?m.661
as := byGoals accomplished! 🐙
  induction h: Palindrome as
h withα✝: Type u_1
as: List α✝
h: Palindrome as
as.reverse = as
  | nil: ∀ {α : Type u_1}, Palindrome []
nil =>α✝: Type u_1
as: List α✝
nil[].reverse = [] rflGoals accomplished! 🐙
  | single: ∀ {α : Type u_1} (a : α), Palindrome [a]
single a: α✝
a =>α✝: Type u_1
as: 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_1
as, 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_1
as, 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_1
as, 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.reverse
example (h: Palindrome as
h : Palindrome: {α : Type u_1} → List α → Prop
Palindrome as: List ?m.903
as) : Palindrome: {α : Type u_1} → List α → Prop
Palindrome as: List ?m.903
as.reverse: {α : Type u_1} → List α → List α
reverse := byGoals accomplished! 🐙
  simp [reverse_eq_of_palindrome: ∀ {α : Type ?u.899} {as : List α}, Palindrome as → as.reverse = as
reverse_eq_of_palindrome h: Palindrome as
h, h: Palindrome as
h]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 (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] = as
List.dropLast_append_last (h: as ≠ []
h : as: List ?m.1443
as ≠ []: List ?m.1443
[]) : as: List ?m.1443
as.dropLast: {α : Type u_1} → List α → List α
dropLast ++ [as: List ?m.1443
as.last: {α : Type u_1} → (as : List α) → as ≠ [] → α
last h: as ≠ []
h] = as: List ?m.1443
as := byGoals accomplished! 🐙
  match as: List α✝
as withα✝: Type u_1
as: List α✝
h: as ≠ []
as.dropLast ++ [as.last h] = as
  | [] =>α✝: Type u_1
as: List α✝
h: [] ≠ []
[].dropLast ++ [[].last h] = [] contradictionGoals accomplished! 🐙
  | [a: α✝
a] =>α✝: Type u_1
as: List α✝
a: α✝
h: [a] ≠ []
[a].dropLast ++ [[a].last h] = [a] simp_all [last: {α : Type ?u.1743} → (as : List α) → as ≠ [] → α
last, dropLast: {α : Type ?u.2176} → List α → List α
dropLast]Goals accomplished! 🐙
  | a₁: α✝
a₁ :: a₂: α✝
a₂ :: as: List α✝
as =>α✝: 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
    simp [last: {α : Type ?u.2254} → (as : List α) → as ≠ [] → α
last, dropLast: {α : Type ?u.2272} → List α → List α
dropLast]α✝: Type u_1
as✝: 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] = as
dropLast_append_last (as := a₂: α✝
a₂ :: as: List α✝
as) (α✝: Type u_1
as✝: 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 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 (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').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.5450
as.reverse: {α : Type u_1} → List α → List α
reverse = as: List ?m.5450
as) : Palindrome: {α : Type u_1} → List α → Prop
Palindrome as: List ?m.5450
as := 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 as
palindrome_indα✝: Type u_1
h: [].reverse = []
h₁Palindrome []
α✝: 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✝]
h₃Palindrome ([a✝¹] ++ as✝ ++ [b✝])
  next   =>α✝: Type u_1
h: [].reverse = []
h₁Palindrome []
α✝: 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✝]
h₃Palindrome ([a✝¹] ++ as✝ ++ [b✝]) exact Palindrome.nil: ∀ {α : Type u_1}, Palindrome []
Palindrome.nilGoals accomplished! 🐙
  next a: α✝
a =>α✝: 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✝]
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 as
ih =>α✝: 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✝])
    have : a: α✝
a = b: α✝
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]) byGoals accomplished! 🐙 simp_allGoals accomplished! 🐙
    subst this: a = b
thisα✝: Type u_1
a: α✝
as: List α✝
ih: as.reverse = as → Palindrome as
h: ([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_1
a: α✝
as: List α✝
ih: as.reverse = as → Palindrome as
h: ([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 as
ih this: as.reverse = as
this)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 α), as.isPalindrome = 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 := byGoals accomplished! 🐙
  simp [isPalindrome: {α : Type ?u.6472} → [inst : DecidableEq α] → List α → Bool
isPalindrome]α: Type u_1
inst✝: 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 = as
h => palindrome_of_eq_reverse: ∀ {α : Type u_1} {as : List α}, as.reverse = as → Palindrome as
palindrome_of_eq_reverse h: as.reverse = as
h) (fun h: Palindrome as
h => reverse_eq_of_palindrome: ∀ {α : Type u_1} {as : List α}, Palindrome as → as.reverse = as
reverse_eq_of_palindrome h: Palindrome as
h)Goals accomplished! 🐙

#evaltrue
 [1: Nat
1, 2: Nat
2, 1: Nat
1].isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome
#evalfalse
 [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

Lean Manual

Palindromes