feat: verification of backwards string patterns

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

@@ -201,6 +201,10 @@ theorem Pos.prev_eq_iff {s : Slice} {p q : s.Pos} {h} :
 theorem Pos.prev_lt {s : Slice} {p : s.Pos} {h} : p.prev h < p := by
   simp
 
+@[simp]
+theorem Pos.prev_le {s : Slice} {p : s.Pos} {h} : p.prev h ≤ p :=
+  Std.le_of_lt (by simp)
+
 @[simp]
 theorem Pos.prev_ne_endPos {s : Slice} {p : s.Pos} {h} : p.prev h ≠ s.endPos :=
   ne_endPos_of_lt prev_lt
@@ -211,6 +215,29 @@ theorem Pos.prevn_le {s : Slice} {p : s.Pos} {n : Nat} : p.prevn n ≤ p := by
   | case2 p n h ih => exact Std.le_of_lt (by simpa using ih)
   | case3 => simp
 
+theorem Pos.ofSliceTo_prev {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
+    Pos.ofSliceTo (p.prev h) = (Pos.ofSliceTo p).prev (by simpa [← Pos.ofSliceTo_inj] using h) := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [Pos.ofSliceTo_lt_ofSliceTo_iff, Pos.le_ofSliceTo_iff]
+  simp [Pos.lt_ofSliceTo_iff]
+
+theorem Pos.prev_ofSliceTo {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
+    (Pos.ofSliceTo p).prev h = Pos.ofSliceTo (p.prev (by simpa [← Pos.ofSliceTo_inj])) := by
+  simp [ofSliceTo_prev]
+
+theorem Pos.ofSliceFrom_prev {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h} :
+    Pos.ofSliceFrom (p.prev h) = (Pos.ofSliceFrom p).prev (by exact ofSliceFrom_ne_startPos h) := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [Pos.ofSliceFrom_lt_ofSliceFrom_iff,  Pos.le_ofSliceFrom_iff]
+  simp [Pos.lt_ofSliceFrom_iff]
+
+theorem Pos.ofSlice_prev {s : Slice} {p₀ p₁ : s.Pos} {h}
+    {p : (s.slice p₀ p₁ h).Pos} {h'} :
+    Pos.ofSlice (p.prev h') = (Pos.ofSlice p).prev (by exact ofSlice_ne_startPos h') := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [ofSlice_lt_ofSlice_iff,  le_ofSlice_iff]
+  simpa +contextual [← ofSlice_lt_ofSlice_iff] using fun q hq => Std.le_of_lt (Std.lt_of_lt_of_le hq ofSlice_le)
+
 @[simp]
 theorem Pos.prev_next {s : Slice} {p : s.Pos} {h} : (p.next h).prev (by simp) = p :=
   prev_eq_iff.2 (by simp)
@@ -439,6 +466,10 @@ theorem Pos.prev_eq_iff {s : String} {p q : s.Pos} {h} :
 theorem Pos.prev_lt {s : String} {p : s.Pos} {h} : p.prev h < p := by
   simp
 
+@[simp]
+theorem Pos.prev_le {s : String} {p : s.Pos} {h} : p.prev h ≤ p :=
+  Std.le_of_lt (by simp)
+
 @[simp]
 theorem Pos.prev_ne_endPos {s : String} {p : s.Pos} {h} : p.prev h ≠ s.endPos :=
   ne_endPos_of_lt prev_lt
@@ -463,6 +494,29 @@ theorem Pos.prevn_le {s : String} {p : s.Pos} {n : Nat} :
     p.prevn n ≤ p := by
   simpa [Pos.le_iff, ← offset_toSlice] using Slice.Pos.prevn_le
 
+theorem Pos.ofSliceTo_prev {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
+    Pos.ofSliceTo (p.prev h) = (Pos.ofSliceTo p).prev (by simpa [← Pos.ofSliceTo_inj] using h) := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [Pos.ofSliceTo_lt_ofSliceTo_iff, Pos.le_ofSliceTo_iff]
+  simp [Pos.lt_ofSliceTo_iff]
+
+theorem Pos.prev_ofSliceTo {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
+    (Pos.ofSliceTo p).prev h = Pos.ofSliceTo (p.prev (by simpa [← Pos.ofSliceTo_inj])) := by
+  simp [ofSliceTo_prev]
+
+theorem Pos.ofSliceFrom_prev {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h} :
+    Pos.ofSliceFrom (p.prev h) = (Pos.ofSliceFrom p).prev (by exact ofSliceFrom_ne_startPos h) := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [Pos.ofSliceFrom_lt_ofSliceFrom_iff, Pos.le_ofSliceFrom_iff]
+  simp [Pos.lt_ofSliceFrom_iff]
+
+theorem Pos.ofSlice_prev {s : String} {p₀ p₁ : s.Pos} {h}
+    {p : (s.slice p₀ p₁ h).Pos} {h'} :
+    Pos.ofSlice (p.prev h') = (Pos.ofSlice p).prev (by exact ofSlice_ne_startPos h') := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [ofSlice_lt_ofSlice_iff, le_ofSlice_iff]
+  simpa +contextual [← ofSlice_lt_ofSlice_iff] using fun q hq => Std.le_of_lt (Std.lt_of_lt_of_le hq ofSlice_le)
+
 @[simp]
 theorem Pos.prev_next {s : String} {p : s.Pos} {h} : (p.next h).prev (by simp) = p :=
   prev_eq_iff.2 (by simp)

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

@@ -204,7 +204,7 @@ theorem Slice.copy_sliceTo_startPos {s : Slice} : (s.sliceTo s.startPos).copy =
   simp
 
 @[simp]
-theorem Slice.copy_sliceFrom_startPos {s : Slice} : (s.sliceFrom s.endPos).copy = "" := by
+theorem Slice.copy_sliceFrom_endPos {s : Slice} : (s.sliceFrom s.endPos).copy = "" := by
   simp
 
 end CopyEqEmpty

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

@@ -11,6 +11,7 @@ import Init.Data.String.OrderInstances
 import Init.Data.String.Lemmas.Basic
 import Init.Data.Order.Lemmas
 import Init.Omega
+import Init.ByCases
 
 public section
 
@@ -70,7 +71,7 @@ theorem Pos.le_startPos {s : String} (p : s.Pos) : p ≤ s.startPos ↔ p = s.st
   ⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩
 
 @[simp]
-theorem Pos.startPos_lt_iff {s : String} {p : s.Pos} : s.startPos < p ↔ p ≠ s.startPos := by
+theorem Pos.startPos_lt_iff {s : String} (p : s.Pos) : s.startPos < p ↔ p ≠ s.startPos := by
   simp [← le_startPos, Std.not_le]
 
 @[simp]
@@ -235,13 +236,21 @@ theorem Slice.Pos.ofSliceFrom_next {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom
     Pos.next_le_iff_lt, true_and]
   simp [Pos.ofSliceFrom_lt_iff]
 
+theorem Slice.Pos.next_ofSliceFrom {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h} :
+    (Pos.ofSliceFrom p).next h = Pos.ofSliceFrom (p.next (by simpa [← Pos.ofSliceFrom_inj])) := by
+  simp [ofSliceFrom_next]
+
 theorem Pos.ofSliceFrom_next {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h} :
     Pos.ofSliceFrom (p.next h) = (Pos.ofSliceFrom p).next (by simpa [← Pos.ofSliceFrom_inj] using h) := by
   rw [eq_comm, Pos.next_eq_iff]
   simp only [Pos.ofSliceFrom_lt_ofSliceFrom_iff, Slice.Pos.lt_next, Pos.ofSliceFrom_le_iff,
     Slice.Pos.next_le_iff_lt, true_and]
   simp [Pos.ofSliceFrom_lt_iff]
 
+theorem Pos.next_ofSliceFrom {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h} :
+    (Pos.ofSliceFrom p).next h = Pos.ofSliceFrom (p.next (by simpa [← Pos.ofSliceFrom_inj])) := by
+  simp [Pos.ofSliceFrom_next]
+
 theorem Slice.Pos.le_ofSliceTo_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} :
     q ≤ Pos.ofSliceTo p ↔ ∃ h, Slice.Pos.sliceTo p₀ q h ≤ p := by
   refine ⟨fun h => ⟨Slice.Pos.le_trans h Pos.ofSliceTo_le, ?_⟩, fun ⟨h, h'⟩ => ?_⟩
@@ -359,11 +368,21 @@ theorem Slice.Pos.ofSliceTo_ne_endPos {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo
   refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₀))
   simpa [← lt_endPos_iff, ← ofSliceTo_lt_ofSliceTo_iff] using h
 
+theorem Slice.Pos.ofSliceFrom_ne_startPos {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos}
+    (h : p ≠ (s.sliceFrom p₀).startPos) : Pos.ofSliceFrom p ≠ s.startPos := by
+  refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
+  simpa [← startPos_lt_iff, ← ofSliceFrom_lt_ofSliceFrom_iff] using h
+
 theorem Pos.ofSliceTo_ne_endPos {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos}
     (h : p ≠ (s.sliceTo p₀).endPos) : Pos.ofSliceTo p ≠ s.endPos := by
   refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₀))
   simpa [← Slice.Pos.lt_endPos_iff, ← ofSliceTo_lt_ofSliceTo_iff] using h
 
+theorem Pos.ofSliceFrom_ne_startPos {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos}
+    (h : p ≠ (s.sliceFrom p₀).startPos) : Pos.ofSliceFrom p ≠ s.startPos := by
+  refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
+  simpa [← Slice.Pos.startPos_lt_iff, ← ofSliceFrom_lt_ofSliceFrom_iff] using h
+
 theorem Slice.Pos.ofSliceTo_next {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
     Pos.ofSliceTo (p.next h) = (Pos.ofSliceTo p).next (ofSliceTo_ne_endPos h) := by
   rw [eq_comm, Pos.next_eq_iff]
@@ -406,16 +425,110 @@ theorem Pos.slice_le_slice_iff {s : String} {p₀ p₁ : s.Pos} {q r : s.Pos}
   simp [Slice.Pos.le_iff, Pos.le_iff, Pos.Raw.le_iff] at h₁ h₁' ⊢
   omega
 
+theorem Slice.Pos.le_ofSlice_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    q ≤ Pos.ofSlice p ↔ ∃ h₁, ∀ h₀, Slice.Pos.slice q p₀ p₁ h₀ h₁ ≤ p := by
+  refine ⟨fun h => ⟨Std.le_trans h ofSlice_le, fun h' => ?_⟩, fun ⟨h₁, h⟩ => ?_⟩
+  · simp only [← Slice.Pos.slice_ofSlice (pos := p), slice_le_slice_iff]
+    simpa
+  · by_cases h₀ : p₀ ≤ q
+    · simpa only [← Slice.Pos.ofSlice_slice (h₁ := h₀) (h₂ := h₁), ofSlice_le_ofSlice_iff] using h h₀
+    · exact Std.le_of_lt (Std.lt_of_lt_of_le (Std.not_le.1 h₀) le_ofSlice)
+
+theorem Slice.Pos.ofSlice_lt_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    Pos.ofSlice p < q ↔ ∀ h₁, ∃ h₀, p < Slice.Pos.slice q p₀ p₁ h₀ h₁ := by
+  simp [← Std.not_le, le_ofSlice_iff]
+
+theorem Slice.Pos.lt_ofSlice_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    q < Pos.ofSlice p ↔ ∃ h₁, ∀ h₀, Slice.Pos.slice q p₀ p₁ h₀ h₁ < p := by
+  refine ⟨fun h => ⟨Std.le_of_lt (Std.lt_of_lt_of_le h ofSlice_le), fun h' => ?_⟩, fun ⟨h₁, h⟩ => ?_⟩
+  · simp only [← Slice.Pos.slice_ofSlice (pos := p), slice_lt_slice_iff]
+    simpa
+  · by_cases h₀ : p₀ ≤ q
+    · simpa only [← Slice.Pos.ofSlice_slice (h₁ := h₀) (h₂ := h₁), ofSlice_lt_ofSlice_iff] using h h₀
+    · exact Std.lt_of_lt_of_le (Std.not_le.1 h₀) le_ofSlice
+
+theorem Slice.Pos.ofSlice_le_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    Pos.ofSlice p ≤ q ↔ ∀ h₁, ∃ h₀, p ≤ Slice.Pos.slice q p₀ p₁ h₀ h₁ := by
+  simp [← Std.not_lt, lt_ofSlice_iff]
+
+theorem Pos.le_ofSlice_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    q ≤ Pos.ofSlice p ↔ ∃ h₁, ∀ h₀, Pos.slice q p₀ p₁ h₀ h₁ ≤ p := by
+  refine ⟨fun h => ⟨Std.le_trans h ofSlice_le, fun h' => ?_⟩, fun ⟨h₁, h⟩ => ?_⟩
+  · simp only [← Pos.slice_ofSlice (pos := p), slice_le_slice_iff]
+    simpa
+  · by_cases h₀ : p₀ ≤ q
+    · simpa only [← Pos.ofSlice_slice (h₁ := h₀) (h₂ := h₁), ofSlice_le_ofSlice_iff] using h h₀
+    · exact Std.le_of_lt (Std.lt_of_lt_of_le (Std.not_le.1 h₀) le_ofSlice)
+
+theorem Pos.ofSlice_lt_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    Pos.ofSlice p < q ↔ ∀ h₁, ∃ h₀, p < Pos.slice q p₀ p₁ h₀ h₁ := by
+  simp [← Std.not_le, le_ofSlice_iff]
+
+theorem Pos.lt_ofSlice_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    q < Pos.ofSlice p ↔ ∃ h₁, ∀ h₀, Pos.slice q p₀ p₁ h₀ h₁ < p := by
+  refine ⟨fun h => ⟨Std.le_of_lt (Std.lt_of_lt_of_le h ofSlice_le), fun h' => ?_⟩, fun ⟨h₁, h⟩ => ?_⟩
+  · simp only [← Pos.slice_ofSlice (pos := p), slice_lt_slice_iff]
+    simpa
+  · by_cases h₀ : p₀ ≤ q
+    · simpa only [← Pos.ofSlice_slice (h₁ := h₀) (h₂ := h₁), ofSlice_lt_ofSlice_iff] using h h₀
+    · exact Std.lt_of_lt_of_le (Std.not_le.1 h₀) le_ofSlice
+
+theorem Pos.ofSlice_le_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    Pos.ofSlice p ≤ q ↔ ∀ h₁, ∃ h₀, p ≤ Pos.slice q p₀ p₁ h₀ h₁ := by
+  simp [← Std.not_lt, lt_ofSlice_iff]
+
+theorem Slice.Pos.slice_le_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    Slice.Pos.slice q p₀ p₁ h₀ h₁ ≤ p ↔ q ≤ Pos.ofSlice p := by
+  simp [le_ofSlice_iff, h₀, h₁]
+
+theorem Slice.Pos.lt_slice_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    p < Slice.Pos.slice q p₀ p₁ h₀ h₁ ↔ Pos.ofSlice p < q := by
+  simp [ofSlice_lt_iff, h₀, h₁]
+
+theorem Slice.Pos.slice_lt_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    Slice.Pos.slice q p₀ p₁ h₀ h₁ < p ↔ q < Pos.ofSlice p := by
+  simp [lt_ofSlice_iff, h₀, h₁]
+
+theorem Slice.Pos.le_slice_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    p ≤ Slice.Pos.slice q p₀ p₁ h₀ h₁ ↔ Pos.ofSlice p ≤ q := by
+  simp [ofSlice_le_iff, h₀, h₁]
+
+theorem Pos.slice_le_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    Pos.slice q p₀ p₁ h₀ h₁ ≤ p ↔ q ≤ Pos.ofSlice p := by
+  simp [le_ofSlice_iff, h₀, h₁]
+
+theorem Pos.lt_slice_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    p < Pos.slice q p₀ p₁ h₀ h₁ ↔ Pos.ofSlice p < q := by
+  simp [ofSlice_lt_iff, h₀, h₁]
+
+theorem Pos.slice_lt_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    Pos.slice q p₀ p₁ h₀ h₁ < p ↔ q < Pos.ofSlice p := by
+  simp [lt_ofSlice_iff, h₀, h₁]
+
+theorem Pos.le_slice_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    p ≤ Pos.slice q p₀ p₁ h₀ h₁ ↔ Pos.ofSlice p ≤ q := by
+  simp [ofSlice_le_iff, h₀, h₁]
+
 theorem Slice.Pos.ofSlice_ne_endPos {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
     (h : p ≠ (s.slice p₀ p₁ h).endPos) : Pos.ofSlice p ≠ s.endPos := by
   refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₁))
   simpa [← lt_endPos_iff, ← ofSlice_lt_ofSlice_iff] using h
 
+theorem Slice.Pos.ofSlice_ne_startPos {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
+    (h : p ≠ (s.slice p₀ p₁ h).startPos) : Pos.ofSlice p ≠ s.startPos := by
+  refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
+  simpa [← startPos_lt_iff, ← ofSlice_lt_ofSlice_iff] using h
+
 theorem Pos.ofSlice_ne_endPos {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
     (h : p ≠ (s.slice p₀ p₁ h).endPos) : Pos.ofSlice p ≠ s.endPos := by
   refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₁))
   simpa [← Slice.Pos.lt_endPos_iff, ← ofSlice_lt_ofSlice_iff] using h
 
+theorem Pos.ofSlice_ne_startPos {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
+    (h : p ≠ (s.slice p₀ p₁ h).startPos) : Pos.ofSlice p ≠ s.startPos := by
+  refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
+  simpa [← Slice.Pos.startPos_lt_iff, ← ofSlice_lt_ofSlice_iff] using h
+
 @[simp]
 theorem Slice.Pos.offset_le_rawEndPos {s : Slice} {p : s.Pos} :
     p.offset ≤ s.rawEndPos :=