English
Induction principle for the String.ltb predicate over iterator-based comparisons of strings.
Русский
Индукционный принцип для предиката String.ltb над сравнением строк через итераторы.
LaTeX
$$$ \text{ltb.inductionOn} \bigl(\text{motive},\text{it}_1,\text{it}_2,\text{ind},\text{eq},\text{base}_1,\text{base}_2\bigr). $$$
Lean4
theorem ltb_cons_addChar (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : Pos) :
ltb ⟨⟨c :: cs₁⟩, i₁ + c⟩ ⟨⟨c :: cs₂⟩, i₂ + c⟩ = ltb ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩ :=
by
apply
ltb.inductionOn ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩ (motive := fun ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩ ↦
ltb ⟨⟨c :: cs₁⟩, i₁ + c⟩ ⟨⟨c :: cs₂⟩, i₂ + c⟩ = ltb ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩) <;>
simp only <;>
intro ⟨cs₁⟩ ⟨cs₂⟩ i₁ i₂ <;>
intros <;>
(conv => lhs; unfold ltb) <;>
(conv => rhs; unfold ltb) <;>
simp only [Iterator.hasNext_cons_addChar, ite_false, ite_true, *, reduceCtorEq]
· rename_i h₂ h₁ heq ih
simp only [Iterator.next, next, heq, Iterator.curr, get_cons_addChar, ite_true] at ih ⊢
repeat rw [Pos.addChar_right_comm _ c]
exact ih
· rename_i h₂ h₁ hne
simp [Iterator.curr, get_cons_addChar, hne]
