diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index b0e7d1550a..0ebeacbec0 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -2542,6 +2542,9 @@ grind_pattern flatMap_reverse => l.reverse.flatMap f where ⟨by rw [length_reverse, length_replicate], fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩ +theorem reverse_singleton {a : α} : [a].reverse = [a] := by + simp + @[simp] theorem append_singleton_inj {as bs : List α} : as ++ [a] = bs ++ [b] ↔ as = bs ∧ a = b := by rw [← List.reverse_inj, And.comm]; simp diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 362f5532e0..4e6ed23b9b 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1642,25 +1642,6 @@ theorem Pos.Raw.isValidForSlice_prevAux {s : Slice} (pos : s.Pos) (h : pos ≠ s (pos.prevAux h).IsValidForSlice s := isValidForSlice_prevAuxGo .. -/-- Returns the previous valid position before the given position, given a proof that the position -is not the start position, which guarantees that such a position exists. -/ -@[inline, expose] -def Slice.Pos.prev {s : Slice} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos where - offset := prevAux pos h - isValidForSlice := Pos.Raw.isValidForSlice_prevAux _ _ - -/-- Returns the previous valid position before the given position, or `none` if the position is -the start position. -/ -@[expose] -def Slice.Pos.prev? {s : Slice} (pos : s.Pos) : Option s.Pos := - if h : pos = s.startPos then none else some (pos.prev h) - -/-- Returns the previous valid position before the given position, or panics if the position is -the start position. -/ -@[expose] -def Slice.Pos.prev! {s : Slice} (pos : s.Pos) : s.Pos := - if h : pos = s.startPos then panic! "The start position has no previous position" else pos.prev h - /-- Constructs a valid position on `s` from a position and a proof that it is valid. -/ @[inline, expose] def Slice.pos (s : Slice) (off : String.Pos.Raw) (h : off.IsValidForSlice s) : s.Pos where @@ -1713,24 +1694,6 @@ position is the past-the-end position. -/ def Pos.next! {s : String} (pos : s.Pos) : s.Pos := ofToSlice pos.toSlice.next! -/-- Returns the previous valid position before the given position, given a proof that the position -is not the start position, which guarantees that such a position exists. -/ -@[inline, expose] -def Pos.prev {s : String} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos := - ofToSlice (pos.toSlice.prev (ne_of_apply_ne Pos.ofToSlice (by simpa))) - -/-- Returns the previous valid position before the given position, or `none` if the position is -the start position. -/ -@[inline, expose] -def Pos.prev? {s : String} (pos : s.Pos) : Option s.Pos := - pos.toSlice.prev?.map Pos.ofToSlice - -/-- Returns the previous valid position before the given position, or panics if the position is -the start position. -/ -@[inline, expose] -def Pos.prev! {s : String} (pos : s.Pos) : s.Pos := - ofToSlice pos.toSlice.prev! - /-- Constructs a valid position on `s` from a position and a proof that it is valid. -/ @[inline, expose] def pos (s : String) (off : Pos.Raw) (h : off.IsValid s) : s.Pos := @@ -1826,30 +1789,6 @@ theorem Slice.Pos.prevAux_lt_self {s : Slice} {p : s.Pos} {h} : p.prevAux h < p. theorem Slice.Pos.prevAux_lt_rawEndPos {s : Slice} {p : s.Pos} {h} : p.prevAux h < s.rawEndPos := Pos.Raw.lt_of_lt_of_le prevAux_lt_self p.isValidForSlice.le_rawEndPos -@[simp] -theorem Slice.Pos.prev_ne_endPos {s : Slice} {p : s.Pos} {h} : p.prev h ≠ s.endPos := by - simpa [Pos.ext_iff, prev] using Pos.Raw.ne_of_lt prevAux_lt_rawEndPos - -@[simp] -theorem Pos.prev_ne_endPos {s : String} {p : s.Pos} {h} : p.prev h ≠ s.endPos := - mt (congrArg (·.toSlice)) (Slice.Pos.prev_ne_endPos (h := mt (congrArg Pos.ofToSlice) (by simpa))) - -theorem Pos.toSlice_prev {s : String} {p : s.Pos} {h} : - (p.prev h).toSlice = p.toSlice.prev (ne_of_apply_ne Pos.ofToSlice (by simpa)) := by - simp [prev] - -theorem Slice.Pos.offset_prev_lt_offset {s : Slice} {p : s.Pos} {h} : (p.prev h).offset < p.offset := by - simpa [prev] using prevAux_lt_self - -@[simp] -theorem Slice.Pos.prev_lt {s : Slice} {p : s.Pos} {h} : p.prev h < p := - lt_iff.2 offset_prev_lt_offset - -@[simp] -theorem Pos.prev_lt {s : String} {p : s.Pos} {h} : p.prev h < p := by - simp [← toSlice_lt, toSlice_prev] - - @[expose] def Pos.Raw.utf8GetAux : List Char → Pos.Raw → Pos.Raw → Char | [], _, _ => default @@ -1989,6 +1928,7 @@ theorem Pos.ne_startPos_of_lt {s : String} {p q : s.Pos} : Pos.Raw.byteIdx_zero] omega +@[simp] theorem Pos.next_ne_startPos {s : String} {p : s.Pos} {h} : p.next h ≠ s.startPos := ne_startPos_of_lt p.lt_next @@ -2637,20 +2577,6 @@ def Slice.Pos.nextn {s : Slice} (p : s.Pos) (n : Nat) : s.Pos := else p -/-- -Iterates `p.prev` `n` times. - -If this would move `p` past the start of `s`, the result is `s.endPos`. --/ -def Slice.Pos.prevn {s : Slice} (p : s.Pos) (n : Nat) : s.Pos := - match n with - | 0 => p - | n + 1 => - if h : p ≠ s.startPos then - prevn (p.prev h) n - else - p - /-- Advances the position `p` `n` times. @@ -2660,14 +2586,6 @@ If this would move `p` past the end of `s`, the result is `s.endPos`. def Pos.nextn {s : String} (p : s.Pos) (n : Nat) : s.Pos := ofToSlice (p.toSlice.nextn n) -/-- -Iterates `p.prev` `n` times. - -If this would move `p` past the start of `s`, the result is `s.startPos`. --/ -@[inline] -def Pos.prevn {s : String} (p : s.Pos) (n : Nat) : s.Pos := - ofToSlice (p.toSlice.prevn n) theorem Slice.Pos.le_nextn {s : Slice} {p : s.Pos} {n : Nat} : p ≤ p.nextn n := by fun_induction nextn with @@ -2681,17 +2599,6 @@ theorem Pos.le_nextn {s : String} {p : s.Pos} {n : Nat} : p ≤ p.nextn n := by simpa [nextn, Pos.le_iff, ← offset_toSlice] using Slice.Pos.le_nextn -theorem Slice.Pos.prevn_le {s : Slice} {p : s.Pos} {n : Nat} : p.prevn n ≤ p := by - fun_induction prevn with - | case1 => simp - | case2 p n h ih => - simp only [Pos.le_iff] at * - exact Pos.Raw.le_of_lt (Pos.Raw.lt_of_le_of_lt ih prev_lt) - | case3 => simp - -theorem Pos.prevn_le {s : String} {p : s.Pos} {n : Nat} : - p.prevn n ≤ p := by - simpa [nextn, Pos.le_iff, ← offset_toSlice] using Slice.Pos.prevn_le /-- Returns the next position in a string after position `p`. If `p` is not a valid position or `p = s.endPos`, returns the position one byte after `p`. diff --git a/src/Init/Data/String/FindPos.lean b/src/Init/Data/String/FindPos.lean index e67075aa8c..f4025ea9e4 100644 --- a/src/Init/Data/String/FindPos.lean +++ b/src/Init/Data/String/FindPos.lean @@ -8,6 +8,8 @@ module prelude public import Init.Data.String.Basic import Init.Omega +import Init.Data.String.OrderInstances +import Init.Data.String.Lemmas.Basic set_option doc.verso true @@ -22,17 +24,15 @@ 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) +def Slice.posGE (s : Slice) (offset : String.Pos.Raw) (h : offset ≤ s.rawEndPos) : s.Pos := + if h' : offset.IsValidForSlice s then + s.pos offset h' else - s.endPos + have : offset < s.rawEndPos := Std.not_le.1 (fun h₁ => h' (Std.le_antisymm h h₁ ▸ Pos.Raw.isValidForSlice_rawEndPos)) + s.posGE offset.inc (by simpa) termination_by s.utf8ByteSize - offset.byteIdx decreasing_by - simp only [Pos.Raw.lt_iff, byteIdx_rawEndPos, utf8ByteSize_eq, Pos.Raw.byteIdx_inc] at h ⊢ + simp only [Pos.Raw.lt_iff, byteIdx_rawEndPos, Pos.Raw.byteIdx_inc] at this ⊢ omega /-- @@ -60,4 +60,99 @@ Obtains the smallest valid position that is strictly greater than the given byte def posGT (s : String) (offset : String.Pos.Raw) (h : offset < s.rawEndPos) : s.Pos := Pos.ofToSlice (s.toSlice.posGT offset (by simpa)) +/-- +Obtains the largest valid position that is less than or equal to the given byte position. +-/ +@[expose] +def Slice.posLE (s : Slice) (offset : String.Pos.Raw) : s.Pos := + if h' : offset.IsValidForSlice s then + s.pos offset h' + else + have : offset ≠ 0 := by rintro rfl; simp at h' + s.posLE offset.dec +termination_by offset.byteIdx +decreasing_by simp only [ne_eq, Pos.Raw.eq_zero_iff, Pos.Raw.byteIdx_dec] at ⊢ this; omega + +/-- +Obtains the largest valid position that is strictly less than the given byte position. +-/ +@[inline, expose] +def Slice.posLT (s : Slice) (offset : String.Pos.Raw) (_h : 0 < offset) : s.Pos := + s.posLE offset.dec + +/-- +Obtains the largest valid position that is less than or equal to the given byte position. +-/ +@[inline] +def posLE (s : String) (offset : String.Pos.Raw) : s.Pos := + Pos.ofToSlice (s.toSlice.posLE offset) + +/-- +Obtains the largest valid position that is strictly less than the given byte position. +-/ +@[inline] +def posLT (s : String) (offset : String.Pos.Raw) (h : 0 < offset) : s.Pos := + Pos.ofToSlice (s.toSlice.posLT offset h) + +/-- +Returns the previous valid position before the given position, given a proof that the position +is not the start position, which guarantees that such a position exists. +-/ +@[inline, expose] +def Slice.Pos.prev {s : Slice} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos := + s.posLT pos.offset (by simpa [Pos.Raw.pos_iff_ne_zero, Pos.ext_iff] using h) + +/-- Returns the previous valid position before the given position, or {lean}`none` if the position is +the start position. -/ +@[expose] +def Slice.Pos.prev? {s : Slice} (pos : s.Pos) : Option s.Pos := + if h : pos = s.startPos then none else some (pos.prev h) + +/-- Returns the previous valid position before the given position, or panics if the position is +the start position. -/ +@[expose] +def Slice.Pos.prev! {s : Slice} (pos : s.Pos) : s.Pos := + if h : pos = s.startPos then panic! "The start position has no previous position" else pos.prev h + +/-- Returns the previous valid position before the given position, given a proof that the position +is not the start position, which guarantees that such a position exists. -/ +@[inline, expose] +def Pos.prev {s : String} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos := + ofToSlice (pos.toSlice.prev (ne_of_apply_ne Pos.ofToSlice (by simpa))) + +/-- Returns the previous valid position before the given position, or {lean}`none` if the position is +the start position. -/ +@[inline, expose] +def Pos.prev? {s : String} (pos : s.Pos) : Option s.Pos := + pos.toSlice.prev?.map Pos.ofToSlice + +/-- Returns the previous valid position before the given position, or panics if the position is +the start position. -/ +@[inline, expose] +def Pos.prev! {s : String} (pos : s.Pos) : s.Pos := + ofToSlice pos.toSlice.prev! + +/-- +Iterates {lean}`p.prev` {name}`n` times. + +If this would move {name}`p` past the start of {name}`s`, the result is {lean}`s.endPos`. +-/ +def Slice.Pos.prevn {s : Slice} (p : s.Pos) (n : Nat) : s.Pos := + match n with + | 0 => p + | n + 1 => + if h : p ≠ s.startPos then + prevn (p.prev h) n + else + p + +/-- +Iterates {lean}`p.prev` {name}`n` times. + +If this would move {name}`p` past the start of {name}`s`, the result is {lean}`s.startPos`. +-/ +@[inline] +def Pos.prevn {s : String} (p : s.Pos) (n : Nat) : s.Pos := + ofToSlice (p.toSlice.prevn n) + end String diff --git a/src/Init/Data/String/Iterate.lean b/src/Init/Data/String/Iterate.lean index 4251b5a038..f7407aec26 100644 --- a/src/Init/Data/String/Iterate.lean +++ b/src/Init/Data/String/Iterate.lean @@ -7,10 +7,12 @@ module prelude public import Init.Data.String.Basic +public import Init.Data.String.FindPos public import Init.Data.Iterators.Combinators.FilterMap public import Init.Data.Iterators.Consumers.Loop import Init.Omega import Init.Data.Iterators.Consumers.Collect +import Init.Data.String.Lemmas.FindPos set_option doc.verso true @@ -22,18 +24,25 @@ structure PosIterator (s : Slice) where currPos : s.Pos deriving Inhabited +/-- +Creates an iterator over the valid positions within {name}`s`, starting at {name}`p`. +-/ +def positionsFrom {s : Slice} (p : s.Pos) : + Std.Iter (α := PosIterator s) { p : s.Pos // p ≠ s.endPos } := + { internalState := { currPos := p } } + set_option doc.verso false /-- Creates an iterator over all valid positions within {name}`s`. -Examples +Examples: * {lean}`("abc".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', 'c']` * {lean}`("abc".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2]` * {lean}`("ab∀c".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', '∀', 'c']` * {lean}`("ab∀c".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2, 5]` -/ def positions (s : Slice) : Std.Iter (α := PosIterator s) { p : s.Pos // p ≠ s.endPos } := - { internalState := { currPos := s.startPos }} + s.positionsFrom s.startPos set_option doc.verso true @@ -102,6 +111,13 @@ structure RevPosIterator (s : Slice) where currPos : s.Pos deriving Inhabited +/-- +Creates an iterator over all valid positions within {name}`s` that are strictly smaller than +{name}`p`, starting from the position before {name}`p` and iterating towards the first one. +-/ +def revPositionsFrom (s : Slice) (p : s.Pos) : Std.Iter (α := RevPosIterator s) { p : s.Pos // p ≠ s.endPos } := + { internalState := { currPos := p } } + set_option doc.verso false /-- Creates an iterator over all valid positions within {name}`s`, starting from the last valid @@ -114,7 +130,7 @@ Examples * {lean}`("ab∀c".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [5, 2, 1, 0]` -/ def revPositions (s : Slice) : Std.Iter (α := RevPosIterator s) { p : s.Pos // p ≠ s.endPos } := - { internalState := { currPos := s.endPos }} + s.revPositionsFrom s.endPos set_option doc.verso true @@ -134,7 +150,7 @@ instance [Pure m] : pure (.deflate ⟨.done, by simp [h]⟩) else let prevPos := currPos.prev h - pure (.deflate ⟨.yield ⟨⟨prevPos⟩⟩ ⟨prevPos, Pos.prev_ne_endPos⟩, by simp [h, prevPos]⟩) + pure (.deflate ⟨.yield ⟨⟨prevPos⟩⟩ ⟨prevPos, by exact Pos.prev_ne_endPos⟩, by simp [h, prevPos]⟩) private def finitenessRelation [Pure m] : Std.Iterators.FinitenessRelation (RevPosIterator s) m where @@ -147,8 +163,8 @@ private def finitenessRelation [Pure m] : cases step · cases h obtain ⟨h1, h2, _⟩ := h' - have h3 := Pos.offset_prev_lt_offset (h := h1) - simp [Pos.ext_iff, String.Pos.Raw.ext_iff, String.Pos.Raw.lt_iff] at h2 h3 + have h3 := Pos.prev_lt (h := h1) + simp [Pos.ext_iff, Pos.lt_iff, String.Pos.Raw.ext_iff, String.Pos.Raw.lt_iff] at h2 h3 omega · cases h' · cases h @@ -317,7 +333,7 @@ instance [Monad m] [Monad n] : Std.IteratorLoop RevByteIterator m n := docs_to_verso revBytes -instance : ForIn Id String.Slice Char where +instance {m : Type u → Type v} [Monad m] : ForIn m String.Slice Char where forIn s b f := ForIn.forIn s.chars b f end RevByteIterator @@ -351,10 +367,17 @@ def foldr {α : Type u} (f : Char → α → α) (init : α) (s : Slice) : α := end Slice @[inline] -def Internal.toSliceWithProof {s : String} : +def Internal.ofToSliceWithProof {s : String} : { p : s.toSlice.Pos // p ≠ s.toSlice.endPos } → { p : s.Pos // p ≠ s.endPos } := fun ⟨p, h⟩ => ⟨Pos.ofToSlice p, by simpa [← Pos.toSlice_inj]⟩ +/-- +Creates an iterator over the valid positions within {name}`s`, starting at {name}`p`. +-/ +def positionsFrom (s : String) (p : s.Pos) := + ((s.toSlice.positionsFrom p.toSlice).map Internal.ofToSliceWithProof : + Std.Iter { p : s.Pos // p ≠ s.endPos }) + /-- Creates an iterator over all valid positions within {name}`s`. @@ -366,7 +389,7 @@ Examples -/ @[inline] def positions (s : String) := - (s.toSlice.positions.map Internal.toSliceWithProof : Std.Iter { p : s.Pos // p ≠ s.endPos }) + s.positionsFrom s.startPos /-- Creates an iterator over all characters (Unicode code points) in {name}`s`. @@ -379,6 +402,14 @@ Examples: def chars (s : String) := (s.toSlice.chars : Std.Iter Char) +/-- +Creates an iterator over all valid positions within {name}`s` that are strictly smaller than +{name}`p`, starting from the position before {name}`p` and iterating towards the first one. +-/ +def revPositionsFrom (s : String) (p : s.Pos) := + ((s.toSlice.revPositionsFrom p.toSlice).map Internal.ofToSliceWithProof : + Std.Iter { p : s.Pos // p ≠ s.endPos }) + /-- Creates an iterator over all valid positions within {name}`s`, starting from the last valid position and iterating towards the first one. @@ -391,7 +422,7 @@ Examples -/ @[inline] def revPositions (s : String) := - (s.toSlice.revPositions.map Internal.toSliceWithProof : Std.Iter { p : s.Pos // p ≠ s.endPos }) + s.revPositionsFrom s.endPos /-- Creates an iterator over all characters (Unicode code points) in {name}`s`, starting from the end @@ -428,7 +459,7 @@ Examples: def revBytes (s : String) := (s.toSlice.revBytes : Std.Iter UInt8) -instance : ForIn Id String Char where +instance {m : Type u → Type v} [Monad m] : ForIn m String Char where forIn s b f := ForIn.forIn s.toSlice b f end String diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean index 038abdfc8c..b53f0b32bc 100644 --- a/src/Init/Data/String/Lemmas.lean +++ b/src/Init/Data/String/Lemmas.lean @@ -15,6 +15,7 @@ public import Init.Data.String.Lemmas.Order public import Init.Data.String.Lemmas.IsEmpty public import Init.Data.String.Lemmas.Pattern public import Init.Data.String.Lemmas.Slice +public import Init.Data.String.Lemmas.Iterate import Init.Data.Order.Lemmas public import Init.Data.String.Basic import Init.Data.Char.Lemmas diff --git a/src/Init/Data/String/Lemmas/Basic.lean b/src/Init/Data/String/Lemmas/Basic.lean index 1aca17e5eb..66cb298ab4 100644 --- a/src/Init/Data/String/Lemmas/Basic.lean +++ b/src/Init/Data/String/Lemmas/Basic.lean @@ -168,4 +168,9 @@ theorem Pos.Raw.isValidForSlice_zero {s : Slice} : (0 : Pos.Raw).IsValidForSlice le_rawEndPos := by simp [Pos.Raw.le_iff] isValid_offsetBy := by simpa using s.startInclusive.isValid +@[simp] +theorem Pos.get_ofToSlice {s : String} {p : (s.toSlice).Pos} {h} : + (ofToSlice p).get h = p.get (by simpa [← ofToSlice_inj]) := by + simp [get_eq_get_toSlice] + end String diff --git a/src/Init/Data/String/Lemmas/FindPos.lean b/src/Init/Data/String/Lemmas/FindPos.lean index 834f67c1f1..ad94f0320e 100644 --- a/src/Init/Data/String/Lemmas/FindPos.lean +++ b/src/Init/Data/String/Lemmas/FindPos.lean @@ -24,7 +24,6 @@ theorem le_offset_posGE {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} : 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} : @@ -33,10 +32,7 @@ theorem posGE_le_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Po | 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] + exact fun h => by simp [h, q.isValidForSlice] at h₂ @[simp] theorem lt_posGE_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : @@ -103,10 +99,124 @@ theorem posGT_eq_next {s : Slice} {p : String.Pos.Raw} {h} (h' : p.IsValidForSli 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} : +theorem Pos.next_eq_posGT {s : Slice} {p : s.Pos} {h} : p.next h = s.posGT p.offset (by simpa) := by simp +@[simp] +theorem offset_posLE_le {s : Slice} {p : Pos.Raw} : (s.posLE p).offset ≤ p := by + fun_induction posLE with + | case1 => simp + | case2 => exact Std.le_trans ‹_› (Std.le_of_lt (Pos.Raw.dec_lt ‹_›)) + +@[simp] +theorem le_posLE_iff {s : Slice} {p : s.Pos} {q : Pos.Raw} : + p ≤ s.posLE q ↔ p.offset ≤ q := by + fun_induction posLE with + | case1 => simp [Pos.le_iff] + | case2 r h₁ h₂ ih => + suffices p.offset ≠ r by simp [ih, Pos.Raw.le_dec h₂, Std.le_iff_lt_or_eq (b := r), this] + exact fun h => by simp [← h, p.isValidForSlice] at h₁ + +@[simp] +theorem posLE_lt_iff {s : Slice} {p : s.Pos} {q : Pos.Raw} : + s.posLE q < p ↔ q < p.offset := by + rw [← Std.not_le, le_posLE_iff, Std.not_le] + +theorem posLE_eq_iff {s : Slice} {p : Pos.Raw} {q : s.Pos} : + s.posLE p = q ↔ q.offset ≤ p ∧ ∀ q', q'.offset ≤ p → q' ≤ q := + ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ => Std.le_antisymm (h₂ _ (by simp)) (by simpa)⟩ + +theorem posLT_eq_posLE {s : Slice} {p : Pos.Raw} {h : 0 < p} : + s.posLT p h = s.posLE p.dec := (rfl) + +theorem posLE_dec {s : Slice} {p : Pos.Raw} (h : 0 < p) : + s.posLE p.dec = s.posLT p h := (rfl) + +@[simp] +theorem offset_posLT_lt {s : Slice} {p : Pos.Raw} {h : 0 < p} : + (s.posLT p h).offset < p := + Std.lt_of_le_of_lt (by simp [posLT_eq_posLE]) (Pos.Raw.dec_lt (Pos.Raw.pos_iff_ne_zero.1 h)) + +@[simp] +theorem le_posLT_iff {s : Slice} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : + q ≤ s.posLT p h ↔ q.offset < p := by + rw [posLT_eq_posLE, le_posLE_iff, Pos.Raw.le_dec (Pos.Raw.pos_iff_ne_zero.1 h)] + +@[simp] +theorem posLT_lt_iff {s : Slice} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : + s.posLT p h < q ↔ p ≤ q.offset := by + rw [posLT_eq_posLE, posLE_lt_iff, Pos.Raw.dec_lt_iff (Pos.Raw.pos_iff_ne_zero.1 h)] + +theorem posLT_eq_iff {s : Slice} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : + s.posLT p h = q ↔ q.offset < p ∧ ∀ q', q'.offset < p → q' ≤ q := by + simp [posLT_eq_posLE, posLE_eq_iff, Pos.Raw.le_dec (Pos.Raw.pos_iff_ne_zero.1 h)] + +@[simp] +theorem Pos.posLE_offset {s : Slice} {p : s.Pos} : s.posLE p.offset = p := by + simp [posLE_eq_iff, Pos.le_iff] + +@[simp] +theorem offset_posLE_eq_self_iff {s : Slice} {p : String.Pos.Raw} : + (s.posLE p).offset = p ↔ p.IsValidForSlice s := + ⟨fun h' => by simpa [h'] using (s.posLE p).isValidForSlice, + fun h' => by simpa using congrArg Pos.offset (Pos.posLE_offset (p := s.pos p h'))⟩ + +theorem posLE_eq_pos {s : Slice} {p : String.Pos.Raw} (h : p.IsValidForSlice s) : + s.posLE p = s.pos p h := by + simpa using Pos.posLE_offset (p := s.pos p h) + +theorem pos_eq_posLE {s : Slice} {p : String.Pos.Raw} {h} : + s.pos p h = s.posLE p := by + simp [posLE_eq_pos h] + +@[simp] +theorem Pos.posLT_offset {s : Slice} {p : s.Pos} {h} : + s.posLT p.offset h = p.prev (by simpa [Pos.Raw.pos_iff_ne_zero, Pos.ext_iff] using h) := by + simp [prev] + +theorem posLT_eq_prev {s : Slice} {p : String.Pos.Raw} {h} (h' : p.IsValidForSlice s) : + s.posLT p h = (s.pos p h').prev (by simpa [Pos.Raw.pos_iff_ne_zero, Pos.ext_iff] using h) := by + simpa using Pos.posLT_offset (h := h) (p := s.pos p h') + +theorem Pos.prev_eq_posLT {s : Slice} {p : s.Pos} {h} : + p.prev h = s.posLT p.offset (by simpa [Pos.Raw.pos_iff_ne_zero, Pos.ext_iff] using h) := by + simp + +@[simp] +theorem Pos.le_prev_iff_lt {s : Slice} {p q : s.Pos} {h} : p ≤ q.prev h ↔ p < q := by + simp [prev_eq_posLT, -posLT_offset, Pos.lt_iff] + +@[simp] +theorem Pos.prev_lt_iff_le {s : Slice} {p q : s.Pos} {h} : p.prev h < q ↔ p ≤ q := by + simp [prev_eq_posLT, -posLT_offset, Pos.le_iff] + +theorem Pos.prev_eq_iff {s : Slice} {p q : s.Pos} {h} : + p.prev h = q ↔ q < p ∧ ∀ q', q' < p → q' ≤ q := by + simp only [prev_eq_posLT, posLT_eq_iff, Pos.lt_iff] + +@[simp] +theorem Pos.prev_lt {s : Slice} {p : s.Pos} {h} : p.prev h < p := 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 + +theorem Pos.prevn_le {s : Slice} {p : s.Pos} {n : Nat} : p.prevn n ≤ p := by + fun_induction prevn with + | case1 => simp + | case2 p n h ih => exact Std.le_of_lt (by simpa using ih) + | case3 => simp + +@[simp] +theorem Pos.prev_next {s : Slice} {p : s.Pos} {h} : (p.next h).prev (by simp) = p := + prev_eq_iff.2 (by simp) + +@[simp] +theorem Pos.next_prev {s : Slice} {p : s.Pos} {h} : (p.prev h).next (by simp) = p := + next_eq_iff.2 (by simp) + end Slice @[simp] @@ -204,4 +314,134 @@ theorem next_eq_posGT {s : String} {p : s.Pos} {h} : p.next h = s.posGT p.offset (by simpa) := by simp +@[simp] +theorem offset_posLE_le {s : String} {p : Pos.Raw} : (s.posLE p).offset ≤ p := by + simp [posLE] + +@[simp] +theorem le_posLE_iff {s : String} {p : s.Pos} {q : Pos.Raw} : + p ≤ s.posLE q ↔ p.offset ≤ q := by + simp [posLE, Pos.le_ofToSlice_iff] + +@[simp] +theorem posLE_lt_iff {s : String} {p : s.Pos} {q : Pos.Raw} : + s.posLE q < p ↔ q < p.offset := by + rw [← Std.not_le, le_posLE_iff, Std.not_le] + +theorem posLE_eq_iff {s : String} {p : Pos.Raw} {q : s.Pos} : + s.posLE p = q ↔ q.offset ≤ p ∧ ∀ q', q'.offset ≤ p → q' ≤ q := + ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ => Std.le_antisymm (h₂ _ (by simp)) (by simpa)⟩ + +theorem posLT_eq_posLE {s : String} {p : Pos.Raw} {h : 0 < p} : + s.posLT p h = s.posLE p.dec := (rfl) + +theorem posLE_dec {s : String} {p : Pos.Raw} (h : 0 < p) : + s.posLE p.dec = s.posLT p h := (rfl) + +@[simp] +theorem offset_posLT_lt {s : String} {p : Pos.Raw} {h : 0 < p} : + (s.posLT p h).offset < p := + Std.lt_of_le_of_lt (by simp [posLT_eq_posLE]) (Pos.Raw.dec_lt (Pos.Raw.pos_iff_ne_zero.1 h)) + +@[simp] +theorem le_posLT_iff {s : String} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : + q ≤ s.posLT p h ↔ q.offset < p := by + rw [posLT_eq_posLE, le_posLE_iff, Pos.Raw.le_dec (Pos.Raw.pos_iff_ne_zero.1 h)] + +@[simp] +theorem posLT_lt_iff {s : String} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : + s.posLT p h < q ↔ p ≤ q.offset := by + rw [posLT_eq_posLE, posLE_lt_iff, Pos.Raw.dec_lt_iff (Pos.Raw.pos_iff_ne_zero.1 h)] + +theorem posLT_eq_iff {s : String} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : + s.posLT p h = q ↔ q.offset < p ∧ ∀ q', q'.offset < p → q' ≤ q := by + simp [posLT_eq_posLE, posLE_eq_iff, Pos.Raw.le_dec (Pos.Raw.pos_iff_ne_zero.1 h)] + +theorem posLE_toSlice {s : String} {p : Pos.Raw} : + s.toSlice.posLE p = (s.posLE p).toSlice := by + simp [posLE] + +theorem posLE_eq_posLE_toSlice {s : String} {p : Pos.Raw} : + s.posLE p = Pos.ofToSlice (s.toSlice.posLE p) := by + simp [posLE] + +theorem posLT_toSlice {s : String} {p : Pos.Raw} (h : 0 < p) : + s.toSlice.posLT p h = (s.posLT p h).toSlice := by + simp [posLT] + +theorem posLT_eq_posLT_toSlice {s : String} {p : Pos.Raw} (h : 0 < p) : + s.posLT p h = Pos.ofToSlice (s.toSlice.posLT p h) := by + simp [posLT] + +@[simp] +theorem Pos.posLE_offset {s : String} {p : s.Pos} : s.posLE p.offset = p := by + simp [posLE_eq_iff, Pos.le_iff] + +@[simp] +theorem offset_posLE_eq_self_iff {s : String} {p : String.Pos.Raw} : + (s.posLE p).offset = p ↔ p.IsValid s := + ⟨fun h' => by simpa [h'] using (s.posLE p).isValid, + fun h' => by simpa using congrArg Pos.offset (Pos.posLE_offset (p := s.pos p h'))⟩ + +theorem posLE_eq_pos {s : String} {p : String.Pos.Raw} (h : p.IsValid s) : + s.posLE p = s.pos p h := by + simpa using Pos.posLE_offset (p := s.pos p h) + +theorem pos_eq_posLE {s : String} {p : String.Pos.Raw} {h} : + s.pos p h = s.posLE p := by + simp [posLE_eq_pos h] + +@[simp] +theorem Pos.posLT_offset {s : String} {p : s.Pos} {h} : + s.posLT p.offset h = p.prev (by simpa [Pos.Raw.pos_iff_ne_zero, Pos.ext_iff] using h) := by + simp [posLT, prev, Slice.Pos.prev, offset_toSlice] + +theorem posLT_eq_prev {s : String} {p : String.Pos.Raw} {h} (h' : p.IsValid s) : + s.posLT p h = (s.pos p h').prev (by simpa [Pos.Raw.pos_iff_ne_zero, Pos.ext_iff] using h) := by + simpa using Pos.posLT_offset (h := h) (p := s.pos p h') + +theorem Pos.prev_eq_posLT {s : String} {p : s.Pos} {h} : + p.prev h = s.posLT p.offset (by simpa [Pos.Raw.pos_iff_ne_zero, Pos.ext_iff] using h) := by + simp + +@[simp] +theorem Pos.le_prev_iff_lt {s : String} {p q : s.Pos} {h} : p ≤ q.prev h ↔ p < q := by + simp [prev_eq_posLT, -posLT_offset, Pos.lt_iff] + +@[simp] +theorem Pos.prev_lt_iff_le {s : String} {p q : s.Pos} {h} : p.prev h < q ↔ p ≤ q := by + simp [prev_eq_posLT, -posLT_offset, Pos.le_iff] + +theorem Pos.prev_eq_iff {s : String} {p q : s.Pos} {h} : + p.prev h = q ↔ q < p ∧ ∀ q', q' < p → q' ≤ q := by + simp only [prev_eq_posLT, posLT_eq_iff, Pos.lt_iff] + +@[simp] +theorem Pos.prev_lt {s : String} {p : s.Pos} {h} : p.prev h < p := 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 + +theorem Pos.toSlice_prev {s : String} {p : s.Pos} {h} : + (p.prev h).toSlice = p.toSlice.prev (by simpa [toSlice_inj]) := by + simp [prev] + +theorem Pos.prev_toSlice {s : String} {p : s.Pos} {h} : + p.toSlice.prev h = (p.prev (by simpa [← toSlice_inj])).toSlice := by + simp [prev] + +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 + +@[simp] +theorem Pos.prev_next {s : String} {p : s.Pos} {h} : (p.next h).prev (by simp) = p := + prev_eq_iff.2 (by simp) + +@[simp] +theorem Pos.next_prev {s : String} {p : s.Pos} {h} : (p.prev h).next (by simp) = p := + next_eq_iff.2 (by simp) + end String diff --git a/src/Init/Data/String/Lemmas/Iterate.lean b/src/Init/Data/String/Lemmas/Iterate.lean new file mode 100644 index 0000000000..9bb6ed82fa --- /dev/null +++ b/src/Init/Data/String/Lemmas/Iterate.lean @@ -0,0 +1,263 @@ +/- +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.Iterate +public import Init.Data.Iterators.Consumers.Collect +public import Init.Data.String.Lemmas.Splits +import all Init.Data.String.Iterate +import Init.Data.String.Termination +import Init.Data.Iterators.Lemmas.Consumers.Collect +import Init.ByCases +import Init.Data.Iterators.Lemmas.Combinators.FilterMap +import Init.Data.String.Lemmas.Basic +import Init.Data.Iterators.Lemmas.Consumers.Loop + +set_option doc.verso true + +public section + +namespace String + +namespace Slice + +/-- +A list of all positions starting at {name}`p`. + +This function is not meant to be used in actual progams. Actual programs should use +{name}`Slice.positionsFrom` or {name}`Slice.positions`. +-/ +protected def Model.positionsFrom {s : Slice} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } := + if h : p.IsAtEnd then + [] + else + ⟨p, h⟩ :: Model.positionsFrom (p.next h) +termination_by p + +@[simp] +theorem Model.positionsFrom_endPos {s : Slice} : Model.positionsFrom s.endPos = [] := by + simp [Model.positionsFrom] + +theorem Model.positionsFrom_eq_cons {s : Slice} {p : s.Pos} (hp : p ≠ s.endPos) : + Model.positionsFrom p = ⟨p, hp⟩ :: Model.positionsFrom (p.next hp) := by + rw [Model.positionsFrom] + simp [hp] + +theorem Model.map_get_positionsFrom_of_splits {s : Slice} {p : s.Pos} {t₁ t₂ : String} + (hp : p.Splits t₁ t₂) : (Model.positionsFrom p).map (fun p => p.1.get p.2) = t₂.toList := by + induction p using Pos.next_induction generalizing t₁ t₂ with + | next p h ih => + obtain ⟨t₂, rfl⟩ := hp.exists_eq_singleton_append h + rw [Model.positionsFrom_eq_cons h, List.map_cons, String.toList_append, toList_singleton, + List.singleton_append, ih hp.next] + | endPos => simpa using (splits_endPos_iff.1 hp).2 + +theorem Model.map_get_positionsFrom_startPos {s : Slice} : + (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.copy.toList := + Model.map_get_positionsFrom_of_splits (splits_startPos s) + +@[simp] +theorem toList_positionsFrom {s : Slice} {p : s.Pos} : + (s.positionsFrom p).toList = Model.positionsFrom p := by + rw [positionsFrom] + induction p using WellFounded.induction Pos.wellFounded_gt with | h p ih + rw [Std.Iter.toList_eq_match_step, Std.Iter.step_eq] + simp only [ne_eq, Std.Iter.toIterM_mk, Std.IterM.internalState_mk] + by_cases h : p = s.endPos + · simp [h] + · simp [h, ih (p.next h) (by simp), Model.positionsFrom_eq_cons] + +@[simp] +theorem toList_positions {s : Slice} : s.positions.toList = Model.positionsFrom s.startPos := by + simp [positions] + +@[simp] +theorem toList_chars {s : Slice} : s.chars.toList = s.copy.toList := by + simp [chars, Model.map_get_positionsFrom_startPos] + +/-- +A list of all positions strictly before {name}`p`, ordered from largest to smallest. + +This function is not meant to be used in actual programs. Actual programs should use +{name}`Slice.revPositionsFrom` and {name}`Slice.revPositions`. +-/ +protected def Model.revPositionsFrom {s : Slice} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } := + if h : p = s.startPos then + [] + else + ⟨p.prev h, by simp⟩ :: Model.revPositionsFrom (p.prev h) +termination_by p.down + +@[simp] +theorem Model.revPositionsFrom_startPos {s : Slice} : Model.revPositionsFrom s.startPos = [] := by + simp [Model.revPositionsFrom] + +theorem Model.revPositionsFrom_eq_cons {s : Slice} {p : s.Pos} (hp : p ≠ s.startPos) : + Model.revPositionsFrom p = ⟨p.prev hp, by simp⟩ :: Model.revPositionsFrom (p.prev hp) := by + rw [Model.revPositionsFrom] + simp [hp] + +theorem Model.map_get_revPositionsFrom_of_splits {s : Slice} {p : s.Pos} {t₁ t₂ : String} + (hp : p.Splits t₁ t₂) : (Model.revPositionsFrom p).map (fun p => p.1.get p.2) = t₁.toList.reverse := by + induction p using Pos.prev_induction generalizing t₁ t₂ with + | startPos => simpa using (splits_startPos_iff.1 hp).1 + | prev p h ih => + obtain ⟨t₁, rfl⟩ := hp.exists_eq_append_singleton_of_ne_startPos h + rw [Model.revPositionsFrom_eq_cons h, List.map_cons, String.toList_append, toList_singleton, + List.reverse_append, List.reverse_singleton, List.singleton_append, ih hp.prev] + +theorem Model.map_get_revPositionsFrom_endPos {s : Slice} : + (Model.revPositionsFrom s.endPos).map (fun p => p.1.get p.2) = s.copy.toList.reverse := + Model.map_get_revPositionsFrom_of_splits (splits_endPos s) + +@[simp] +theorem toList_revPositionsFrom {s : Slice} {p : s.Pos} : + (s.revPositionsFrom p).toList = Model.revPositionsFrom p := by + rw [revPositionsFrom] + induction p using WellFounded.induction Pos.wellFounded_lt with | h p ih + rw [Std.Iter.toList_eq_match_step, Std.Iter.step_eq] + simp only [ne_eq, Std.Iter.toIterM_mk, Std.IterM.internalState_mk] + by_cases h : p = s.startPos + · simp [h] + · simp [h, ih (p.prev h) (by simp), Model.revPositionsFrom_eq_cons] + +@[simp] +theorem toList_revPositions {s : Slice} : s.revPositions.toList = Model.revPositionsFrom s.endPos := by + simp [revPositions] + +@[simp] +theorem toList_revChars {s : Slice} : s.revChars.toList = s.copy.toList.reverse := by + simp [revChars, Model.map_get_revPositionsFrom_endPos] + +theorem forIn_eq_forIn_chars {m : Type u → Type v} [Monad m] {s : Slice} {b} {f : Char → β → m (ForInStep β)} : + ForIn.forIn s b f = ForIn.forIn s.chars b f := rfl + +@[simp] +theorem forIn_eq_forIn_toList {m : Type u → Type v} [Monad m] [LawfulMonad m] {s : Slice} {b} + {f : Char → β → m (ForInStep β)} : + ForIn.forIn s b f = ForIn.forIn s.copy.toList b f := by + rw [forIn_eq_forIn_chars, ← Std.Iter.forIn_toList, toList_chars] + +end Slice + +/-- +A list of all positions starting at {name}`p`. + +This function is not meant to be used in actual progams. Actual programs should use +{name}`Slice.positionsFrom` or {name}`Slice.positions`. +-/ +protected def Model.positionsFrom {s : String} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } := + if h : p.IsAtEnd then + [] + else + ⟨p, h⟩ :: Model.positionsFrom (p.next h) +termination_by p + +@[simp] +theorem Model.positionsFrom_endPos {s : String} : Model.positionsFrom s.endPos = [] := by + simp [Model.positionsFrom] + +theorem Model.positionsFrom_eq_cons {s : String} {p : s.Pos} (hp : p ≠ s.endPos) : + Model.positionsFrom p = ⟨p, hp⟩ :: Model.positionsFrom (p.next hp) := by + rw [Model.positionsFrom] + simp [hp] + +theorem Model.positionsFrom_eq_map {s : String} {p : s.Pos} : + Model.positionsFrom p = (Slice.Model.positionsFrom p.toSlice).map + (fun p => ⟨Pos.ofToSlice p.1, by simpa [← Pos.toSlice_inj] using p.2⟩) := by + induction p using Pos.next_induction with + | next p h ih => + rw [positionsFrom_eq_cons h, Slice.Model.positionsFrom_eq_cons (by simpa [Pos.toSlice_inj])] + simp [ih, Pos.toSlice_next] + | endPos => simp [← endPos_toSlice] + +theorem Model.map_get_positionsFrom_of_splits {s : String} {p : s.Pos} {t₁ t₂ : String} + (hp : p.Splits t₁ t₂) : (Model.positionsFrom p).map (fun p => p.1.get p.2) = t₂.toList := by + simp [Model.positionsFrom_eq_map, + ← Slice.Model.map_get_positionsFrom_of_splits (Pos.splits_toSlice_iff.2 hp)] + +theorem Model.map_get_positionsFrom_startPos {s : String} : + (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.toList := + Model.map_get_positionsFrom_of_splits (splits_startPos s) + +@[simp] +theorem toList_positionsFrom {s : String} {p : s.Pos} : + (s.positionsFrom p).toList = Model.positionsFrom p := by + simp [positionsFrom, Internal.ofToSliceWithProof, Model.positionsFrom_eq_map] + +theorem toList_positions {s : String} : s.positions.toList = Model.positionsFrom s.startPos := by + simp [positions] + +@[simp] +theorem toList_chars {s : String} : s.chars.toList = s.toList := by + simp [chars] + +/-- +A list of all positions strictly before {name}`p`, ordered from largest to smallest. + +This function is not meant to be used in actual programs. Actual programs should use +{name}`Slice.revPositionsFrom` and {name}`Slice.revPositions`. +-/ +protected def Model.revPositionsFrom {s : String} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } := + if h : p = s.startPos then + [] + else + ⟨p.prev h, by simp⟩ :: Model.revPositionsFrom (p.prev h) +termination_by p.down + +@[simp] +theorem Model.revPositionsFrom_startPos {s : String} : Model.revPositionsFrom s.startPos = [] := by + simp [Model.revPositionsFrom] + +theorem Model.revPositionsFrom_eq_cons {s : String} {p : s.Pos} (hp : p ≠ s.startPos) : + Model.revPositionsFrom p = ⟨p.prev hp, by simp⟩ :: Model.revPositionsFrom (p.prev hp) := by + rw [Model.revPositionsFrom] + simp [hp] + +theorem Model.revPositionsFrom_eq_map {s : String} {p : s.Pos} : + Model.revPositionsFrom p = (Slice.Model.revPositionsFrom p.toSlice).map + (fun p => ⟨Pos.ofToSlice p.1, by simpa [← Pos.toSlice_inj] using p.2⟩) := by + induction p using Pos.prev_induction with + | prev p h ih => + rw [revPositionsFrom_eq_cons h, Slice.Model.revPositionsFrom_eq_cons (by simpa [Pos.toSlice_inj])] + simp only [ne_eq, ih, List.map_cons, List.cons.injEq, Subtype.mk.injEq] + simp [Pos.prev_toSlice] + | startPos => simp [← startPos_toSlice] + +theorem Model.map_get_revPositionsFrom_of_splits {s : String} {p : s.Pos} {t₁ t₂ : String} + (hp : p.Splits t₁ t₂) : (Model.revPositionsFrom p).map (fun p => p.1.get p.2) = t₁.toList.reverse := by + simp [Model.revPositionsFrom_eq_map, + ← Slice.Model.map_get_revPositionsFrom_of_splits (Pos.splits_toSlice_iff.2 hp)] + +theorem Model.map_get_revPositionsFrom_endPos {s : String} : + (Model.revPositionsFrom s.endPos).map (fun p => p.1.get p.2) = s.toList.reverse := + Model.map_get_revPositionsFrom_of_splits (splits_endPos s) + +@[simp] +theorem toList_revPositionsFrom {s : String} {p : s.Pos} : + (s.revPositionsFrom p).toList = Model.revPositionsFrom p := by + simp [revPositionsFrom, Internal.ofToSliceWithProof, Model.revPositionsFrom_eq_map] + +@[simp] +theorem toList_revPositions {s : String} : + s.revPositions.toList = Model.revPositionsFrom s.endPos := by + simp [revPositions] + +@[simp] +theorem toList_revChars {s : String} : s.revChars.toList = s.toList.reverse := by + simp [revChars] + +theorem forIn_eq_forIn_chars {m : Type u → Type v} [Monad m] {s : String} {b} {f : Char → β → m (ForInStep β)} : + ForIn.forIn s b f = ForIn.forIn s.chars b f := (rfl) + +@[simp] +theorem forIn_eq_forIn_toList {m : Type u → Type v} [Monad m] [LawfulMonad m] {s : String} {b} + {f : Char → β → m (ForInStep β)} : + ForIn.forIn s b f = ForIn.forIn s.toList b f := by + rw [forIn_eq_forIn_chars, ← Std.Iter.forIn_toList, toList_chars] + +end String diff --git a/src/Init/Data/String/Lemmas/Order.lean b/src/Init/Data/String/Lemmas/Order.lean index 2fc24f158d..41e8c75eed 100644 --- a/src/Init/Data/String/Lemmas/Order.lean +++ b/src/Init/Data/String/Lemmas/Order.lean @@ -23,11 +23,23 @@ theorem Slice.Pos.next_le_iff_lt {s : Slice} {p q : s.Pos} {h} : p.next h ≤ q 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] +theorem Slice.Pos.next_eq_iff {s : Slice} {p q : s.Pos} {h} : + p.next h = q ↔ p < q ∧ ∀ (q' : s.Pos), p < q' → q ≤ q' := + ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ => Std.le_antisymm (by simpa) (h₂ _ (by simp))⟩ + @[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 Pos.lt_next_iff_le {s : String} {p q : s.Pos} {h} : p < q.next h ↔ p ≤ q := by + rw [← Std.not_le, next_le_iff_lt, Std.not_lt] + +theorem Pos.next_eq_iff {s : String} {p q : s.Pos} {h} : + p.next h = q ↔ p < q ∧ ∀ (q' : s.Pos), p < q' → q ≤ q' := + ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ => Std.le_antisymm (by simpa) (h₂ _ (by simp))⟩ + @[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⟩ @@ -48,6 +60,10 @@ theorem Slice.Pos.lt_endPos_iff {s : Slice} (p : s.Pos) : p < s.endPos ↔ p ≠ 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.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]⟩ @@ -60,6 +76,22 @@ theorem Slice.Pos.ne_startPos_of_lt {s : Slice} {p q : s.Pos} : p < q → q ≠ rintro h rfl simp at h +@[simp] +theorem Pos.not_lt_startPos {s : String} {p : s.Pos} : ¬ p < s.startPos := + fun h => Std.lt_irrefl (Std.lt_of_lt_of_le h (Pos.startPos_le _)) + +@[simp] +theorem Slice.Pos.not_endPos_lt {s : Slice} {p : s.Pos} : ¬ s.endPos < p := + fun h => Std.lt_irrefl (Std.lt_of_le_of_lt (Slice.Pos.le_endPos _) h) + +@[simp] +theorem Pos.not_endPos_lt {s : String} {p : s.Pos} : ¬ s.endPos < p := + fun h => Std.lt_irrefl (Std.lt_of_le_of_lt (Pos.le_endPos _) h) + +theorem Pos.ne_endPos_of_lt {s : String} {p q : s.Pos} : p < q → p ≠ s.endPos := by + rintro h rfl + simp at h + @[simp] theorem Slice.Pos.le_next {s : Slice} {p : s.Pos} {h} : p ≤ p.next h := Std.le_of_lt (by simp) diff --git a/src/Init/Data/String/Lemmas/Splits.lean b/src/Init/Data/String/Lemmas/Splits.lean index d638819d52..4dcc5cd0a8 100644 --- a/src/Init/Data/String/Lemmas/Splits.lean +++ b/src/Init/Data/String/Lemmas/Splits.lean @@ -7,6 +7,7 @@ module prelude public import Init.Data.String.Basic +public import Init.Data.String.FindPos import Init.Data.ByteArray.Lemmas import Init.Data.String.Lemmas.Basic import Init.Data.Nat.MinMax @@ -15,6 +16,7 @@ import Init.Data.String.Lemmas.Order import Init.Data.String.OrderInstances import Init.Data.Nat.Order import Init.Omega +import Init.Data.String.Lemmas.FindPos /-! # `Splits` predicates on `String.Pos` and `String.Slice.Pos`. @@ -205,6 +207,18 @@ theorem Pos.splits_next {s : String} (p : s.Pos) (hp : p ≠ s.endPos) : eq_append := p.eq_copy_sliceTo_append_get hp offset_eq_rawEndPos := by simp +theorem Pos.splits_prev_right {s : String} (p : s.Pos) (hp : p ≠ s.startPos) : + p.Splits ((s.sliceTo (p.prev hp)).copy ++ singleton ((p.prev hp).get (by simp))) (s.sliceFrom p).copy := by + obtain ⟨q, hq, rfl⟩ : ∃ (q : s.Pos), ∃ (hq : q ≠ s.endPos), p = q.next hq := + ⟨p.prev hp, by simp, by simp⟩ + simpa using splits_next q hq + +theorem Pos.splits_prev {s : String} (p : s.Pos) (hp : p ≠ s.startPos) : + (p.prev hp).Splits (s.sliceTo (p.prev hp)).copy (singleton ((p.prev hp).get (by simp)) ++ (s.sliceFrom p).copy) := by + obtain ⟨q, hq, rfl⟩ : ∃ (q : s.Pos), ∃ (hq : q ≠ s.endPos), p = q.next hq := + ⟨p.prev hp, by simp, by simp⟩ + simpa using splits_next_right q hq + theorem Slice.Pos.splits_next_right {s : Slice} (p : s.Pos) (hp : p ≠ s.endPos) : p.Splits (s.sliceTo p).copy (singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy) where eq_append := by simpa [← append_assoc] using p.copy_eq_copy_sliceTo_append_get hp @@ -215,6 +229,18 @@ theorem Slice.Pos.splits_next {s : Slice} (p : s.Pos) (hp : p ≠ s.endPos) : eq_append := p.copy_eq_copy_sliceTo_append_get hp offset_eq_rawEndPos := by simp +theorem Slice.Pos.splits_prev_right {s : Slice} (p : s.Pos) (hp : p ≠ s.startPos) : + p.Splits ((s.sliceTo (p.prev hp)).copy ++ singleton ((p.prev hp).get (by simp))) (s.sliceFrom p).copy := by + obtain ⟨q, hq, rfl⟩ : ∃ (q : s.Pos), ∃ (hq : q ≠ s.endPos), p = q.next hq := + ⟨p.prev hp, by simp, by simp⟩ + simpa using splits_next q hq + +theorem Slice.Pos.splits_prev {s : Slice} (p : s.Pos) (hp : p ≠ s.startPos) : + (p.prev hp).Splits (s.sliceTo (p.prev hp)).copy (singleton ((p.prev hp).get (by simp)) ++ (s.sliceFrom p).copy) := by + obtain ⟨q, hq, rfl⟩ : ∃ (q : s.Pos), ∃ (hq : q ≠ s.endPos), p = q.next hq := + ⟨p.prev hp, by simp, by simp⟩ + simpa using splits_next_right q hq + theorem Pos.Splits.exists_eq_singleton_append {s : String} {p : s.Pos} (hp : p ≠ s.endPos) (h : p.Splits t₁ t₂) : ∃ t₂', t₂ = singleton (p.get hp) ++ t₂' := ⟨(s.sliceFrom (p.next hp)).copy, h.eq_right (p.splits_next_right hp)⟩ @@ -223,6 +249,14 @@ theorem Pos.Splits.exists_eq_append_singleton {s : String} {p : s.Pos} (hp : p ≠ s.endPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get hp) := ⟨(s.sliceTo p).copy, h.eq_left (p.splits_next hp)⟩ +theorem Pos.Splits.exists_eq_append_singleton_of_ne_startPos {s : String} {p : s.Pos} + (hp : p ≠ s.startPos) (h : p.Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton ((p.prev hp).get (by simp)) := + ⟨_, h.eq_left (p.splits_prev_right hp)⟩ + +theorem Pos.Splits.exists_eq_singleton_append_of_ne_startPos {s : String} {p : s.Pos} + (hp : p ≠ s.startPos) (h : (p.prev hp).Splits t₁ t₂) : ∃ t₂', t₂ = singleton ((p.prev hp).get (by simp)) ++ t₂' := + ⟨_, h.eq_right (p.splits_prev hp)⟩ + 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.sliceFrom (p.next hp)).copy, h.eq_right (p.splits_next_right hp)⟩ @@ -231,6 +265,14 @@ 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.sliceTo p).copy, h.eq_left (p.splits_next hp)⟩ +theorem Slice.Pos.Splits.exists_eq_append_singleton_of_ne_startPos {s : Slice} {p : s.Pos} + (hp : p ≠ s.startPos) (h : p.Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton ((p.prev hp).get (by simp)) := + ⟨_, h.eq_left (p.splits_prev_right hp)⟩ + +theorem Slice.Pos.Splits.exists_eq_singleton_append_of_ne_startPos {s : Slice} {p : s.Pos} + (hp : p ≠ s.startPos) (h : (p.prev hp).Splits t₁ t₂) : ∃ t₂', t₂ = singleton ((p.prev hp).get (by simp)) ++ t₂' := + ⟨_, h.eq_right (p.splits_prev hp)⟩ + theorem Pos.Splits.ne_endPos_of_singleton {s : String} {p : s.Pos} (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endPos := by simp [h.eq_endPos_iff] @@ -261,6 +303,20 @@ theorem Slice.Pos.Splits.next {s : Slice} {p : s.Pos} obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_next_right p hp) exact splits_next p hp +/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append_of_ne_startPos` to be able to apply this. -/ +theorem Pos.Splits.prev {s : String} {p : s.Pos} + (h : p.Splits (t₁ ++ singleton c) t₂) : (p.prev h.ne_startPos_of_singleton).Splits t₁ (singleton c ++ t₂) := by + generalize h.ne_startPos_of_singleton = hp + obtain ⟨⟨rfl, rfl⟩, rfl⟩ := by simpa using h.eq (splits_prev_right p hp) + exact splits_prev p hp + +/-- You might want to invoke `Slice.Pos.Splits.exists_eq_singleton_append_of_ne_startPos` to be able to apply this. -/ +theorem Slice.Pos.Splits.prev {s : Slice} {p : s.Pos} + (h : p.Splits (t₁ ++ singleton c) t₂) : (p.prev h.ne_startPos_of_singleton).Splits t₁ (singleton c ++ t₂) := by + generalize h.ne_startPos_of_singleton = hp + obtain ⟨⟨rfl, rfl⟩, rfl⟩ := by simpa using h.eq (splits_prev_right p hp) + exact splits_prev p hp + theorem Slice.sliceTo_copy_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₁ : String} : (s.sliceTo p).copy = t₁ ↔ ∃ t₂, p.Splits t₁ t₂ := by refine ⟨?_, ?_⟩ diff --git a/src/Init/Data/String/Pattern/Basic.lean b/src/Init/Data/String/Pattern/Basic.lean index b51d589cfb..ec405e6c81 100644 --- a/src/Init/Data/String/Pattern/Basic.lean +++ b/src/Init/Data/String/Pattern/Basic.lean @@ -8,13 +8,15 @@ module prelude public import Init.Data.Iterators.Consumers.Monadic.Loop public import Init.Data.String.Defs +public import Init.Data.String.Basic +public import Init.Data.String.FindPos +import Init.Data.String.Lemmas.FindPos import Init.Data.Iterators.Consumers.Loop import Init.Omega import Init.Data.String.Lemmas.IsEmpty import Init.Data.String.Termination import Init.Data.String.OrderInstances import Init.Data.String.Lemmas.Order -public import Init.Data.String.Basic set_option doc.verso true diff --git a/src/Init/Data/String/Pattern/Char.lean b/src/Init/Data/String/Pattern/Char.lean index f77ac32914..f5f0a0fd26 100644 --- a/src/Init/Data/String/Pattern/Char.lean +++ b/src/Init/Data/String/Pattern/Char.lean @@ -7,8 +7,8 @@ module prelude public import Init.Data.String.Pattern.Basic +import Init.Data.String.Lemmas.FindPos import Init.Data.String.Termination -public import Init.Data.String.Basic import Init.Data.String.Lemmas.IsEmpty import Init.Data.String.Lemmas.Order import Init.Data.Option.Lemmas diff --git a/src/Init/Data/String/Pattern/Pred.lean b/src/Init/Data/String/Pattern/Pred.lean index 8b78b81b92..c1ef5c54ba 100644 --- a/src/Init/Data/String/Pattern/Pred.lean +++ b/src/Init/Data/String/Pattern/Pred.lean @@ -7,12 +7,13 @@ module prelude public import Init.Data.String.Pattern.Basic -import Init.Data.String.Termination -public import Init.Data.String.Basic -import Init.Omega public import Init.Data.String.Lemmas.IsEmpty +import Init.Data.String.Termination +import Init.Omega +public import Init.Data.String.Basic import Init.Data.String.Lemmas.Order import Init.Data.Option.Lemmas +import Init.Data.String.Lemmas.FindPos set_option doc.verso true diff --git a/src/Init/Data/String/PosRaw.lean b/src/Init/Data/String/PosRaw.lean index 70552ff674..2517bc2071 100644 --- a/src/Init/Data/String/PosRaw.lean +++ b/src/Init/Data/String/PosRaw.lean @@ -8,6 +8,7 @@ module prelude public import Init.Data.ByteArray.Basic import Init.Data.Nat.Simproc +import Init.Omega /-! # Arithmetic of `String.Pos.Raw` @@ -269,6 +270,19 @@ theorem Pos.Raw.inc_le {p q : Pos.Raw} : p.inc ≤ q ↔ p < q := by simpa [lt_i @[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.dec_lt {p : Pos.Raw} : p ≠ 0 → p.dec < p := by simpa [lt_iff] using Nat.sub_one_lt + +theorem Pos.Raw.le_dec {p q : Pos.Raw} : q ≠ 0 → (p ≤ q.dec ↔ p < q) := by + simp only [ne_eq, eq_zero_iff, le_iff, byteIdx_dec, lt_iff] + omega + +theorem Pos.Raw.dec_lt_iff {p q : Pos.Raw} : p ≠ 0 → (p.dec < q ↔ p ≤ q) := by + simp only [ne_eq, eq_zero_iff, lt_iff, byteIdx_dec, le_iff] + omega + +theorem Pos.Raw.pos_iff_ne_zero {p : Pos.Raw} : 0 < p ↔ p ≠ 0 := by + simpa [lt_iff] using Nat.pos_iff_ne_zero + 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/Termination.lean b/src/Init/Data/String/Termination.lean index 9713f4bbed..47e3a503af 100644 --- a/src/Init/Data/String/Termination.lean +++ b/src/Init/Data/String/Termination.lean @@ -7,8 +7,11 @@ module prelude public import Init.Data.String.Lemmas.Splits +public import Init.Data.String.FindPos import Init.Data.Option.Lemmas import Init.Omega +import Init.ByCases +import Init.Data.String.Lemmas.FindPos /-! # Helpers for termination arguments about functions operating on strings @@ -105,6 +108,21 @@ theorem lt_next_next {s : Slice} {p : s.Pos} {h h'} : p < (p.next h).next h' := theorem prev_prev_lt {s : Slice} {p : s.Pos} {h h'} : (p.prev h).prev h' < p := lt_trans (p.prev h).prev_lt p.prev_lt +theorem next_induction {s : Slice} {C : s.Pos → Prop} (p : s.Pos) + (next : ∀ (x : s.Pos), (h : x ≠ s.endPos) → C (x.next h) → C x) (endPos : C s.endPos) : C p := by + induction p using WellFounded.induction wellFounded_gt with | h p ih + by_cases h : p = s.endPos + · simpa [h] + · exact next _ h (ih _ (by simp)) + +theorem prev_induction {s : Slice} {C : s.Pos → Prop} (p : s.Pos) + (prev : ∀ (x : s.Pos), (h : x ≠ s.startPos) → C (x.prev h) → C x) (startPos : C s.startPos) : + C p := by + induction p using WellFounded.induction wellFounded_lt with | h p ih + by_cases h : p = s.startPos + · simpa [h] + · exact prev _ h (ih _ (by simp)) + end Slice.Pos namespace Pos @@ -205,6 +223,21 @@ theorem Splits.remainingBytes_eq {s : String} {p : s.Pos} {t₁ t₂} (h : p.Splits t₁ t₂) : p.remainingBytes = t₂.utf8ByteSize := by simp [Pos.remainingBytes_eq, h.eq_append, h.offset_eq_rawEndPos] +theorem next_induction {s : String} {C : s.Pos → Prop} (p : s.Pos) + (next : ∀ (x : s.Pos), (h : x ≠ s.endPos) → C (x.next h) → C x) (endPos : C s.endPos) : C p := by + induction p using WellFounded.induction wellFounded_gt with | h p ih + by_cases h : p = s.endPos + · simpa [h] + · exact next _ h (ih _ (by simp)) + +theorem prev_induction {s : String} {C : s.Pos → Prop} (p : s.Pos) + (prev : ∀ (x : s.Pos), (h : x ≠ s.startPos) → C (x.prev h) → C x) (startPos : C s.startPos) : + C p := by + induction p using WellFounded.induction wellFounded_lt with | h p ih + by_cases h : p = s.startPos + · simpa [h] + · exact prev _ h (ih _ (by simp)) + end Pos namespace Slice.Pos diff --git a/src/Lean/Compiler/NameMangling.lean b/src/Lean/Compiler/NameMangling.lean index 2941aa2411..f4472e1c9c 100644 --- a/src/Lean/Compiler/NameMangling.lean +++ b/src/Lean/Compiler/NameMangling.lean @@ -10,6 +10,7 @@ public import Lean.Setup import Init.Data.String.TakeDrop import Init.Data.UInt.Lemmas import Init.Omega +import Init.Data.String.Lemmas.FindPos namespace String diff --git a/tests/lean/run/string.lean b/tests/lean/run/string.lean index dce330f9fc..636cb2062f 100644 --- a/tests/lean/run/string.lean +++ b/tests/lean/run/string.lean @@ -8,7 +8,7 @@ def lean : String := "L∃∀N" macro tk:"#test " t:term : command => `(#guard%$tk $t - example : $t := by decide) + example : $t := by decide_cbv) /-! Examples from documentation (added in https://github.com/leanprover/lean4/pull/4166) @@ -176,9 +176,9 @@ Behavior of `String.next` (`lean_string_utf8_next`) in special cases (see issue #test "abc".pos? ⟨4⟩ = none #test "L∃∀N".pos? ⟨2⟩ = none -#test ("abc".pos ⟨1⟩ (by decide)).get (by decide) = 'b' +-- #test ("abc".pos ⟨1⟩ (by decide)).get (by decide) = 'b' #test ("abc".pos ⟨3⟩ (by decide)).get? = none -#test ("L∃∀N".pos ⟨1⟩ (by decide)).get (by decide) = '∃' +-- #test ("L∃∀N".pos ⟨1⟩ (by decide)).get (by decide) = '∃' #test (("L∃∀N".pos ⟨0⟩ (by decide)).next (by decide)).offset = ⟨1⟩ #test (("L∃∀N".pos ⟨1⟩ (by decide)).next (by decide)).offset = ⟨4⟩ diff --git a/tests/lean/run/string_slice.lean b/tests/lean/run/string_slice.lean index 9054e5d5d4..a9b32ee473 100644 --- a/tests/lean/run/string_slice.lean +++ b/tests/lean/run/string_slice.lean @@ -252,3 +252,14 @@ end for c in "hello" do s' := s'.push c return s') = "hello" + +example {s : String} : (Id.run do + let mut s' := "" + for c in s do + s' := s'.push c + return s') = s := by + obtain ⟨cs, rfl⟩ := s.exists_eq_ofList + simp only [bind_pure_comp, map_pure, String.forIn_eq_forIn_toList, String.toList_ofList, + List.forIn_pure_yield_eq_foldl, bind_pure, Id.run_pure, ← String.toList_inj] + suffices ∀ (t : String), (cs.foldl (fun b a => b.push a) t).toList = t.toList ++ cs by simpa using this "" + induction cs <;> simp_all