Do not expose nfa.nodes.size (#161)

* Do not expose nfa.nodes.size

* Simpify proofs

Author: pandaman64

correctness/RegexCorrectness/Backtracker/Basic.lean

@@ -32,14 +32,14 @@ theorem capture_of_some_compile {s e pos update} (hres : captureNext (HistoryStr
   exact ⟨pos', pos'', groups, le, c, eqv⟩
 
 theorem ne_done_of_path_of_none {s nfa wf pos} (hres : captureNext (HistoryStrategy s) nfa wf pos = .none) :
-  ∀ (pos' pos'' : Pos s) (state : Fin nfa.nodes.size) (update : List (Nat × Pos s)),
+  ∀ (pos' pos'' : Pos s) (state : Fin nfa.size) (update : List (Nat × Pos s)),
     pos ≤ pos' →
     Path nfa wf pos' pos'' state update →
     nfa[state] ≠ .done := by
   dsimp [captureNext] at hres
 
   let bvpos : BVPos pos := ⟨pos, Pos.le_refl _⟩
-  let visited := BitMatrix.zero nfa.nodes.size (pos.remainingBytes + 1)
+  let visited := BitMatrix.zero nfa.size (pos.remainingBytes + 1)
 
   have h := go.ne_done_of_path_of_none hres (BVPos.le_refl _) go.Inv.zero captureNextAux.NotDoneInv.zero
 
@@ -55,7 +55,7 @@ theorem not_captures_of_none_compile {s e pos} (hres : captureNext (HistoryStrat
   intro c
   have ⟨update, _, path⟩ := NFA.path_of_captures_compile rfl c
 
-  let zero : Fin (NFA.compile e).nodes.size := ⟨0, NFA.lt_zero_size_compile rfl⟩
+  let zero : Fin (NFA.compile e).size := ⟨0, NFA.lt_zero_size_compile rfl⟩
   have hne := ne_done_of_path_of_none hres pos' pos'' zero update le (Path.of_nfaPath (path.liftBound (by decide)))
   have hn := (NFA.done_iff_zero_compile (e := e) rfl zero).mpr (by simp [zero])
   exact hne hn

correctness/RegexCorrectness/Backtracker/Compile.lean

@@ -8,15 +8,15 @@ open Regex.Data (BVPos)
 
 namespace Regex.Backtracker
 
-inductive Path {s : String} (nfa : NFA) (wf : nfa.WellFormed) (pos : Pos s) : Pos s → Fin nfa.nodes.size → List (Nat × Pos s) → Prop where
+inductive Path {s : String} (nfa : NFA) (wf : nfa.WellFormed) (pos : Pos s) : Pos s → Fin nfa.size → List (Nat × Pos s) → Prop where
   | init : Path nfa wf pos pos ⟨nfa.start, wf.start_lt⟩ []
-  | 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₂)
+  | more {i j : Fin nfa.size} {pos' pos'' update₁ update₂ update₃} (prev : Path nfa wf pos pos' i update₁) (step : nfa.Step 0 i pos' j pos'' update₂)
     (equpdate : update₃ = update₁ ++ List.ofOption update₂) :
     Path nfa wf pos pos'' j update₃
 
 namespace Path
 
-variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' pos'' : Pos s} {i j : Fin nfa.nodes.size}
+variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' pos'' : Pos s} {i j : Fin nfa.size}
   {update update₁ update₂ update₃ : List (Nat × Pos s)}
 
 theorem le (path : Path nfa wf pos pos' i update) :
@@ -43,7 +43,7 @@ theorem nfaPath_of_ne (path : Path nfa wf pos pos' i update) (ne : i.val ≠ nfa
   nfa.Path 0 nfa.start pos i pos' update := by
   simpa [ne] using eq_or_nfaPath path
 
-theorem concat_nfaPath {i j : Nat} (isLt : i < nfa.nodes.size)
+theorem concat_nfaPath {i j : Nat} (isLt : i < nfa.size)
   (path₁ : Path nfa wf pos pos' ⟨i, isLt⟩ update₁) (path₂ : nfa.Path 0 i pos' j pos'' update₂) (equpdate : update₃ = update₁ ++ update₂) :
   Path nfa wf pos pos'' ⟨j, path₂.lt_right wf⟩ update₃ := by
   induction path₂ generalizing update₁ with

correctness/RegexCorrectness/Backtracker/Path.lean

@@ -25,7 +25,7 @@ theorem materializeStack.nil : materializeStack [] = ([] : List (StackEntry (Buf
 theorem materializeStack.cons {entryH stackH} :
   materializeStack (entryH :: stackH) = (StackEntry.materialize entryH :: materializeStack stackH : List (StackEntry (BufferStrategy s bufferSize) nfa startPos)) := rfl
 
-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) :=
+def materializeResultAux (resultH : Option (List (Nat × Pos s)) × BitMatrix nfa.size (startPos.remainingBytes + 1)) : Option (Buffer s bufferSize) × BitMatrix nfa.size (startPos.remainingBytes + 1) :=
   ⟨resultH.1.map (materializeUpdates bufferSize), resultH.2⟩
 
 def materializeResult (resultH : Option (List (Nat × Pos s))) : Option (Buffer s bufferSize) :=

correctness/RegexCorrectness/Backtracker/Refinement.lean

@@ -47,7 +47,7 @@ end
 section
 
 variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s}
-  {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {update' visited'}
+  {visited : BitMatrix nfa.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {update' visited'}
 
 def StackInv (wf : nfa.WellFormed) (bvpos : BVPos startPos) (stack : List (StackEntry (HistoryStrategy s) nfa startPos)) : Prop :=
   ∀ entry ∈ stack, Path nfa wf bvpos.current entry.pos.current entry.state entry.update
@@ -137,7 +137,7 @@ end StackInv
 
 theorem path_done_of_some {bvpos} (hres : captureNextAux (HistoryStrategy s) nfa wf startPos visited stack = (.some update', visited'))
   (inv : StackInv wf bvpos stack) :
-  ∃ (state : Fin nfa.nodes.size) (bvpos' : BVPos startPos),
+  ∃ (state : Fin nfa.size) (bvpos' : BVPos startPos),
     nfa[state] = .done ∧ bvpos ≤ bvpos' ∧ Path nfa wf bvpos.current bvpos'.current state update' := by
   induction visited, stack using captureNextAux.induct' (HistoryStrategy s) nfa wf startPos with
   | base visited => simp [captureNextAux_base] at hres
@@ -157,10 +157,10 @@ end
 section
 
 variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s}
-  {bvpos₀ : BVPos startPos} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
+  {bvpos₀ : BVPos startPos} {visited : BitMatrix nfa.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
 
-def ClosureInv (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (stack : List (StackEntry (HistoryStrategy s) nfa startPos)) : Prop :=
-  ∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
+def ClosureInv (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.size (startPos.remainingBytes + 1)) (stack : List (StackEntry (HistoryStrategy s) nfa startPos)) : Prop :=
+  ∀ (state : Fin nfa.size) (bvpos : BVPos startPos) (state' : Fin nfa.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
     bvpos₀ ≤ bvpos →
     visited.get state bvpos.index →
     nfa.Step 0 state bvpos.current state' bvpos'.current update →
@@ -171,7 +171,7 @@ namespace ClosureInv
 -- Preservation of the non-visited cases
 theorem preserves' {entry stack'} (inv : ClosureInv bvpos₀ visited (entry :: stack))
   (nextEntries : List (StackEntry (HistoryStrategy s) nfa startPos)) (hstack : stack' = nextEntries ++ stack)
-  (hnext : ∀ (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
+  (hnext : ∀ (state' : Fin nfa.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
     nfa.Step 0 entry.state entry.pos.current state' bvpos'.current update →
     ∃ entry' ∈ nextEntries, entry'.state = state' ∧ entry'.pos = bvpos') :
   ClosureInv bvpos₀ (visited.set entry.state entry.pos.index) stack' := by
@@ -310,29 +310,29 @@ theorem step_closure {bvpos₀ bvpos : BVPos startPos} {result} (hres : captureN
     simp [captureNextAux_next mem hn] at hres
     exact ih hres (cinv.preserves wf hn) stinv.preserves
 
-def StepClosure (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
-  ∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
+def StepClosure (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.size (startPos.remainingBytes + 1)) : Prop :=
+  ∀ (state : Fin nfa.size) (bvpos : BVPos startPos) (state' : Fin nfa.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
     bvpos₀ ≤ bvpos →
     visited.get state bvpos.index →
     nfa.Step 0 state bvpos.current state' bvpos'.current update →
     visited.get state' bvpos'.index
 
-def PathClosure (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
-  ∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : List (Nat × Pos s)),
+def PathClosure (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.size (startPos.remainingBytes + 1)) : Prop :=
+  ∀ (state : Fin nfa.size) (bvpos : BVPos startPos) (state' : Fin nfa.size) (bvpos' : BVPos startPos) (update : List (Nat × Pos s)),
     bvpos₀ ≤ bvpos →
     visited.get state bvpos.index →
     nfa.Path 0 state bvpos.current state' bvpos'.current update →
     visited.get state' bvpos'.index
 
 namespace PathClosure
 
-theorem zero : PathClosure bvpos₀ (BitMatrix.zero nfa.nodes.size (startPos.remainingBytes + 1)) := by
+theorem zero : PathClosure bvpos₀ (BitMatrix.zero nfa.size (startPos.remainingBytes + 1)) := by
   intro state bvpos state' bvpos' update reaches hmem path
   simp at hmem
 
 theorem of_step_closure {bvpos₀ : BVPos startPos} (wf : nfa.WellFormed) (h : StepClosure bvpos₀ visited) : PathClosure bvpos₀ visited := by
   let motive (i : Nat) (pos : Pos s) : Prop :=
-    ∃ (isLt : i < nfa.nodes.size) (bvpos : BVPos startPos), bvpos₀ ≤ bvpos ∧ pos = bvpos.current ∧ visited.get ⟨i, isLt⟩ bvpos.index
+    ∃ (isLt : i < nfa.size) (bvpos : BVPos startPos), bvpos₀ ≤ bvpos ∧ pos = bvpos.current ∧ visited.get ⟨i, isLt⟩ bvpos.index
   have cls i pos j pos' update (base : motive i pos) (step : nfa.Step 0 i pos j pos' update) : motive j pos' := by
     have ⟨_, bvpos, le, hbvpos, hmem⟩ := base
 
@@ -370,10 +370,10 @@ end
 section
 
 variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {bvpos₀ bvpos : BVPos startPos}
-  {visited visited' : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
+  {visited visited' : BitMatrix nfa.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
 
-def VisitedInv (wf : nfa.WellFormed) (bvpos₀ bvpos : BVPos startPos) (visited visited' : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
-  ∀ (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos),
+def VisitedInv (wf : nfa.WellFormed) (bvpos₀ bvpos : BVPos startPos) (visited visited' : BitMatrix nfa.size (startPos.remainingBytes + 1)) : Prop :=
+  ∀ (state' : Fin nfa.size) (bvpos' : BVPos startPos),
     bvpos₀ ≤ bvpos' →
     visited'.get state' bvpos'.index →
     visited.get state' bvpos'.index ∨ ∃ update, Path nfa wf bvpos.current bvpos'.current state' update
@@ -384,7 +384,7 @@ theorem rfl (wf : nfa.WellFormed) (bvpos₀ bvpos : BVPos startPos) : VisitedInv
   intro state bvpos _ hmem
   exact .inl hmem
 
-theorem preserves {bvpos' : BVPos startPos} {state : Fin nfa.nodes.size}
+theorem preserves {bvpos' : BVPos startPos} {state : Fin nfa.size}
   (inv : VisitedInv wf bvpos₀ bvpos visited visited')
   (update : List (Nat × Pos s)) (path : Path nfa wf bvpos.current bvpos'.current state update) :
   VisitedInv wf bvpos₀ bvpos visited (visited'.set state bvpos'.index) := by
@@ -423,16 +423,16 @@ end
 
 section
 
-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)}
+variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {bvpos₀ bvpos : BVPos startPos} {visited : BitMatrix nfa.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
 
-def NotDoneInv (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
-  ∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos),
+def NotDoneInv (visited : BitMatrix nfa.size (startPos.remainingBytes + 1)) : Prop :=
+  ∀ (state : Fin nfa.size) (bvpos : BVPos startPos),
     visited.get state bvpos.index →
     nfa[state] ≠ .done
 
 namespace NotDoneInv
 
-theorem zero : NotDoneInv (BitMatrix.zero nfa.nodes.size (startPos.remainingBytes + 1)) := by
+theorem zero : NotDoneInv (BitMatrix.zero nfa.size (startPos.remainingBytes + 1)) := by
   intro state bvpos hmem
   simp at hmem
 

correctness/RegexCorrectness/Backtracker/Traversal/Invariants.lean

@@ -10,7 +10,7 @@ namespace Regex.Backtracker
 namespace captureNextAux
 
 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)}
+  {visited : BitMatrix nfa.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
 
 theorem mem_or_path_of_mem_of_none {result} (hres : captureNextAux (HistoryStrategy s) nfa wf startPos visited [⟨(HistoryStrategy s).empty, ⟨nfa.start, wf.start_lt⟩, bvpos⟩] = result)
   (isNone : result.1 = .none) :
@@ -27,7 +27,7 @@ theorem PathClosure.preserves {result} (hres : captureNextAux (HistoryStrategy s
 
 theorem mem_of_path_of_none {result} (hres : captureNextAux (HistoryStrategy s) nfa wf startPos visited [⟨(HistoryStrategy s).empty, ⟨nfa.start, wf.start_lt⟩, bvpos⟩] = result)
   (isNone : result.1 = .none) (le₀ : bvpos₀ ≤ bvpos) (cls : PathClosure bvpos₀ visited)
-  (bvpos' : BVPos startPos) (state : Fin nfa.nodes.size) (update : List (Nat × Pos s)) (path : Path nfa wf bvpos.current bvpos'.current state update) :
+  (bvpos' : BVPos startPos) (state : Fin nfa.size) (update : List (Nat × Pos s)) (path : Path nfa wf bvpos.current bvpos'.current state update) :
   result.2.get state bvpos'.index := by
   have mem_start : result.2.get ⟨nfa.start, wf.start_lt⟩ bvpos.index := hres ▸ mem_stack_top ⟨(HistoryStrategy s).empty, ⟨nfa.start, wf.start_lt⟩, bvpos⟩ [] rfl
   match path.eq_or_nfaPath with
@@ -40,7 +40,7 @@ theorem mem_of_path_of_none {result} (hres : captureNextAux (HistoryStrategy s)
 
 theorem mem_iff_mem_or_path_of_none {result} (hres : captureNextAux (HistoryStrategy s) nfa wf startPos visited [⟨(HistoryStrategy s).empty, ⟨nfa.start, wf.start_lt⟩, bvpos⟩] = result)
   (isNone : result.1 = .none) (le₀ : bvpos₀ ≤ bvpos) (cls : PathClosure bvpos₀ visited)
-  (bvpos' : BVPos startPos) (state : Fin nfa.nodes.size) (le₀' : bvpos₀ ≤ bvpos') :
+  (bvpos' : BVPos startPos) (state : Fin nfa.size) (le₀' : bvpos₀ ≤ bvpos') :
   result.2.get state bvpos'.index ↔ visited.get state bvpos'.index ∨ ∃ update, Path nfa wf bvpos.current bvpos'.current state update := by
   apply Iff.intro
   . intro mem
@@ -56,27 +56,27 @@ namespace captureNext.go
 
 open captureNextAux (StackInv NotDoneInv PathClosure)
 
-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)}
+variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {bvpos₀ bvpos : BVPos startPos} {visited : BitMatrix nfa.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
 
-structure Inv (wf : nfa.WellFormed) (bvpos₀ bvpos : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop where
+structure Inv (wf : nfa.WellFormed) (bvpos₀ bvpos : BVPos startPos) (visited : BitMatrix nfa.size (startPos.remainingBytes + 1)) : Prop where
   closure : PathClosure bvpos₀ visited
-  mem_iff_path : ∀ (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos),
+  mem_iff_path : ∀ (state' : Fin nfa.size) (bvpos' : BVPos startPos),
     bvpos₀ ≤ bvpos' →
     (visited.get state' bvpos'.index ↔
       ∃ (bvposPrev : BVPos startPos) (update : List (Nat × Pos s)),
         bvpos₀ ≤ bvposPrev ∧ bvposPrev < bvpos ∧ Path nfa wf bvposPrev.current bvpos'.current state' update)
 
 namespace Inv
 
-theorem zero : Inv wf bvpos₀ bvpos₀ (BitMatrix.zero nfa.nodes.size (startPos.remainingBytes + 1)) := by
+theorem zero : Inv wf bvpos₀ bvpos₀ (BitMatrix.zero nfa.size (startPos.remainingBytes + 1)) := by
   refine ⟨PathClosure.zero, ?_⟩
   simp only [BitMatrix.get_zero, Bool.false_eq_true, exists_and_left, false_iff, not_exists, not_and]
   intro _ _ _ bvpos le lt
   exact (BVPos.not_lt_of_le le lt).elim
 
 theorem mem_iff_of_aux_none {result} (haux : captureNextAux (HistoryStrategy s) nfa wf startPos visited [⟨(HistoryStrategy s).empty, ⟨nfa.start, wf.start_lt⟩, bvpos⟩] = result)
   (isNone : result.1 = .none) (le₀ : bvpos₀ ≤ bvpos) (inv : Inv wf bvpos₀ bvpos visited)
-  (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (le₀' : bvpos₀ ≤ bvpos') :
+  (state' : Fin nfa.size) (bvpos' : BVPos startPos) (le₀' : bvpos₀ ≤ bvpos') :
   result.2.get state' bvpos'.index ↔
     (∃ (bvposPrev : BVPos startPos) (update : List (Nat × Pos s)), bvpos₀ ≤ bvposPrev ∧ bvposPrev < bvpos ∧ Path nfa wf bvposPrev.current bvpos'.current state' update) ∨
       ∃ (update : List (Nat × Pos s)), Path nfa wf bvpos.current bvpos'.current state' update := by
@@ -95,7 +95,7 @@ theorem preservesAux {result} (haux : captureNextAux (HistoryStrategy s) nfa wf
 theorem mem_iff_path_of_aux_none_endBVPos {result}
   (haux : captureNextAux (HistoryStrategy s) nfa wf startPos visited [⟨(HistoryStrategy s).empty, ⟨nfa.start, wf.start_lt⟩, s.endBVPos startPos⟩] = result)
   (isNone : result.1 = .none) (inv : Inv wf bvpos₀ (s.endBVPos startPos) visited)
-  (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (le₀' : bvpos₀ ≤ bvpos') :
+  (state' : Fin nfa.size) (bvpos' : BVPos startPos) (le₀' : bvpos₀ ≤ bvpos') :
   result.2.get state' bvpos'.index ↔
     ∃ (bvposPrev : BVPos startPos) (update : List (Nat × Pos s)), bvpos₀ ≤ bvposPrev ∧ Path nfa wf bvposPrev.current bvpos'.current state' update := by
   rw [inv.mem_iff_of_aux_none haux isNone bvpos₀.le_endBVPos state' bvpos' le₀']
@@ -114,7 +114,7 @@ end Inv
 theorem ne_done_of_path_of_none (hres : go (HistoryStrategy s) nfa wf startPos bvpos visited = .none)
   (le₀ : bvpos₀ ≤ bvpos)
   (inv : Inv wf bvpos₀ bvpos visited) (ndinv : NotDoneInv visited) :
-  ∀ (bvpos' bvpos'' : BVPos startPos) (state : Fin nfa.nodes.size) (update : List (Nat × Pos s)),
+  ∀ (bvpos' bvpos'' : BVPos startPos) (state : Fin nfa.size) (update : List (Nat × Pos s)),
     bvpos₀ ≤ bvpos' →
     Path nfa wf bvpos'.current bvpos''.current state update →
     nfa[state] ≠ .done := by
@@ -140,7 +140,7 @@ theorem ne_done_of_path_of_none (hres : go (HistoryStrategy s) nfa wf startPos b
     exact ndinv' state bvpos'' mem hn
 
 theorem path_done_of_some {update} (hres : go (HistoryStrategy s) nfa wf startPos bvpos visited = .some update) :
-  ∃ (state : Fin nfa.nodes.size) (bvpos' bvpos'' : BVPos startPos),
+  ∃ (state : Fin nfa.size) (bvpos' bvpos'' : BVPos startPos),
     nfa[state] = .done ∧ bvpos ≤ bvpos' ∧ Path nfa wf bvpos'.current bvpos''.current state update := by
   induction bvpos, visited using go.induct' (HistoryStrategy s) nfa wf startPos with
   | found bvpos visited update visited' haux =>

correctness/RegexCorrectness/Backtracker/Traversal/Lemmas.lean

@@ -62,14 +62,14 @@ def nfaToSubstance (regex : Regex) : String := Id.run do
 Let TRUE := True()
 Let FALSE := False()
 "###
-  for i in [0:regex.nfa.nodes.size] do
+  for i in [0:regex.nfa.size] do
     sub := sub ++ createNode i
     if i > 0 then sub := sub ++ relateSuccessorNodes i
 
   sub := sub ++ declareStartNode regex.nfa.start
 
-  for h : i in [0:regex.nfa.nodes.size] do
-    let node := regex.nfa.nodes[i]
+  for h : i in [0:regex.nfa.size] do
+    let node := regex.nfa[i]
     match node with
     | .done =>
         sub := sub ++ labelNode i "done"