English
An induction principle for the less-than-by (ltb) comparison on strings, enabling a recursive argument over the structure of two strings as we compare their characters step by step.
Русский
Принцип индукции для сравнения строк по лексикографическому правилу ltb, позволяющий строить рекурсивное доказательство по структуре двух строк при пошаговом сравнении символов.
LaTeX
$$$\\text{inductionOn} : \\text{мотив} \\to (\\text{it}_1,\\text{it}_2) \\to \\dots$$$
Lean4
/-- Induction on `String.ltb`. -/
def inductionOn.{u} {motive : Iterator → Iterator → Sort u} (it₁ it₂ : Iterator)
(ind :
∀ s₁ s₂ i₁ i₂,
Iterator.hasNext ⟨s₂, i₂⟩ →
Iterator.hasNext ⟨s₁, i₁⟩ →
get s₁ i₁ = get s₂ i₂ → motive (Iterator.next ⟨s₁, i₁⟩) (Iterator.next ⟨s₂, i₂⟩) → motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩)
(eq :
∀ s₁ s₂ i₁ i₂,
Iterator.hasNext ⟨s₂, i₂⟩ → Iterator.hasNext ⟨s₁, i₁⟩ → ¬get s₁ i₁ = get s₂ i₂ → motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩)
(base₁ : ∀ s₁ s₂ i₁ i₂, Iterator.hasNext ⟨s₂, i₂⟩ → ¬Iterator.hasNext ⟨s₁, i₁⟩ → motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩)
(base₂ : ∀ s₁ s₂ i₁ i₂, ¬Iterator.hasNext ⟨s₂, i₂⟩ → motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩) : motive it₁ it₂ :=
if h₂ : it₂.hasNext then
if h₁ : it₁.hasNext then
if heq : it₁.curr = it₂.curr then
ind it₁.s it₂.s it₁.i it₂.i h₂ h₁ heq (inductionOn it₁.next it₂.next ind eq base₁ base₂)
else eq it₁.s it₂.s it₁.i it₂.i h₂ h₁ heq
else base₁ it₁.s it₂.s it₁.i it₂.i h₂ h₁
else base₂ it₁.s it₂.s it₁.i it₂.i h₂
