internlm/Lean-Github huggingface dataset:
Theorem: Substring.ValidFor.expand
Proof 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
Proof 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])
Theorem: Substring.ValidFor.expand
Proof 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]
Proof 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])
Theorem: Substring.ValidFor.expand
Proof 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]
Proof state after:
no goals
Theorem: Substring.ValidFor.expand
Proof 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]
Proof 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))
Theorem: Substring.ValidFor.expand
Proof 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
Proof 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))
Theorem: Substring.ValidFor.expand
Proof 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
Proof state after:
no goals
Theorem: Substring.ValidFor.expand
Proof 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
Proof 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
Theorem: Substring.ValidFor.expand
Proof 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
Proof 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
Theorem: Substring.ValidFor.expand
Proof 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]
Proof 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
Theorem: Substring.ValidFor.expand
Proof 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
Proof state after:
no goals
Theorem: Substring.ValidFor.expand
Proof 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
Proof state after:
no goals
Theorem: Substring.ValidFor.expand
Proof 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
Proof state after:
no goals
Theorem: Substring.ValidFor.expand
Proof 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
Proof state after:
no goals
Theorem: Substring.ValidFor.expand
Proof 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]
Proof state after:
no goals
Theorem: Substring.ValidFor.expand
Proof 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]
Proof state after:
no goals
Theorem: String.Iterator.Valid.next'
Proof state before:
it : Iterator
v : it.Valid
h : ¬it.atEnd = true
⊢ it.next.Valid
Tactic:
apply v.next
Proof state after:
it : Iterator
v : it.Valid
h : ¬it.atEnd = true
⊢ it.hasNext = true
Theorem: String.Iterator.Valid.next'
Proof state before:
it : Iterator
v : it.Valid
h : ¬it.atEnd = true
⊢ it.hasNext = true
Tactic:
simp [hasNext, atEnd] at *
Proof state after:
it : Iterator
v : it.Valid
h : it.i.byteIdx < it.s.endPos.byteIdx
⊢ it.i.byteIdx < it.s.endPos.byteIdx
Theorem: String.Iterator.Valid.next'
Proof state before:
it : Iterator
v : it.Valid
h : it.i.byteIdx < it.s.endPos.byteIdx
⊢ it.i.byteIdx < it.s.endPos.byteIdx
Tactic:
exact h
Proof state after:
no goals
Theorem: String.Iterator.ValidFor.exists_cons_of_not_atEnd
Proof state before:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
⊢ ∃ r', r = it.curr :: r'
Tactic:
have := v.atEnd
Proof state after:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : it.atEnd = true ↔ r = []
⊢ ∃ r', r = it.curr :: r'
Theorem: String.Iterator.ValidFor.exists_cons_of_not_atEnd
Proof state before:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : it.atEnd = true ↔ r = []
⊢ ∃ r', r = it.curr :: r'
Tactic:
simp [h] at this
Proof state after:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : ¬r = []
⊢ ∃ r', r = it.curr :: r'
Theorem: String.Iterator.ValidFor.exists_cons_of_not_atEnd
Proof state before:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : ¬r = []
⊢ ∃ r', r = it.curr :: r'
Tactic:
have ⟨c, r', heq⟩ := List.exists_cons_of_ne_nil this
Proof state after:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : ¬r = []
c : Char
r' : List Char
heq : r = c :: r'
⊢ ∃ r', r = it.curr :: r'
Theorem: String.Iterator.ValidFor.exists_cons_of_not_atEnd
Proof state before:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : ¬r = []
c : Char
r' : List Char
heq : r = c :: r'
⊢ ∃ r', r = it.curr :: r'
Tactic:
subst heq
Proof state after:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this : ¬c :: r' = []
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1
Theorem: String.Iterator.ValidFor.exists_cons_of_not_atEnd
Proof state before:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this : ¬c :: r' = []
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1
Tactic:
have := v.curr
Proof state after:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this✝ : ¬c :: r' = []
this : it.curr = (c :: r').headD default
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1
Theorem: String.Iterator.ValidFor.exists_cons_of_not_atEnd
Proof state before:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this✝ : ¬c :: r' = []
this : it.curr = (c :: r').headD default
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1
Tactic:
simp at this
Proof state after:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this✝ : ¬c :: r' = []
this : it.curr = c
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1
Theorem: String.Iterator.ValidFor.exists_cons_of_not_atEnd
Proof state before:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this✝ : ¬c :: r' = []
this : it.curr = c
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1
Tactic:
subst this
Proof state after:
l : List Char
it : Iterator
h : ¬it.atEnd = true
r' : List Char
v : ValidFor l (it.curr :: r') it
this : ¬it.curr :: r' = []
⊢ ∃ r'_1, it.curr :: r' = it.curr :: r'_1
Theorem: String.Iterator.ValidFor.exists_cons_of_not_atEnd
Proof state before:
l : List Char
it : Iterator
h : ¬it.atEnd = true
r' : List Char
v : ValidFor l (it.curr :: r') it
this : ¬it.curr :: r' = []
⊢ ∃ r'_1, it.curr :: r' = it.curr :: r'_1
Tactic:
exact ⟨r', rfl⟩
Proof state after:
no goals
Theorem: Regex.VM.matches_of_captureNext
Proof state before:
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re
Tactic:
have ⟨s, l, m, r, sv, eqs, i, hr, hdone⟩ := captureNext_spec h v hsome
Proof state after:
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
eqs : it.toString = { data := l ++ m ++ r }
i : Fin nfa.nodes.size
hr : nfa.reaches i m
hdone : nfa[i] = Node.done
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re
Theorem: Regex.VM.matches_of_captureNext
Proof state before:
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
eqs : it.toString = { data := l ++ m ++ r }
i : Fin nfa.nodes.size
hr : nfa.reaches i m
hdone : nfa[i] = Node.done
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re
Tactic:
have ma := matches_of_reaches eq hr hdone
Proof state after:
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
eqs : it.toString = { data := l ++ m ++ r }
i : Fin nfa.nodes.size
hr : nfa.reaches i m
hdone : nfa[i] = Node.done
ma : Data.Expr.matches m re
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re
Theorem: Regex.VM.matches_of_captureNext
Proof state before:
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
eqs : it.toString = { data := l ++ m ++ r }
i : Fin nfa.nodes.size
hr : nfa.reaches i m
hdone : nfa[i] = Node.done
ma : Data.Expr.matches m re
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re
Tactic:
exact ⟨s, l, m, r, sv, eqs, ma⟩
Proof state after:
no goals
Theorem: Array.zero_lt_size_of_not_empty
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ 0 < a.size
Tactic:
apply Nat.zero_lt_of_ne_zero
Proof state after:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.size ≠ 0
Theorem: Array.zero_lt_size_of_not_empty
Proof state before:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.size ≠ 0
Tactic:
intro heq
Proof state after:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
heq : a.size = 0
⊢ False
Theorem: Array.zero_lt_size_of_not_empty
Proof state before:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
heq : a.size = 0
⊢ False
Tactic:
have : a = #[] := eq_empty_of_size_eq_zero heq
Proof state after:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
heq : a.size = 0
this : a = #[]
⊢ False
Theorem: Array.zero_lt_size_of_not_empty
Proof state before:
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
heq : a.size = 0
this : a = #[]
⊢ False
Tactic:
simp [this] at hemp
Proof state after:
no goals
Theorem: Array.lt_size_of_pop_of_not_empty
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.pop.size < a.size
Tactic:
have : 0 < a.size := zero_lt_size_of_not_empty hemp
Proof state after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ a.pop.size < a.size
Theorem: Array.lt_size_of_pop_of_not_empty
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ a.pop.size < a.size
Tactic:
have : a.size - 1 < a.size := Nat.sub_lt_of_pos_le (by decide) this
Proof state after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
this : a.size - 1 < a.size
⊢ a.pop.size < a.size
Theorem: Array.lt_size_of_pop_of_not_empty
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
this : a.size - 1 < a.size
⊢ a.pop.size < a.size
Tactic:
simp [Array.pop]
Proof state after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
this : a.size - 1 < a.size
⊢ a.size - 1 < a.size
Theorem: Array.lt_size_of_pop_of_not_empty
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
this : a.size - 1 < a.size
⊢ a.size - 1 < a.size
Tactic:
exact this
Proof state after:
no goals
Theorem: Array.lt_size_of_pop_of_not_empty
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ 0 < 1
Tactic:
decide
Proof state after:
no goals
Theorem: Regex.NFA.pushNode_size
Proof state before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
⊢ (nfa.pushNode node inBounds).val.nodes.size = nfa.nodes.size + 1
Tactic:
simp [pushNode]
Proof state after:
no goals
Theorem: Regex.NFA.pushNode_get_lt
Proof state before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h : i < nfa.nodes.size
⊢ (nfa.pushNode node inBounds).val[i] = nfa[i]
Tactic:
simp [pushNode, get_eq_nodes_get]
Proof state after:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h : i < nfa.nodes.size
⊢ (nfa.nodes.push node)[i] = nfa.nodes[i]
Theorem: Regex.NFA.pushNode_get_lt
Proof state before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h : i < nfa.nodes.size
⊢ (nfa.nodes.push node)[i] = nfa.nodes[i]
Tactic:
rw [Array.get_push_lt]
Proof state after:
no goals
Theorem: Regex.NFA.pushNode_get_eq
Proof state before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
⊢ (nfa.pushNode node inBounds).val[nfa.nodes.size] = node
Tactic:
simp [pushNode, get_eq_nodes_get]
Proof state after:
no goals
Theorem: Regex.NFA.pushNode_get
Proof state before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h : i < (nfa.pushNode node inBounds).val.nodes.size
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node
Tactic:
simp at h
Proof state after:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h✝ : i < (nfa.pushNode node inBounds).val.nodes.size
h : i < nfa.nodes.size + 1
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node
Theorem: Regex.NFA.pushNode_get
Proof state before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h✝ : i < (nfa.pushNode node inBounds).val.nodes.size
h : i < nfa.nodes.size + 1
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node
Tactic:
cases Nat.lt_or_eq_of_le (Nat.le_of_succ_le_succ h) with
| inl lt => simp [lt, pushNode_get_lt _ lt]
| inr eq => simp [eq]
Proof state after:
no goals
Theorem: Regex.NFA.pushNode_get
Proof state before:
case inl
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h✝ : i < (nfa.pushNode node inBounds).val.nodes.size
h : i < nfa.nodes.size + 1
lt : i < nfa.nodes.size
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node
Tactic:
simp [lt, pushNode_get_lt _ lt]
Proof state after:
no goals
Theorem: Regex.NFA.pushNode_get
Proof state before:
case inr
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h✝ : i < (nfa.pushNode node inBounds).val.nodes.size
h : i < nfa.nodes.size + 1
eq : i = nfa.nodes.size
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node
Tactic:
simp [eq]
Proof state after:
no goals
Theorem: Probly.flip.pdf_wrt_flip
Proof state before:
θ θ' : ℝ
⊢ Rand.pdf' (flip θ) ↑(flip θ').μ = fun b => if b = true then θ / θ' else (1 - θ) / (1 - θ')
Tactic:
sorry
Proof state after:
no goals
Theorem: Probly.dflip.density_wrt_flip
Proof state before:
θ : ℝ
⊢ DRand.density dflip ↑(flip θ).μ = fun b => if b = true then 1 / θ else 1 / (θ - 1)
Tactic:
sorry
Proof state after:
no goals
Theorem: Probly.flip.pdf
Proof state before:
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ Rand.pdf' (flip x) Measure.count = fun b => if b = true then x else 1 - x
Tactic:
sorry
Proof state after:
no goals
Theorem: Probly.flip_integral
Proof state before:
W : Type ?u.3072
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_1
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3307
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3424
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3541
inst✝¹ : MeasurableSpace α
β : Type ?u.3547
inst✝ : MeasurableSpace β
θ : ℝ
f : Bool → X
⊢ ∫ (x : Bool), f x ∂↑(flip θ).μ = θ • f true + (1 - θ) • f false
Tactic:
simp [flip,rand_simp]
Proof state after:
no goals
Theorem: Probly.flip_expectedValue
Proof state before:
W : Type ?u.13866
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_1
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.14101
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.14218
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.14335
inst✝¹ : MeasurableSpace α
β : Type ?u.14341
inst✝ : MeasurableSpace β
θ : ℝ
f : Bool → X
⊢ Rand.E (flip θ) f = θ • f true + (1 - θ) • f false
Tactic:
simp[Rand.E,Rand.expectedValue,rand_simp]
Proof state after:
no goals