feat: verification of String.positions, String.chars, String.revPositions, String.revChars, ForIn m String Char (#12456)
This PR verifies all of the `String` iterators except for the bytes iterator by relating them to `String.toList`. Along the way we define `String.posLE` and `String.posLT` analogously to `String.posGE` and `String.posGT` and redefine `String.prev` to go through `String.posLT`. We also define and verify `String.positionsFrom` and `String.revPositionsFrom`, which are the obvious generaliziations of `String.positions` and `String.revPositions` starting at a positions other than the start/end. Finally, we get various lemmas about strings and positions, including some nice induction principles `String.Pos.next_induction` and `String.Pos.prev_induction`. Of course, we also have all of the analogous results for `String.Slice`.
This commit is contained in:
Markus Himmel
GitHub
parent
db12e64845
commit
6cbaada1bf
18 changed files with 822 additions and 127 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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`.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
263
src/Init/Data/String/Lemmas/Iterate.lean
Normal file
263
src/Init/Data/String/Lemmas/Iterate.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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 ⟨?_, ?_⟩
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue