Missing material

Author: TwoFX

src/Init/Data/String/Lemmas/Basic.lean

@@ -39,4 +39,8 @@ theorem push_ne_empty : push s c ≠ "" := by
 theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
   simp [singleton]
 
+@[simp]
+theorem Slice.Pos.toCopy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.toCopy = p₂.toCopy ↔ p₁ = p₂ := by
+  simp [Pos.ext_iff, ValidPos.ext_iff]
+
 end String

src/Init/Data/String/Lemmas/Modify.lean

@@ -49,4 +49,12 @@ theorem toList_mapAux {f : Char → Char} {s : String} {p : s.ValidPos}
 theorem toList_map {f : Char → Char} {s : String} : (s.map f).toList = s.toList.map f := by
   simp [map, toList_mapAux s.splits_startValidPos]
 
+@[simp]
+theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.length := by
+  simp [← length_toList]
+
+@[simp]
+theorem map_eq_empty {f : Char → Char} {s : String} : s.map f = "" ↔ s = "" := by
+  simp [← toList_eq_nil_iff]
+
 end String

src/Init/Data/String/Lemmas/Splits.lean

@@ -110,6 +110,18 @@ theorem ValidPos.Splits.eq {s : String} {p : s.ValidPos} {t₁ t₂ t₃ t₄}
     (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ ∧ t₂ = t₄ :=
   ⟨h₁.eq_left h₂, h₁.eq_right h₂⟩
 
+theorem Slice.Pos.Splits.eq_left {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
+    (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ :=
+  (splits_toCopy_iff.2 h₁).eq_left (splits_toCopy_iff.2 h₂)
+
+theorem Slice.Pos.Splits.eq_right {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
+    (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₂ = t₄ :=
+  (splits_toCopy_iff.2 h₁).eq_right (splits_toCopy_iff.2 h₂)
+
+theorem Slice.Pos.Splits.eq {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
+    (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ ∧ t₂ = t₄ :=
+  (splits_toCopy_iff.2 h₁).eq (splits_toCopy_iff.2 h₂)
+
 @[simp]
 theorem splits_endValidPos (s : String) : s.endValidPos.Splits s "" where
   eq_append := by simp
@@ -121,10 +133,54 @@ theorem splits_endValidPos_iff {s : String} :
   ⟨fun h => ⟨h.eq_left s.splits_endValidPos, h.eq_right s.splits_endValidPos⟩,
    by rintro ⟨rfl, rfl⟩; exact t₁.splits_endValidPos⟩
 
+theorem ValidPos.Splits.eq_endValidPos_iff {s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) :
+    p = s.endValidPos ↔ t₂ = "" :=
+  ⟨fun h' => h.eq_right (h' ▸ s.splits_endValidPos),
+   by rintro rfl; simp [ValidPos.ext_iff, h.offset_eq_rawEndPos, h.eq_append]⟩
+
 theorem splits_startValidPos (s : String) : s.startValidPos.Splits "" s where
   eq_append := by simp
   offset_eq_rawEndPos := by simp
 
+@[simp]
+theorem splits_startValidPos_iff {s : String} :
+    s.startValidPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s :=
+  ⟨fun h => ⟨h.eq_left s.splits_startValidPos, h.eq_right s.splits_startValidPos⟩,
+   by rintro ⟨rfl, rfl⟩; exact t₂.splits_startValidPos⟩
+
+theorem ValidPos.Splits.eq_startValidPos_iff {s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) :
+    p = s.startValidPos ↔ t₁ = "" :=
+  ⟨fun h' => h.eq_left (h' ▸ s.splits_startValidPos),
+   by rintro rfl; simp [ValidPos.ext_iff, h.offset_eq_rawEndPos]⟩
+
+@[simp]
+theorem Slice.splits_endPos (s : Slice) : s.endPos.Splits s.copy "" where
+  eq_append := by simp
+  offset_eq_rawEndPos := by simp
+
+@[simp]
+theorem Slice.splits_endPos_iff {s : Slice} :
+    s.endPos.Splits t₁ t₂ ↔ t₁ = s.copy ∧ t₂ = "" := by
+  rw [← Pos.splits_toCopy_iff, ← endValidPos_copy, splits_endValidPos_iff]
+
+theorem Slice.Pos.Splits.eq_endPos_iff {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) :
+    p = s.endPos ↔ t₂ = "" := by
+  rw [← toCopy_inj, ← endValidPos_copy, h.toCopy.eq_endValidPos_iff]
+
+@[simp]
+theorem Slice.splits_startPos (s : Slice) : s.startPos.Splits "" s.copy where
+  eq_append := by simp
+  offset_eq_rawEndPos := by simp
+
+@[simp]
+theorem Slice.splits_startPos_iff {s : Slice} :
+    s.startPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s.copy := by
+  rw [← Pos.splits_toCopy_iff, ← startValidPos_copy, splits_startValidPos_iff]
+
+theorem Slice.Pos.Splits.eq_startPos_iff {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) :
+    p = s.startPos ↔ t₁ = "" := by
+  rw [← toCopy_inj, ← startValidPos_copy, h.toCopy.eq_startValidPos_iff]
+
 theorem ValidPos.splits_next_right {s : String} (p : s.ValidPos) (hp : p ≠ s.endValidPos) :
     p.Splits (s.replaceEnd p).copy (singleton (p.get hp) ++ (s.replaceStart (p.next hp)).copy) where
   eq_append := by simpa [← append_assoc] using p.eq_copy_replaceEnd_append_get hp
@@ -135,6 +191,16 @@ theorem ValidPos.splits_next {s : String} (p : s.ValidPos) (hp : p ≠ s.endVali
   eq_append := p.eq_copy_replaceEnd_append_get hp
   offset_eq_rawEndPos := by simp
 
+theorem Slice.Pos.splits_next_right {s : Slice} (p : s.Pos) (hp : p ≠ s.endPos) :
+    p.Splits (s.replaceEnd p).copy (singleton (p.get hp) ++ (s.replaceStart (p.next hp)).copy) where
+  eq_append := by simpa [← append_assoc] using p.copy_eq_copy_replaceEnd_append_get hp
+  offset_eq_rawEndPos := by simp
+
+theorem Slice.Pos.splits_next {s : Slice} (p : s.Pos) (hp : p ≠ s.endPos) :
+    (p.next hp).Splits ((s.replaceEnd p).copy ++ singleton (p.get hp)) (s.replaceStart (p.next hp)).copy where
+  eq_append := p.copy_eq_copy_replaceEnd_append_get hp
+  offset_eq_rawEndPos := by simp
+
 theorem ValidPos.Splits.exists_eq_singleton_append {s : String} {p : s.ValidPos}
     (hp : p ≠ s.endValidPos) (h : p.Splits t₁ t₂) : ∃ t₂', t₂ = singleton (p.get hp) ++ t₂' :=
   ⟨(s.replaceStart (p.next hp)).copy, h.eq_right (p.splits_next_right hp)⟩
@@ -143,20 +209,42 @@ theorem ValidPos.Splits.exists_eq_append_singleton {s : String} {p : s.ValidPos}
     (hp : p ≠ s.endValidPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get hp) :=
   ⟨(s.replaceEnd p).copy, h.eq_left (p.splits_next hp)⟩
 
-theorem ValidPos.Splits.eq_endValidPos_iff {s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) :
-    p = s.endValidPos ↔ t₂ = "" :=
-  ⟨fun h' => h.eq_right (h' ▸ s.splits_endValidPos),
-   by rintro rfl; simp [ValidPos.ext_iff, h.offset_eq_rawEndPos, h.eq_append] ⟩
+theorem Slice.Pos.Splits.exists_eq_singleton_append {s : Slice} {p : s.Pos}
+    (hp : p ≠ s.endPos) (h : p.Splits t₁ t₂) : ∃ t₂', t₂ = singleton (p.get hp) ++ t₂' :=
+  ⟨(s.replaceStart (p.next hp)).copy, h.eq_right (p.splits_next_right hp)⟩
+
+theorem Slice.Pos.Splits.exists_eq_append_singleton {s : Slice} {p : s.Pos}
+    (hp : p ≠ s.endPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get hp) :=
+  ⟨(s.replaceEnd p).copy, h.eq_left (p.splits_next hp)⟩
 
 theorem ValidPos.Splits.ne_endValidPos_of_singleton {s : String} {p : s.ValidPos}
     (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endValidPos := by
   simp [h.eq_endValidPos_iff]
 
+theorem ValidPos.Splits.ne_startValidPos_of_singleton {s : String} {p : s.ValidPos}
+    (h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startValidPos := by
+  simp [h.eq_startValidPos_iff]
+
+theorem Slice.Pos.Splits.ne_endPos_of_singleton {s : Slice} {p : s.Pos}
+    (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endPos := by
+  simp [h.eq_endPos_iff]
+
+theorem Slice.Pos.Splits.ne_startPos_of_singleton {s : Slice} {p : s.Pos}
+    (h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startPos := by
+  simp [h.eq_startPos_iff]
+
 /-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
 theorem ValidPos.Splits.next {s : String} {p : s.ValidPos}
     (h : p.Splits t₁ (singleton c ++ t₂)) : (p.next h.ne_endValidPos_of_singleton).Splits (t₁ ++ singleton c) t₂ := by
   generalize h.ne_endValidPos_of_singleton = hp
   obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_next_right p hp)
   exact splits_next p hp
 
+/-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
+theorem Slice.Pos.Splits.next {s : Slice} {p : s.Pos}
+    (h : p.Splits t₁ (singleton c ++ t₂)) : (p.next h.ne_endPos_of_singleton).Splits (t₁ ++ singleton c) t₂ := by
+  generalize h.ne_endPos_of_singleton = hp
+  obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_next_right p hp)
+  exact splits_next p hp
+
 end String