From 1e0bfe931f28f0d73d40554aac2662815fac27ca Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 25 Feb 2026 10:39:59 +0100 Subject: [PATCH] feat: more lemmas about `String.Slice.Pos.ofSlice(From|To)?` (#12685) This PR adds some missing material about transferring positions across the subslicing operations `slice`, `sliceFrom`, `sliceTo`. --- src/Init/Data/String/Basic.lean | 104 +++++++++++++++ src/Init/Data/String/Lemmas/Order.lean | 178 ++++++++++++++++++++++++- 2 files changed, 278 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index c60873fdfe..f95f358706 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1525,6 +1525,11 @@ def Slice.Pos.toReplaceEnd {s : Slice} (p₀ : s.Pos) (pos : s.Pos) (h : pos ≤ theorem Slice.Pos.offset_sliceTo {s : Slice} {p₀ : s.Pos} {pos : s.Pos} {h : pos ≤ p₀} : (sliceTo p₀ pos h).offset = pos.offset := (rfl) +@[simp] +theorem Slice.Pos.sliceTo_inj {s : Slice} {p₀ : s.Pos} {pos pos' : s.Pos} {h h'} : + p₀.sliceTo pos h = p₀.sliceTo pos' h' ↔ pos = pos' := by + simp [Pos.ext_iff] + @[simp] theorem Slice.Pos.ofSliceTo_startPos {s : Slice} {pos : s.Pos} : ofSliceTo (s.sliceTo pos).startPos = s.startPos := by @@ -2347,6 +2352,16 @@ theorem Slice.Pos.ofSliceTo_le {s : Slice} {p₀ : s.Pos} {pos : (s.sliceTo p₀ ofSliceTo pos ≤ p₀ := by simpa [Pos.le_iff, Pos.Raw.le_iff] using pos.isValidForSlice.le_utf8ByteSize +@[simp] +theorem Pos.ofSliceTo_lt_ofSliceTo_iff {s : String} {p : s.Pos} + {q r : (s.sliceTo p).Pos} : Pos.ofSliceTo q < Pos.ofSliceTo r ↔ q < r := by + simp [Pos.lt_iff, Slice.Pos.lt_iff, Pos.Raw.lt_iff] + +@[simp] +theorem Pos.ofSliceTo_le_ofSliceTo_iff {s : String} {p : s.Pos} + {q r : (s.sliceTo p).Pos} : Pos.ofSliceTo q ≤ Pos.ofSliceTo r ↔ q ≤ r := by + simp [Pos.le_iff, Slice.Pos.le_iff, Pos.Raw.le_iff] + /-- Given a position in `s` that is at most `p₀`, obtain the corresponding position in `s.sliceTo p₀`. -/ @[inline] def Pos.sliceTo {s : String} (p₀ : s.Pos) (pos : s.Pos) (h : pos ≤ p₀) : @@ -2363,6 +2378,11 @@ def Pos.toReplaceEnd {s : String} (p₀ : s.Pos) (pos : s.Pos) (h : pos ≤ p₀ theorem Pos.offset_sliceTo {s : String} {p₀ : s.Pos} {pos : s.Pos} {h : pos ≤ p₀} : (sliceTo p₀ pos h).offset = pos.offset := (rfl) +@[simp] +theorem Pos.sliceTo_inj {s : String} {p₀ : s.Pos} {pos pos' : s.Pos} {h h'} : + p₀.sliceTo pos h = p₀.sliceTo pos' h' ↔ pos = pos' := by + simp [Pos.ext_iff, Slice.Pos.ext_iff] + @[simp] theorem Slice.Pos.ofSliceTo_sliceTo {s : Slice} {p₀ p : s.Pos} {h : p ≤ p₀} : Slice.Pos.ofSliceTo (p₀.sliceTo p h) = p := by @@ -2431,6 +2451,27 @@ theorem Slice.Pos.ofSlice_inj {s : Slice} {p₀ p₁ : s.Pos} {h} (pos₁ pos₂ ofSlice pos₁ = ofSlice pos₂ ↔ pos₁ = pos₂ := by simp [Pos.ext_iff, Pos.Raw.ext_iff] +@[simp] +theorem Slice.Pos.le_ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h} + {pos : (s.slice p₀ p₁ h).Pos} : p₀ ≤ ofSlice pos := by + simp [Pos.le_iff, Pos.Raw.le_iff] + +@[simp] +theorem Slice.Pos.ofSlice_le {s : Slice} {p₀ p₁ : s.Pos} {h} + {pos : (s.slice p₀ p₁ h).Pos} : ofSlice pos ≤ p₁ := by + have := (Pos.Raw.isValidForSlice_slice _).1 pos.isValidForSlice |>.1 + simpa [Pos.le_iff, Pos.Raw.le_iff] + +@[simp] +theorem Slice.Pos.ofSlice_lt_ofSlice_iff {s : Slice} {p₀ p₁ : s.Pos} {h} + {q r : (s.slice p₀ p₁ h).Pos} : Slice.Pos.ofSlice q < Slice.Pos.ofSlice r ↔ q < r := by + simp [Slice.Pos.lt_iff, Pos.Raw.lt_iff] + +@[simp] +theorem Slice.Pos.ofSlice_le_ofSlice_iff {s : Slice} {p₀ p₁ : s.Pos} {h} + {q r : (s.slice p₀ p₁ h).Pos} : Slice.Pos.ofSlice q ≤ Slice.Pos.ofSlice r ↔ q ≤ r := by + simp [Slice.Pos.le_iff, Pos.Raw.le_iff] + /-- Given a position in `s.slice p₀ p₁ h`, obtain the corresponding position in `s`. -/ @[inline] def Pos.ofSlice {s : String} {p₀ p₁ : s.Pos} {h} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos := @@ -2461,6 +2502,27 @@ theorem Pos.ofSlice_inj {s : String} {p₀ p₁ : s.Pos} {h} (pos₁ pos₂ : (s ofSlice pos₁ = ofSlice pos₂ ↔ pos₁ = pos₂ := by simp [Pos.ext_iff, Pos.Raw.ext_iff, Slice.Pos.ext_iff] +@[simp] +theorem Pos.le_ofSlice {s : String} {p₀ p₁ : s.Pos} {h} + {pos : (s.slice p₀ p₁ h).Pos} : p₀ ≤ ofSlice pos := by + simp [Pos.le_iff, Pos.Raw.le_iff] + +@[simp] +theorem Pos.ofSlice_le {s : String} {p₀ p₁ : s.Pos} {h} + {pos : (s.slice p₀ p₁ h).Pos} : ofSlice pos ≤ p₁ := by + have := (Pos.Raw.isValidForSlice_slice _).1 pos.isValidForSlice |>.1 + simpa [Pos.le_iff, Pos.Raw.le_iff] + +@[simp] +theorem Pos.ofSlice_lt_ofSlice_iff {s : String} {p₀ p₁ : s.Pos} {h} + {q r : (s.slice p₀ p₁ h).Pos} : Pos.ofSlice q < Pos.ofSlice r ↔ q < r := by + simp [Pos.lt_iff, Slice.Pos.lt_iff, Pos.Raw.lt_iff] + +@[simp] +theorem Pos.ofSlice_le_ofSlice_iff {s : String} {p₀ p₁ : s.Pos} {h} + {q r : (s.slice p₀ p₁ h).Pos} : Pos.ofSlice q ≤ Pos.ofSlice r ↔ q ≤ r := by + simp [Pos.le_iff, Slice.Pos.le_iff, Pos.Raw.le_iff] + theorem Slice.Pos.le_trans {s : Slice} {p q r : s.Pos} : p ≤ q → q ≤ r → p ≤ r := by simpa [Pos.le_iff, Pos.Raw.le_iff] using Nat.le_trans @@ -2484,6 +2546,48 @@ def Pos.slice {s : String} (pos : s.Pos) (p₀ p₁ : s.Pos) (h₁ : p₀ ≤ po theorem Pos.offset_slice {s : String} {p₀ p₁ pos : s.Pos} {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁} : (pos.slice p₀ p₁ h₁ h₂).offset = pos.offset.unoffsetBy p₀.offset := (rfl) +@[simp] +theorem Slice.Pos.offset_slice {s : Slice} {p₀ p₁ pos : s.Pos} {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁} : + (pos.slice p₀ p₁ h₁ h₂).offset = pos.offset.unoffsetBy p₀.offset := (rfl) + +@[simp] +theorem Slice.Pos.ofSlice_slice {s : Slice} {p₀ p₁ pos : s.Pos} + {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁} : + Slice.Pos.ofSlice (pos.slice p₀ p₁ h₁ h₂) = pos := by + simpa [Pos.ext_iff] using Pos.Raw.offsetBy_unoffsetBy_of_le h₁ + +@[simp] +theorem Slice.Pos.slice_ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h} + {pos : (s.slice p₀ p₁ h).Pos} : + (Slice.Pos.ofSlice pos).slice p₀ p₁ Slice.Pos.le_ofSlice Slice.Pos.ofSlice_le = pos := by + simp [← Slice.Pos.ofSlice_inj] + +@[simp] +theorem Pos.ofSlice_slice {s : String} {p₀ p₁ pos : s.Pos} + {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁} : + Pos.ofSlice (pos.slice p₀ p₁ h₁ h₂) = pos := by + simpa [Pos.ext_iff] using Pos.Raw.offsetBy_unoffsetBy_of_le h₁ + +@[simp] +theorem Pos.slice_ofSlice {s : String} {p₀ p₁ : s.Pos} {h} + {pos : (s.slice p₀ p₁ h).Pos} : + (Pos.ofSlice pos).slice p₀ p₁ Pos.le_ofSlice Pos.ofSlice_le = pos := by + simp [← Pos.ofSlice_inj] + +@[simp] +theorem Slice.Pos.slice_inj {s : Slice} {p₀ p₁ : s.Pos} {pos pos' : s.Pos} + {h₁ h₁' h₂ h₂'} : + pos.slice p₀ p₁ h₁ h₂ = pos'.slice p₀ p₁ h₁' h₂' ↔ pos = pos' := by + simp [Pos.ext_iff, Pos.Raw.ext_iff, Pos.le_iff, Pos.Raw.le_iff] at ⊢ h₁ h₁' + omega + +@[simp] +theorem Pos.slice_inj {s : String} {p₀ p₁ : s.Pos} {pos pos' : s.Pos} + {h₁ h₁' h₂ h₂'} : + pos.slice p₀ p₁ h₁ h₂ = pos'.slice p₀ p₁ h₁' h₂' ↔ pos = pos' := by + simp [Pos.ext_iff, Pos.Raw.ext_iff, Slice.Pos.ext_iff, Pos.le_iff, Pos.Raw.le_iff] at ⊢ h₁ h₁' + omega + /-- Given a position in `s`, obtain the corresponding position in `s.slice p₀ p₁ h`, or panic if `pos` is not between `p₀` and `p₁`. diff --git a/src/Init/Data/String/Lemmas/Order.lean b/src/Init/Data/String/Lemmas/Order.lean index a75c2a02e5..a1584b5a2a 100644 --- a/src/Init/Data/String/Lemmas/Order.lean +++ b/src/Init/Data/String/Lemmas/Order.lean @@ -57,6 +57,14 @@ theorem Slice.Pos.endPos_le {s : Slice} (p : s.Pos) : s.endPos ≤ p ↔ p = s.e theorem Slice.Pos.lt_endPos_iff {s : Slice} (p : s.Pos) : p < s.endPos ↔ p ≠ s.endPos := by simp [← endPos_le, Std.not_le] +@[simp] +theorem Pos.endPos_le {s : String} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos := + ⟨fun h => Std.le_antisymm (le_endPos _) h, by simp +contextual⟩ + +@[simp] +theorem Pos.lt_endPos_iff {s : String} (p : s.Pos) : p < s.endPos ↔ p ≠ s.endPos := by + simp [← endPos_le, Std.not_le] + @[simp] theorem Pos.le_startPos {s : String} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos := ⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩ @@ -65,10 +73,6 @@ theorem Pos.le_startPos {s : String} (p : s.Pos) : p ≤ s.startPos ↔ p = s.st theorem Pos.startPos_lt_iff {s : String} {p : s.Pos} : s.startPos < p ↔ p ≠ s.startPos := by simp [← le_startPos, Std.not_le] -@[simp] -theorem Pos.endPos_le {s : String} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos := - ⟨fun h => Std.le_antisymm (le_endPos _) h, by simp +contextual [Std.le_refl]⟩ - @[simp] theorem Slice.Pos.not_lt_startPos {s : Slice} {p : s.Pos} : ¬ p < s.startPos := fun h => Std.lt_irrefl (Std.lt_of_lt_of_le h (Slice.Pos.startPos_le _)) @@ -106,14 +110,36 @@ theorem Slice.Pos.next_ne_startPos {s : Slice} {p : s.Pos} {h} : p.next h ≠ s.startPos := ne_startPos_of_lt lt_next +@[simp] theorem Slice.Pos.ofSliceTo_lt_ofSliceTo_iff {s : Slice} {p : s.Pos} {q r : (s.sliceTo p).Pos} : Slice.Pos.ofSliceTo q < Slice.Pos.ofSliceTo r ↔ q < r := by simp [Slice.Pos.lt_iff, Pos.Raw.lt_iff] +@[simp] theorem Slice.Pos.ofSliceTo_le_ofSliceTo_iff {s : Slice} {p : s.Pos} {q r : (s.sliceTo p).Pos} : Slice.Pos.ofSliceTo q ≤ Slice.Pos.ofSliceTo r ↔ q ≤ r := by simp [Slice.Pos.le_iff, Pos.Raw.le_iff] +@[simp] +theorem Slice.Pos.sliceTo_lt_sliceTo_iff {s : Slice} {p₀ : s.Pos} {q r : s.Pos} {h₁ h₂} : + Pos.sliceTo p₀ q h₁ < Pos.sliceTo p₀ r h₂ ↔ q < r := by + simp [Slice.Pos.lt_iff, Pos.Raw.lt_iff] + +@[simp] +theorem Slice.Pos.sliceTo_le_sliceTo_iff {s : Slice} {p₀ : s.Pos} {q r : s.Pos} {h₁ h₂} : + Pos.sliceTo p₀ q h₁ ≤ Pos.sliceTo p₀ r h₂ ↔ q ≤ r := by + simp [Slice.Pos.le_iff, Pos.Raw.le_iff] + +@[simp] +theorem Pos.sliceTo_lt_sliceTo_iff {s : String} {p₀ : s.Pos} {q r : s.Pos} {h₁ h₂} : + Pos.sliceTo p₀ q h₁ < Pos.sliceTo p₀ r h₂ ↔ q < r := by + simp [Slice.Pos.lt_iff, Pos.lt_iff, Pos.Raw.lt_iff] + +@[simp] +theorem Pos.sliceTo_le_sliceTo_iff {s : String} {p₀ : s.Pos} {q r : s.Pos} {h₁ h₂} : + Pos.sliceTo p₀ q h₁ ≤ Pos.sliceTo p₀ r h₂ ↔ q ≤ r := by + simp [Slice.Pos.le_iff, Pos.le_iff, Pos.Raw.le_iff] + @[simp] theorem Slice.Pos.sliceFrom_lt_sliceFrom_iff {s : Slice} {p₀ : s.Pos} {q r : s.Pos} {h₁ h₂} : Pos.sliceFrom p₀ q h₁ < Pos.sliceFrom p₀ r h₂ ↔ q < r := by @@ -200,6 +226,116 @@ theorem Pos.ofSliceFrom_next {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀) Slice.Pos.next_le_iff_lt, true_and] simp [Pos.ofSliceFrom_lt_iff] +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'⟩ => ?_⟩ + · simp +singlePass only [← Pos.sliceTo_ofSliceTo (p := p)] + rwa [Pos.sliceTo_le_sliceTo_iff] + · simp +singlePass only [← Pos.ofSliceTo_sliceTo (h := h)] + rwa [Pos.ofSliceTo_le_ofSliceTo_iff] + +theorem Slice.Pos.ofSliceTo_lt_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : + Pos.ofSliceTo p < q ↔ ∀ h, p < Slice.Pos.sliceTo p₀ q h := by + simp [← Std.not_le, Slice.Pos.le_ofSliceTo_iff] + +theorem Slice.Pos.lt_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 => ⟨Std.le_of_lt (Std.lt_of_le_of_lt (Std.le_refl q) (Std.lt_of_lt_of_le h Pos.ofSliceTo_le)), ?_⟩, fun ⟨h, h'⟩ => ?_⟩ + · simp +singlePass only [← Pos.sliceTo_ofSliceTo (p := p)] + rwa [Pos.sliceTo_lt_sliceTo_iff] + · simp +singlePass only [← Pos.ofSliceTo_sliceTo (h := h)] + rwa [Pos.ofSliceTo_lt_ofSliceTo_iff] + +theorem Slice.Pos.ofSliceTo_le_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : + Pos.ofSliceTo p ≤ q ↔ ∀ h, p ≤ Slice.Pos.sliceTo p₀ q h := by + simp [← Std.not_lt, Slice.Pos.lt_ofSliceTo_iff] + +theorem Pos.le_ofSliceTo_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : + q ≤ Pos.ofSliceTo p ↔ ∃ h, Pos.sliceTo p₀ q h ≤ p := by + refine ⟨fun h => ⟨Pos.le_trans h Pos.ofSliceTo_le, ?_⟩, fun ⟨h, h'⟩ => ?_⟩ + · simp +singlePass only [← Pos.sliceTo_ofSliceTo (p := p)] + rwa [Pos.sliceTo_le_sliceTo_iff] + · simp +singlePass only [← Pos.ofSliceTo_sliceTo (h := h)] + rwa [Pos.ofSliceTo_le_ofSliceTo_iff] + +theorem Pos.ofSliceTo_lt_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : + Pos.ofSliceTo p < q ↔ ∀ h, p < Pos.sliceTo p₀ q h := by + simp [← Std.not_le, Pos.le_ofSliceTo_iff] + +theorem Pos.lt_ofSliceTo_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : + q < Pos.ofSliceTo p ↔ ∃ h, Pos.sliceTo p₀ q h < p := by + refine ⟨fun h => ⟨Pos.le_of_lt (Pos.lt_of_lt_of_le h Pos.ofSliceTo_le), ?_⟩, fun ⟨h, h'⟩ => ?_⟩ + · simp +singlePass only [← Pos.sliceTo_ofSliceTo (p := p)] + rwa [Pos.sliceTo_lt_sliceTo_iff] + · simp +singlePass only [← Pos.ofSliceTo_sliceTo (h := h)] + rwa [Pos.ofSliceTo_lt_ofSliceTo_iff] + +theorem Pos.ofSliceTo_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : + Pos.ofSliceTo p ≤ q ↔ ∀ h, p ≤ Pos.sliceTo p₀ q h := by + simp [← Std.not_lt, Pos.lt_ofSliceTo_iff] + +theorem Slice.Pos.ofSliceTo_ne_endPos {s : Slice} {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 [← lt_endPos_iff, ← ofSliceTo_lt_ofSliceTo_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 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] + simp only [Pos.ofSliceTo_lt_ofSliceTo_iff, Pos.lt_next, Pos.ofSliceTo_le_iff, + Pos.next_le_iff_lt, true_and] + simp [Pos.ofSliceTo_lt_iff] + +theorem Pos.ofSliceTo_next {s : String} {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] + simp only [Pos.ofSliceTo_lt_ofSliceTo_iff, Slice.Pos.lt_next, Pos.ofSliceTo_le_iff, + Slice.Pos.next_le_iff_lt, true_and] + simp [Pos.ofSliceTo_lt_iff] + +@[simp] +theorem Slice.Pos.slice_lt_slice_iff {s : Slice} {p₀ p₁ : s.Pos} {q r : s.Pos} + {h₁ h₁' h₂ h₂'} : + q.slice p₀ p₁ h₁ h₂ < r.slice p₀ p₁ h₁' h₂' ↔ q < r := by + simp [Slice.Pos.lt_iff, Pos.Raw.lt_iff, Slice.Pos.le_iff, Pos.Raw.le_iff] at h₁ h₁' ⊢ + omega + +@[simp] +theorem Slice.Pos.slice_le_slice_iff {s : Slice} {p₀ p₁ : s.Pos} {q r : s.Pos} + {h₁ h₁' h₂ h₂'} : + q.slice p₀ p₁ h₁ h₂ ≤ r.slice p₀ p₁ h₁' h₂' ↔ q ≤ r := by + simp [Slice.Pos.le_iff, Pos.Raw.le_iff] at h₁ h₁' ⊢ + omega + +@[simp] +theorem Pos.slice_lt_slice_iff {s : String} {p₀ p₁ : s.Pos} {q r : s.Pos} + {h₁ h₁' h₂ h₂'} : + q.slice p₀ p₁ h₁ h₂ < r.slice p₀ p₁ h₁' h₂' ↔ q < r := by + simp [Slice.Pos.lt_iff, Pos.lt_iff, Pos.Raw.lt_iff, Pos.le_iff, Pos.Raw.le_iff] at h₁ h₁' ⊢ + omega + +@[simp] +theorem Pos.slice_le_slice_iff {s : String} {p₀ p₁ : s.Pos} {q r : s.Pos} + {h₁ h₁' h₂ h₂'} : + q.slice p₀ p₁ h₁ h₂ ≤ r.slice p₀ p₁ h₁' h₂' ↔ q ≤ r := by + simp [Slice.Pos.le_iff, Pos.le_iff, Pos.Raw.le_iff] at h₁ h₁' ⊢ + omega + +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 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 + @[simp] theorem Slice.Pos.offset_le_rawEndPos {s : Slice} {p : s.Pos} : p.offset ≤ s.rawEndPos := @@ -248,4 +384,38 @@ theorem Pos.isUTF8FirstByte_getUTF8Byte_offset {s : String} {p : s.Pos} {h} : (s.getUTF8Byte p.offset h).IsUTF8FirstByte := by simpa [getUTF8Byte_offset] using isUTF8FirstByte_byte +theorem Slice.Pos.get_eq_get_ofSliceTo {s : Slice} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} {h} : + pos.get h = (ofSliceTo pos).get (ofSliceTo_ne_endPos h) := by + simp [Slice.Pos.get] + +theorem Pos.get_eq_get_ofSliceTo {s : String} {p₀ : s.Pos} + {pos : (s.sliceTo p₀).Pos} {h} : + pos.get h = (ofSliceTo pos).get (ofSliceTo_ne_endPos h) := by + simp [Pos.get, Slice.Pos.get] + +theorem Slice.Pos.get_eq_get_ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h} + {pos : (s.slice p₀ p₁ h).Pos} {h'} : + pos.get h' = (ofSlice pos).get (ofSlice_ne_endPos h') := by + simp [Slice.Pos.get, Nat.add_assoc] + +theorem Pos.get_eq_get_ofSlice {s : String} {p₀ p₁ : s.Pos} {h} + {pos : (s.slice p₀ p₁ h).Pos} {h'} : + pos.get h' = (ofSlice pos).get (ofSlice_ne_endPos h') := by + simp [Pos.get, Slice.Pos.get] + +theorem Slice.Pos.ofSlice_next {s : Slice} {p₀ p₁ : s.Pos} {h} + {p : (s.slice p₀ p₁ h).Pos} {h'} : + Pos.ofSlice (p.next h') = (Pos.ofSlice p).next (ofSlice_ne_endPos h') := by + simp only [Slice.Pos.ext_iff, Pos.Raw.ext_iff, Slice.Pos.offset_next, Slice.Pos.offset_ofSlice] + rw [Slice.Pos.get_eq_get_ofSlice (h' := h')] + simp [Pos.Raw.offsetBy, Nat.add_assoc] + +theorem Pos.ofSlice_next {s : String} {p₀ p₁ : s.Pos} {h} + {p : (s.slice p₀ p₁ h).Pos} {h'} : + Pos.ofSlice (p.next h') = (Pos.ofSlice p).next (ofSlice_ne_endPos h') := by + simp only [Pos.ext_iff, Pos.Raw.ext_iff, Slice.Pos.offset_next, Pos.offset_next, + Pos.offset_ofSlice] + rw [Pos.get_eq_get_ofSlice (h' := h')] + simp [Pos.Raw.offsetBy, Nat.add_assoc] + end String