internlm/Lean-Github huggingface dataset:
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
tmp : w✝ = ε ∧ step.suf = ε
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have tmp' := tmp.1 ▸ 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 = ε
tmp' : Production.lhs ↑step.prod = 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 : ∃ 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 = ε
tmp' : Production.lhs ↑step.prod = Sum.inl v :: ε
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
simp 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 = []
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 = ε
tmp' : Production.lhs ↑step.prod = [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 : ∃ 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
constructor
Proof state after:
case left
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v]

case right
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
case left
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v]

case right
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε ∧ step.suf = ε
Tactic:
. assumption
Proof state after:
case right
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε ∧ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
case right
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε ∧ step.suf = ε
Tactic:
. constructor; rfl; exact tmp.right
Proof state after:
no goals
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
case left
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v]
Tactic:
assumption
Proof state after:
no goals
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
case right
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε ∧ step.suf = ε
Tactic:
constructor
Proof state after:
case right.left
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε

case right.right
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
case right.left
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε

case right.right
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ step.suf = ε
Tactic:
rfl
Proof state after:
case right.right
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ step.suf = ε
Theorem: Grammar.DerivationStep.lhs_singleton
Proof state before:
case right.right
α 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 = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ step.suf = ε
Tactic:
exact tmp.right
Proof state after:
no goals
Theorem: Grammar.Derivation.augment_left
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝ u v w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
d : Derivation G u v
⊢ Derivation G (w * u) (w * v)
Tactic:
induction d with
| same h => apply same; simp [h]
| step s _ sound =>
  apply step
  . assumption
  swap
  . exact s.augment_left w
  . rw [<- sound]; exact s.augment_left_result _
Proof state after:
no goals
Theorem: Grammar.Derivation.augment_left
Proof state before:
case same
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : u✝ = v✝
⊢ Derivation G (w * u✝) (w * v✝)
Tactic:
apply same
Proof state after:
case same.h
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : u✝ = v✝
⊢ w * u✝ = w * v✝
Theorem: Grammar.Derivation.augment_left
Proof state before:
case same.h
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : u✝ = v✝
⊢ w * u✝ = w * v✝
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Grammar.Derivation.augment_left
Proof state before:
case step
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ Derivation G (w * u✝) (w * v✝)
Tactic:
apply step
Proof state after:
case step.x
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ Derivation G ?step.u' (w * v✝)

case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result ?step.step = ?step.u'

case step.u'
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })

case step.step
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep G (w * u✝)
Theorem: Grammar.Derivation.augment_left
Proof state before:
case step.x
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ Derivation G ?step.u' (w * v✝)

case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result ?step.step = ?step.u'

case step.u'
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })

case step.step
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep G (w * u✝)
Tactic:
. assumption
Proof state after:
case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result ?step.step = w * u'✝

case step.step
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep G (w * u✝)
Theorem: Grammar.Derivation.augment_left
Proof state before:
case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result ?step.step = w * u'✝

case step.step
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep G (w * u✝)
Tactic:
swap
Proof state after:
case step.step
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep G (w * u✝)

case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result ?step.step = w * u'✝
Theorem: Grammar.Derivation.augment_left
Proof state before:
case step.step
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep G (w * u✝)

case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result ?step.step = w * u'✝
Tactic:
. exact s.augment_left w
Proof state after:
case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result (DerivationStep.augment_left s w) = w * u'✝
Theorem: Grammar.Derivation.augment_left
Proof state before:
case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result (DerivationStep.augment_left s w) = w * u'✝
Tactic:
. rw [<- sound]; exact s.augment_left_result _
Proof state after:
no goals
Theorem: Grammar.Derivation.augment_left
Proof state before:
case step.x
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ Derivation G ?step.u' (w * v✝)
Tactic:
assumption
Proof state after:
no goals
Theorem: Grammar.Derivation.augment_left
Proof state before:
case step.step
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep G (w * u✝)
Tactic:
exact s.augment_left w
Proof state after:
no goals
Theorem: Grammar.Derivation.augment_left
Proof state before:
case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result (DerivationStep.augment_left s w) = w * u'✝
Tactic:
rw [<- sound]
Proof state after:
case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result (DerivationStep.augment_left s w) = w * DerivationStep.result s
Theorem: Grammar.Derivation.augment_left
Proof state before:
case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result (DerivationStep.augment_left s w) = w * DerivationStep.result s
Tactic:
exact s.augment_left_result _
Proof state after:
no goals
Theorem: Grammar.Derivation.trans
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝ u v w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
d1 : Derivation G u v
d2 : Derivation G v w
⊢ Derivation G u w
Tactic:
induction d1 with
| same h => exact h ▸ d2
| step l _ sound ih => exact step l (ih d2) sound
Proof state after:
no goals
Theorem: Grammar.Derivation.trans
Proof state before:
case same
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : u✝ = v✝
d2 : Derivation G v✝ w
⊢ Derivation G u✝ w
Tactic:
exact h ▸ d2
Proof state after:
no goals
Theorem: Grammar.Derivation.trans
Proof state before:
case step
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
l : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result l = u'✝
ih : Derivation G v✝ w → Derivation G u'✝ w
d2 : Derivation G v✝ w
⊢ Derivation G u✝ w
Tactic:
exact step l (ih d2) sound
Proof state after:
no goals