Leftmost Deriviations in Context-Free Gammars

This file contains the definition of a leftmost deriviation. These are deriviations where in each rewriting step the leftmost nonterminal is replaced

Main Definitions

• ContextFreeRule.RewritesLeftmost: Leftmost counterpart to ContextFreeRule.Rewrites
• ContextFreeGrammar.ProducesLeftmost: Leftmost counterpart to ContextFreeRule.Produces
• ContextFreeGrammar.DerivesLeftmost: Leftmost counterpart to ContextFreeRule.Derives

Main Result

• ContextFreeGrammar.derives_leftmost_iff : A string of terminals can be derived from a string of symbols iff it can be leftmost derived.

inductive ContextFreeRule.RewritesLeftmost {T : Type uT} {N : Type uN} (r : ContextFreeRule T N) : List (Symbol T N) → List (Symbol T N) → Prop

• head {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} (s : List (Symbol T N)) : r.RewritesLeftmost (Symbol.nonterminal r.input :: s) (r.output ++ s)

  The replaced nonterminal is the leftmost symbol

• cons {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} (x : T) {s₁ s₂ : List (Symbol T N)} (hrs : r.RewritesLeftmost s₁ s₂) : r.RewritesLeftmost (Symbol.terminal x :: s₁) (Symbol.terminal x :: s₂)

  There are terminals further left than the replaced symbol

theorem ContextFreeRule.RewritesLeftmost.exists_parts {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u v : List (Symbol T N)} (hr : r.RewritesLeftmost u v) : ∃ (p : List T) (q : List (Symbol T N)), u = List.map Symbol.terminal p ++ [Symbol.nonterminal r.input] ++ q ∧ v = List.map Symbol.terminal p ++ r.output ++ q

theorem ContextFreeRule.RewritesLeftmost.rewrites_leftmost_of_exists_parts {T : Type uT} {N : Type uN} (r : ContextFreeRule T N) (p : List T) (q : List (Symbol T N)) : r.RewritesLeftmost (List.map Symbol.terminal p ++ [Symbol.nonterminal r.input] ++ q) (List.map Symbol.terminal p ++ r.output ++ q)

theorem ContextFreeRule.RewritesLeftmost.rewrites_leftmost_iff {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u v : List (Symbol T N)} : r.RewritesLeftmost u v ↔ ∃ (p : List T) (q : List (Symbol T N)), u = List.map Symbol.terminal p ++ [Symbol.nonterminal r.input] ++ q ∧ v = List.map Symbol.terminal p ++ r.output ++ q

theorem ContextFreeRule.RewritesLeftmost.rewrite_terminal {T : Type uT} {N : Type uN} (r : ContextFreeRule T N) (w : List T) (u : List (Symbol T N)) : ¬r.RewritesLeftmost (List.map Symbol.terminal w) u

theorem ContextFreeRule.RewritesLeftmost.append_left {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {v w : List (Symbol T N)} (hr : r.RewritesLeftmost v w) (p : List T) : r.RewritesLeftmost (List.map Symbol.terminal p ++ v) (List.map Symbol.terminal p ++ w)

theorem ContextFreeRule.RewritesLeftmost.append_right {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {v w : List (Symbol T N)} (hr : r.RewritesLeftmost v w) (p : List (Symbol T N)) : r.RewritesLeftmost (v ++ p) (w ++ p)

theorem ContextFreeRule.RewritesLeftmost.rewrites_of_rewrites_leftmost {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u v : List (Symbol T N)} (hr : r.RewritesLeftmost u v) : r.Rewrites u v

theorem ContextFreeRule.rewrites_leftmost_cons {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {x : Symbol T N} {v u : List (Symbol T N)} (h : r.RewritesLeftmost (x :: v) u) : (∃ (u₁ : List (Symbol T N)) (u₂ : List (Symbol T N)), u = u₁ ++ u₂ ∧ r.RewritesLeftmost [x] u₁ ∧ u₂ = v) ∨ ∃ (w₁ : List T) (u₂ : List (Symbol T N)), u = List.map Symbol.terminal w₁ ++ u₂ ∧ [x] = List.map Symbol.terminal w₁ ∧ r.RewritesLeftmost v u₂

theorem ContextFreeRule.rewrites_leftmost_append {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {v₁ v₂ u : List (Symbol T N)} (h : r.RewritesLeftmost (v₁ ++ v₂) u) : (∃ (u₁ : List (Symbol T N)) (u₂ : List (Symbol T N)), u = u₁ ++ u₂ ∧ r.RewritesLeftmost v₁ u₁ ∧ u₂ = v₂) ∨ ∃ (w₁ : List T) (u₂ : List (Symbol T N)), u = List.map Symbol.terminal w₁ ++ u₂ ∧ v₁ = List.map Symbol.terminal w₁ ∧ r.RewritesLeftmost v₂ u₂

theorem ContextFreeRule.rewrites_cons {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {x : Symbol T N} {v u : List (Symbol T N)} (h : r.Rewrites (x :: v) u) : ∃ (u₁ : List (Symbol T N)) (u₂ : List (Symbol T N)), u = u₁ ++ u₂ ∧ (r.Rewrites [x] u₁ ∧ u₂ = v ∨ r.Rewrites v u₂ ∧ [x] = u₁)

theorem ContextFreeRule.rewrites_append {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {v₁ v₂ u : List (Symbol T N)} (h : r.Rewrites (v₁ ++ v₂) u) : ∃ (u₁ : List (Symbol T N)) (u₂ : List (Symbol T N)), u = u₁ ++ u₂ ∧ (r.Rewrites v₁ u₁ ∧ v₂ = u₂ ∨ r.Rewrites v₂ u₂ ∧ v₁ = u₁)

def ContextFreeGrammar.ProducesLeftmost {T : Type uT} (g : ContextFreeGrammar T) (u v : List (Symbol T g.NT)) : Prop

Given a context-free grammar g and strings u and v g.ProducesLeftmost u v means that one application of a rule from g to the leftmost nonterminal of u send u to v.

Equations

• g.ProducesLeftmost u v = ∃ r ∈ g.rules, r.RewritesLeftmost u v

@[reducible, inline]

abbrev ContextFreeGrammar.DerivesLeftmost {T : Type uT} (g : ContextFreeGrammar T) : List (Symbol T g.NT) → List (Symbol T g.NT) → Prop

Given a context-free grammar g and strings u and v g.DerivesLeftmost u v means that g can transform u to v in some number of rewriting steps, by applying the transformation always to the leftmost symbol of u.

Equations

• g.DerivesLeftmost = Relation.ReflTransGen g.ProducesLeftmost

theorem ContextFreeGrammar.DerivesLeftmost.refl {T : Type uT} {g : ContextFreeGrammar T} (w : List (Symbol T g.NT)) : g.DerivesLeftmost w w

theorem ContextFreeGrammar.ProducesLeftmost.single {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.ProducesLeftmost v w) : g.DerivesLeftmost v w

theorem ContextFreeGrammar.DerivesLeftmost.trans {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} (huv : g.DerivesLeftmost u v) (hvw : g.DerivesLeftmost v w) : g.DerivesLeftmost u w

theorem ContextFreeGrammar.DerivesLeftmost.trans_produces {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} (huv : g.DerivesLeftmost u v) (hvw : g.ProducesLeftmost v w) : g.DerivesLeftmost u w

theorem ContextFreeGrammar.Leftmost.trans_derives {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} (huv : g.ProducesLeftmost u v) (hvw : g.DerivesLeftmost v w) : g.DerivesLeftmost u w

theorem ContextFreeGrammar.DerivesLeftmost.eq_or_head {T : Type uT} {g : ContextFreeGrammar T} {u w : List (Symbol T g.NT)} (huw : g.DerivesLeftmost u w) : u = w ∨ ∃ (v : List (Symbol T g.NT)), g.ProducesLeftmost u v ∧ g.DerivesLeftmost v w

theorem ContextFreeGrammar.DerivesLeftmost.eq_or_tail {T : Type uT} {g : ContextFreeGrammar T} {u w : List (Symbol T g.NT)} (huw : g.DerivesLeftmost u w) : u = w ∨ ∃ (v : List (Symbol T g.NT)), g.DerivesLeftmost u v ∧ g.ProducesLeftmost v w

theorem ContextFreeGrammar.ProducesLeftmost.append_left {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.ProducesLeftmost v w) (p : List T) : g.ProducesLeftmost (List.map Symbol.terminal p ++ v) (List.map Symbol.terminal p ++ w)

Add extra prefix to context-free leftmost producing.

theorem ContextFreeGrammar.ProducesLeftmost.append_right {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.ProducesLeftmost v w) (p : List (Symbol T g.NT)) : g.ProducesLeftmost (v ++ p) (w ++ p)

Add extra postfix to context-free leftmost producing.

theorem ContextFreeGrammar.DerivesLeftmost.append_left {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.DerivesLeftmost v w) (p : List T) : g.DerivesLeftmost (List.map Symbol.terminal p ++ v) (List.map Symbol.terminal p ++ w)

Add extra prefix to context-free leftmost deriving.

theorem ContextFreeGrammar.DerivesLeftmost.append_right {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.DerivesLeftmost v w) (p : List (Symbol T g.NT)) : g.DerivesLeftmost (v ++ p) (w ++ p)

Add extra postfix to context-free leftmost deriving.

theorem ContextFreeGrammar.produces_of_produces_leftmost {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (h : g.ProducesLeftmost u v) : g.Produces u v

theorem ContextFreeGrammar.derives_of_derives_leftmost {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (h : g.DerivesLeftmost u v) : g.Derives u v

theorem ContextFreeGrammar.derives_leftmost_cons {T : Type uT} {g : ContextFreeGrammar T} {x : Symbol T g.NT} {v u : List (Symbol T g.NT)} (h : g.DerivesLeftmost (x :: v) u) : (∃ (u' : List (Symbol T g.NT)), u = u' ++ v ∧ g.DerivesLeftmost [x] u') ∨ ∃ (w₁ : List T) (u₂ : List (Symbol T g.NT)), u = List.map Symbol.terminal w₁ ++ u₂ ∧ g.DerivesLeftmost [x] (List.map Symbol.terminal w₁) ∧ g.DerivesLeftmost v u₂

theorem ContextFreeGrammar.derives_leftmost_append {T : Type uT} {g : ContextFreeGrammar T} {v₁ v₂ u : List (Symbol T g.NT)} (h : g.DerivesLeftmost (v₁ ++ v₂) u) : (∃ (u' : List (Symbol T g.NT)), u = u' ++ v₂ ∧ g.DerivesLeftmost v₁ u') ∨ ∃ (w₁ : List T) (u₂ : List (Symbol T g.NT)), u = List.map Symbol.terminal w₁ ++ u₂ ∧ g.DerivesLeftmost v₁ (List.map Symbol.terminal w₁) ∧ g.DerivesLeftmost v₂ u₂

theorem ContextFreeGrammar.derives_cons {T : Type uT} {g : ContextFreeGrammar T} {x : Symbol T g.NT} {v u : List (Symbol T g.NT)} (h : g.Derives (x :: v) u) : ∃ (u₁ : List (Symbol T g.NT)) (u₂ : List (Symbol T g.NT)), u = u₁ ++ u₂ ∧ g.Derives [x] u₁ ∧ g.Derives v u₂

theorem ContextFreeGrammar.derives_leftmost_iff {T : Type uT} {g : ContextFreeGrammar T} {w : List T} {α : List (Symbol T g.NT)} : g.DerivesLeftmost α (List.map Symbol.terminal w) ↔ g.Derives α (List.map Symbol.terminal w)