internlm/Lean-Github huggingface dataset:
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : l = p₂.lhs
h₂ : r = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂
Tactic:
simp_rw [h₁, h₂]
Proof state after:
no goals
Theorem: Grammar.DerivationStep.augment_left_result
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step : DerivationStep G u
w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
⊢ result (augment_left step w) = w * result step
Tactic:
unfold DerivationStep.result
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step : DerivationStep G u
w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
⊢ (augment_left step w).pre * Production.rhs ↑(augment_left step w).prod * (augment_left step w).suf =
    w * (step.pre * Production.rhs ↑step.prod * step.suf)
Theorem: Grammar.DerivationStep.augment_left_result
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step : DerivationStep G u
w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
⊢ (augment_left step w).pre * Production.rhs ↑(augment_left step w).prod * (augment_left step w).suf =
    w * (step.pre * Production.rhs ↑step.prod * step.suf)
Tactic:
unfold augment_left
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step : DerivationStep G u
w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
⊢ { prod := step.prod, pre := w * step.pre, suf := step.suf, sound := ⋯ }.pre *
        Production.rhs ↑{ prod := step.prod, pre := w * step.pre, suf := step.suf, sound := ⋯ }.prod *
      { prod := step.prod, pre := w * step.pre, suf := step.suf, sound := ⋯ }.suf =
    w * (step.pre * Production.rhs ↑step.prod * step.suf)
Theorem: Grammar.DerivationStep.augment_left_result
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step : DerivationStep G u
w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
⊢ { prod := step.prod, pre := w * step.pre, suf := step.suf, sound := ⋯ }.pre *
        Production.rhs ↑{ prod := step.prod, pre := w * step.pre, suf := step.suf, sound := ⋯ }.prod *
      { prod := step.prod, pre := w * step.pre, suf := step.suf, sound := ⋯ }.suf =
    w * (step.pre * Production.rhs ↑step.prod * step.suf)
Tactic:
simp [mul_assoc]
Proof state after:
no goals
Theorem: Grammar.DerivationStep.from_rule_result
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
p : { x // x ∈ G.productions }
⊢ result (fromRule p) = Production.rhs ↑p
Tactic:
simp [result, DerivationStep.fromRule, Word.epsilon]
Proof state after:
no goals
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ step.pre = ε ∧ step.suf = ε
Tactic:
match hpre:step.pre with
| .cons _ _ =>
  have tmp := Eq.symm $ hpre ▸ step.sound
  simp [mul_assoc, HMul.hMul, Mul.mul, List.cons_append] at tmp
  rw [List.cons_eq_cons] at tmp
  simp_rw [List.append_eq_nil] at tmp
  have tmp := tmp.2.2.1
  have ⟨_, h⟩ := Production.lhs_contains_var step.prod.val
  rw [tmp] at h
  contradiction
| .nil =>
  have tmp := Eq.symm $ hpre ▸ step.sound
  simp [<- Word.eps_eq_nil, Word.mul_eq_cons] at tmp
  cases tmp
  case inl h =>
    have ⟨_, c⟩ := Production.lhs_contains_var step.prod.val
    have ⟨h, _⟩ := h
    rw [h] at c
    contradiction
  case inr h =>
    have ⟨_, ⟨h₁, h₂⟩ ⟩ := h
    have tmp := Word.mul_eq_eps.mp $ Eq.symm h₂
    have tmp' := tmp.1 ▸ h₁
    simp at tmp'
    constructor
    . assumption
    . constructor; rfl; exact tmp.right
Proof state after:
no goals
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
have tmp := Eq.symm $ hpre ▸ step.sound
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : (head✝ :: tail✝) * Production.lhs ↑step.prod * step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : (head✝ :: tail✝) * Production.lhs ↑step.prod * step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
simp [mul_assoc, HMul.hMul, Mul.mul, List.cons_append] at tmp
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ :: (tail✝ ++ (Production.lhs ↑step.prod ++ step.suf)) = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ :: (tail✝ ++ (Production.lhs ↑step.prod ++ step.suf)) = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
rw [List.cons_eq_cons] at tmp
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ = Sum.inl v ∧ tail✝ ++ (Production.lhs ↑step.prod ++ step.suf) = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ = Sum.inl v ∧ tail✝ ++ (Production.lhs ↑step.prod ++ step.suf) = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
simp_rw [List.append_eq_nil] at tmp
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
have tmp := tmp.2.2.1
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
have ⟨_, h⟩ := Production.lhs_contains_var step.prod.val
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
w✝ : { x // x ∈ G.V }
h : Sum.inl w✝ ∈ Production.lhs ↑step.prod
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
w✝ : { x // x ∈ G.V }
h : Sum.inl w✝ ∈ Production.lhs ↑step.prod
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
rw [tmp] at h
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
w✝ : { x // x ∈ G.V }
h : Sum.inl w✝ ∈ []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
w✝ : { x // x ∈ G.V }
h : Sum.inl w✝ ∈ []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
contradiction
Proof state after:
no goals
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have tmp := Eq.symm $ hpre ▸ step.sound
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
tmp : [] * Production.lhs ↑step.prod * step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
tmp : [] * Production.lhs ↑step.prod * step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
simp [<- Word.eps_eq_nil, Word.mul_eq_cons] at tmp
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
tmp :
  Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v] ∨
    ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
tmp :
  Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v] ∨
    ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
cases tmp
Proof state after:
case inl
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε

case inr
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
case inl h =>
  have ⟨_, c⟩ := Production.lhs_contains_var step.prod.val
  have ⟨h, _⟩ := h
  rw [h] at c
  contradiction
Proof state after:
no goals
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
case inr h =>
  have ⟨_, ⟨h₁, h₂⟩ ⟩ := h
  have tmp := Word.mul_eq_eps.mp $ Eq.symm h₂
  have tmp' := tmp.1 ▸ h₁
  simp at tmp'
  constructor
  . assumption
  . constructor; rfl; exact tmp.right
Proof state after:
no goals
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have ⟨_, c⟩ := Production.lhs_contains_var step.prod.val
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ Production.lhs ↑step.prod
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ Production.lhs ↑step.prod
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have ⟨h, _⟩ := h
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ Production.lhs ↑step.prod
h : Production.lhs ↑step.prod = ε
right✝ : step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ Production.lhs ↑step.prod
h : Production.lhs ↑step.prod = ε
right✝ : step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
rw [h] at c
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ ε
h : Production.lhs ↑step.prod = ε
right✝ : step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ ε
h : Production.lhs ↑step.prod = ε
right✝ : step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
contradiction
Proof state after:
no goals
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have ⟨_, ⟨h₁, h₂⟩ ⟩ := h
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have tmp := Word.mul_eq_eps.mp $ Eq.symm h₂
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε