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
.
theorempalindrome_reverse (palindrome_reverse: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome as.reverseh :h: Palindrome asPalindromePalindrome: {α : Type u_1} → List α → Propas) :as: List ?m.423PalindromePalindrome: {α : Type u_1} → List α → Propas.as: List ?m.423reverse :=reverse: {α : Type u_1} → List α → List αGoals accomplished! 🐙α✝: Type u_1
as: List α✝
h: Palindrome asPalindrome as.reverseGoals accomplished! 🐙Goals accomplished! 🐙Goals accomplished! 🐙Goals accomplished! 🐙Goals accomplished! 🐙;α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: Palindrome as✝.reverse
sandwichPalindrome (a :: (as✝.reverse ++ [a]))Goals accomplished! 🐙
If a list as
is a palindrome, then the reverse of as
is equal to itself.
theoremreverse_eq_of_palindrome (reverse_eq_of_palindrome: ∀ {α : Type u_1} {as : List α}, Palindrome as → as.reverse = ash :h: Palindrome asPalindromePalindrome: {α : Type u_1} → List α → Propas) :as: List ?m.698as.as: List ?m.698reverse =reverse: {α : Type u_1} → List α → List αas :=as: List ?m.698Goals accomplished! 🐙α✝: Type u_1
as: List α✝
h: Palindrome asas.reverse = asGoals 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 (example: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome as.reverseh :h: Palindrome asPalindromePalindrome: {α : Type u_1} → List α → Propas) :as: List ?m.944PalindromePalindrome: {α : Type u_1} → List α → Propas.as: List ?m.944reverse :=reverse: {α : Type u_1} → List α → List α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.
defList.last : (List.last: {α : Type u_1} → (as : List α) → as ≠ [] → αas :as: List αListList: Type u_1 → Type u_1α) →α: Type u_1as ≠as: List α[] →[]: List αα | [α: Type u_1a], _ =>a: αa | _::a: αa₂::a₂: αas, _ => (as: List αa₂::a₂: αas).as: List αlast (last: {α : Type u_1} → (as : List α) → as ≠ [] → α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] theoremList.dropLast_append_last (List.dropLast_append_last: ∀ {α : Type u_1} {as : List α} (h : as ≠ []), as.dropLast ++ [as.last h] = ash :h: as ≠ []as ≠as: List ?m.1483[]) :[]: List ?m.1483as.as: List ?m.1483dropLast ++ [dropLast: {α : Type u_1} → List α → List αas.as: List ?m.1483lastlast: {α : Type u_1} → (as : List α) → as ≠ [] → αh] =h: as ≠ []as :=as: List ?m.1483Goals 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₂ :: asGoals 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.
theoremList.palindrome_ind (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 asmotive :motive: List α → PropListList: Type u_1 → Type u_1α →α: Type u_1Prop) (Prop: Typeh₁ :h₁: motive []motivemotive: List α → Prop[]) ([]: List αh₂ : (h₂: ∀ (a : α), motive [a]a :a: αα) →α: Type u_1motive [motive: List α → Propa]) (a: αh₃ : (h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])aa: αb :b: αα) → (α: Type u_1as :as: List αListList: Type u_1 → Type u_1α) →α: Type u_1motivemotive: List α → Propas →as: List αmotive ([motive: List α → Propa] ++a: αas ++ [as: List αb])) (b: αas :as: List αListList: Type u_1 → Type u_1α) :α: Type u_1motivemotive: List α → Propas := matchas: List αas with | [] =>as: List αh₁ | [h₁: motive []a] =>a: αh₂h₂: ∀ (a : α), motive [a]a |a: αa₁::a₁: αa₂::a₂: αas' => haveas': List αih :=ih: motive (a₂ :: as').dropLastpalindrome_indpalindrome_ind: ∀ {α : Type u_1} (motive : List α → Prop), motive [] → (∀ (a : α), motive [a]) → (∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive asmotivemotive: List α → Proph₁h₁: motive []h₂h₂: ∀ (a : α), motive [a]h₃ (h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])a₂::a₂: αas').as': List αdropLast have : [dropLast: {α : Type u_1} → List α → List αa₁] ++ (a₁: αa₂::a₂: αas').as': List αdropLast ++ [(dropLast: {α : Type u_1} → List α → List αa₂::a₂: αas').as': List αlast (last: {α : Type u_1} → (as : List α) → as ≠ [] → αGoals accomplished! 🐙)] =Goals accomplished! 🐙a₁::a₁: αa₂::a₂: αas' :=as': List αGoals accomplished! 🐙Goals accomplished! 🐙this ▸this: [a₁] ++ (a₂ :: as').dropLast ++ [(a₂ :: as').last ⋯] = a₁ :: a₂ :: as'h₃h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])__: α__: α__: List αih termination_byih: motive (a₂ :: as').dropLastas.as: List αlengthlength: {α : Type u_1} → List α → Nat
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.
theoremList.palindrome_of_eq_reverse (List.palindrome_of_eq_reverse: ∀ {α : Type u_1} {as : List α}, as.reverse = as → Palindrome ash :h: as.reverse = asas.as: List ?m.5832reverse =reverse: {α : Type u_1} → List α → List αas) :as: List ?m.5832PalindromePalindrome: {α : Type u_1} → List α → Propas :=as: List ?m.5832Goals 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.
theoremList.isPalindrome_correct [List.isPalindrome_correct: ∀ {α : Type u_1} [inst : DecidableEq α] (as : List α), as.isPalindrome = true ↔ Palindrome asDecidableEqDecidableEq: Type u_1 → Type (max 0 u_1)α] (α: Type u_1as :as: List αListList: Type u_1 → Type u_1α) :α: Type u_1as.as: List αisPalindrome ↔isPalindrome: {α : Type u_1} → [inst : DecidableEq α] → List α → BoolPalindromePalindrome: {α : Type u_1} → List α → Propas :=as: List αGoals accomplished! 🐙α: Type u_1
inst✝: DecidableEq α
as: List αas.reverse = as ↔ Palindrome asGoals accomplished! 🐙[1,1: Nat2,2: Nat1].1: NatisPalindromeisPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool[1,1: Nat2,2: Nat3,3: Nat1].1: NatisPalindromeisPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Boolexample : [example: [1, 2, 1].isPalindrome = true1,1: Nat2,2: Nat1].1: NatisPalindrome :=isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Boolrflrfl: ∀ {α : Type} {a : α}, a = aexample : [example: [1, 2, 2, 1].isPalindrome = true1,1: Nat2,2: Nat2,2: Nat1].1: NatisPalindrome :=isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Boolrflrfl: ∀ {α : Type} {a : α}, a = aexample : ![example: (![1, 2, 3, 1].isPalindrome) = true1,1: Nat2,2: Nat3,3: Nat1].1: NatisPalindrome :=isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Boolrflrfl: ∀ {α : Type} {a : α}, a = a