lt_iff_toList_lt — Mathlib

English

Induction principle and related equalities for String.ltb under iterator-based comparison; supports deriving properties by stepwise examination of matching and non-matching curr values.

Русский

Индукционный принцип и связанные равенства для String.ltb при сравнении итераторами; позволяет выводить свойства по шагам анализа текущих значений.

LaTeX

$$$ \text{ltb.inductionOn} \,\text{(вариант eq_def)} \text{(см. выше)} $$$

Lean4

@[simp]
theorem lt_iff_toList_lt : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ s₁.toList < s₂.toList
  | ⟨s₁⟩, ⟨s₂⟩ =>
    show ltb ⟨⟨s₁⟩, 0⟩ ⟨⟨s₂⟩, 0⟩ ↔ s₁ < s₂
      by
      induction s₁ generalizing s₂ <;> cases s₂
      · unfold ltb; decide
      · rename_i c₂ cs₂; apply iff_of_true
        · unfold ltb
          simp [Iterator.hasNext, Char.utf8Size_pos]
        · apply List.nil_lt_cons
      · rename_i c₁ cs₁ ih; apply iff_of_false
        · unfold ltb
          simp [Iterator.hasNext]
        · apply not_lt_of_gt; apply List.nil_lt_cons
      · rename_i c₁ cs₁ ih c₂ cs₂; unfold ltb
        simp only [Iterator.hasNext, Pos.byteIdx_zero, endPos, utf8ByteSize, utf8ByteSize.go, add_pos_iff,
          Char.utf8Size_pos, or_true, decide_eq_true_eq, ↓reduceIte, Iterator.curr, get, utf8GetAux, Iterator.next,
          next, Bool.ite_eq_true_distrib]
        split_ifs with h
        · subst c₂
          suffices ltb ⟨⟨c₁ :: cs₁⟩, (0 : Pos) + c₁⟩ ⟨⟨c₁ :: cs₂⟩, (0 : Pos) + c₁⟩ = ltb ⟨⟨cs₁⟩, 0⟩ ⟨⟨cs₂⟩, 0⟩ by
            rw [this]; exact (ih cs₂).trans List.lex_cons_iff.symm
          apply ltb_cons_addChar
        · refine ⟨List.Lex.rel, fun e ↦ ?_⟩
          cases e <;> rename_i h'
          · assumption
          · contradiction

Похожие утверждения