Lemmas for Init.Data.String.Modify

This file contains lemmas for the operations defined in Init.Data.String.Modify.

Note that Init.Data.String.Modify already proves a few lemmas which are needed immediately.

theorem String.ValidPos.Splits.pastSet {s : String} {p : s.ValidPos} {t₁ t₂ : String} {c d : Char} (h : p.Splits t₁ (singleton c ++ t₂)) : (p.pastSet d ⋯).Splits (t₁ ++ singleton d) t₂

You might want to invoke ValidPos.Splits.exists_eq_singleton_append to be able to apply this.

theorem String.ValidPos.Splits.pastModify {f : Char → Char} {s : String} {p : s.ValidPos} {t₁ t₂ : String} {c : Char} (h : p.Splits t₁ (singleton c ++ t₂)) : (p.pastModify f ⋯).Splits (t₁ ++ singleton (f (p.get ⋯))) t₂

You might want to invoke ValidPos.Splits.exists_eq_singleton_append to be able to apply this.

theorem String.toList_mapAux {t₁ t₂ : String} {f : Char → Char} {s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) : (mapAux f s p).toList = t₁.toList ++ List.map f t₂.toList

@[simp]

theorem String.toList_map {f : Char → Char} {s : String} : (map f s).toList = List.map f s.toList

@[simp]

theorem String.length_map {f : Char → Char} {s : String} : (map f s).length = s.length

@[simp]

theorem String.map_eq_empty {f : Char → Char} {s : String} : map f s = "" ↔ s = ""