Documentation

Regex.Compiler.Lemmas.Patch

source
def Compiler.Lemmas.State.patchAssignable (state : NFA.Unchecked.State) :
Prop
Equations
Instances For
    source
    def Compiler.Lemmas.patchAssignable (s : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) :
    Prop
    Equations
    Instances For
      source
      def Compiler.Lemmas.State.patch2Assignable (state : NFA.Unchecked.State) :
      Prop
      Equations
      Instances For
        source
        @[simp]
        theorem Compiler.Lemmas.State.patchAssignable_of_empty :
        patchAssignable (NFA.Unchecked.State.Empty 0)
        source
        @[simp]
        theorem Compiler.Lemmas.State.patchAssignable_of_next_char (offset : Nat) :
        patchAssignable (NFA.Unchecked.State.NextChar offset 0)
        source
        @[simp]
        theorem Compiler.Lemmas.State.patchAssignable_of_look {look : NFA.Look} :
        patchAssignable (NFA.Unchecked.State.Look look 0)
        source
        @[simp]
        theorem Compiler.Lemmas.State.patchAssignable_of_remove_frame_step :
        patchAssignable (NFA.Unchecked.State.RemoveFrameStep 0)
        source
        @[simp]
        theorem Compiler.Lemmas.State.patchAssignable_of_byte_range (trans : NFA.Unchecked.Transition) :
        patchAssignable (NFA.Unchecked.State.ByteRange trans)
        source
        @[simp]
        theorem Compiler.Lemmas.State.patchAssignable_of_sparse_transistions (trans : Array NFA.Unchecked.Transition) :
        patchAssignable (NFA.Unchecked.State.SparseTransitions trans)
        source
        @[simp]
        theorem Compiler.Lemmas.State.patchAssignable_of_union :
        patchAssignable (NFA.Unchecked.State.Union #[])
        source
        @[simp]
        theorem Compiler.Lemmas.State.patchAssignable_of_union_reverse :
        patchAssignable (NFA.Unchecked.State.UnionReverse #[])
        source
        @[simp]
        theorem Compiler.Lemmas.State.patchAssignable_of_capture (role : NFA.Capture.Role) (group : Nat) :
        patchAssignable (NFA.Unchecked.State.Capture role 0 0 group)
        source
        @[simp]
        theorem Compiler.Lemmas.State.patch2Assignable_of_changeframe_step :
        patch2Assignable (NFA.Unchecked.State.ChangeFrameStep 0 0)
        source
        def Compiler.Lemmas.patch2Assignable (s : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) :
        Prop
        Equations
        Instances For
          source
          @[simp]
          theorem Compiler.Lemmas.State.patchAssignable_of_backRef {b : Nat} {case_insensitive : Bool} :
          patchAssignable (NFA.Unchecked.State.BackRef b case_insensitive 0)
          source
          def Compiler.Lemmas.assignableIf (s1 s2 : Array NFA.Unchecked.State) :
          Prop
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Compiler.Lemmas.patchAssignable_of_some {f : Nat} {s : Array NFA.Unchecked.State} (hlt : f < s.size) {state : NFA.Unchecked.State} (h : s[f]? = some state) (hp : State.patchAssignable state) :
            patchAssignable s f
            source
            @[simp]
            theorem Compiler.Lemmas.patchAssignable_of_eq {sid : NFA.Unchecked.StateID} (s1 s2 : Array NFA.Unchecked.State) (h1 : patchAssignable s1 sid) (h2 : sid < s1.size) (h3 : sid < s2.size) (h4 : s1[sid] = s2[sid]) :
            patchAssignable s2 sid
            source
            @[simp]
            theorem Compiler.Lemmas.patchAssignable_of_append {sid : NFA.Unchecked.StateID} (s1 s2 : Array NFA.Unchecked.State) (h1 : patchAssignable s1 sid) (h2 : isAppend s1 s2) :
            patchAssignable s2 sid
            source
            @[simp]
            theorem Compiler.Lemmas.assignableIf_trans {s3 : Array NFA.Unchecked.State} (s1 s2 : Array NFA.Unchecked.State) (h1 : assignableIf s1 s2) (h2 : assignableIf s2 s3) :
            assignableIf s1 s3
            source
            @[simp]
            theorem Compiler.Lemmas.patchAssignable_of_assignableIf {sid : NFA.Unchecked.StateID} (s1 s2 : Array NFA.Unchecked.State) (h1 : patchAssignable s1 sid) (h2 : assignableIf s1 s2) :
            patchAssignable s2 sid
            source
            @[simp]
            theorem Compiler.Lemmas.patch2Assignable_of_assignableIf {sid : NFA.Unchecked.StateID} (s1 s2 : Array NFA.Unchecked.State) (h1 : patch2Assignable s1 sid) (h2 : assignableIf s1 s2) :
            patch2Assignable s2 sid
            source
            @[simp]
            theorem Compiler.Lemmas.not_patchAssignable_if_patch_eq_error {f t : NFA.Unchecked.StateID} {e : String} {s1 s2 : Array NFA.Unchecked.State} (h : Code.patch f t s1 = EStateM.Result.error e s2) (hlt : f < s1.size) :
            ¬patchAssignable s1 f
            source
            @[simp]
            theorem Compiler.Lemmas.patch2Assignable_of_eq {sid : NFA.Unchecked.StateID} (s1 s2 : Array NFA.Unchecked.State) (h1 : patch2Assignable s1 sid) (h2 : sid < s1.size) (h3 : sid < s2.size) (h4 : s1[sid] = s2[sid]) :
            patch2Assignable s2 sid
            source
            @[simp]
            theorem Compiler.Lemmas.patch2Assignable_of_append {sid : NFA.Unchecked.StateID} (s1 s2 : Array NFA.Unchecked.State) (h1 : patch2Assignable s1 sid) (h2 : isAppend s1 s2) :
            patch2Assignable s2 sid
            source
            @[simp]
            theorem Compiler.Lemmas.not_patch2Assignable_if_patch2_eq_error {f t1 t2 : NFA.Unchecked.StateID} {e : String} {s1 s2 : Array NFA.Unchecked.State} (h : Code.patch2 f t1 t2 s1 = EStateM.Result.error e s2) (hlt : f < s1.size) :
            ¬patch2Assignable s1 f
            source
            @[simp]
            theorem Compiler.Lemmas.not_patch2Assignable_if_patch_eq {f t : NFA.Unchecked.StateID} (s1 s2 : Array NFA.Unchecked.State) (h : Code.patch f t s1 = EStateM.Result.ok () s2) :
            ¬patch2Assignable s1 f
            source
            theorem Compiler.Lemmas.patch_spec_constant («from» to : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) :
            ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ «from» < states.size ∧ to < states.size⌝⦄ Code.patch «from» to ⦃(fun (x : Unit) (r : Array NFA.Unchecked.State) => ⌜stateIdNextOfEqLt states to r ∧ ∀ (sid : Fin r.size) (x : ↑sid < states.size), ↑sid ≠ «from» → r[sid] = states[sid]⌝, fun (x : String) => ⌜True⌝, PUnit.unit)⦄
            source
            theorem Compiler.Lemmas.patch_spec_assignable («from» to : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) :
            ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ «from» < states.size ∧ to < states.size⌝⦄ Code.patch «from» to ⦃(fun (x : Unit) (r : Array NFA.Unchecked.State) => ⌜patchAssignable r «from»⌝, fun (x : String) => ⌜True⌝, PUnit.unit)⦄
            source
            @[simp]
            theorem Compiler.Lemmas.patchAssignable_of_patch_eq {f t : NFA.Unchecked.StateID} {e : Unit} (s1 s2 : Array NFA.Unchecked.State) (h : Code.patch f t s1 = EStateM.Result.ok e s2) (hf : f < s1.size) (ht : t < s1.size) :
            patchAssignable s2 f
            source
            theorem Compiler.Lemmas.patch_spec («from» : NFA.Unchecked.StateID) {to : NFA.Unchecked.StateID} {states : Array NFA.Unchecked.State} :
            ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ «from» < states.size ∧ to < states.size ∧ patchAssignable states «from»⌝⦄ Code.patch «from» to ⦃(fun (x : Unit) (r : Array NFA.Unchecked.State) => ⌜stateIdNextOfEqLt states to r ∧ assignableIf states r⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄
            source
            theorem Compiler.Lemmas.patch_lift_spec {captures : Array NFA.Capture} («from» : NFA.Unchecked.StateID) {to : NFA.Unchecked.StateID} {states : Array NFA.Unchecked.State} :
            ⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ NextOfLt states ∧ «from» < states.size ∧ to < states.size ∧ patchAssignable states «from») ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.patch «from» to) ⦃(fun (x : Unit) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(stateIdNextOfEqLt states to s.fst ∧ assignableIf states s.fst) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄
            source
            theorem Compiler.Lemmas.patch2_spec_constant («from» to₁ to₂ : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) :
            ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ «from» < states.size ∧ to₁ < states.size ∧ to₂ < states.size⌝⦄ Code.patch2 «from» to₁ to₂ ⦃(fun (x : Unit) (r : Array NFA.Unchecked.State) => ⌜stateIdNextOfEqLt states to₁ r ∧ ∀ (sid : Fin r.size) (x : ↑sid < states.size), ↑sid ≠ «from» → r[sid] = states[sid]⌝, fun (x : String) => ⌜True⌝, PUnit.unit)⦄
            source
            theorem Compiler.Lemmas.patch2_spec_assignable («from» to₁ to₂ : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) :
            ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ «from» < states.size ∧ to₁ < states.size ∧ to₂ < states.size⌝⦄ Code.patch2 «from» to₁ to₂ ⦃(fun (x : Unit) (r : Array NFA.Unchecked.State) => ⌜patch2Assignable r «from»⌝, fun (x : String) => ⌜True⌝, PUnit.unit)⦄
            source
            @[simp]
            theorem Compiler.Lemmas.patch2Assignable_of_patch_eq {f t1 t2 : NFA.Unchecked.StateID} {e : Unit} (s1 s2 : Array NFA.Unchecked.State) (h : Code.patch2 f t1 t2 s1 = EStateM.Result.ok e s2) (hf : f < s1.size) (ht1 : t1 < s1.size) (ht2 : t2 < s1.size) :
            patch2Assignable s2 f
            source
            @[simp]
            theorem Compiler.Lemmas.not_patchAssignable_if_patch2_eq {f t1 t2 : NFA.Unchecked.StateID} (s1 s2 : Array NFA.Unchecked.State) (h : Code.patch2 f t1 t2 s1 = EStateM.Result.ok () s2) :
            ¬patchAssignable s1 f
            source
            theorem Compiler.Lemmas.patch2_spec («from» : NFA.Unchecked.StateID) {to₁ to₂ : NFA.Unchecked.StateID} {states : Array NFA.Unchecked.State} :
            ⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ NextOfLt states ∧ «from» < states.size ∧ to₁ < states.size ∧ to₂ < states.size ∧ patch2Assignable states «from»⌝⦄ Code.patch2 «from» to₁ to₂ ⦃(fun (x : Unit) (r : Array NFA.Unchecked.State) => ⌜stateIdNextOfEqLt states to₁ r ∧ to₂ < r.size ∧ assignableIf states r⌝, fun (x : String) => ⌜False⌝, PUnit.unit)⦄