internlm/Lean-Github huggingface dataset:
Theorem: Regex.Data.SparseSet.lt_of_mem
Proof state before:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
ge : n ≤ s.count
⊢ s.dense[↑s.sparse[↑i]] = i
Tactic:
exact dense_sparse_of_full ge
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
⊢ i ∈ s.insert i
Tactic:
unfold insert
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
⊢ i ∈
    if mem : i ∈ s then s
    else
      match s, mem with
      | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
        let_fun isLt := ⋯;
        let dense' := dense.set count isLt i;
        let sparse' := sparse.set ↑i ⋯ ⟨count, isLt⟩;
        let_fun sparse_dense' := ⋯;
        { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Theorem: Regex.Data.SparseSet.mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
⊢ i ∈
    if mem : i ∈ s then s
    else
      match s, mem with
      | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
        let_fun isLt := ⋯;
        let dense' := dense.set count isLt i;
        let sparse' := sparse.set ↑i ⋯ ⟨count, isLt⟩;
        let_fun sparse_dense' := ⋯;
        { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Tactic:
split
Proof state after:
case inl
n : Nat
s : SparseSet n
i j : Fin n
h✝ : i ∈ s
⊢ i ∈ s

case inr
n : Nat
s : SparseSet n
i j : Fin n
h✝ : ¬i ∈ s
⊢ i ∈
    match s, h✝ with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt i;
      let sparse' := sparse.set ↑i ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Theorem: Regex.Data.SparseSet.mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
m : i ∈ s
⊢ i ∈ s
Tactic:
case inl m => exact m
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
m : ¬i ∈ s
⊢ i ∈
    match s, m with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt i;
      let sparse' := sparse.set ↑i ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Tactic:
case inr m => simp [mem]
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
m : i ∈ s
⊢ i ∈ s
Tactic:
exact m
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
m : ¬i ∈ s
⊢ i ∈
    match s, m with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt i;
      let sparse' := sparse.set ↑i ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Tactic:
simp [mem]
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.not_mem_of_isEmpty
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : s.isEmpty = true
⊢ ¬i ∈ s
Tactic:
intro m
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : s.isEmpty = true
m : i ∈ s
⊢ False
Theorem: Regex.Data.SparseSet.not_mem_of_isEmpty
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : s.isEmpty = true
m : i ∈ s
⊢ False
Tactic:
simp [isEmpty] at h
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
m : i ∈ s
h : s.count = 0
⊢ False
Theorem: Regex.Data.SparseSet.not_mem_of_isEmpty
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
m : i ∈ s
h : s.count = 0
⊢ False
Tactic:
simp [mem, h] at m
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : s.count = 0
m : ↑s.sparse[↑i] < 0 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ False
Theorem: Regex.Data.SparseSet.not_mem_of_isEmpty
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : s.count = 0
m : ↑s.sparse[↑i] < 0 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ False
Tactic:
have := m.left
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : s.count = 0
m : ↑s.sparse[↑i] < 0 ∧ s.dense[↑s.sparse[↑i]] = i
this : ↑s.sparse[↑i] < 0
⊢ False
Theorem: Regex.Data.SparseSet.not_mem_of_isEmpty
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : s.count = 0
m : ↑s.sparse[↑i] < 0 ∧ s.dense[↑s.sparse[↑i]] = i
this : ↑s.sparse[↑i] < 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.measure_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬i ∈ s
⊢ (s.insert i).measure = s.measure - 1
Tactic:
simp at h
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : s.mem i = false
⊢ (s.insert i).measure = s.measure - 1
Theorem: Regex.Data.SparseSet.measure_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : s.mem i = false
⊢ (s.insert i).measure = s.measure - 1
Tactic:
simp [measure, insert, h, Nat.sub_add_eq]
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.lt_measure_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ (s.insert i).measure < s.measure
Tactic:
simp [measure, insert, h, Nat.sub_add_eq]
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ n - s.count - 1 < n - s.count
Theorem: Regex.Data.SparseSet.lt_measure_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ n - s.count - 1 < n - s.count
Tactic:
apply Nat.sub_lt ?_ (by decide)
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ 0 < n - s.count
Theorem: Regex.Data.SparseSet.lt_measure_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ 0 < n - s.count
Tactic:
apply Nat.zero_lt_sub_of_lt (lt_of_mem i (by simp [h]))
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.lt_measure_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ 0 < 1
Tactic:
decide
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.lt_measure_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ ¬i ∈ s
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Regex.NFA.charStep_of_charStep
Proof state before:
j : ℕ
nfa : NFA
i : ℕ
c : Char
h : i < nfa.nodes.size
mem : j ∈ nfa[i].charStep c
⊢ j ∈ nfa.charStep i c
Tactic:
simp [charStep, h, mem]
Proof state after:
no goals
Theorem: Regex.NFA.εStep_of_εStep
Proof state before:
j : ℕ
nfa : NFA
i : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].εStep
⊢ j ∈ nfa.εStep i
Tactic:
simp [εStep, h, mem]
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_inBounds_of_charStep
Proof state before:
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
mem : j ∈ node.charStep c
⊢ j < k
Tactic:
unfold Node.charStep at mem
Proof state after:
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.char c' next => if (c == c') = true then {next} else ∅
    | Node.sparse cs next => if c ∈ cs then {next} else ∅
    | x => ∅
⊢ j < k
Theorem: Regex.NFA.lt_of_inBounds_of_charStep
Proof state before:
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.char c' next => if (c == c') = true then {next} else ∅
    | Node.sparse cs next => if c ∈ cs then {next} else ∅
    | x => ∅
⊢ j < k
Tactic:
split at mem <;> try simp [Node.inBounds] at *
Proof state after:
case h_1
j k : ℕ
c : Char
n✝ : Node
c'✝ : Char
next✝ : ℕ
inBounds : next✝ < k
mem : c = c'✝ ∧ j = next✝
⊢ j < k

case h_2
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
mem : c ∈ cs✝ ∧ j = next✝
⊢ j < k
Theorem: Regex.NFA.lt_of_inBounds_of_charStep
Proof state before:
case h_1
j k : ℕ
c : Char
n✝ : Node
c'✝ : Char
next✝ : ℕ
inBounds : next✝ < k
mem : c = c'✝ ∧ j = next✝
⊢ j < k

case h_2
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
mem : c ∈ cs✝ ∧ j = next✝
⊢ j < k
Tactic:
simp [*]
Proof state after:
case h_2
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
mem : c ∈ cs✝ ∧ j = next✝
⊢ j < k
Theorem: Regex.NFA.lt_of_inBounds_of_charStep
Proof state before:
case h_2
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
mem : c ∈ cs✝ ∧ j = next✝
⊢ j < k
Tactic:
cases mem
Proof state after:
case h_2.intro
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
left✝ : c ∈ cs✝
right✝ : j = next✝
⊢ j < k
Theorem: Regex.NFA.lt_of_inBounds_of_charStep
Proof state before:
case h_2.intro
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
left✝ : c ∈ cs✝
right✝ : j = next✝
⊢ j < k
Tactic:
simp [*]
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_inBounds_of_charStep
Proof state before:
case h_3
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
n✝ : Node
x✝¹ : ∀ (c' : Char) (next : ℕ), node = Node.char c' next → False
x✝ : ∀ (cs : Data.Classes) (next : ℕ), node = Node.sparse cs next → False
mem : j ∈ ∅
⊢ j < k
Tactic:
simp [Node.inBounds] at *
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_inBounds_of_εStep
Proof state before:
node : Node
j k : ℕ
inBounds : node.inBounds k
mem : j ∈ node.εStep
⊢ j < k
Tactic:
unfold Node.εStep at mem
Proof state after:
node : Node
j k : ℕ
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.epsilon next => {next}
    | Node.split next₁ next₂ => {next₁, next₂}
    | Node.save offset next => {next}
    | x => ∅
⊢ j < k
Theorem: Regex.NFA.lt_of_inBounds_of_εStep
Proof state before:
node : Node
j k : ℕ
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.epsilon next => {next}
    | Node.split next₁ next₂ => {next₁, next₂}
    | Node.save offset next => {next}
    | x => ∅
⊢ j < k
Tactic:
split at mem <;>
  try simp [Node.inBounds] at * <;>
  try cases mem <;>
  simp [*]
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_inBounds_of_εStep
Proof state before:
case h_4
node : Node
j k : ℕ
inBounds : node.inBounds k
n✝ : Node
x✝² : ∀ (next : ℕ), node = Node.epsilon next → False
x✝¹ : ∀ (next₁ next₂ : ℕ), node = Node.split next₁ next₂ → False
x✝ : ∀ (offset next : ℕ), node = Node.save offset next → False
mem : j ∈ ∅
⊢ j < k
Tactic:
simp [Node.inBounds] at * <;>
try cases mem <;>
simp [*]
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_inBounds_of_εStep
Proof state before:
case h_3
j k : ℕ
n✝ : Node
offset✝ next✝ : ℕ
inBounds : next✝ < k
mem : j = next✝
⊢ j < k
Tactic:
cases mem <;>
simp [*]
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_εStep
Proof state before:
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].εStep
⊢ j < nfa.nodes.size
Tactic:
have inBounds := nfa.inBounds ⟨i, h⟩
Proof state after:
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].εStep
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
Theorem: Regex.NFA.lt_of_εStep
Proof state before:
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].εStep
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
simp [get_eq_nodes_get] at mem
Proof state after:
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa.nodes[i].εStep
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
Theorem: Regex.NFA.lt_of_εStep
Proof state before:
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa.nodes[i].εStep
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_inBounds_of_εStep inBounds mem
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_charStep
Proof state before:
c : Char
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].charStep c
⊢ j < nfa.nodes.size
Tactic:
have inBounds := nfa.inBounds ⟨i, h⟩
Proof state after:
c : Char
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].charStep c
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
Theorem: Regex.NFA.lt_of_charStep
Proof state before:
c : Char
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].charStep c
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
simp [get_eq_nodes_get] at mem
Proof state after:
c : Char
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa.nodes[i].charStep c
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
Theorem: Regex.NFA.lt_of_charStep
Proof state before:
c : Char
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa.nodes[i].charStep c
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_inBounds_of_charStep inBounds mem
Proof state after:
no goals
Theorem: Regex.Data.Vec.get_set_eq
Proof state before:
α : Type
n i : Nat
a : α
v : Vec α n
h : i < n
⊢ (v.set i h a)[i] = a
Tactic:
simp [Vec.set, getElem]
Proof state after:
α : Type
n i : Nat
a : α
v : Vec α n
h : i < n
⊢ get ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩ i h = a
Theorem: Regex.Data.Vec.get_set_eq
Proof state before:
α : Type
n i : Nat
a : α
v : Vec α n
h : i < n
⊢ get ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩ i h = a
Tactic:
unfold Vec.get
Proof state after:
α : Type
n i : Nat
a : α
v : Vec α n
h : i < n
⊢ ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩.val[i] = a
Theorem: Regex.Data.Vec.get_set_eq
Proof state before:
α : Type
n i : Nat
a : α
v : Vec α n
h : i < n
⊢ ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩.val[i] = a
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.Data.Vec.get_set_ne
Proof state before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ (v.set i h₁ a)[j] = v[j]
Tactic:
simp [Vec.set, getElem]
Proof state after:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ get ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩ j h₂ = v.get j h₂
Theorem: Regex.Data.Vec.get_set_ne
Proof state before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ get ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩ j h₂ = v.get j h₂
Tactic:
unfold Vec.get
Proof state after:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩.val[j] = v.val[j]
Theorem: Regex.Data.Vec.get_set_ne
Proof state before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩.val[j] = v.val[j]
Tactic:
simp
Proof state after:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ (v.val.set ⟨i, ⋯⟩ a)[j] = v.val[j]
Theorem: Regex.Data.Vec.get_set_ne
Proof state before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ (v.val.set ⟨i, ⋯⟩ a)[j] = v.val[j]
Tactic:
rw [Array.get_set_ne]
Proof state after:
case h
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ ↑⟨i, ⋯⟩ ≠ j
Theorem: Regex.Data.Vec.get_set_ne
Proof state before:
case h
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ ↑⟨i, ⋯⟩ ≠ j
Tactic:
assumption
Proof state after:
no goals
Theorem: Regex.Data.Vec.get_set
Proof state before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
⊢ (v.set i h₁ a)[j] = if i = j then a else v[j]
Tactic:
if h : i = j then
  subst j
  simp
else
  simp [h]
Proof state after:
no goals
Theorem: Regex.Data.Vec.get_set
Proof state before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
h : i = j
⊢ (v.set i h₁ a)[j] = if i = j then a else v[j]
Tactic:
subst j
Proof state after:
α : Type
n i : Nat
a : α
v : Vec α n
h₁ h₂ : i < n
⊢ (v.set i h₁ a)[i] = if i = i then a else v[i]
Theorem: Regex.Data.Vec.get_set
Proof state before:
α : Type
n i : Nat
a : α
v : Vec α n
h₁ h₂ : i < n
⊢ (v.set i h₁ a)[i] = if i = i then a else v[i]
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.Data.Vec.get_set
Proof state before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
h : ¬i = j
⊢ (v.set i h₁ a)[j] = if i = j then a else v[j]
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Regex.Data.Vec.set_set
Proof state before:
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ (v.set i h a).set i h b = v.set i h b
Tactic:
apply Subtype.eq
Proof state after:
case a
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ ((v.set i h a).set i h b).val = (v.set i h b).val
Theorem: Regex.Data.Vec.set_set
Proof state before:
case a
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ ((v.set i h a).set i h b).val = (v.set i h b).val
Tactic:
simp [Vec.set]
Proof state after:
case a
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ (v.val.set ⟨i, ⋯⟩ a).set ⟨i, ⋯⟩ b = v.val.set ⟨i, ⋯⟩ b
Theorem: Regex.Data.Vec.set_set
Proof state before:
case a
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ (v.val.set ⟨i, ⋯⟩ a).set ⟨i, ⋯⟩ b = v.val.set ⟨i, ⋯⟩ b
Tactic:
rw [Array.set_set]
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
⊢ 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
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
⊢ ValidFor l (m ++ [c]) r s.expand
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
⊢ ValidFor l (m ++ [c]) r s.expand
Tactic:
unfold expand
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
⊢ 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)
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
⊢ 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]
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
⊢ ValidFor l (m ++ [c]) r { str := s.str, startPos := s.startPos, stopPos := s.str.next s.stopPos }
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
⊢ 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]
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
⊢ 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 } }
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
⊢ 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
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
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 } }
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
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]
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
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 }
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
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
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 }.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])