Documentation

Regex.Compiler.Lemmas

Lemmas #

Proof that Compiler.Code.compile gives an array with the Compiler.NextOfLt and NFA.Capture.valid property

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

Equations
Instances For

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

    Equations
    Instances For
      theorem Compiler.Lemmas.lift_StackT_to_EStateM_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_StackT_to_EStateM {σ α ε : 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
      Instances For
        instance Compiler.Lemmas.instCoeTripleStateTIdPureEStateMLiftM_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
        Equations
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              theorem Compiler.Lemmas.cValid_of_empty (captures : Array NFA.Capture) (h : captures.size = 0) :
              cValid captures
              @[simp]
              theorem Compiler.Lemmas.cMemAndValid_of_cValid_of_eq (captures s : Array NFA.Capture) :
              s = captures cValid capturescMemAndValid captures s
              @[simp]
              theorem Compiler.Lemmas.cMemAndValid_of_push_of_role_start (captures : Array NFA.Capture) (capture : NFA.Capture) (hr : capture.role = NFA.Capture.Role.Start) (hc : cValid captures) :
              cMemAndValid captures (captures.push capture)
              theorem Compiler.Lemmas.cMemAndValid_of_push_of_role_end (captures : Array NFA.Capture) (capture : NFA.Capture) (hc : cValid captures) (h : (c : NFA.Capture), c captures c.role = NFA.Capture.Role.Start c.group = capture.group) :
              cMemAndValid captures (captures.push capture)
              theorem Compiler.Lemmas.pure_of_imp_spec {α σ ε : Type} {x : α} {P1 P2 : ασProp} (h : ∀ (a : α) (s : σ), P1 a sP2 a s) :
              fun (s : σ) => P1 x s EStateM.pure x (fun (r : α) (s : σ) => P2 r s, fun (x : ε) => True, ())
              @[simp]
              theorem Compiler.Lemmas.c_back_ref_spec (case_insensitive : Bool) (n : Nat) (states : Array NFA.Unchecked.State) :
              theorem Compiler.Lemmas.c_back_ref_lift_spec (case_insensitive : Bool) (n : Nat) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :
              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 NFA.Capture × Array Nat) => s.fst = states s.snd.snd = groups Code.c_at_least_set possible_empty_capture_group greedy (fun (x : Unit) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => states = s.fst groups.size s.snd.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) (captures : Array NFA.Capture) :
              fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => (s.fst = states plus < states.size compiled.start < states.size NextOfLt states) s.snd.fst = captures cValid captures liftM (Code.c_at_least_0_post compiled plus greedy possessive) (fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => tRefNextOfLeLt states r s.fst s.snd.fst = captures cMemAndValid captures s.snd.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) (captures : Array NFA.Capture) :
              fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => s.fst = states tRefLt compiled states NextOfLt states s.snd.fst = captures cValid captures Code.c_at_least_0 compiled possible_empty_capture_group greedy (fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => stateIdNextOfLt states r s.fst s.snd.fst = captures cMemAndValid captures s.snd.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) (captures : Array NFA.Capture) :
              fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => (s.fst = states union < states.size tRefLt compiled states NextOfLt states) s.snd.fst = captures cValid captures liftM (Code.c_at_least_1_post compiled union possessive) (fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => tRefNextOfLeLt states r s.fst s.snd.fst = captures cMemAndValid captures s.snd.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) (captures : Array NFA.Capture) :
              fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => (s.fst = states NextOfLt states) s.snd.fst = captures cValid captures Code.c_at_least_1 possible_empty_capture_group greedy (fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => stateIdNextOfLt states r s.fst s.snd.fst = captures cMemAndValid captures s.snd.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) (captures : Array NFA.Capture) :
              fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => (s.fst = states tRefLt «prefix» states tRefLt last states NextOfLt states) s.snd.fst = captures cValid captures liftM (Code.c_at_least_2 «prefix» last greedy possessive) (fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => tRefNextOfLeLt states r s.fst s.snd.fst = captures cMemAndValid captures s.snd.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_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) (captures : Array NFA.Capture) :
              fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => (s.fst = states tRefLt compiled states prev_end < states.size empty < states.size NextOfLt states) s.snd.fst = captures cValid captures liftM (Code.c_bounded.fold.patch compiled prev_end empty greedy possessive) (fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => stateIdNextOfLt states r s.fst s.snd.fst = captures cMemAndValid captures s.snd.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) (captures : Array NFA.Capture) :
              @[irreducible]
              @[irreducible]
              theorem Compiler.Lemmas.c_at_least_spec (hir : Syntax.Hir) (n : Nat) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :
              @[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) (captures : Array NFA.Capture) :
              fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => s.fst = states tRefLt «prefix» states empty < states.size NextOfLt states s.snd.fst = captures cValid captures Code.c_bounded.fold hir n «prefix» empty greedy possessive (fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => stateIdNextOfLeLt states r s.fst cMemAndValid captures s.snd.fst, fun (x : String) => True, ())
              theorem Compiler.Lemmas.compile_nextOf_lt {states : Array NFA.Unchecked.State} {captures : Array NFA.Capture} {groups : Array Nat} {anchored : Bool} {expr : Syntax.Hir} (h : Code.compile anchored expr (#[], #[], #[]) = EStateM.Result.ok () (states, captures, groups)) :
              NextOfLt states
              theorem Compiler.Lemmas.compile_captures_valid {states : Array NFA.Unchecked.State} {captures : Array NFA.Capture} {groups : Array Nat} {anchored : Bool} {expr : Syntax.Hir} (h : Code.compile anchored expr (#[], #[], #[]) = EStateM.Result.ok () (states, captures, groups)) :