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 := α✝:Type u_1as:List α✝h:Palindrome as⊢ Palindrome as.reverse
induction h with
α✝:Type u_1as:List α✝⊢ Palindrome [].reverse All goals completed! 🐙
α✝:Type u_1as:List α✝a:α✝⊢ Palindrome [a].reverse All goals completed! 🐙
α✝:Type u_1as:List α✝as✝:List α✝a:α✝h:Palindrome as✝ih:Palindrome as✝.reverse⊢ Palindrome ([a] ++ as✝ ++ [a]).reverse α✝:Type u_1as:List α✝as✝:List α✝a:α✝h:Palindrome as✝ih:Palindrome as✝.reverse⊢ Palindrome (a :: (as✝.reverse ++ [a])); All 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 := α✝:Type u_1as:List α✝h:Palindrome as⊢ as.reverse = as
induction h with
α✝:Type u_1as:List α✝⊢ [].reverse = [] All goals completed! 🐙
α✝:Type u_1as:List α✝a:α✝⊢ [a].reverse = [a] All goals completed! 🐙
α✝:Type u_1as:List α✝as✝:List α✝a:α✝h:Palindrome as✝ih:as✝.reverse = as✝⊢ ([a] ++ as✝ ++ [a]).reverse = [a] ++ as✝ ++ [a] All goals completed! 🐙
Note that you can also easily prove palindrome_reverse using reverse_eq_of_palindrome.
example (h : Palindrome as) : Palindrome as.reverse := α✝:Type u_1as:List α✝h:Palindrome as⊢ Palindrome as.reverse
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 (α:Type ?u.4head✝:αa₂:αas:List αx✝:head✝ :: a₂ :: as ≠ []⊢ a₂ :: as ≠ [] All 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 := α✝:Type u_1as:List α✝h:as ≠ []⊢ as.dropLast ++ [as.last h] = as
match as with
α✝:Type u_1as:List α✝h:[] ≠ []⊢ [].dropLast ++ [[].last h] = [] All goals completed! 🐙
α✝:Type u_1as:List α✝a:α✝h:[a] ≠ []⊢ [a].dropLast ++ [[a].last h] = [a] All goals completed! 🐙
α✝:Type u_1as✝:List α✝a₁:α✝a₂:α✝as:List α✝h:a₁ :: a₂ :: as ≠ []⊢ (a₁ :: a₂ :: as).dropLast ++ [(a₁ :: a₂ :: as).last h] = a₁ :: a₂ :: as
α✝: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) (α✝:Type u_1as✝:List α✝a₁:α✝a₂:α✝as:List α✝h:a₁ :: a₂ :: as ≠ []⊢ a₂ :: as ≠ [] All 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 (α: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' ≠ [] All goals completed! 🐙)] = a₁::a₂::as' := α: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' All 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 := α✝:Type u_1as:List α✝h:as.reverse = as⊢ Palindrome as
α✝:Type u_1h:[].reverse = []⊢ Palindrome []α✝:Type u_1a✝:α✝h:[a✝].reverse = [a✝]⊢ Palindrome [a✝]α✝: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 [] All goals completed! 🐙
next a α✝:Type u_1a:α✝h:[a✝].reverse = [a✝]⊢ Palindrome [a✝] All goals completed! 🐙
next a b as ih α✝:Type u_1a:α✝b:α✝as:List α✝ih:as✝.reverse = as✝ → Palindrome as✝h:([a✝¹] ++ as✝ ++ [b✝]).reverse = [a✝¹] ++ as✝ ++ [b✝]⊢ Palindrome ([a✝¹] ++ as✝ ++ [b✝])
α✝:Type u_1b:α✝as:List α✝ih:as✝.reverse = as✝ → Palindrome as✝h✝:([b] ++ as ++ [b]).reverse = [b] ++ as ++ [b]h:as.reverse = as⊢ Palindrome ([b] ++ as ++ [b])
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 := α:Type u_1inst✝:DecidableEq αas:List α⊢ as.isPalindrome = true ↔ Palindrome as
α:Type u_1inst✝:DecidableEq αas:List α⊢ as.reverse = as ↔ Palindrome as
All goals completed! 🐙true#eval [1, 2, 1].isPalindrometruefalse#eval [1, 2, 3, 1].isPalindromefalseexample : [1, 2, 1].isPalindrome := rflexample : [1, 2, 2, 1].isPalindrome := rflexample : ![1, 2, 3, 1].isPalindrome := rfl