Documentation

Regex.Compiler.Lemmas.Basic

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)

Instances For

def Compiler.Lemmas.tacticInst_mvars :

Lean.ParserDescr

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

Equations

Compiler.Lemmas.tacticInst_mvars = Lean.ParserDescr.node `Compiler.Lemmas.tacticInst_mvars 1024 (Lean.ParserDescr.nonReservedSymbol "inst_mvars" false)

Instances For

def Compiler.Lemmas.isAppend (s1 s2 : Array NFA.Unchecked.State) :

Equations

Compiler.Lemmas.isAppend s1 s2 = ∃ (s' : Array NFA.Unchecked.State), s2 = s1 ++ s'

Instances For

@[simp]

theorem Compiler.Lemmas.isAppend_trans {s1 s2 s3 : Array NFA.Unchecked.State} (h1 : isAppend s1 s2) (h2 : isAppend s2 s3) :

theorem Compiler.Lemmas.all_push {sid : NFA.Unchecked.State} (states : Array NFA.Unchecked.State) (h : sid.nextOf ≤ states.size) (hlt : ∀ (i : Nat) (x : i < states.size), states[i].nextOf < states.size) (i : Nat) (x✝ : i < (states.push sid).size) :

(states.push sid)[i].nextOf < (states.push sid).size

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

⦃fun (s : σ) => ⌜s = n ∧ P n⌝⦄ liftM v ⦃(fun (a : α) (s : σ) => ⌜Q n a s⌝, fun (x : ε) => ⌜False ⌝, PUnit.unit )⦄

def Compiler.Lemmas.coe_spec_StackT_to_EStateM {σ α ε : Type u_1} {v : StateT σ Id α} {P : σ → Prop} {Q : α → σ → Prop} (hspec : ⦃fun (s : σ) => ⌜P s⌝⦄ v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, PUnit.unit )⦄) :

⦃fun (s : σ) => ⌜P s⌝⦄ liftM v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, fun (x : ε) (x_1 : σ) => ⌜False ⌝, PUnit.unit )⦄

Equations

⋯ = hspec

Instances For

@[implicit_reducible]

instance Compiler.Lemmas.instCoeTripleStateTIdPureEStateMLiftM_regex {σ α ε : Type u_1} {v : StateT σ Id α} {P : σ → Prop} {Q : α → σ → Prop} :

Coe (⦃fun (s : σ) => ⌜P s⌝⦄ v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, PUnit.unit )⦄) (⦃fun (s : σ) => ⌜P s⌝⦄ liftM v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, fun (x : ε) (x_1 : σ) => ⌜False ⌝, PUnit.unit )⦄)

Equations

Compiler.Lemmas.instCoeTripleStateTIdPureEStateMLiftM_regex = { coe := ⋯ }

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

def Compiler.Lemmas.cValid (caps : Array NFA.Capture) :

Equations

Compiler.Lemmas.cValid caps = NFA.Capture.Valid caps

Instances For

def Compiler.Lemmas.cMemAndValid (prev caps : Array NFA.Capture) :

Equations

Compiler.Lemmas.cMemAndValid prev caps = ((∀ (a : NFA.Capture), a ∈ prev → a ∈ caps) ∧ NFA.Capture.Valid caps)

Instances For

def Compiler.Lemmas.cValidFunc (captures : Array NFA.Capture) :

Array NFA.Capture → Prop

Equations

Compiler.Lemmas.cValidFunc captures curr = (curr = captures ∧ Compiler.Lemmas.cValid captures)

Instances For

def Compiler.Lemmas.cMemAndValidFunc (captures : Array NFA.Capture) :

Array NFA.Capture → Prop

Equations

Compiler.Lemmas.cMemAndValidFunc captures curr = (curr = captures ∧ Compiler.Lemmas.cMemAndValid captures curr)

Instances For

theorem Compiler.Lemmas.cap_exists_of_cap_role_end_of_cValid (caps : Array NFA.Capture) (h : cValid caps) (a : NFA.Capture) (h1 : a ∈ caps) (h2 : a.role = NFA.Capture.Role.End) :

∃ (a' : NFA.Capture ), a' ∈ caps ∧ a'.role = NFA.Capture.Role.Start ∧ a.group = a'.group

theorem Compiler.Lemmas.cValid_of_empty (captures : Array NFA.Capture) (h : captures.size = 0) :

cValid captures

theorem Compiler.Lemmas.cValid_of_cMemAndValid (prevs caps : Array NFA.Capture) (h : cMemAndValid prevs caps) :

@[simp]

theorem Compiler.Lemmas.cMemAndValid_of_cValid_of_eq (captures s : Array NFA.Capture) :

s = captures ∧ cValid captures → cMemAndValid captures s

@[simp]

theorem Compiler.Lemmas.valid_of_push_of_role_start (captures : Array NFA.Capture) (capture : NFA.Capture) (hr : capture.role = NFA.Capture.Role.Start) (hc : NFA.Capture.Valid captures) :

NFA.Capture.Valid (captures.push capture)

@[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)

@[simp]

theorem Compiler.Lemmas.cMemAndValidFunc_of_cValidFunc (captures s : Array NFA.Capture) :

cValidFunc captures s → cMemAndValidFunc captures s

theorem Compiler.Lemmas.coe_spec_EStateM_to_EStateM_Prod {ε σ₁ α : Type (max u_1 u_2)} {σ₂ : Type u_2} (σ₃ : Type) {v₁ : EStateM ε σ₁ α} {P₁ : σ₁ → Prop} {Q₁ : α → σ₁ → Prop} (hspec₁ : ⦃fun (s : σ₁) => ⌜P₁ s⌝⦄ v₁ ⦃(fun (a : α) (s : σ₁) => ⌜Q₁ a s⌝, fun (x : ε) => ⌜False ⌝, PUnit.unit )⦄) (P₂ Q₂ : σ₂ → Prop) (hpq : ∀ (s : σ₂), P₂ s → Q₂ s) :

⦃fun (s : σ₁ × σ₂ × σ₃) => ⌜P₁ s.fst ∧ P₂ s.snd.fst⌝⦄ liftM v₁ ⦃(fun (r : α) (s : σ₁ × σ₂ × σ₃) => ⌜Q₁ r s.fst ∧ Q₂ s.snd.fst⌝, fun (x : ε) (x_1 : σ₁ × σ₂ × σ₃) => ⌜False ⌝, PUnit.unit )⦄

theorem Compiler.Lemmas.coe_spec_EStateM_to_CompilerM {ε σ₁ α : Type u_1} {captures : Array NFA.Capture} {v₁ : EStateM ε σ₁ α} {P₁ : σ₁ → Prop} {Q₁ : α → σ₁ → Prop} (hspec₁ : ⦃fun (s : σ₁) => ⌜P₁ s⌝⦄ v₁ ⦃(fun (a : α) (s : σ₁) => ⌜Q₁ a s⌝, fun (x : ε) => ⌜False ⌝, PUnit.unit )⦄) :

⦃fun (s : σ₁ × Array NFA.Capture × Array Nat) => ⌜P₁ s.fst ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM v₁ ⦃(fun (r : α) (s : σ₁ × Array NFA.Capture × Array Nat) => ⌜Q₁ r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : ε) (x_1 : σ₁ × Array NFA.Capture × Array Nat) => ⌜False ⌝, PUnit.unit )⦄

theorem Compiler.Lemmas.coe_spec_StateT_to_CompilerM {σ₁ α ε : Type u_1} {captures : Array NFA.Capture} {v : StateT σ₁ Id α} {P₁ : σ₁ → Prop} {Q₁ : α → σ₁ → Prop} (hspec : ⦃fun (s : σ₁) => ⌜P₁ s⌝⦄ v ⦃(fun (a : α) (s : σ₁) => ⌜Q₁ a s⌝, PUnit.unit )⦄) :

⦃fun (s : σ₁ × Array NFA.Capture × Array Nat) => ⌜P₁ s.fst ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM v ⦃(fun (r : α) (s : σ₁ × Array NFA.Capture × Array Nat) => ⌜Q₁ r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : ε) (x_1 : σ₁ × Array NFA.Capture × Array Nat) => ⌜False ⌝, PUnit.unit )⦄

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 u_1} {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 : ε) => ⌜False ⌝, PUnit.unit )⦄

theorem Compiler.Lemmas.nextOf_look_eq {look : NFA.Look} :

(NFA.Unchecked.State.Look look 0).nextOf = 0

theorem Compiler.Lemmas.nextOf_union_eq :

(NFA.Unchecked.State.Union #[]).nextOf = 0

theorem Compiler.Lemmas.nextOf_union_reverse_eq :

(NFA.Unchecked.State.UnionReverse #[]).nextOf = 0

theorem Compiler.Lemmas.nextOf_transition_le_of_le (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