Theorem: ContextFreeGrammar.derivation_step_prefix (FormalSystems/Chomsky/ContextFree/ContextFreeGrammar.lean)

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
⊢ step.pre = Sum.inr a :: List.tail step.pre
Tactic:
have sound := step.sound
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound :
  let_fun x := Production.lhs ↑step.prod;
  lhs = step.pre * x * step.suf
⊢ step.pre = Sum.inr a :: List.tail step.pre

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound :
  let_fun x := Production.lhs ↑step.prod;
  lhs = step.pre * x * step.suf
⊢ step.pre = Sum.inr a :: List.tail step.pre
Tactic:
simp_rw [Production.ContextFree.lhs_eq_lhs step.prod.val, h_lhs] at sound
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound : Sum.inr a :: xs = step.pre * [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)] * step.suf
⊢ step.pre = Sum.inr a :: List.tail step.pre

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound : Sum.inr a :: xs = step.pre * [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)] * step.suf
⊢ step.pre = Sum.inr a :: List.tail step.pre
Tactic:
match hpre:step.pre with
| [] =>
  simp_rw [hpre, HMul.hMul, Mul.mul] at sound
  simp at sound
  rw [List.cons_eq_cons] at sound
  let ⟨_, _⟩ := sound
  contradiction
| x :: pres => 
  simp_rw [hpre, HMul.hMul, Mul.mul] at sound
  simp at sound; rw [List.cons_eq_cons] at sound
  simp [sound.left]
State after:
no goals

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound : Sum.inr a :: xs = step.pre * [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)] * step.suf
hpre : step.pre = []
⊢ [] = Sum.inr a :: List.tail []
Tactic:
simp_rw [hpre, HMul.hMul, Mul.mul] at sound
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a :: xs = List.append (List.append [] [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)]) step.suf
⊢ [] = Sum.inr a :: List.tail []

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a :: xs = List.append (List.append [] [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)]) step.suf
⊢ [] = Sum.inr a :: List.tail []
Tactic:
simp at sound
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a :: xs = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf
⊢ [] = Sum.inr a :: List.tail []

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a :: xs = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf
⊢ [] = Sum.inr a :: List.tail []
Tactic:
rw [List.cons_eq_cons] at sound
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) ∧ xs = step.suf
⊢ [] = Sum.inr a :: List.tail []

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) ∧ xs = step.suf
⊢ [] = Sum.inr a :: List.tail []
Tactic:
let ⟨_, _⟩ := sound
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) ∧ xs = step.suf
left✝ : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod)
right✝ : xs = step.suf
⊢ [] = Sum.inr a :: List.tail []

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) ∧ xs = step.suf
left✝ : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod)
right✝ : xs = step.suf
⊢ [] = Sum.inr a :: List.tail []
Tactic:
contradiction
State after:
no goals

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound : Sum.inr a :: xs = step.pre * [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)] * step.suf
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)
Tactic:
simp_rw [hpre, HMul.hMul, Mul.mul] at sound
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound :
  Sum.inr a :: xs = List.append (List.append (x :: pres) [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)]) step.suf
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound :
  Sum.inr a :: xs = List.append (List.append (x :: pres) [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)]) step.suf
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)
Tactic:
simp at sound
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound : Sum.inr a :: xs = x :: (pres ++ Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf)
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound : Sum.inr a :: xs = x :: (pres ++ Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf)
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)
Tactic:
rw [List.cons_eq_cons] at sound
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound : Sum.inr a = x ∧ xs = pres ++ Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound : Sum.inr a = x ∧ xs = pres ++ Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)
Tactic:
simp [sound.left]
State after:
no goals