mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
d24ece1396
This PR adds more theory about `Splits` for strings and deduces the first user-facing `String` lemma, `String.toList_map`.
121 lines
4.9 KiB
Lean4
121 lines
4.9 KiB
Lean4
/-!
|
||
# 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
|
||
induction h with
|
||
| nil => exact Palindrome.nil
|
||
| single a => exact Palindrome.single a
|
||
| sandwich a h ih => simp; exact Palindrome.sandwich _ ih
|
||
|
||
/-! 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
|
||
induction h with
|
||
| nil => rfl
|
||
| single a => rfl
|
||
| sandwich a h ih => simp [ih]
|
||
|
||
/-! Note that you can also easily prove `palindrome_reverse` using `reverse_eq_of_palindrome`. -/
|
||
example (h : Palindrome as) : Palindrome as.reverse := by
|
||
simp [reverse_eq_of_palindrome h, h]
|
||
|
||
/-!
|
||
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 simp)
|
||
|
||
/-!
|
||
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
|
||
match as with
|
||
| [] => contradiction
|
||
| [a] => simp_all [last, dropLast]
|
||
| a₁ :: a₂ :: as =>
|
||
simp [last, dropLast]
|
||
exact dropLast_append_last (as := a₂ :: as) (by simp)
|
||
|
||
/-!
|
||
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 simp)] = a₁::a₂::as' := by simp
|
||
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
|
||
induction as using palindrome_ind
|
||
next => exact Palindrome.nil
|
||
next a => exact Palindrome.single a
|
||
next a b as ih =>
|
||
obtain ⟨rfl, h, -⟩ := by simpa using h
|
||
exact Palindrome.sandwich b (ih h)
|
||
|
||
/-!
|
||
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
|
||
simp [isPalindrome]
|
||
exact Iff.intro (fun h => palindrome_of_eq_reverse h) (fun h => reverse_eq_of_palindrome h)
|
||
|
||
#eval [1, 2, 1].isPalindrome
|
||
#eval [1, 2, 3, 1].isPalindrome
|
||
|
||
example : [1, 2, 1].isPalindrome := rfl
|
||
example : [1, 2, 2, 1].isPalindrome := rfl
|
||
example : ![1, 2, 3, 1].isPalindrome := rfl
|