internlm/Lean-Github huggingface dataset:
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof 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
Proof 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)
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof 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]
Proof state after:
no goals
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
⊢ w = a :: List.tail w
Tactic:
match d with
| .same h =>
  rw [<- h, h_lhs] at h_rhs
  cases w
  simp [List.map_nil] at h_rhs
  simp [List.map_cons] at h_rhs
  rw [List.cons_eq_cons] at h_rhs
  have _ := (Sum.inr_injective h_rhs.left).symm
  simp; rw [List.cons_eq_cons]
  simp; assumption
| .step s d r =>
  unfold Grammar.DerivationStep.result at r
  rw [ContextFreeGrammar.derivation_step_prefix s h_lhs] at r
  simp_rw [HMul.hMul, Mul.mul] at r
  simp at r
  let h_lhs' := r.symm
  exact ContextFreeGrammar.derivation_preserves_prefix d h_lhs' h_rhs
Proof state after:
no goals
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
h : lhs = rhs
⊢ w = a :: List.tail w
Tactic:
rw [<- h, h_lhs] at h_rhs
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : Sum.inr a :: xs = Sum.inr <$> w
h : lhs = rhs
⊢ w = a :: List.tail w
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : Sum.inr a :: xs = Sum.inr <$> w
h : lhs = rhs
⊢ w = a :: List.tail w
Tactic:
cases w
Proof state after:
case nil
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
h_rhs : Sum.inr a :: xs = Sum.inr <$> []
⊢ [] = a :: List.tail []

case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a :: xs = Sum.inr <$> (head✝ :: tail✝)
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
case nil
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
h_rhs : Sum.inr a :: xs = Sum.inr <$> []
⊢ [] = a :: List.tail []

case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a :: xs = Sum.inr <$> (head✝ :: tail✝)
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)
Tactic:
simp [List.map_nil] at h_rhs
Proof state after:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a :: xs = Sum.inr <$> (head✝ :: tail✝)
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a :: xs = Sum.inr <$> (head✝ :: tail✝)
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)
Tactic:
simp [List.map_cons] at h_rhs
Proof state after:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a :: xs = Sum.inr head✝ :: List.map Sum.inr tail✝
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a :: xs = Sum.inr head✝ :: List.map Sum.inr tail✝
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)
Tactic:
rw [List.cons_eq_cons] at h_rhs
Proof state after:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a = Sum.inr head✝ ∧ xs = List.map Sum.inr tail✝
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a = Sum.inr head✝ ∧ xs = List.map Sum.inr tail✝
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)
Tactic:
have _ := (Sum.inr_injective h_rhs.left).symm
Proof state after:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a = Sum.inr head✝ ∧ xs = List.map Sum.inr tail✝
x✝ : head✝ = a
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a = Sum.inr head✝ ∧ xs = List.map Sum.inr tail✝
x✝ : head✝ = a
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)
Tactic:
simp
Proof state after:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a = Sum.inr head✝ ∧ xs = List.map Sum.inr tail✝
x✝ : head✝ = a
⊢ head✝ :: tail✝ = a :: tail✝
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a = Sum.inr head✝ ∧ xs = List.map Sum.inr tail✝
x✝ : head✝ = a
⊢ head✝ :: tail✝ = a :: tail✝
Tactic:
rw [List.cons_eq_cons]
Proof state after:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a = Sum.inr head✝ ∧ xs = List.map Sum.inr tail✝
x✝ : head✝ = a
⊢ head✝ = a ∧ tail✝ = tail✝
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a = Sum.inr head✝ ∧ xs = List.map Sum.inr tail✝
x✝ : head✝ = a
⊢ head✝ = a ∧ tail✝ = tail✝
Tactic:
simp
Proof state after:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a = Sum.inr head✝ ∧ xs = List.map Sum.inr tail✝
x✝ : head✝ = a
⊢ head✝ = a
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a = Sum.inr head✝ ∧ xs = List.map Sum.inr tail✝
x✝ : head✝ = a
⊢ head✝ = a
Tactic:
assumption
Proof state after:
no goals
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : Grammar.DerivationStep.result s = u'✝
⊢ w = a :: List.tail w
Tactic:
unfold Grammar.DerivationStep.result at r
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : s.pre * Production.rhs ↑s.prod * s.suf = u'✝
⊢ w = a :: List.tail w
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : s.pre * Production.rhs ↑s.prod * s.suf = u'✝
⊢ w = a :: List.tail w
Tactic:
rw [ContextFreeGrammar.derivation_step_prefix s h_lhs] at r
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : (Sum.inr a :: List.tail s.pre) * Production.rhs ↑s.prod * s.suf = u'✝
⊢ w = a :: List.tail w
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : (Sum.inr a :: List.tail s.pre) * Production.rhs ↑s.prod * s.suf = u'✝
⊢ w = a :: List.tail w
Tactic:
simp_rw [HMul.hMul, Mul.mul] at r
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : List.append (List.append (Sum.inr a :: List.tail s.pre) (Production.rhs ↑s.prod)) s.suf = u'✝
⊢ w = a :: List.tail w
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : List.append (List.append (Sum.inr a :: List.tail s.pre) (Production.rhs ↑s.prod)) s.suf = u'✝
⊢ w = a :: List.tail w
Tactic:
simp at r
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : Sum.inr a :: (List.tail s.pre ++ (Production.rhs ↑s.prod ++ s.suf)) = u'✝
⊢ w = a :: List.tail w
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : Sum.inr a :: (List.tail s.pre ++ (Production.rhs ↑s.prod ++ s.suf)) = u'✝
⊢ w = a :: List.tail w
Tactic:
let h_lhs' := r.symm
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : Sum.inr a :: (List.tail s.pre ++ (Production.rhs ↑s.prod ++ s.suf)) = u'✝
h_lhs' : u'✝ = Sum.inr a :: (List.tail s.pre ++ (Production.rhs ↑s.prod ++ s.suf)) := r.symm
⊢ w = a :: List.tail w
Theorem: ContextFreeGrammar.derivation_preserves_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d✝ : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : Sum.inr a :: (List.tail s.pre ++ (Production.rhs ↑s.prod ++ s.suf)) = u'✝
h_lhs' : u'✝ = Sum.inr a :: (List.tail s.pre ++ (Production.rhs ↑s.prod ++ s.suf)) := r.symm
⊢ w = a :: List.tail w
Tactic:
exact ContextFreeGrammar.derivation_preserves_prefix d h_lhs' h_rhs
Proof state after:
no goals
Theorem: Grammar.Derivation.cancelLeft_len_same
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
a✝¹ a✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : a✝¹ = a✝
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : a✝¹ = Sum.inr val✝ :: tail✝
w : Word { x // x ∈ G.Z }
h_rhs : a✝ = Sum.inr <$> w
⊢ len (cancelLeft (same h) h_lhs h_rhs) = 0
Tactic:
simp [cancelLeft]
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
a✝¹ a✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : a✝¹ = a✝
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : a✝¹ = Sum.inr val✝ :: tail✝
w : Word { x // x ∈ G.Z }
h_rhs : a✝ = Sum.inr <$> w
⊢ len (same ⋯) = 0
Theorem: Grammar.Derivation.cancelLeft_len_same
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
a✝¹ a✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : a✝¹ = a✝
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : a✝¹ = Sum.inr val✝ :: tail✝
w : Word { x // x ∈ G.Z }
h_rhs : a✝ = Sum.inr <$> w
⊢ len (same ⋯) = 0
Tactic:
unfold len
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
a✝¹ a✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : a✝¹ = a✝
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : a✝¹ = Sum.inr val✝ :: tail✝
w : Word { x // x ∈ G.Z }
h_rhs : a✝ = Sum.inr <$> w
⊢ 0 = 0
Theorem: Grammar.Derivation.cancelLeft_len_same
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
a✝¹ a✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : a✝¹ = a✝
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : a✝¹ = Sum.inr val✝ :: tail✝
w : Word { x // x ∈ G.Z }
h_rhs : a✝ = Sum.inr <$> w
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Grammar.Derivation.cancelLeft_len
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : lhs = Sum.inr val✝ :: tail✝
a✝ : Word { x // x ∈ G.Z }
h_rhs : rhs = Sum.inr <$> a✝
d : Derivation G lhs rhs
⊢ len (cancelLeft d h_lhs h_rhs) = len d
Tactic:
match d with
| .same _ => simp [len]
| .step _ _ _ =>
  simp [len]
  apply cancelLeft_len
Proof state after:
no goals
Theorem: Grammar.Derivation.cancelLeft_len
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : lhs = Sum.inr val✝ :: tail✝
a✝ : Word { x // x ∈ G.Z }
h_rhs : rhs = Sum.inr <$> a✝
d : Derivation G lhs rhs
h✝ : lhs = rhs
⊢ len (cancelLeft (same h✝) h_lhs h_rhs) = len (same h✝)
Tactic:
simp [len]
Proof state after:
no goals
Theorem: Grammar.Derivation.cancelLeft_len
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : lhs = Sum.inr val✝ :: tail✝
a✝ : Word { x // x ∈ G.Z }
h_rhs : rhs = Sum.inr <$> a✝
d : Derivation G lhs rhs
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step✝ : DerivationStep G lhs
x✝ : Derivation G u'✝ rhs
sound✝ : DerivationStep.result step✝ = u'✝
⊢ len (cancelLeft (step step✝ x✝ sound✝) h_lhs h_rhs) = len (step step✝ x✝ sound✝)
Tactic:
simp [len]
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : lhs = Sum.inr val✝ :: tail✝
a✝ : Word { x // x ∈ G.Z }
h_rhs : rhs = Sum.inr <$> a✝
d : Derivation G lhs rhs
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step✝ : DerivationStep G lhs
x✝ : Derivation G u'✝ rhs
sound✝ : DerivationStep.result step✝ = u'✝
⊢ len (cancelLeft x✝ ⋯ h_rhs) = len x✝
Theorem: Grammar.Derivation.cancelLeft_len
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : lhs = Sum.inr val✝ :: tail✝
a✝ : Word { x // x ∈ G.Z }
h_rhs : rhs = Sum.inr <$> a✝
d : Derivation G lhs rhs
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step✝ : DerivationStep G lhs
x✝ : Derivation G u'✝ rhs
sound✝ : DerivationStep.result step✝ = u'✝
⊢ len (cancelLeft x✝ ⋯ h_rhs) = len x✝
Tactic:
apply cancelLeft_len
Proof state after:
no goals