Skip to content

Commit 153ed60

Browse files
pandaman64pandaman64
authored
v4.27.0-rc1 (#147)
* Update regex to v4.27.0-rc1 * Update correctness to v4.27.0-rc1 * Migrate remaining ValidPos * Upgrade docbuild to v4.27.0-rc1
1 parent a763ee1 commit 153ed60

66 files changed

Lines changed: 582 additions & 657 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎correctness/RegexCorrectness/Backtracker/Basic.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,14 +4,14 @@ import Mathlib.Tactic.DepRewrite
44
set_option autoImplicit false
55

66
open Regex.Data (BitMatrix BVPos)
7-
open String (ValidPos)
7+
open String (Pos)
88

99
namespace Regex.Backtracker
1010

1111
namespace captureNextAux.pushNext
1212

1313
variable {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed}
14-
{startPos : ValidPos s} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : BVPos startPos}
14+
{startPos : Pos s} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : BVPos startPos}
1515

1616
theorem done (hn : nfa[state] = .done) : pushNext σ nfa wf startPos stack update state pos = stack := by
1717
rw! [pushNext, hn]
@@ -75,7 +75,7 @@ theorem sparse_neg {cs : Data.Classes} {state' : Nat} (hn : nfa[state] = .sparse
7575
| .inl h => simp [h]
7676
| .inr ⟨ne, hc⟩ => simp [ne, hc]
7777

78-
theorem fun_cases' (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : ValidPos s)
78+
theorem fun_cases' (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : Pos s)
7979
{motive : List (StackEntry σ nfa startPos) → σ.Update → Fin nfa.nodes.size → BVPos startPos → Prop}
8080
(done : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : BVPos startPos),
8181
nfa[state] = .done → motive stack update state pos)
@@ -147,7 +147,7 @@ theorem fun_cases' (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos
147147

148148
end captureNextAux.pushNext
149149

150-
theorem captureNextAux.induct' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : ValidPos s)
150+
theorem captureNextAux.induct' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : Pos s)
151151
(motive : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1) → List (StackEntry σ nfa startPos) → Prop)
152152
(base : ∀ (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)), motive visited [])
153153
(visited : ∀ (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : BVPos startPos) (stack' : List (StackEntry σ nfa startPos)),
@@ -175,7 +175,7 @@ Simplification lemmas for `captureNextAux`.
175175
-/
176176
section
177177

178-
variable {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
178+
variable {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
179179

180180
theorem captureNextAux_base :
181181
captureNextAux σ nfa wf startPos visited [] = (.none, visited) := by
@@ -206,7 +206,7 @@ theorem captureNextAux_next {update state pos stack'} (mem : ¬visited.get state
206206

207207
end
208208

209-
theorem captureNext.go.induct' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : ValidPos s)
209+
theorem captureNext.go.induct' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : Pos s)
210210
(motive : (pos : BVPos startPos) → BitMatrix nfa.nodes.size (startPos.remainingBytes + 1) → Prop)
211211
(found : ∀ (pos : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (update : σ.Update) (visited' : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)),
212212
captureNextAux σ nfa wf startPos visited [⟨σ.empty, ⟨nfa.start, wf.start_lt⟩, pos⟩] = (.some update, visited') →
@@ -231,7 +231,7 @@ Simplification lemmas for `captureNext.go`.
231231
section
232232

233233
variable {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed}
234-
{startPos : ValidPos s} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {pos : BVPos startPos}
234+
{startPos : Pos s} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {pos : BVPos startPos}
235235

236236
theorem captureNext.go_found {update visited'} (h : captureNextAux σ nfa wf startPos visited [⟨σ.empty, ⟨nfa.start, wf.start_lt⟩, pos⟩] = (.some update, visited')) :
237237
captureNext.go σ nfa wf startPos pos visited = .some update := by

‎correctness/RegexCorrectness/Backtracker/Compile.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ import RegexCorrectness.NFA.Semantics
44

55
set_option autoImplicit false
66

7-
open String (ValidPos)
7+
open String (Pos)
88
open Regex.NFA (EquivUpdate)
99
open Regex.Data (CaptureGroups BitMatrix BVPos)
1010

@@ -14,7 +14,7 @@ namespace captureNext
1414

1515
theorem path_done_of_some {s nfa wf pos update} (hres : captureNext (HistoryStrategy s) nfa wf pos = .some update) :
1616
∃ state pos' pos'', nfa[state] = .done ∧ pos ≤ pos' ∧ Path nfa wf pos' pos'' state update := by
17-
let bvpos : BVPos pos := ⟨pos, ValidPos.le_refl _⟩
17+
let bvpos : BVPos pos := ⟨pos, Pos.le_refl _⟩
1818
dsimp [captureNext] at hres
1919
have ⟨state, bvpos', bvpos'', hn, le, path⟩ := go.path_done_of_some hres
2020
exact ⟨state, bvpos'.current, bvpos''.current, hn, le, path⟩
@@ -32,25 +32,25 @@ theorem capture_of_some_compile {s e pos update} (hres : captureNext (HistoryStr
3232
exact ⟨pos', pos'', groups, le, c, eqv⟩
3333

3434
theorem ne_done_of_path_of_none {s nfa wf pos} (hres : captureNext (HistoryStrategy s) nfa wf pos = .none) :
35-
∀ (pos' pos'' : ValidPos s) (state : Fin nfa.nodes.size) (update : List (Nat × ValidPos s)),
35+
∀ (pos' pos'' : Pos s) (state : Fin nfa.nodes.size) (update : List (Nat × Pos s)),
3636
pos ≤ pos' →
3737
Path nfa wf pos' pos'' state update →
3838
nfa[state] ≠ .done := by
3939
dsimp [captureNext] at hres
4040

41-
let bvpos : BVPos pos := ⟨pos, ValidPos.le_refl _⟩
41+
let bvpos : BVPos pos := ⟨pos, Pos.le_refl _⟩
4242
let visited := BitMatrix.zero nfa.nodes.size (pos.remainingBytes + 1)
4343

4444
have h := go.ne_done_of_path_of_none hres (BVPos.le_refl _) go.Inv.zero captureNextAux.NotDoneInv.zero
4545

4646
intro pos' pos'' state update le path hn
4747
let bvpos' : BVPos pos := ⟨pos', le⟩
48-
let bvpos'' : BVPos pos := ⟨pos'', ValidPos.le_trans le path.le⟩
48+
let bvpos'' : BVPos pos := ⟨pos'', Pos.le_trans le path.le⟩
4949

5050
exact h bvpos' bvpos'' state update bvpos'.le path hn
5151

5252
theorem not_captures_of_none_compile {s e pos} (hres : captureNext (HistoryStrategy s) (NFA.compile e) NFA.compile_wf pos = .none)
53-
(pos' pos'' : ValidPos s) (groups : CaptureGroups s) (le : pos ≤ pos') :
53+
(pos' pos'' : Pos s) (groups : CaptureGroups s) (le : pos ≤ pos') :
5454
¬e.Captures pos' pos'' groups := by
5555
intro c
5656
have ⟨update, _, path⟩ := NFA.path_of_captures_compile rfl c

‎correctness/RegexCorrectness/Backtracker/Correctness.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,14 +8,14 @@ open Regex (NFA)
88
open Regex.Data (Expr CaptureGroups)
99
open Regex.Strategy (EquivMaterializedUpdate materializeRegexGroups materializeUpdates)
1010
open RegexCorrectness.Spec (SearchProblem)
11-
open String (ValidPos)
11+
open String (Pos)
1212

1313
namespace Regex.Backtracker
1414

1515
theorem captureNext_soundness {s e bufferSize pos matchedB}
1616
(disj : e.Disjoint)
1717
(hresB : captureNext (BufferStrategy s bufferSize) (NFA.compile e) NFA.compile_wf pos = .some matchedB) :
18-
∃ (pos' pos'' : ValidPos s) (groups : CaptureGroups s),
18+
∃ (pos' pos'' : Pos s) (groups : CaptureGroups s),
1919
pos ≤ pos' ∧
2020
e.Captures pos' pos'' groups ∧
2121
EquivMaterializedUpdate (materializeRegexGroups groups) matchedB := by
@@ -31,7 +31,7 @@ theorem captureNext_soundness {s e bufferSize pos matchedB}
3131

3232
theorem captureNext_completeness' {s e bufferSize pos}
3333
(hresB : captureNext (BufferStrategy s bufferSize) (NFA.compile e) NFA.compile_wf pos = .none)
34-
(pos' pos'' : ValidPos s) (groups : CaptureGroups s) (le : pos ≤ pos') (c : e.Captures pos' pos'' groups) :
34+
(pos' pos'' : Pos s) (groups : CaptureGroups s) (le : pos ≤ pos') (c : e.Captures pos' pos'' groups) :
3535
False := by
3636
match hresH : captureNext (HistoryStrategy s) (NFA.compile e) NFA.compile_wf pos with
3737
| .some matchedH =>
@@ -41,13 +41,13 @@ theorem captureNext_completeness' {s e bufferSize pos}
4141

4242
theorem captureNext_completeness {s e bufferSize pos}
4343
(hresB : captureNext (BufferStrategy s bufferSize) (NFA.compile e) NFA.compile_wf pos = .none) :
44-
¬∃ (pos' pos'' : ValidPos s) (groups : CaptureGroups s),
44+
¬∃ (pos' pos'' : Pos s) (groups : CaptureGroups s),
4545
pos ≤ pos' ∧
4646
e.Captures pos' pos'' groups := by
4747
grind [captureNext_completeness']
4848

4949
-- NOTE: we don't make this an instance because there are multiple decision procedures
50-
def decideSearchProblem {s : String} (e : Expr) (pos : ValidPos s) (disj : e.Disjoint) : Decidable (SearchProblem e pos) :=
50+
def decideSearchProblem {s : String} (e : Expr) (pos : Pos s) (disj : e.Disjoint) : Decidable (SearchProblem e pos) :=
5151
match hresB : captureNext (BufferStrategy s 0) (NFA.compile e) NFA.compile_wf pos with
5252
| .some _ => .isTrue <|
5353
have ⟨pos', pos'', groups, le, c, _⟩ := captureNext_soundness disj hresB

‎correctness/RegexCorrectness/Backtracker/Path.lean‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,27 +3,27 @@ import RegexCorrectness.NFA.Semantics.Path
33

44
set_option autoImplicit false
55

6-
open String (ValidPos)
6+
open String (Pos)
77
open Regex.Data (BVPos)
88

99
namespace Regex.Backtracker
1010

11-
inductive Path {s : String} (nfa : NFA) (wf : nfa.WellFormed) (pos : ValidPos s) : ValidPos s → Fin nfa.nodes.size → List (Nat × ValidPos s) → Prop where
11+
inductive Path {s : String} (nfa : NFA) (wf : nfa.WellFormed) (pos : Pos s) : Pos s → Fin nfa.nodes.size → List (Nat × Pos s) → Prop where
1212
| init : Path nfa wf pos pos ⟨nfa.start, wf.start_lt⟩ []
1313
| more {i j : Fin nfa.nodes.size} {pos' pos'' update₁ update₂ update₃} (prev : Path nfa wf pos pos' i update₁) (step : nfa.Step 0 i pos' j pos'' update₂)
1414
(equpdate : update₃ = update₁ ++ List.ofOption update₂) :
1515
Path nfa wf pos pos'' j update₃
1616

1717
namespace Path
1818

19-
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' pos'' : ValidPos s} {i j : Fin nfa.nodes.size}
20-
{update update₁ update₂ update₃ : List (Nat × ValidPos s)}
19+
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' pos'' : Pos s} {i j : Fin nfa.nodes.size}
20+
{update update₁ update₂ update₃ : List (Nat × Pos s)}
2121

2222
theorem le (path : Path nfa wf pos pos' i update) :
2323
pos ≤ pos' := by
2424
induction path with
25-
| init => exact ValidPos.le_refl _
26-
| more _ step _ ih => exact ValidPos.le_trans ih step.le
25+
| init => exact Pos.le_refl _
26+
| more _ step _ ih => exact Pos.le_trans ih step.le
2727

2828
theorem eq_or_nfaPath (path : Path nfa wf pos pos' i update) :
2929
(pos' = pos ∧ i.val = nfa.start ∧ update = []) ∨
@@ -56,9 +56,9 @@ theorem of_nfaPath {i : Nat} (path : nfa.Path 0 nfa.start pos i pos' update) :
5656
have path₁ : Path nfa wf pos pos ⟨nfa.start, wf.start_lt⟩ [] := .init
5757
exact path₁.concat_nfaPath wf.start_lt path (by simp)
5858

59-
def bvpos' {startPos : ValidPos s} {bvpos : BVPos startPos} {pos' i update}
59+
def bvpos' {startPos : Pos s} {bvpos : BVPos startPos} {pos' i update}
6060
(path : Path nfa wf bvpos.current pos' i update) : BVPos startPos :=
61-
⟨pos', ValidPos.le_trans bvpos.le path.le⟩
61+
⟨pos', Pos.le_trans bvpos.le path.le⟩
6262

6363
end Path
6464

‎correctness/RegexCorrectness/Backtracker/Refinement.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,10 @@ set_option autoImplicit false
66
open Regex (NFA)
77
open Regex.Data (BitMatrix BVPos)
88
open Regex.Strategy (materializeUpdates)
9-
open String (ValidPos ValidPosPlusOne)
9+
open String (Pos PosPlusOne)
1010
namespace Regex.Backtracker
1111

12-
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s} {bufferSize : Nat}
12+
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {bufferSize : Nat}
1313

1414
def StackEntry.materialize (entryH : StackEntry (HistoryStrategy s) nfa startPos) : StackEntry (BufferStrategy s bufferSize) nfa startPos :=
1515
⟨materializeUpdates bufferSize entryH.update, entryH.state, entryH.pos⟩
@@ -24,10 +24,10 @@ theorem materializeStack.nil : materializeStack [] = ([] : List (StackEntry (Buf
2424
theorem materializeStack.cons {entryH stackH} :
2525
materializeStack (entryH :: stackH) = (StackEntry.materialize entryH :: materializeStack stackH : List (StackEntry (BufferStrategy s bufferSize) nfa startPos)) := rfl
2626

27-
def materializeResultAux (resultH : Option (List (Nat × ValidPos s)) × BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Option (Buffer s bufferSize) × BitMatrix nfa.nodes.size (startPos.remainingBytes + 1) :=
27+
def materializeResultAux (resultH : Option (List (Nat × Pos s)) × BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Option (Buffer s bufferSize) × BitMatrix nfa.nodes.size (startPos.remainingBytes + 1) :=
2828
⟨resultH.1.map (materializeUpdates bufferSize), resultH.2⟩
2929

30-
def materializeResult (resultH : Option (List (Nat × ValidPos s))) : Option (Buffer s bufferSize) :=
30+
def materializeResult (resultH : Option (List (Nat × Pos s))) : Option (Buffer s bufferSize) :=
3131
resultH.map (materializeUpdates bufferSize)
3232

3333
theorem captureNextAux.pushNext.refines {s nfa wf startPos bufferSize stackH stackB updateH updateB state pos}

‎correctness/RegexCorrectness/Backtracker/Traversal/Invariants.lean‎

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ import RegexCorrectness.Backtracker.Path
66
set_option autoImplicit false
77

88
open Regex.Data (BitMatrix BVPos)
9-
open String (ValidPos)
9+
open String (Pos)
1010
open Regex.NFA (Step)
1111

1212
namespace Regex.Backtracker.captureNextAux
@@ -46,7 +46,7 @@ end
4646

4747
section
4848

49-
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s}
49+
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s}
5050
{visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {update' visited'}
5151

5252
def StackInv (wf : nfa.WellFormed) (bvpos : BVPos startPos) (stack : List (StackEntry (HistoryStrategy s) nfa startPos)) : Prop :=
@@ -156,11 +156,11 @@ end
156156

157157
section
158158

159-
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s}
159+
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s}
160160
{bvpos₀ : BVPos startPos} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
161161

162162
def ClosureInv (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (stack : List (StackEntry (HistoryStrategy s) nfa startPos)) : Prop :=
163-
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × ValidPos s)),
163+
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
164164
bvpos₀ ≤ bvpos →
165165
visited.get state bvpos.index →
166166
nfa.Step 0 state bvpos.current state' bvpos'.current update →
@@ -171,7 +171,7 @@ namespace ClosureInv
171171
-- Preservation of the non-visited cases
172172
theorem preserves' {entry stack'} (inv : ClosureInv bvpos₀ visited (entry :: stack))
173173
(nextEntries : List (StackEntry (HistoryStrategy s) nfa startPos)) (hstack : stack' = nextEntries ++ stack)
174-
(hnext : ∀ (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × ValidPos s)),
174+
(hnext : ∀ (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
175175
nfa.Step 0 entry.state entry.pos.current state' bvpos'.current update →
176176
∃ entry' ∈ nextEntries, entry'.state = state' ∧ entry'.pos = bvpos') :
177177
ClosureInv bvpos₀ (visited.set entry.state entry.pos.index) stack' := by
@@ -256,7 +256,7 @@ theorem preserves {stack update state bvpos} (wf : nfa.WellFormed) (inv : Closur
256256
| char_neg stack' update state bvpos c state' hn h =>
257257
rw [pushNext.char_neg hn h]
258258
apply inv.preserves' [] (by simp)
259-
have {ne : bvpos.current ≠ s.endValidPos} : bvpos.current.get ne ≠ c := by
259+
have {ne : bvpos.current ≠ s.endPos} : bvpos.current.get ne ≠ c := by
260260
match h with
261261
| .inl eq => simp [eq] at ne
262262
| .inr ⟨ne', hc⟩ => simpa [BVPos.get] using hc
@@ -272,7 +272,7 @@ theorem preserves {stack update state bvpos} (wf : nfa.WellFormed) (inv : Closur
272272
| sparse_neg stack' update state bvpos cs state' hn h =>
273273
rw [pushNext.sparse_neg hn h]
274274
apply inv.preserves' [] (by simp)
275-
have {ne : bvpos.current ≠ s.endValidPos} : bvpos.current.get ne ∉ cs := by
275+
have {ne : bvpos.current ≠ s.endPos} : bvpos.current.get ne ∉ cs := by
276276
match h with
277277
| .inl eq => simp [eq] at ne
278278
| .inr ⟨ne', hc⟩ => simpa [BVPos.get] using hc
@@ -311,14 +311,14 @@ theorem step_closure {bvpos₀ bvpos : BVPos startPos} {result} (hres : captureN
311311
exact ih hres (cinv.preserves wf hn) stinv.preserves
312312

313313
def StepClosure (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
314-
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × ValidPos s)),
314+
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
315315
bvpos₀ ≤ bvpos →
316316
visited.get state bvpos.index →
317317
nfa.Step 0 state bvpos.current state' bvpos'.current update →
318318
visited.get state' bvpos'.index
319319

320320
def PathClosure (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
321-
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : List (Nat × ValidPos s)),
321+
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : List (Nat × Pos s)),
322322
bvpos₀ ≤ bvpos →
323323
visited.get state bvpos.index →
324324
nfa.Path 0 state bvpos.current state' bvpos'.current update →
@@ -331,12 +331,12 @@ theorem zero : PathClosure bvpos₀ (BitMatrix.zero nfa.nodes.size (startPos.rem
331331
simp at hmem
332332

333333
theorem of_step_closure {bvpos₀ : BVPos startPos} (wf : nfa.WellFormed) (h : StepClosure bvpos₀ visited) : PathClosure bvpos₀ visited := by
334-
let motive (i : Nat) (pos : ValidPos s) : Prop :=
334+
let motive (i : Nat) (pos : Pos s) : Prop :=
335335
∃ (isLt : i < nfa.nodes.size) (bvpos : BVPos startPos), bvpos₀ ≤ bvpos ∧ pos = bvpos.current ∧ visited.get ⟨i, isLt⟩ bvpos.index
336336
have cls i pos j pos' update (base : motive i pos) (step : nfa.Step 0 i pos j pos' update) : motive j pos' := by
337337
have ⟨_, bvpos, le, hbvpos, hmem⟩ := base
338338

339-
let bvpos' : BVPos startPos := ⟨pos', ValidPos.le_trans (hbvpos ▸ bvpos.le) step.le⟩
339+
let bvpos' : BVPos startPos := ⟨pos', Pos.le_trans (hbvpos ▸ bvpos.le) step.le⟩
340340

341341
have le₀' : bvpos₀ ≤ bvpos' := BVPos.le_trans le (BVPos.le_iff.mpr (hbvpos ▸ step.le))
342342
have visited' := h ⟨i, step.lt⟩ bvpos ⟨j, step.lt_right wf⟩ bvpos' update le hmem (by simp [←hbvpos, bvpos', step])
@@ -369,7 +369,7 @@ end
369369

370370
section
371371

372-
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s} {bvpos₀ bvpos : BVPos startPos}
372+
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {bvpos₀ bvpos : BVPos startPos}
373373
{visited visited' : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
374374

375375
def VisitedInv (wf : nfa.WellFormed) (bvpos₀ bvpos : BVPos startPos) (visited visited' : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
@@ -386,7 +386,7 @@ theorem rfl (wf : nfa.WellFormed) (bvpos₀ bvpos : BVPos startPos) : VisitedInv
386386

387387
theorem preserves {bvpos' : BVPos startPos} {state : Fin nfa.nodes.size}
388388
(inv : VisitedInv wf bvpos₀ bvpos visited visited')
389-
(update : List (Nat × ValidPos s)) (path : Path nfa wf bvpos.current bvpos'.current state update) :
389+
(update : List (Nat × Pos s)) (path : Path nfa wf bvpos.current bvpos'.current state update) :
390390
VisitedInv wf bvpos₀ bvpos visited (visited'.set state bvpos'.index) := by
391391
intro state' bvpos'' le' hmem
392392
simp [visited'.get_set] at hmem
@@ -423,7 +423,7 @@ end
423423

424424
section
425425

426-
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s} {bvpos₀ bvpos : BVPos startPos} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
426+
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {bvpos₀ bvpos : BVPos startPos} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
427427

428428
def NotDoneInv (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
429429
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos),

0 commit comments

Comments
 (0)