Theorem: Regex.NFA.reaches_of_matches (RegexCorrectness/NFA/Transition/Closure/Equivalence.lean)

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
have := (matches_iff_pathToNext eq).mp m
State after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
have := pathIn_of_pathToNext this
State after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn (min 1 0) (↑nfa.start) 0 cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn (min 1 0) (↑nfa.start) 0 cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
simp at this
State after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
let i' : Fin nfa.nodes.size := ⟨0, lt_zero_size_compile eq⟩
State after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
have := reaches_of_pathIn (i := i') this
State after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝¹ : nfa.pathToNext 0 1 (↑nfa.start) cs
this✝ : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
this : nfa.reaches i' cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝¹ : nfa.pathToNext 0 1 (↑nfa.start) cs
this✝ : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
this : nfa.reaches i' cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
have hdone := (done_iff_zero_compile eq i').mpr rfl
State after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝¹ : nfa.pathToNext 0 1 (↑nfa.start) cs
this✝ : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
this : nfa.reaches i' cs
hdone : nfa[i'] = Node.done
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝¹ : nfa.pathToNext 0 1 (↑nfa.start) cs
this✝ : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
this : nfa.reaches i' cs
hdone : nfa[i'] = Node.done
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
exact ⟨i', this, hdone⟩
State after:
no goals