diff --git a/src/Init/Data/List/MinMaxOn.lean b/src/Init/Data/List/MinMaxOn.lean index f90f09f0f6..e7f2df6428 100644 --- a/src/Init/Data/List/MinMaxOn.lean +++ b/src/Init/Data/List/MinMaxOn.lean @@ -130,7 +130,7 @@ protected theorem apply_minOn_le_of_mem [LE β] [DecidableLE β] [IsLinearPreord | x :: xs => fun_induction xs.foldl (init := x) (_root_.minOn f) generalizing y · simp only [mem_cons] at hx - simp_all [le_refl _] + simp_all · rename_i x y _ ih simp at ih ⊢ rcases mem_cons.mp hx with rfl | hx diff --git a/src/Init/Data/Order/Lemmas.lean b/src/Init/Data/Order/Lemmas.lean index 95c2badc2a..d06a6253a8 100644 --- a/src/Init/Data/Order/Lemmas.lean +++ b/src/Init/Data/Order/Lemmas.lean @@ -90,9 +90,13 @@ end AxiomaticInstances section LE +@[simp] public theorem le_refl {α : Type u} [LE α] [Refl (α := α) (· ≤ ·)] (a : α) : a ≤ a := by simp [Refl.refl] +public theorem le_of_eq [LE α] [Refl (α := α) (· ≤ ·)] {a b : α} : a = b → a ≤ b := + (· ▸ le_refl _) + public theorem le_antisymm {α : Type u} [LE α] [Std.Antisymm (α := α) (· ≤ ·)] {a b : α} (hab : a ≤ b) (hba : b ≤ a) : a = b := Antisymm.antisymm _ _ hab hba @@ -226,6 +230,18 @@ public theorem lt_of_le_of_ne {α : Type u} [LE α] [LT α] intro hge exact hne.elim <| Std.Antisymm.antisymm a b hle hge +public theorem ne_of_lt {α : Type u} [LT α] [Std.Irrefl (α := α) (· < ·)] {a b : α} : a < b → a ≠ b := + fun h h' => absurd (h' ▸ h) (h' ▸ lt_irrefl) + +public theorem le_iff_lt_or_eq [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrder α] {a b : α} : + a ≤ b ↔ a < b ∨ a = b := by + refine ⟨fun h => ?_, fun h => h.elim le_of_lt le_of_eq⟩ + simp [Classical.or_iff_not_imp_left, Std.lt_iff_le_and_not_ge, h, ← Std.le_antisymm_iff] + +public theorem lt_iff_le_and_ne [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrder α] {a b : α} : + a < b ↔ a ≤ b ∧ a ≠ b := by + simpa [le_iff_lt_or_eq, or_and_right] using Std.ne_of_lt + end LT end Std diff --git a/src/Init/Data/Order/LemmasExtra.lean b/src/Init/Data/Order/LemmasExtra.lean index da19cc194a..370a100935 100644 --- a/src/Init/Data/Order/LemmasExtra.lean +++ b/src/Init/Data/Order/LemmasExtra.lean @@ -66,7 +66,7 @@ public theorem compare_eq_eq_iff_eq {α : Type u} [Ord α] [LawfulEqOrd α] {a b public theorem IsLinearPreorder.of_ord {α : Type u} [LE α] [Ord α] [LawfulOrderOrd α] [TransOrd α] : IsLinearPreorder α where - le_refl a := by simp [← isLE_compare] + le_refl a := by simp le_trans a b c := by simpa [← isLE_compare] using TransOrd.isLE_trans le_total a b := Total.total a b diff --git a/src/Init/Data/Order/PackageFactories.lean b/src/Init/Data/Order/PackageFactories.lean index 540662e548..502c259808 100644 --- a/src/Init/Data/Order/PackageFactories.lean +++ b/src/Init/Data/Order/PackageFactories.lean @@ -663,7 +663,7 @@ public def LinearPreorderPackage.ofOrd (α : Type u) isGE_compare] decidableLE := args.decidableLE decidableLT := args.decidableLT - le_refl a := by simp [← isLE_compare] + le_refl a := by simp le_total a b := by cases h : compare a b <;> simp [h, ← isLE_compare (a := a), ← isGE_compare (a := a)] le_trans a b c := by simpa [← isLE_compare] using TransOrd.isLE_trans } diff --git a/src/Init/Data/String.lean b/src/Init/Data/String.lean index 0a223710b9..858625cdd0 100644 --- a/src/Init/Data/String.lean +++ b/src/Init/Data/String.lean @@ -25,4 +25,5 @@ public import Init.Data.String.Termination public import Init.Data.String.ToSlice public import Init.Data.String.Search public import Init.Data.String.Legacy -public import Init.Data.String.Grind +public import Init.Data.String.OrderInstances +public import Init.Data.String.FindPos diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 42f4b1b236..5624cf033e 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1740,38 +1740,6 @@ theorem Pos.copy_toSlice_eq_cast {s : String} (p : s.Pos) : p.toSlice.copy = p.cast copy_toSlice.symm := Pos.ext (by simp) -/-- Given a byte position within a string slice, obtains the smallest valid position that is -strictly greater than the given byte position. -/ -@[inline] -def Slice.findNextPos (offset : String.Pos.Raw) (s : Slice) (_h : offset < s.rawEndPos) : s.Pos := - go offset.inc -where - go (offset : String.Pos.Raw) : s.Pos := - if h : offset < s.rawEndPos then - if h' : (s.getUTF8Byte offset h).IsUTF8FirstByte then - s.pos offset (Pos.Raw.isValidForSlice_iff_isUTF8FirstByte.2 (Or.inr ⟨_, h'⟩)) - else - go offset.inc - else - s.endPos - termination_by s.utf8ByteSize - offset.byteIdx - decreasing_by - simp only [Pos.Raw.lt_iff, byteIdx_rawEndPos, utf8ByteSize_eq, Pos.Raw.byteIdx_inc] at h ⊢ - omega - -private theorem Slice.le_offset_findNextPosGo {s : Slice} {o : String.Pos.Raw} (h : o ≤ s.rawEndPos) : - o ≤ (findNextPos.go s o).offset := by - fun_induction findNextPos.go with - | case1 => simp - | case2 x h₁ h₂ ih => - refine Pos.Raw.le_of_lt (Pos.Raw.lt_of_lt_of_le Pos.Raw.lt_inc (ih ?_)) - rw [Pos.Raw.le_iff, Pos.Raw.byteIdx_inc] - exact Nat.succ_le_iff.2 h₁ - | case3 x h => exact h - -theorem Slice.lt_offset_findNextPos {s : Slice} {o : String.Pos.Raw} (h) : o < (s.findNextPos o h).offset := - Pos.Raw.lt_of_lt_of_le Pos.Raw.lt_inc (le_offset_findNextPosGo (Pos.Raw.inc_le.2 h)) - theorem Slice.Pos.prevAuxGo_le_self {s : Slice} {p : Nat} {h : p < s.utf8ByteSize} : prevAux.go p h ≤ ⟨p⟩ := by induction p with @@ -2044,6 +2012,15 @@ theorem Slice.Pos.next_le_of_lt {s : Slice} {p q : s.Pos} {h} : p < q → p.next theorem Pos.ofToSlice_le_iff {s : String} {p : s.toSlice.Pos} {q : s.Pos} : ofToSlice p ≤ q ↔ p ≤ q.toSlice := Iff.rfl +theorem Pos.ofToSlice_lt_iff {s : String} {p : s.toSlice.Pos} {q : s.Pos} : + ofToSlice p < q ↔ p < q.toSlice := Iff.rfl + +theorem Pos.lt_ofToSlice_iff {s : String} {p : s.Pos} {q : s.toSlice.Pos} : + p < ofToSlice q ↔ p.toSlice < q := Iff.rfl + +theorem Pos.le_ofToSlice_iff {s : String} {p : s.Pos} {q : s.toSlice.Pos} : + p ≤ ofToSlice q ↔ p.toSlice ≤ q := Iff.rfl + @[simp] theorem Pos.toSlice_lt_toSlice_iff {s : String} {p q : s.Pos} : p.toSlice < q.toSlice ↔ p < q := Iff.rfl diff --git a/src/Init/Data/String/FindPos.lean b/src/Init/Data/String/FindPos.lean new file mode 100644 index 0000000000..4a887afd50 --- /dev/null +++ b/src/Init/Data/String/FindPos.lean @@ -0,0 +1,62 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Init.Data.String.Basic + +set_option doc.verso true + +/-! +# Finding positions in a string relative to a given raw position +-/ + +public section + +namespace String + +/-- +Obtains the smallest valid position that is greater than or equal to the given byte position. +-/ +def Slice.posGE (s : Slice) (offset : String.Pos.Raw) (_h : offset ≤ s.rawEndPos) : s.Pos := + if h : offset < s.rawEndPos then + if h' : (s.getUTF8Byte offset h).IsUTF8FirstByte then + s.pos offset (Pos.Raw.isValidForSlice_iff_isUTF8FirstByte.2 (Or.inr ⟨_, h'⟩)) + else + s.posGE offset.inc (by simpa) + else + s.endPos +termination_by s.utf8ByteSize - offset.byteIdx +decreasing_by + simp only [Pos.Raw.lt_iff, byteIdx_rawEndPos, utf8ByteSize_eq, Pos.Raw.byteIdx_inc] at h ⊢ + omega + +/-- +Obtains the smallest valid position that is strictly greater than the given byte position. +-/ +@[inline] +def Slice.posGT (s : Slice) (offset : String.Pos.Raw) (h : offset < s.rawEndPos) : s.Pos := + s.posGE offset.inc (by simpa) + +@[deprecated Slice.posGT (since := "2026-02-03")] +def Slice.findNextPos (offset : String.Pos.Raw) (s : Slice) (h : offset < s.rawEndPos) : s.Pos := + s.posGT offset h + +/-- +Obtains the smallest valid position that is greater than or equal to the given byte position. +-/ +@[inline] +def posGE (s : String) (offset : String.Pos.Raw) (h : offset ≤ s.rawEndPos) : s.Pos := + Pos.ofToSlice (s.toSlice.posGE offset (by simpa)) + +/-- +Obtains the smallest valid position that is strictly greater than the given byte position. +-/ +@[inline] +def posGT (s : String) (offset : String.Pos.Raw) (h : offset < s.rawEndPos) : s.Pos := + Pos.ofToSlice (s.toSlice.posGT offset (by simpa)) + +end String diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean index bf133f78d5..f712538ec8 100644 --- a/src/Init/Data/String/Lemmas.lean +++ b/src/Init/Data/String/Lemmas.lean @@ -9,6 +9,9 @@ prelude public import Init.Data.String.Lemmas.Splits public import Init.Data.String.Lemmas.Modify public import Init.Data.String.Lemmas.Search +public import Init.Data.String.Lemmas.FindPos +public import Init.Data.String.Lemmas.Basic +public import Init.Data.String.Lemmas.Order public import Init.Data.Char.Order public import Init.Data.Char.Lemmas public import Init.Data.List.Lex diff --git a/src/Init/Data/String/Lemmas/Basic.lean b/src/Init/Data/String/Lemmas/Basic.lean index db5e3ff260..b62a6e953e 100644 --- a/src/Init/Data/String/Lemmas/Basic.lean +++ b/src/Init/Data/String/Lemmas/Basic.lean @@ -55,4 +55,21 @@ theorem Slice.Pos.startPos_le {s : Slice} (p : s.Pos) : s.startPos ≤ p := by theorem Slice.Pos.le_endPos {s : Slice} (p : s.Pos) : p ≤ s.endPos := p.isValidForSlice.le_rawEndPos +theorem getUTF8Byte_eq_getUTF8Byte_toSlice {s : String} {p : String.Pos.Raw} {h} : + s.getUTF8Byte p h = s.toSlice.getUTF8Byte p (by simpa) := by + simp [Slice.getUTF8Byte] + +theorem getUTF8Byte_toSlice {s : String} {p : String.Pos.Raw} {h} : + s.toSlice.getUTF8Byte p h = s.getUTF8Byte p (by simpa) := by + simp [Slice.getUTF8Byte] + +@[simp] +theorem Pos.byte_toSlice {s : String} {p : s.Pos} {h} : + p.toSlice.byte h = p.byte (ne_of_apply_ne Pos.toSlice (by simpa)) := by + simp [byte] + +theorem Pos.byte_eq_byte_toSlice {s : String} {p : s.Pos} {h} : + p.byte h = p.toSlice.byte (ne_of_apply_ne Pos.ofToSlice (by simpa)) := by + simp + end String diff --git a/src/Init/Data/String/Lemmas/FindPos.lean b/src/Init/Data/String/Lemmas/FindPos.lean new file mode 100644 index 0000000000..c69550487c --- /dev/null +++ b/src/Init/Data/String/Lemmas/FindPos.lean @@ -0,0 +1,207 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Init.Data.String.FindPos +import all Init.Data.String.FindPos +import Init.Data.String.OrderInstances +import Init.Data.String.Lemmas.Basic +import Init.Data.String.Lemmas.Order + +public section + +namespace String + +namespace Slice + +@[simp] +theorem le_offset_posGE {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} : + p ≤ (s.posGE p h).offset := by + fun_induction posGE with + | case1 => simp + | case2 => exact Std.le_trans (Std.le_of_lt (Pos.Raw.lt_inc)) ‹_› + | case3 => assumption + +@[simp] +theorem posGE_le_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : + s.posGE p h ≤ q ↔ p ≤ q.offset := by + fun_induction posGE with + | case1 => simp [Pos.le_iff] + | case2 r h₁ h₂ h₃ ih => + suffices r ≠ q.offset by simp [ih, Pos.Raw.inc_le, Std.le_iff_lt_or_eq (a := r), this] + exact fun h => h₃ (h ▸ q.isUTF8FirstByte_getUTF8Byte_offset) + | case3 r h₁ h₂ => + obtain rfl : r = s.rawEndPos := Std.le_antisymm h₁ (Std.not_lt.1 h₂) + simp only [Pos.endPos_le, ← offset_endPos, ← Pos.le_iff] + +@[simp] +theorem lt_posGE_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : + q < s.posGE p h ↔ q.offset < p := by + rw [← Std.not_le, posGE_le_iff, Std.not_le] + +theorem posGE_eq_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : + s.posGE p h = q ↔ p ≤ q.offset ∧ ∀ q', p ≤ q'.offset → q ≤ q' := + ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ => Std.le_antisymm (by simpa) (h₂ _ (by simp))⟩ + +theorem posGT_eq_posGE {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} : + s.posGT p h = s.posGE p.inc (by simpa) := + (rfl) + +@[simp] +theorem posGE_inc {s : Slice} {p : Pos.Raw} {h : p.inc ≤ s.rawEndPos} : + s.posGE p.inc h = s.posGT p (by simpa) := + (rfl) + +@[simp] +theorem lt_offset_posGT {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} : + p < (s.posGT p h).offset := + Std.lt_of_lt_of_le p.lt_inc (by simp [posGT_eq_posGE, -posGE_inc]) + +@[simp] +theorem posGT_le_iff {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : + s.posGT p h ≤ q ↔ p < q.offset := by + rw [posGT_eq_posGE, posGE_le_iff, Pos.Raw.inc_le] + +@[simp] +theorem lt_posGT_iff {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : + q < s.posGT p h ↔ q.offset ≤ p := by + rw [posGT_eq_posGE, lt_posGE_iff, Pos.Raw.lt_inc_iff] + +theorem posGT_eq_iff {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : + s.posGT p h = q ↔ p < q.offset ∧ ∀ q', p < q'.offset → q ≤ q' := by + simp [posGT_eq_posGE, -posGE_inc, posGE_eq_iff] + +@[simp] +theorem Pos.posGE_offset {s : Slice} {p : s.Pos} : s.posGE p.offset (by simp) = p := by + simp [posGE_eq_iff, Pos.le_iff] + +@[simp] +theorem offset_posGE_eq_self_iff {s : Slice} {p : String.Pos.Raw} {h} : + (s.posGE p h).offset = p ↔ p.IsValidForSlice s := + ⟨fun h' => by simpa [h'] using (s.posGE p h).isValidForSlice, + fun h' => by simpa using congrArg Pos.offset (Pos.posGE_offset (p := s.pos p h'))⟩ + +theorem posGE_eq_pos {s : Slice} {p : String.Pos.Raw} (h : p.IsValidForSlice s) : + s.posGE p h.le_rawEndPos = s.pos p h := by + simpa using Pos.posGE_offset (p := s.pos p h) + +theorem pos_eq_posGE {s : Slice} {p : String.Pos.Raw} {h} : + s.pos p h = s.posGE p h.le_rawEndPos := by + simp [posGE_eq_pos h] + +@[simp] +theorem Pos.posGT_offset {s : Slice} {p : s.Pos} {h} : + s.posGT p.offset h = p.next (by simpa using h) := by + rw [posGT_eq_iff, ← Pos.lt_iff] + simp [← Pos.lt_iff] + +theorem posGT_eq_next {s : Slice} {p : String.Pos.Raw} {h} (h' : p.IsValidForSlice s) : + s.posGT p h = (s.pos p h').next (by simpa [Pos.ext_iff] using Pos.Raw.ne_of_lt h) := by + simpa using Pos.posGT_offset (h := h) (p := s.pos p h') + +theorem next_eq_posGT {s : Slice} {p : s.Pos} {h} : + p.next h = s.posGT p.offset (by simpa) := by + simp + +end Slice + +@[simp] +theorem le_offset_posGE {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} : + p ≤ (s.posGE p h).offset := by + simp [posGE] + +@[simp] +theorem posGE_le_iff {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : + s.posGE p h ≤ q ↔ p ≤ q.offset := by + simp [posGE, Pos.ofToSlice_le_iff] + +@[simp] +theorem lt_posGE_iff {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : + q < s.posGE p h ↔ q.offset < p := by + simp [posGE, Pos.lt_ofToSlice_iff] + +theorem posGE_eq_iff {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : + s.posGE p h = q ↔ p ≤ q.offset ∧ ∀ q', p ≤ q'.offset → q ≤ q' := + ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ => Std.le_antisymm (by simpa) (h₂ _ (by simp))⟩ + +theorem posGT_eq_posGE {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} : + s.posGT p h = s.posGE p.inc (by simpa) := + (rfl) + +@[simp] +theorem posGE_inc {s : String} {p : Pos.Raw} {h : p.inc ≤ s.rawEndPos} : + s.posGE p.inc h = s.posGT p (by simpa) := + (rfl) + +@[simp] +theorem lt_offset_posGT {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} : + p < (s.posGT p h).offset := + Std.lt_of_lt_of_le p.lt_inc (by simp [posGT_eq_posGE, -posGE_inc]) + +@[simp] +theorem posGT_le_iff {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : + s.posGT p h ≤ q ↔ p < q.offset := by + rw [posGT_eq_posGE, posGE_le_iff, Pos.Raw.inc_le] + +@[simp] +theorem lt_posGT_iff {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : + q < s.posGT p h ↔ q.offset ≤ p := by + rw [posGT_eq_posGE, lt_posGE_iff, Pos.Raw.lt_inc_iff] + +theorem posGT_eq_iff {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : + s.posGT p h = q ↔ p < q.offset ∧ ∀ q', p < q'.offset → q ≤ q' := by + simp [posGT_eq_posGE, -posGE_inc, posGE_eq_iff] + +theorem posGE_toSlice {s : String} {p : Pos.Raw} (h : p ≤ s.toSlice.rawEndPos) : + s.toSlice.posGE p h = (s.posGE p (by simpa)).toSlice := by + simp [posGE] + +theorem posGE_eq_posGE_toSlice {s : String} {p : Pos.Raw} (h : p ≤ s.rawEndPos) : + s.posGE p h = Pos.ofToSlice (s.toSlice.posGE p (by simpa)) := by + simp [posGE] + +theorem posGT_toSlice {s : String} {p : Pos.Raw} (h : p < s.toSlice.rawEndPos) : + s.toSlice.posGT p h = (s.posGT p (by simpa)).toSlice := by + simp [posGT] + +theorem posGT_eq_posGT_toSlice {s : String} {p : Pos.Raw} (h : p < s.rawEndPos) : + s.posGT p h = Pos.ofToSlice (s.toSlice.posGT p (by simpa)) := by + simp [posGT] + +@[simp] +theorem Pos.posGE_offset {s : String} {p : s.Pos} : s.posGE p.offset (by simp) = p := by + simp [posGE_eq_iff, Pos.le_iff] + +@[simp] +theorem offset_posGE_eq_self_iff {s : String} {p : String.Pos.Raw} {h} : + (s.posGE p h).offset = p ↔ p.IsValid s := + ⟨fun h' => by simpa [h'] using (s.posGE p h).isValid, + fun h' => by simpa using congrArg Pos.offset (Pos.posGE_offset (p := s.pos p h'))⟩ + +theorem posGE_eq_pos {s : String} {p : String.Pos.Raw} (h : p.IsValid s) : + s.posGE p h.le_rawEndPos = s.pos p h := by + simpa using Pos.posGE_offset (p := s.pos p h) + +theorem pos_eq_posGE {s : String} {p : String.Pos.Raw} {h} : + s.pos p h = s.posGE p h.le_rawEndPos := by + simp [posGE_eq_pos h] + +@[simp] +theorem Pos.posGT_offset {s : String} {p : s.Pos} {h} : + s.posGT p.offset h = p.next (by simpa using h) := by + rw [posGT_eq_iff, ← Pos.lt_iff] + simp [← Pos.lt_iff] + +theorem posGT_eq_next {s : String} {p : String.Pos.Raw} {h} (h' : p.IsValid s) : + s.posGT p h = (s.pos p h').next (by simpa [Pos.ext_iff] using Pos.Raw.ne_of_lt h) := by + simpa using Pos.posGT_offset (h := h) (p := s.pos p h') + +theorem next_eq_posGT {s : String} {p : s.Pos} {h} : + p.next h = s.posGT p.offset (by simpa) := by + simp + +end String diff --git a/src/Init/Data/String/Lemmas/Order.lean b/src/Init/Data/String/Lemmas/Order.lean new file mode 100644 index 0000000000..a19d9e490c --- /dev/null +++ b/src/Init/Data/String/Lemmas/Order.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Markus Himmel +-/ +module + +prelude +public import Init.Data.String.Basic +import Init.Data.String.OrderInstances +import Init.Data.String.Lemmas.Basic + +public section + +namespace String + +@[simp] +theorem Slice.Pos.next_le_iff_lt {s : Slice} {p q : s.Pos} {h} : p.next h ≤ q ↔ p < q := + ⟨fun h => Std.lt_of_lt_of_le lt_next h, next_le_of_lt⟩ + +@[simp] +theorem Slice.Pos.lt_next_iff_le {s : Slice} {p q : s.Pos} {h} : p < q.next h ↔ p ≤ q := by + rw [← Decidable.not_iff_not, Std.not_lt, next_le_iff_lt, Std.not_le] + +@[simp] +theorem Pos.next_le_iff_lt {s : String} {p q : s.Pos} {h} : p.next h ≤ q ↔ p < q := by + rw [next, Pos.ofToSlice_le_iff, ← Pos.toSlice_lt_toSlice_iff] + exact Slice.Pos.next_le_iff_lt + +@[simp] +theorem Slice.Pos.le_startPos {s : Slice} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos := + ⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩ + +@[simp] +theorem Slice.Pos.startPos_lt_iff {s : Slice} (p : s.Pos) : s.startPos < p ↔ p ≠ s.startPos := by + simp [← le_startPos, Std.not_le] + +@[simp] +theorem Slice.Pos.endPos_le {s : Slice} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos := + ⟨fun h => Std.le_antisymm (le_endPos _) h, by simp +contextual⟩ + +@[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⟩ + +@[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 _)) + +theorem Slice.Pos.ne_startPos_of_lt {s : Slice} {p q : s.Pos} : p < q → q ≠ s.startPos := by + rintro h rfl + simp at h + +@[simp] +theorem Slice.Pos.next_ne_startPos {s : Slice} {p : s.Pos} {h} : + p.next h ≠ s.startPos := + ne_startPos_of_lt lt_next + +theorem Slice.Pos.ofSliceFrom_lt_ofSliceFrom_iff {s : Slice} {p : s.Pos} + {q r : (s.sliceFrom p).Pos} : Slice.Pos.ofSliceFrom q < Slice.Pos.ofSliceFrom r ↔ q < r := by + simp [Slice.Pos.lt_iff, Pos.Raw.lt_iff] + +theorem Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff {s : Slice} {p : s.Pos} + {q r : (s.sliceFrom p).Pos} : Slice.Pos.ofSliceFrom q ≤ Slice.Pos.ofSliceFrom r ↔ q ≤ r := by + simp [Slice.Pos.le_iff, Pos.Raw.le_iff] + +@[simp] +theorem Slice.Pos.offset_le_rawEndPos {s : Slice} {p : s.Pos} : + p.offset ≤ s.rawEndPos := + p.isValidForSlice.le_rawEndPos + +@[simp] +theorem Pos.offset_le_rawEndPos {s : String} {p : s.Pos} : + p.offset ≤ s.rawEndPos := + p.isValid.le_rawEndPos + +@[simp] +theorem Slice.Pos.offset_lt_rawEndPos_iff {s : Slice} {p : s.Pos} : + p.offset < s.rawEndPos ↔ p ≠ s.endPos := by + simp [Std.lt_iff_le_and_ne, p.offset_le_rawEndPos, Pos.ext_iff] + +@[simp] +theorem Pos.offset_lt_rawEndPos_iff {s : String} {p : s.Pos} : + p.offset < s.rawEndPos ↔ p ≠ s.endPos := by + simp [Std.lt_iff_le_and_ne, p.offset_le_rawEndPos, Pos.ext_iff] + +@[simp] +theorem Slice.Pos.getUTF8Byte_offset {s : Slice} {p : s.Pos} {h} : + s.getUTF8Byte p.offset h = p.byte (by simpa using h) := by + simp [Pos.byte] + +theorem Slice.Pos.isUTF8FirstByte_getUTF8Byte_offset {s : Slice} {p : s.Pos} {h} : + (s.getUTF8Byte p.offset h).IsUTF8FirstByte := by + simpa [getUTF8Byte_offset] using isUTF8FirstByte_byte + +theorem Pos.getUTF8Byte_offset {s : String} {p : s.Pos} {h} : + s.getUTF8Byte p.offset h = p.byte (by simpa using h) := by + simp only [getUTF8Byte_eq_getUTF8Byte_toSlice, ← Pos.offset_toSlice, + Slice.Pos.getUTF8Byte_offset, byte_toSlice] + +theorem Pos.isUTF8FirstByte_getUTF8Byte_offset {s : String} {p : s.Pos} {h} : + (s.getUTF8Byte p.offset h).IsUTF8FirstByte := by + simpa [getUTF8Byte_offset] using isUTF8FirstByte_byte + +end String diff --git a/src/Init/Data/String/Grind.lean b/src/Init/Data/String/OrderInstances.lean similarity index 100% rename from src/Init/Data/String/Grind.lean rename to src/Init/Data/String/OrderInstances.lean diff --git a/src/Init/Data/String/Pattern/String.lean b/src/Init/Data/String/Pattern/String.lean index 720e1bcd3d..1d7fe24d67 100644 --- a/src/Init/Data/String/Pattern/String.lean +++ b/src/Init/Data/String/Pattern/String.lean @@ -8,8 +8,10 @@ module prelude public import Init.Data.String.Pattern.Basic public import Init.Data.Iterators.Consumers.Monadic.Loop -import Init.Data.String.Termination public import Init.Data.Vector.Basic +public import Init.Data.String.FindPos +import Init.Data.String.Termination +import Init.Data.String.Lemmas.FindPos set_option doc.verso true @@ -148,15 +150,15 @@ instance (s : Slice) : Std.Iterator (ForwardSliceSearcher s) Id (SearchStep s) w let basePos := s.pos! stackPos -- Since we report (mis)matches by code point and not by byte, missing in the first byte -- means that we should skip ahead to the next code point. - let nextStackPos := s.findNextPos stackPos h₁ + let nextStackPos := s.posGT stackPos h₁ let res := .rejected basePos nextStackPos -- Invariants still satisfied pure (.deflate ⟨.yield ⟨.proper needle table htable nextStackPos.offset 0 (by simp [Pos.Raw.lt_iff] at hn ⊢; omega)⟩ res, by simpa using ⟨_, _, ⟨rfl, rfl⟩, by simp [Pos.Raw.lt_iff] at hn ⊢; omega, Or.inl (by - have := lt_offset_findNextPos h₁ - have t₀ := (findNextPos _ _ h₁).isValidForSlice.le_utf8ByteSize + have := lt_offset_posGT (h := h₁) + have t₀ := (posGT _ _ h₁).isValidForSlice.le_utf8ByteSize simp [nextStackPos, Pos.Raw.lt_iff] at this ⊢; omega)⟩⟩) else let newNeedlePos := table[needlePos.byteIdx - 1]'(by simp [Pos.Raw.lt_iff] at hn; omega) @@ -165,19 +167,16 @@ instance (s : Slice) : Std.Iterator (ForwardSliceSearcher s) Id (SearchStep s) w let basePos := s.pos! (stackPos.unoffsetBy needlePos) -- Since we report (mis)matches by code point and not by byte, missing in the first byte -- means that we should skip ahead to the next code point. - let nextStackPos := (s.pos? stackPos).getD (s.findNextPos stackPos h₁) + let nextStackPos := s.posGE stackPos (Pos.Raw.le_of_lt h₁) let res := .rejected basePos nextStackPos -- Invariants still satisfied pure (.deflate ⟨.yield ⟨.proper needle table htable nextStackPos.offset 0 (by simp [Pos.Raw.lt_iff] at hn ⊢; omega)⟩ res, by simpa using ⟨_, _, ⟨rfl, rfl⟩, by simp [Pos.Raw.lt_iff] at hn ⊢; omega, by - simp only [pos?, Pos.Raw.isValidForSlice_eq_true_iff, nextStackPos] - split - · exact Or.inr (by simp [Pos.Raw.lt_iff]; omega) - · refine Or.inl ?_ - have := lt_offset_findNextPos h₁ - have t₀ := (findNextPos _ _ h₁).isValidForSlice.le_utf8ByteSize - simp [Pos.Raw.lt_iff] at this ⊢; omega⟩⟩) + have h₂ := le_offset_posGE (h := Pos.Raw.le_of_lt h₁) + have h₃ := (s.posGE _ (Pos.Raw.le_of_lt h₁)).isValidForSlice.le_utf8ByteSize + simp [Pos.Raw.le_iff, Pos.Raw.lt_iff, Pos.Raw.ext_iff, nextStackPos] at ⊢ h₂ + omega⟩⟩) else let oldBasePos := s.pos! (stackPos.decreaseBy needlePos.byteIdx) let newBasePos := s.pos! (stackPos.decreaseBy newNeedlePos) @@ -264,8 +263,7 @@ def startsWith (pat : Slice) (s : Slice) : Bool := have hs := by simp [Pos.Raw.le_iff] at h ⊢ omega - have hp := by - simp [Pos.Raw.le_iff] + have hp := by simp Internal.memcmpSlice s pat s.startPos.offset pat.startPos.offset pat.rawEndPos hs hp else false @@ -301,7 +299,7 @@ def endsWith (pat : Slice) (s : Slice) : Bool := simp [sStart, Pos.Raw.le_iff] at h ⊢ omega have hp := by - simp [patStart, Pos.Raw.le_iff] at h ⊢ + simp [patStart] at h ⊢ Internal.memcmpSlice s pat sStart patStart pat.rawEndPos hs hp else false diff --git a/src/Init/Data/String/PosRaw.lean b/src/Init/Data/String/PosRaw.lean index da3379fda2..30411fb565 100644 --- a/src/Init/Data/String/PosRaw.lean +++ b/src/Init/Data/String/PosRaw.lean @@ -144,8 +144,11 @@ theorem Pos.Raw.offsetBy_assoc {p q r : Pos.Raw} : @[simp] theorem Pos.Raw.offsetBy_zero_left {p : Pos.Raw} : (0 : Pos.Raw).offsetBy p = p := by - ext - simp + simp [Pos.Raw.ext_iff] + +@[simp] +theorem Pos.Raw.offsetBy_zero {p : Pos.Raw} : p.offsetBy 0 = p := by + simp [Pos.Raw.ext_iff] /-- Decreases `p` by `offset`. This is not an `HSub` instance because it should be a relatively @@ -174,6 +177,14 @@ theorem Pos.Raw.unoffsetBy_offsetBy {p q : Pos.Raw} : (p.offsetBy q).unoffsetBy ext simp +@[simp] +theorem Pos.Raw.unoffsetBy_zero {p : Pos.Raw} : p.unoffsetBy 0 = p := by + simp [Pos.Raw.ext_iff] + +@[simp] +theorem Pos.Raw.unoffsetBy_le_self {p q : Pos.Raw} : p.unoffsetBy q ≤ p := by + simp [Pos.Raw.le_iff] + @[simp] theorem Pos.Raw.eq_zero_iff {p : Pos.Raw} : p = 0 ↔ p.byteIdx = 0 := Pos.Raw.ext_iff @@ -195,6 +206,10 @@ def Pos.Raw.increaseBy (p : Pos.Raw) (n : Nat) : Pos.Raw where theorem Pos.Raw.byteIdx_increaseBy {p : Pos.Raw} {n : Nat} : (p.increaseBy n).byteIdx = p.byteIdx + n := (rfl) +@[simp] +theorem Pos.Raw.increaseBy_zero {p : Pos.Raw} : p.increaseBy 0 = p := by + simp [Pos.Raw.ext_iff] + /-- Move the position `p` back by `n` bytes. This is not an `HSub` instance because it should be a relatively rare operation, so we use a name to make accidental use less likely. To remove the size @@ -212,6 +227,10 @@ def Pos.Raw.decreaseBy (p : Pos.Raw) (n : Nat) : Pos.Raw where theorem Pos.Raw.byteIdx_decreaseBy {p : Pos.Raw} {n : Nat} : (p.decreaseBy n).byteIdx = p.byteIdx - n := (rfl) +@[simp] +theorem Pos.Raw.decreaseBy_zero {p : Pos.Raw} : p.decreaseBy 0 = p := by + simp [Pos.Raw.ext_iff] + theorem Pos.Raw.increaseBy_charUtf8Size {p : Pos.Raw} {c : Char} : p.increaseBy c.utf8Size = p + c := by simp [Pos.Raw.ext_iff] @@ -224,6 +243,10 @@ def Pos.Raw.inc (p : Pos.Raw) : Pos.Raw := @[simp] theorem Pos.Raw.byteIdx_inc {p : Pos.Raw} : p.inc.byteIdx = p.byteIdx + 1 := (rfl) +@[simp] +theorem Pos.Raw.inc_unoffsetBy_inc {p q : Pos.Raw} : p.inc.unoffsetBy q.inc = p.unoffsetBy q := by + simp [Pos.Raw.ext_iff] + /-- Decreases the byte offset of the position by `1`. Not to be confused with `Pos.prev`. -/ @[inline, expose] def Pos.Raw.dec (p : Pos.Raw) : Pos.Raw := @@ -235,12 +258,17 @@ theorem Pos.Raw.byteIdx_dec {p : Pos.Raw} : p.dec.byteIdx = p.byteIdx - 1 := (rf @[simp] theorem Pos.Raw.le_refl {p : Pos.Raw} : p ≤ p := by simp [le_iff] +@[simp] theorem Pos.Raw.lt_inc {p : Pos.Raw} : p < p.inc := by simp [lt_iff] theorem Pos.Raw.le_of_lt {p q : Pos.Raw} : p < q → p ≤ q := by simpa [lt_iff, le_iff] using Nat.le_of_lt +@[simp] theorem Pos.Raw.inc_le {p q : Pos.Raw} : p.inc ≤ q ↔ p < q := by simpa [lt_iff, le_iff] using Nat.succ_le_iff +@[simp] +theorem Pos.Raw.lt_inc_iff {p q : Pos.Raw} : p < q.inc ↔ p ≤ q := by simpa [lt_iff, le_iff] using Nat.lt_add_one_iff + theorem Pos.Raw.lt_of_le_of_lt {a b c : Pos.Raw} : a ≤ b → b < c → a < c := by simpa [le_iff, lt_iff] using Nat.lt_of_le_of_lt diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean index a54f2ffb5e..4820bbb957 100644 --- a/src/Init/Data/String/Slice.lean +++ b/src/Init/Data/String/Slice.lean @@ -66,7 +66,7 @@ The implementation is an efficient equivalent of {lean}`s1.copy == s2.copy` -/ def beq (s1 s2 : Slice) : Bool := if h : s1.utf8ByteSize = s2.utf8ByteSize then - have h1 := by simp [h, String.Pos.Raw.le_iff] + have h1 := by simp have h2 := by simp [h, String.Pos.Raw.le_iff] Internal.memcmpSlice s1 s2 s1.startPos.offset s2.startPos.offset s1.rawEndPos h1 h2 else diff --git a/src/Init/Grind/Module/Envelope.lean b/src/Init/Grind/Module/Envelope.lean index 9180c19ad8..b676da308e 100644 --- a/src/Init/Grind/Module/Envelope.lean +++ b/src/Init/Grind/Module/Envelope.lean @@ -305,7 +305,7 @@ instance [LE α] [IsPreorder α] [OrderedAdd α] : IsPreorder (OfNatModule.Q α) obtain ⟨⟨a₁, a₂⟩⟩ := a change Q.mk _ ≤ Q.mk _ simp only [mk_le_mk] - simp [AddCommMonoid.add_comm]; exact le_refl (a₁ + a₂) + simp [AddCommMonoid.add_comm] le_trans {a b c} h₁ h₂ := by induction a using Q.ind with | _ a induction b using Q.ind with | _ b diff --git a/src/Init/Grind/Order.lean b/src/Init/Grind/Order.lean index 8c55cd32f1..06f17d4008 100644 --- a/src/Init/Grind/Order.lean +++ b/src/Init/Grind/Order.lean @@ -225,7 +225,7 @@ theorem le_eq_true_of_lt {α} [LE α] [LT α] [Std.LawfulOrderLT α] theorem le_eq_true {α} [LE α] [Std.IsPreorder α] {a : α} : (a ≤ a) = True := by - simp; exact Std.le_refl a + simp theorem le_eq_true_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a : α} {k : Int} : (0 : Int).ble' k → (a ≤ a + k) = True := by diff --git a/src/Init/Grind/Ordered/Linarith.lean b/src/Init/Grind/Ordered/Linarith.lean index dab4a5bba8..1239955158 100644 --- a/src/Init/Grind/Ordered/Linarith.lean +++ b/src/Init/Grind/Ordered/Linarith.lean @@ -327,7 +327,6 @@ theorem eq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Pol theorem le_of_eq {α} [IntModule α] [LE α] [IsPreorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote' ctx ≤ 0 := by simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self] - apply le_refl theorem diseq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p → lhs.denote ctx ≠ rhs.denote ctx → p.denote' ctx ≠ 0 := by diff --git a/src/Init/Grind/Ordered/Ring.lean b/src/Init/Grind/Ordered/Ring.lean index 3bea9e8d09..9dbeac9ac7 100644 --- a/src/Init/Grind/Ordered/Ring.lean +++ b/src/Init/Grind/Ordered/Ring.lean @@ -44,7 +44,7 @@ theorem neg_one_lt_zero : (-1 : R) < 0 := by theorem ofNat_nonneg (x : Nat) : (OfNat.ofNat x : R) ≥ 0 := by induction x - next => simp [OfNat.ofNat, Zero.zero]; apply le_refl + next => simp [OfNat.ofNat, Zero.zero] next n ih => have := OrderedRing.zero_lt_one (R := R) rw [Semiring.ofNat_succ] @@ -134,8 +134,8 @@ theorem lt_of_intCast_lt_intCast (a b : Int) : (a : R) < (b : R) → a < b := by omega theorem natCast_le_natCast_of_le (a b : Nat) : a ≤ b → (a : R) ≤ (b : R) := by - induction a generalizing b <;> cases b <;> simp - next => simp [Semiring.natCast_zero, Std.IsPreorder.le_refl] + induction a generalizing b <;> cases b <;> simp [- Std.le_refl] + next => simp [Semiring.natCast_zero] next n => have := ofNat_nonneg (R := R) n simp [Semiring.ofNat_eq_natCast] at this diff --git a/src/Init/Grind/Ring/Envelope.lean b/src/Init/Grind/Ring/Envelope.lean index 180c3461ff..6daca3677b 100644 --- a/src/Init/Grind/Ring/Envelope.lean +++ b/src/Init/Grind/Ring/Envelope.lean @@ -393,7 +393,7 @@ instance [LE α] [IsPreorder α] [OrderedAdd α] : IsPreorder (OfSemiring.Q α) obtain ⟨⟨a₁, a₂⟩⟩ := a change Q.mk _ ≤ Q.mk _ simp only [mk_le_mk] - simp [Semiring.add_comm]; exact le_refl (a₁ + a₂) + simp [Semiring.add_comm] le_trans {a b c} h₁ h₂ := by induction a using Q.ind with | _ a induction b using Q.ind with | _ b