Lemmas

Proof that Compiler.Code.compile gives an array with the Compiler.nextOfLt property

• c_compile_spec: main result

def Compiler.Lemmas.tacticInst_mvar : Lean.ParserDescr

instantiate mvar, mspec with a precondition like fun s => s = states ∧ P gives a uninstantiated mvar

Equations

• Compiler.Lemmas.tacticInst_mvar = Lean.ParserDescr.node `Compiler.Lemmas.tacticInst_mvar 1024 (Lean.ParserDescr.nonReservedSymbol "inst_mvar" false)

theorem Compiler.Lemmas.lift_StackM_to_PatchM_spec {σ α : Type} {n : σ} {ε : Type} (v : StateT σ Id α) {P : σ → Prop} (Q : σ → α → σ → Prop) (hspec : ⦃fun (s : σ) => ⌜s = n ∧ P n⌝⦄ v ⦃(fun (a : α) (s : σ) => ⌜Q n a s⌝, ())⦄) : ⦃fun (s : σ) => ⌜s = n ∧ P n⌝⦄ liftM v ⦃(fun (a : α) (s : σ) => ⌜Q n a s⌝, fun (x : ε) => ⌜True⌝, ())⦄

def Compiler.Lemmas.coe_spec_StackM_to_PatchM {σ α ε : Type} {v : StateT σ Id α} {P : σ → Prop} {Q : α → σ → Prop} (hspec : ⦃fun (s : σ) => ⌜P s⌝⦄ v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, ())⦄) : ⦃fun (s : σ) => ⌜P s⌝⦄ liftM v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, fun (x : ε) (x : σ) => ⌜True⌝, ())⦄

Equations

• ⋯ = hspec

instance Compiler.Lemmas.instCoeTripleStateTIdCurryEStateMLiftM_regex {σ α ε : Type} {v : StateT σ Id α} {P : σ → Prop} {Q : α → σ → Prop} : Coe (⦃fun (s : σ) => ⌜P s⌝⦄ v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, ())⦄) (⦃fun (s : σ) => ⌜P s⌝⦄ liftM v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, fun (x : ε) (x : σ) => ⌜True⌝, ())⦄)

Equations

• Compiler.Lemmas.instCoeTripleStateTIdCurryEStateMLiftM_regex = { coe := ⋯ }

def Compiler.Lemmas.coe_spec_PatchM_to_CompilerM {ε σ₁ α σ₂ : Type} {v : EStateM ε σ₁ α} {P : σ₁ → Prop} {Q : α → σ₁ → Prop} (hspec : ⦃fun (s : σ₁) => ⌜P s⌝⦄ v ⦃(fun (a : α) (s : σ₁) => ⌜Q a s⌝, fun (x : ε) => ⌜True⌝, ())⦄) : ⦃fun (s : σ₁ × σ₂) => ⌜P s.fst⌝⦄ liftM v ⦃(fun (r : α) (s : σ₁ × σ₂) => ⌜Q r s.fst⌝, fun (x : ε) (x : σ₁ × σ₂) => ⌜True⌝, ())⦄

Equations

• ⋯ = ⋯

instance Compiler.Lemmas.instCoeTripleEStateMCurryProdLiftMFst_regex {ε σ₁ α σ₂ : Type} {v : EStateM ε σ₁ α} {P : σ₁ → Prop} {Q : α → σ₁ → Prop} : Coe (⦃fun (s : σ₁) => ⌜P s⌝⦄ v ⦃(fun (a : α) (s : σ₁) => ⌜Q a s⌝, fun (x : ε) => ⌜True⌝, ())⦄) (⦃fun (s : σ₁ × σ₂) => ⌜P s.fst⌝⦄ liftM v ⦃(fun (r : α) (s : σ₁ × σ₂) => ⌜Q r s.fst⌝, fun (x : ε) => ⌜True⌝, ())⦄)

Equations

• Compiler.Lemmas.instCoeTripleEStateMCurryProdLiftMFst_regex = { coe := ⋯ }

def Compiler.Lemmas.coe_spec_StackM_to_CompilerM {σ₁ α ε σ₂ : Type} {v : StateT σ₁ Id α} {P : σ₁ → Prop} {Q : α → σ₁ → Prop} (hspec : ⦃fun (s : σ₁) => ⌜P s⌝⦄ v ⦃(fun (a : α) (s : σ₁) => ⌜Q a s⌝, ())⦄) : ⦃fun (s : σ₁ × σ₂) => ⌜P s.fst⌝⦄ liftM v ⦃(fun (r : α) (s : σ₁ × σ₂) => ⌜Q r s.fst⌝, fun (x : ε) (x : σ₁ × σ₂) => ⌜True⌝, ())⦄

Equations

• ⋯ = ⋯

instance Compiler.Lemmas.instCoeTripleStateTIdCurryEStateMProdLiftMFst_regex {σ₁ α ε σ₂ : Type} {v : StateT σ₁ Id α} {P : σ₁ → Prop} {Q : α → σ₁ → Prop} : Coe (⦃fun (s : σ₁) => ⌜P s⌝⦄ v ⦃(fun (a : α) (s : σ₁) => ⌜Q a s⌝, ())⦄) (⦃fun (s : σ₁ × σ₂) => ⌜P s.fst⌝⦄ liftM v ⦃(fun (r : α) (s : σ₁ × σ₂) => ⌜Q r s.fst⌝, fun (x : ε) (x : σ₁ × σ₂) => ⌜True⌝, ())⦄)

Equations

• Compiler.Lemmas.instCoeTripleStateTIdCurryEStateMProdLiftMFst_regex = { coe := ⋯ }

def Compiler.Lemmas.tRefLt (t : ThompsonRef) (r : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.tRefLt t r = (t.start < r.size ∧ t.end < r.size)

def Compiler.Lemmas.statesNextOfLeLt (prevs s : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.statesNextOfLeLt prevs s = (prevs.size ≤ s.size ∧ Compiler.nextOfLt s)

def Compiler.Lemmas.stateIdNextOfLt (prevs : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.stateIdNextOfLt prevs sid s = (prevs.size < s.size ∧ sid < s.size ∧ Compiler.nextOfLt s)

def Compiler.Lemmas.stateIdNextOfLeLt (prevs : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.stateIdNextOfLeLt prevs sid s = (prevs.size ≤ s.size ∧ sid < s.size ∧ Compiler.nextOfLt s)

def Compiler.Lemmas.stateIdNextOfEqLt (prevs : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.stateIdNextOfEqLt prevs sid s = (prevs.size = s.size ∧ sid < s.size ∧ Compiler.nextOfLt s)

def Compiler.Lemmas.tRefNextOfLt (prevs : Array NFA.Unchecked.State) (t : ThompsonRef) (s : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.tRefNextOfLt prevs t s = (prevs.size < s.size ∧ Compiler.Lemmas.tRefLt t s ∧ Compiler.nextOfLt s)

def Compiler.Lemmas.tRefNextOfLeLt (prevs : Array NFA.Unchecked.State) (t : ThompsonRef) (s : Array NFA.Unchecked.State) : Prop

Equations

• Compiler.Lemmas.tRefNextOfLeLt prevs t s = (prevs.size ≤ s.size ∧ Compiler.Lemmas.tRefLt t s ∧ Compiler.nextOfLt s)

theorem Compiler.Lemmas.lift_CompilerM_bind_pure {ε σ α : Type} [MonadLiftT (EStateM ε σ) Code.CompilerM] (x : EStateM ε σ α) : liftM x >>= EStateM.pure = liftM x

theorem Compiler.Lemmas.pure_of_imp_spec {α σ ε : Type} {x : α} {P1 P2 : α → σ → Prop} (h : ∀ (a : α) (s : σ), P1 a s → P2 a s) : ⦃fun (s : σ) => ⌜P1 x s⌝⦄ EStateM.pure x ⦃(fun (r : α) (s : σ) => ⌜P2 r s⌝, fun (x : ε) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.patch_lift_spec («from» : NFA.Unchecked.StateID) {to : NFA.Unchecked.StateID} (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ «from» < states.size ∧ to < states.size⌝⦄ liftM (Code.patch «from» to) ⦃(fun (x : Unit) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfEqLt states to s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.push_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ sid.nextOf ≤ states.size⌝⦄ Code.push sid ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.push_lift_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ sid.nextOf ≤ states.size⌝⦄ liftM (Code.push sid) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.push'_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ sid.nextOf ≤ states.size⌝⦄ Code.push' sid ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_match_spec (pattern_id : NFA.PatternID) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_match pattern_id ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_match_lift_spec (pattern_id : NFA.PatternID) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM (Code.add_match pattern_id) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.add_union_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_union ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_union_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM Code.add_union ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.add_union_lift'_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM Code.add_union ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.add_union_reverse_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_union_reverse ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_union_reverse_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM Code.add_union_reverse ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.add_backrefence_spec (case_insensitive : Bool) (b : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_backrefence case_insensitive b ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_backrefence_lift_spec (case_insensitive : Bool) (b : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM (Code.add_backrefence case_insensitive b) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_range_spec (start «end» : UInt32) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_range start «end» ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_empty_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_empty_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM Code.add_empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.add_empty_lift'_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM Code.add_empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.add_fail_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_fail ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_fail_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM Code.add_fail ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.eat_next_of_le {mode : NFA.Unchecked.EatMode} (states : Array NFA.Unchecked.State) (h : mode.nextOf < states.size) : (NFA.Unchecked.State.Eat mode 0).nextOf ≤ states.size

theorem Compiler.Lemmas.add_eat_spec (mode : NFA.Unchecked.EatMode) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ mode.nextOf < states.size⌝⦄ Code.add_eat mode ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_change_state_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_change_state ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_change_state_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM Code.add_change_state ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.add_remove_state_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_remove_state ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_next_char_spec (offset : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_next_char offset ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.add_next_char_lift_spec (offset : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM (Code.add_next_char offset) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_empty_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_empty ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.c_empty_lift_spec (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM Code.c_empty ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[simp]

theorem Compiler.Lemmas.transition_lt_of_lt (states : Array NFA.Unchecked.State) (trans : Array NFA.Unchecked.Transition) (h : ∀ (i : Nat) (x : i < trans.size), trans[i].next ≤ states.size) : (NFA.Unchecked.State.SparseTransitions trans).nextOf ≤ states.size

theorem Compiler.Lemmas.add_sparse_spec (trans : Array NFA.Unchecked.Transition) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ ∀ (i : Nat) (x : i < trans.size), trans[i].next ≤ states.size⌝⦄ Code.add_sparse trans ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.c_unicode_class_spec (cls : Syntax.ClassUnicode) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_unicode_class cls ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.c_unicode_class_lift_spec (cls : Syntax.ClassUnicode) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM (Code.c_unicode_class cls) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_literal_spec (c : Char) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_literal c ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.c_literal_lift_spec (c : Char) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM (Code.c_literal c) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_look_spec (look : Syntax.Look) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_look look ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.c_look_lift_spec (look : Syntax.Look) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM (Code.c_look look) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_possessive_spec (tref : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tref.start < states.size ∧ tref.end < states.size ∧ nextOfLt states⌝⦄ Code.c_possessive tref ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_possessive_lift_spec (tref : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ tref.start < states.size ∧ tref.end < states.size ∧ nextOfLt states⌝⦄ liftM (Code.c_possessive tref) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.tref_le_of_lt_spec (states : Array NFA.Unchecked.State) (tref : ThompsonRef) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states tref s.fst⌝⦄ EStateM.pure tref ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_possessive_le_lift_spec (tref : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ tref.start < states.size ∧ tref.end < states.size ∧ nextOfLt states⌝⦄ liftM (Code.c_possessive tref) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_cap'_spec (role : NFA.Capture.Role) (pattern_id slot : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_cap' role pattern_id slot ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

theorem Compiler.Lemmas.c_cap'_lift_spec (role : NFA.Capture.Role) (pattern_id slot : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM (Code.c_cap' role pattern_id slot) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_back_ref_spec (case_insensitive : Bool) (n : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_back_ref case_insensitive n ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_back_ref_lift_spec (case_insensitive : Bool) (n : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM (Code.c_back_ref case_insensitive n) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_lookaround_PositiveLookahead_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_lookaround_PositiveLookahead compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_lookaround_PositiveLookahead_lift_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ liftM (Code.c_lookaround_PositiveLookahead compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_lookaround_NegativeLookahead_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_lookaround_NegativeLookahead compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_lookaround_NegativeLookahead_lift_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ liftM (Code.c_lookaround_NegativeLookahead compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_lookaround_PositiveLookbehind_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_lookaround_PositiveLookbehind next_char compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_lookaround_PositiveLookbehind_lift_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ liftM (Code.c_lookaround_PositiveLookbehind next_char compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_lookaround_NegativeLookbehind_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_lookaround_NegativeLookbehind next_char compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_lookaround_NegativeLookbehind_lift_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ liftM (Code.c_lookaround_NegativeLookbehind next_char compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_repetition_0_some_1_false_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_repetition_0_some_1_false union compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_repetition_0_some_1_false_lift_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ liftM (Code.c_repetition_0_some_1_false union compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_repetition_0_some_1_true_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_repetition_0_some_1_true union compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_repetition_0_some_1_true_lift_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ liftM (Code.c_repetition_0_some_1_true union compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_repetition_0_none_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_repetition_0_none union compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_repetition_0_none_lift_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ liftM (Code.c_repetition_0_none union compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.greedy_union_spec (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ if greedy = true then liftM Code.add_union else liftM Code.add_union_reverse ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_0_pre_spec (compiled : ThompsonRef) (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_at_least_0_pre compiled greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_0_pre_lift_spec (compiled : ThompsonRef) (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ liftM (Code.c_at_least_0_pre compiled greedy) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_set_spec (possible_empty_capture_group : Option Nat) (greedy : Bool) (states : Array NFA.Unchecked.State) {groups : Array Nat} : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ s.snd = groups⌝⦄ Code.c_at_least_set possible_empty_capture_group greedy ⦃(fun (x : Unit) (s : Array NFA.Unchecked.State × Array Nat) => ⌜states = s.fst ∧ groups.size ≤ s.snd.size⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_0_post_spec (compiled : ThompsonRef) (plus : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ plus < states.size ∧ compiled.start < states.size ∧ nextOfLt states⌝⦄ Code.c_at_least_0_post compiled plus greedy possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_0_post_lift_spec (compiled : ThompsonRef) (plus : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ plus < states.size ∧ compiled.start < states.size ∧ nextOfLt states⌝⦄ liftM (Code.c_at_least_0_post compiled plus greedy possessive) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_0_spec (compiled : ThompsonRef) (possible_empty_capture_group : Option Nat) (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_at_least_0 compiled possible_empty_capture_group greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_1_pre_spec (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_at_least_1_pre greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_1_pre_lift_spec (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM (Code.c_at_least_1_pre greedy) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_1_post_spec (compiled : ThompsonRef) (union : NFA.Unchecked.StateID) (possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_at_least_1_post compiled union possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_1_post_lift_spec (compiled : ThompsonRef) (union : NFA.Unchecked.StateID) (possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ liftM (Code.c_at_least_1_post compiled union possessive) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_1_spec (possible_empty_capture_group : Option Nat) (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ Code.c_at_least_1 possible_empty_capture_group greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_2_spec («prefix» last : ThompsonRef) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt «prefix» states ∧ tRefLt last states ∧ nextOfLt states⌝⦄ Code.c_at_least_2 «prefix» last greedy possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_at_least_2_lift_spec («prefix» last : ThompsonRef) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ tRefLt «prefix» states ∧ tRefLt last states ∧ nextOfLt states⌝⦄ liftM (Code.c_at_least_2 «prefix» last greedy possessive) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_bounded.fold.patch.pre_spec (compiled : ThompsonRef) (prev_end : NFA.Unchecked.StateID) (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ prev_end < states.size ∧ nextOfLt states⌝⦄ Code.c_bounded.fold.patch.pre compiled prev_end greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_bounded.fold.patch.possessive_spec (compiled : ThompsonRef) (empty : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ empty < states.size ∧ nextOfLt states⌝⦄ Code.c_bounded.fold.patch.possessive compiled empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_bounded.fold.patch.post_spec (compiled : ThompsonRef) (union empty : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ compiled.end < states.size ∧ union < states.size ∧ empty < states.size ∧ nextOfLt states⌝⦄ Code.c_bounded.fold.patch.post compiled union empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLeLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_bounded.fold.patch_spec (compiled : ThompsonRef) (prev_end empty : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ prev_end < states.size ∧ empty < states.size ∧ nextOfLt states⌝⦄ Code.c_bounded.fold.patch compiled prev_end empty greedy possessive ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_bounded.fold.patch_lift_spec (compiled : ThompsonRef) (prev_end empty : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ tRefLt compiled states ∧ prev_end < states.size ∧ empty < states.size ∧ nextOfLt states⌝⦄ liftM (Code.c_bounded.fold.patch compiled prev_end empty greedy possessive) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_alt_iter_step_spec (first second : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt first states ∧ tRefLt second states ∧ nextOfLt states⌝⦄ Code.c_alt_iter_step first second ⦃(fun (r : NFA.Unchecked.StateID × NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states { start := r.fst, «end» := r.snd } s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_alt_iter_step_lift_spec (first second : ThompsonRef) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ tRefLt first states ∧ tRefLt second states ∧ nextOfLt states⌝⦄ liftM (Code.c_alt_iter_step first second) ⦃(fun (r : NFA.Unchecked.StateID × NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states { start := r.fst, «end» := r.snd } s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_rep_pre_spec (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_rep_pre greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_rep_pre_lift_spec (greedy : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ liftM (Code.c_rep_pre greedy) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_concat_fold_spec (tail : Array Syntax.Hir) (sid : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ sid < states.size ∧ nextOfLt states⌝⦄ Code.c_concat.fold tail sid ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_concat_spec (hirs : Array Syntax.Hir) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ Code.c_concat hirs ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_alt_iter_fold_spec (hirs : Array Syntax.Hir) (union «end» : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ union < states.size ∧ «end» < states.size ∧ nextOfLt states⌝⦄ Code.c_alt_iter.fold hirs union «end» ⦃(fun (x : Unit) (s : Array NFA.Unchecked.State × Array Nat) => ⌜statesNextOfLeLt states s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_alt_iter_spec (hirs : Array Syntax.Hir) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ Code.c_alt_iter hirs ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_exactly_fold_spec (hir : Syntax.Hir) (n : Nat) («end» : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ «end» < states.size ∧ nextOfLt states⌝⦄ Code.c_exactly.fold hir n «end» ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_exactly_spec (hir : Syntax.Hir) (n : Nat) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ Code.c_exactly hir n ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_at_least_spec (hir : Syntax.Hir) (n : Nat) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ Code.c_at_least hir n greedy possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_bounded_fold_spec (hir : Syntax.Hir) (n : Nat) («prefix» : ThompsonRef) (empty : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ tRefLt «prefix» states ∧ empty < states.size ∧ nextOfLt states⌝⦄ Code.c_bounded.fold hir n «prefix» empty greedy possessive ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array Nat) => ⌜stateIdNextOfLeLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_bounded_spec (hir : Syntax.Hir) (min max : Nat) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ Code.c_bounded hir min max greedy possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_lookaround_spec (look : Syntax.Lookaround) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ Code.c_lookaround look ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_repetition_spec (rep : Syntax.Repetition) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ Code.c_repetition rep ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_cap_spec (hir : Syntax.Capture) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ Code.c_cap hir ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

@[irreducible]

theorem Compiler.Lemmas.c_spec (hir : Syntax.Hir) (states : Array NFA.Unchecked.State) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst = states ∧ nextOfLt states⌝⦄ Code.c hir ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefNextOfLt states r s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_init_spec (anchored : Bool) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst.size = 0⌝⦄ Code.init anchored ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array Nat) => ⌜tRefLt r s.fst ∧ nextOfLt s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.c_compile_spec (anchored : Bool) (hir : Syntax.Hir) : ⦃fun (s : Array NFA.Unchecked.State × Array Nat) => ⌜s.fst.size = 0⌝⦄ Code.compile anchored hir ⦃(fun (x : Unit) (s : Array NFA.Unchecked.State × Array Nat) => ⌜nextOfLt s.fst⌝, fun (x : String) => ⌜True⌝, ())⦄

theorem Compiler.Lemmas.compile_nextOf_lt {states : Array NFA.Unchecked.State} {groups : Array Nat} {anchored : Bool} {expr : Syntax.Hir} (h : Code.compile anchored expr (#[], #[]) = EStateM.Result.ok () (states, groups)) : nextOfLt states