Theorem: Substring.ValidFor.expand (RegexCorrectness/Data/String.lean)

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
⊢ ValidFor l (m ++ [c]) r s.expand
Tactic:
have : s.stopPos < s.str.endPos := by
  simp [v.stopPos, v.str]
  have : 0 < String.csize c := String.csize_pos c
  omega
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r s.expand

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r s.expand
Tactic:
unfold expand
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r
    (if s.stopPos < s.str.endPos then { str := s.str, startPos := s.startPos, stopPos := s.str.next s.stopPos } else s)

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r
    (if s.stopPos < s.str.endPos then { str := s.str, startPos := s.startPos, stopPos := s.str.next s.stopPos } else s)
Tactic:
simp [this]
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r { str := s.str, startPos := s.startPos, stopPos := s.str.next s.stopPos }

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r { str := s.str, startPos := s.startPos, stopPos := s.str.next s.stopPos }
Tactic:
simp [v.stopPos, v.str, String.next]
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r
    { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
      stopPos :=
        { byteIdx := String.utf8Len l + String.utf8Len m } +
          { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } }

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r
    { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
      stopPos :=
        { byteIdx := String.utf8Len l + String.utf8Len m } +
          { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } }
Tactic:
have : String.get ⟨l ++ (m ++ c :: r)⟩ ⟨String.utf8Len l + String.utf8Len m⟩ = c := by
  have eq₁ : l ++ (m ++ c :: r) = (l ++ m) ++ (c :: r) := by simp
  have eq₂ : String.utf8Len l + String.utf8Len m = String.utf8Len (l ++ m) := by simp
  rw [eq₁, eq₂, String.get_of_valid]
  simp
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ ValidFor l (m ++ [c]) r
    { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
      stopPos :=
        { byteIdx := String.utf8Len l + String.utf8Len m } +
          { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } }

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ ValidFor l (m ++ [c]) r
    { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
      stopPos :=
        { byteIdx := String.utf8Len l + String.utf8Len m } +
          { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } }
Tactic:
rw [this]
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ ValidFor l (m ++ [c]) r
    { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
      stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ ValidFor l (m ++ [c]) r
    { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
      stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }
Tactic:
apply of_eq
State after:
case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.str.data =
    l ++ (m ++ [c]) ++ r

case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.startPos.byteIdx =
    String.utf8Len l

case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.stopPos.byteIdx =
    String.utf8Len l + String.utf8Len (m ++ [c])

State before:
case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.str.data =
    l ++ (m ++ [c]) ++ r

case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.startPos.byteIdx =
    String.utf8Len l

case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.stopPos.byteIdx =
    String.utf8Len l + String.utf8Len (m ++ [c])
Tactic:
. simp
State after:
case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.startPos.byteIdx =
    String.utf8Len l

case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.stopPos.byteIdx =
    String.utf8Len l + String.utf8Len (m ++ [c])

State before:
case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.startPos.byteIdx =
    String.utf8Len l

case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.stopPos.byteIdx =
    String.utf8Len l + String.utf8Len (m ++ [c])
Tactic:
. simp [v.startPos]
State after:
case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.stopPos.byteIdx =
    String.utf8Len l + String.utf8Len (m ++ [c])

State before:
case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.stopPos.byteIdx =
    String.utf8Len l + String.utf8Len (m ++ [c])
Tactic:
. simp [Nat.add_assoc]
State after:
no goals

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
⊢ s.stopPos < s.str.endPos
Tactic:
simp [v.stopPos, v.str]
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
⊢ String.utf8Len l + String.utf8Len m < String.utf8Len l + (String.utf8Len m + (String.utf8Len r + String.csize c))

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
⊢ String.utf8Len l + String.utf8Len m < String.utf8Len l + (String.utf8Len m + (String.utf8Len r + String.csize c))
Tactic:
have : 0 < String.csize c := String.csize_pos c
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : 0 < String.csize c
⊢ String.utf8Len l + String.utf8Len m < String.utf8Len l + (String.utf8Len m + (String.utf8Len r + String.csize c))

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : 0 < String.csize c
⊢ String.utf8Len l + String.utf8Len m < String.utf8Len l + (String.utf8Len m + (String.utf8Len r + String.csize c))
Tactic:
omega
State after:
no goals

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
Tactic:
have eq₁ : l ++ (m ++ c :: r) = (l ++ m) ++ (c :: r) := by simp
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
eq₁ : l ++ (m ++ c :: r) = l ++ m ++ c :: r
⊢ { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
eq₁ : l ++ (m ++ c :: r) = l ++ m ++ c :: r
⊢ { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
Tactic:
have eq₂ : String.utf8Len l + String.utf8Len m = String.utf8Len (l ++ m) := by simp
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
eq₁ : l ++ (m ++ c :: r) = l ++ m ++ c :: r
eq₂ : String.utf8Len l + String.utf8Len m = String.utf8Len (l ++ m)
⊢ { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
eq₁ : l ++ (m ++ c :: r) = l ++ m ++ c :: r
eq₂ : String.utf8Len l + String.utf8Len m = String.utf8Len (l ++ m)
⊢ { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
Tactic:
rw [eq₁, eq₂, String.get_of_valid]
State after:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
eq₁ : l ++ (m ++ c :: r) = l ++ m ++ c :: r
eq₂ : String.utf8Len l + String.utf8Len m = String.utf8Len (l ++ m)
⊢ (c :: r).headD default = c

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
eq₁ : l ++ (m ++ c :: r) = l ++ m ++ c :: r
eq₂ : String.utf8Len l + String.utf8Len m = String.utf8Len (l ++ m)
⊢ (c :: r).headD default = c
Tactic:
simp
State after:
no goals

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ l ++ (m ++ c :: r) = l ++ m ++ c :: r
Tactic:
simp
State after:
no goals

State before:
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
eq₁ : l ++ (m ++ c :: r) = l ++ m ++ c :: r
⊢ String.utf8Len l + String.utf8Len m = String.utf8Len (l ++ m)
Tactic:
simp
State after:
no goals

State before:
case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.str.data =
    l ++ (m ++ [c]) ++ r
Tactic:
simp
State after:
no goals

State before:
case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.startPos.byteIdx =
    String.utf8Len l
Tactic:
simp [v.startPos]
State after:
no goals

State before:
case a
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } + c }.stopPos.byteIdx =
    String.utf8Len l + String.utf8Len (m ++ [c])
Tactic:
simp [Nat.add_assoc]
State after:
no goals