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`.
This commit is contained in:
Markus Himmel
GitHub
parent
1bf43863e6
commit
1e0bfe931f
2 changed files with 278 additions and 4 deletions
|
|
@ -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₁`.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue