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 : List α → Prop where
  | nil      : Palindrome []
  | single   : (a : α) → Palindrome [a]
  | sandwich : (a : α) → Palindrome as → Palindrome ([a] ++ as ++ [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 (h : Palindrome as) : Palindrome as.reverse := byα✝:Type u_1as:List α✝h:Palindrome as⊢ Palindrome as.reverse
  induction h with
  | nil => exact Palindrome.nilAll goals completed! 🐙
  | single a => exact Palindrome.single aAll goals completed! 🐙
  | sandwich a h ih => simpsandwichα✝:Type u_1as:List α✝as✝:List α✝a:α✝h:Palindrome as✝ih:Palindrome as✝.reverse⊢ Palindrome (a :: (as✝.reverse ++ [a])); exact Palindrome.sandwich _ ihAll goals completed! 🐙

If a list as is a palindrome, then the reverse of as is equal to itself.

theorem reverse_eq_of_palindrome (h : Palindrome as) : as.reverse = as := byα✝:Type u_1as:List α✝h:Palindrome as⊢ as.reverse = as
  induction h with
  | nil => rflAll goals completed! 🐙
  | single a => rflAll goals completed! 🐙
  | sandwich a h ih => simp [ih]All goals completed! 🐙

Note that you can also easily prove palindrome_reverse using reverse_eq_of_palindrome.

example (h : Palindrome as) : Palindrome as.reverse := byα✝:Type u_1as:List α✝h:Palindrome as⊢ Palindrome as.reverse
  simp [reverse_eq_of_palindrome h, h]All goals completed! 🐙

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 : (as : List α) → as ≠ [] → α
  | [a],         _ => a
  | _::a₂:: as, _ => (a₂::as).last (byα:Type ?u.1049head✝:αa₂:αas:List αx✝:head✝ :: a₂ :: as ≠ []⊢ a₂ :: as ≠ [] simpAll goals completed! 🐙)

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 (h : as ≠ []) : as.dropLast ++ [as.last h] = as := byα✝:Type u_1as:List α✝h:as ≠ []⊢ as.dropLast ++ [as.last h] = as
  match as with
  | [] => contradictionAll goals completed! 🐙
  | [a] => simp_all [last, dropLast]All goals completed! 🐙
  | a₁ :: a₂ :: as =>
    simp [last, 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 (as := a₂ :: as) (byα✝:Type u_1as✝:List α✝a₁:α✝a₂:α✝as:List α✝h:a₁ :: a₂ :: as ≠ []⊢ a₂ :: as ≠ [] simpAll goals completed! 🐙)

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 (motive : List α → Prop)
    (h₁ : motive [])
    (h₂ : (a : α) → motive [a])
    (h₃ : (a b : α) → (as : List α) → motive as → motive ([a] ++ as ++ [b]))
    (as : List α)
    : motive as :=
  match as with
  | []  => h₁
  | [a] => h₂ a
  | a₁::a₂::as' =>
    have ih := palindrome_ind motive h₁ h₂ h₃ (a₂::as').dropLast
    have : [a₁] ++ (a₂::as').dropLast ++ [(a₂::as').last (byα:Type u_1motive:List α → Proph₁:motive []h₂:∀ (a : α), motive [a]h₃:∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])as:List αa₁:αa₂:αas':List αih:motive (a₂ :: as').dropLast⊢ a₂ :: as' ≠ [] simpAll goals completed! 🐙)] = a₁::a₂::as' := byα:Type u_1motive:List α → Proph₁:motive []h₂:∀ (a : α), motive [a]h₃:∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])as:List αa₁:αa₂:αas':List αih:motive (a₂ :: as').dropLast⊢ [a₁] ++ (a₂ :: as').dropLast ++ [(a₂ :: as').last ⋯] = a₁ :: a₂ :: as' simpAll goals completed! 🐙
    this ▸ h₃ _ _ _ ih
termination_by as.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 (h : as.reverse = as) : Palindrome as := byα✝:Type u_1as:List α✝h:as.reverse = as⊢ Palindrome as
  induction as using palindrome_indh₁α✝:Type u_1h:[].reverse = []⊢ Palindrome []h₂α✝:Type u_1a✝:α✝h:[a✝].reverse = [a✝]⊢ Palindrome [a✝]h₃α✝:Type u_1a✝¹:α✝b✝:α✝as✝:List α✝a✝:as✝.reverse = as✝ → Palindrome as✝h:([a✝¹] ++ as✝ ++ [b✝]).reverse = [a✝¹] ++ as✝ ++ [b✝]⊢ Palindrome ([a✝¹] ++ as✝ ++ [b✝])
  next   =>α✝:Type u_1h:[].reverse = []⊢ Palindrome [] exact Palindrome.nilAll goals completed! 🐙
  next a =>α✝:Type u_1a:α✝h:[a].reverse = [a]⊢ Palindrome [a] exact Palindrome.single aAll goals completed! 🐙
  next a b as ih =>α✝:Type u_1a:α✝b:α✝as:List α✝ih:as.reverse = as → Palindrome ash:([a] ++ as ++ [b]).reverse = [a] ++ as ++ [b]⊢ Palindrome ([a] ++ as ++ [b])
    have : a = b := byα✝:Type u_1as:List α✝h:as.reverse = as⊢ Palindrome as simp_allAll goals completed! 🐙
    subst thisα✝:Type u_1a:α✝as:List α✝ih:as.reverse = as → Palindrome ash:([a] ++ as ++ [a]).reverse = [a] ++ as ++ [a]⊢ Palindrome ([a] ++ as ++ [a])
    have : as.reverse = as := byα✝:Type u_1as:List α✝h:as.reverse = as⊢ Palindrome as simp_allAll goals completed! 🐙
    exact Palindrome.sandwich a (ih this)All goals completed! 🐙

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 [DecidableEq α] (as : List α) : Bool :=
    as.reverse = as

It is straightforward to prove that isPalindrome is correct using the previously proved theorems.

theorem List.isPalindrome_correct [DecidableEq α] (as : List α) : as.isPalindrome ↔ Palindrome as := byα:Type u_1inst✝:DecidableEq αas:List α⊢ as.isPalindrome = true ↔ Palindrome as
  simp [isPalindrome]α:Type u_1inst✝:DecidableEq αas:List α⊢ as.reverse = as ↔ Palindrome as
  exact Iff.intro (fun h => palindrome_of_eq_reverse h) (fun h => reverse_eq_of_palindrome h)All goals completed! 🐙

true#eval [1, 2, 1].isPalindrome

true

false#eval [1, 2, 3, 1].isPalindrome

false

example : [1, 2, 1].isPalindrome := rflexample : [1, 2, 2, 1].isPalindrome := rflexample : ![1, 2, 3, 1].isPalindrome := rfl