Theorem: Grammar.Derivation.augment_left (FormalSystems/Chomsky/Grammar.lean)

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 _
State after:
no goals

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
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✝

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]
State after:
no goals

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
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✝)

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
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✝)

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
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'✝

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
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'✝

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 _
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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

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 _
State after:
no goals