Rightmost derivations

This file supplies the structural facts about rightmost derivations which are independent of the LR conflict condition. In particular, an ordinary context-free derivation whose result is a terminal word can always be scheduled rightmost.

Counted rightmost derivations

inductive CF_grammar.DerivesRightmostIn {T : Type} (G : CF_grammar T) : ℕ → List (symbol T G.nt) → List (symbol T G.nt) → Prop

A rightmost derivation using exactly n production steps. Unlike DerivesRightmost, this relation retains the measure needed for well-founded arguments which trace a surviving nonterminal back through its ancestors.

• refl {T : Type} {G : CF_grammar T} (w : List (symbol T G.nt)) : G.DerivesRightmostIn 0 w w
• tail {T : Type} {G : CF_grammar T} {n : ℕ} {u v w : List (symbol T G.nt)} : G.DerivesRightmostIn n u v → G.ProducesRightmost v w → G.DerivesRightmostIn (n + 1) u w

theorem CF_grammar.DerivesRightmostIn.derives {T : Type} {G : CF_grammar T} {n : ℕ} {u v : List (symbol T G.nt)} (h : G.DerivesRightmostIn n u v) : G.DerivesRightmost u v

theorem CF_grammar.exists_derivesRightmostIn_of_derivesRightmost {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} (h : G.DerivesRightmost u v) : ∃ (n : ℕ), G.DerivesRightmostIn n u v

theorem CF_grammar.derivesRightmost_iff_exists_derivesRightmostIn {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} : G.DerivesRightmost u v ↔ ∃ (n : ℕ), G.DerivesRightmostIn n u v

theorem CF_grammar.ProducesRightmost.derivesRightmostIn_one {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} (h : G.ProducesRightmost u v) : G.DerivesRightmostIn 1 u v

theorem CF_grammar.DerivesRightmostIn.trans {T : Type} {G : CF_grammar T} {m n : ℕ} {u v w : List (symbol T G.nt)} (huv : G.DerivesRightmostIn m u v) (hvw : G.DerivesRightmostIn n v w) : G.DerivesRightmostIn (m + n) u w

Context closure

theorem CF_grammar.RewritesRightmost.append_left {T N : Type} {r : N × List (symbol T N)} {u v : List (symbol T N)} (h : RewritesRightmost r u v) (pre : List (symbol T N)) : RewritesRightmost r (pre ++ u) (pre ++ v)

theorem CF_grammar.RewritesRightmost.append_terminals_right {T N : Type} {r : N × List (symbol T N)} {u v : List (symbol T N)} (h : RewritesRightmost r u v) (suf : List T) : RewritesRightmost r (u ++ List.map symbol.terminal suf) (v ++ List.map symbol.terminal suf)

theorem CF_grammar.ProducesRightmost.single {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} (h : G.ProducesRightmost u v) : G.DerivesRightmost u v

theorem CF_grammar.ProducesRightmost.append_left {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} (h : G.ProducesRightmost u v) (pre : List (symbol T G.nt)) : G.ProducesRightmost (pre ++ u) (pre ++ v)

theorem CF_grammar.ProducesRightmost.append_terminals_right {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} (h : G.ProducesRightmost u v) (suf : List T) : G.ProducesRightmost (u ++ List.map symbol.terminal suf) (v ++ List.map symbol.terminal suf)

theorem CF_grammar.DerivesRightmost.append_left {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} (h : G.DerivesRightmost u v) (pre : List (symbol T G.nt)) : G.DerivesRightmost (pre ++ u) (pre ++ v)

theorem CF_grammar.DerivesRightmost.append_terminals_right {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} (h : G.DerivesRightmost u v) (suf : List T) : G.DerivesRightmost (u ++ List.map symbol.terminal suf) (v ++ List.map symbol.terminal suf)

theorem CF_grammar.DerivesRightmost.append_to_terminals {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} {wu wv : List T} (hu : G.DerivesRightmost u (List.map symbol.terminal wu)) (hv : G.DerivesRightmost v (List.map symbol.terminal wv)) : G.DerivesRightmost (u ++ v) (List.map symbol.terminal (wu ++ wv))

Rightmost derivations of adjacent pieces can be scheduled from right to left. This is the basic commutation principle used below.

Terminal sentential forms

theorem CF_grammar.not_producesRightmost_map_terminal {T : Type} {G : CF_grammar T} {w : List T} {v : List (symbol T G.nt)} : ¬G.ProducesRightmost (List.map symbol.terminal w) v

theorem CF_grammar.DerivesRightmost.eq_of_map_terminal_source {T : Type} {G : CF_grammar T} {w : List T} {v : List (symbol T G.nt)} (h : G.DerivesRightmost (List.map symbol.terminal w) v) : v = List.map symbol.terminal w

Splitting rightmost derivations

theorem CF_grammar.ProducesRightmost.append_cases {T : Type} {G : CF_grammar T} {u v x : List (symbol T G.nt)} (h : G.ProducesRightmost (u ++ v) x) : (∃ (u' : List (symbol T G.nt)) (wv : List T), v = List.map symbol.terminal wv ∧ x = u' ++ v ∧ G.ProducesRightmost u u') ∨ ∃ (v' : List (symbol T G.nt)), x = u ++ v' ∧ G.ProducesRightmost v v'

A rightmost step in an append either occurs in the right component, or it occurs in the left component after the right component is already terminal.

theorem CF_grammar.ProducesRightmost.preimage_nonterminal {T : Type} {G : CF_grammar T} {y p q : List (symbol T G.nt)} {A : G.nt} (h : G.ProducesRightmost y (p ++ [symbol.nonterminal A] ++ q)) : (∃ (q₀ : List (symbol T G.nt)), y = p ++ [symbol.nonterminal A] ++ q₀ ∧ G.ProducesRightmost q₀ q) ∨ ∃ r ∈ G.rules, ∃ (p₀ : List (symbol T G.nt)) (α : List (symbol T G.nt)) (β : List (symbol T G.nt)) (t : List T), r.2 = α ++ [symbol.nonterminal A] ++ β ∧ p = p₀ ++ α ∧ q = β ++ List.map symbol.terminal t ∧ y = p₀ ++ [symbol.nonterminal r.1] ++ List.map symbol.terminal t

Trace a nonterminal in the result of one rightmost step. It was either already to the left of the rewritten (rightmost) nonterminal, or it occurs in the right-hand side of the rule used by the step.

theorem CF_grammar.DerivesRightmost.append_to_terminals_split {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} {w : List T} (h : G.DerivesRightmost (u ++ v) (List.map symbol.terminal w)) : ∃ (wu : List T) (wv : List T), w = wu ++ wv ∧ G.DerivesRightmost u (List.map symbol.terminal wu) ∧ G.DerivesRightmost v (List.map symbol.terminal wv)

A derivation of an append to a terminal word uniquely separates into rightmost derivations of its two components.

Ancestry of a surviving nonterminal

theorem CF_grammar.derivesRightmost_nonterminal_ancestry {T : Type} (G : CF_grammar T) {p : List (symbol T G.nt)} {A : G.nt} {s : List T} (h : G.DerivesRightmost [symbol.nonterminal G.initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal s)) : p = [] ∧ A = G.initial ∧ s = [] ∨ ∃ r ∈ G.rules, ∃ (p₀ : List (symbol T G.nt)) (α : List (symbol T G.nt)) (β : List (symbol T G.nt)) (t : List T) (z : List T), r.2 = α ++ [symbol.nonterminal A] ++ β ∧ p = p₀ ++ α ∧ s = z ++ t ∧ G.DerivesRightmost [symbol.nonterminal G.initial] (p₀ ++ [symbol.nonterminal r.1] ++ List.map symbol.terminal t) ∧ G.DerivesRightmost β (List.map symbol.terminal z)

A nonterminal surviving in a right-sentential form is either the untouched start symbol, or descends from a concrete occurrence in the right-hand side of a rule. The rule's suffix derives exactly the terminal segment immediately following that occurrence; the remaining terminal suffix was already present when the rule was applied.

theorem CF_grammar.derivesRightmostIn_nonterminal_ancestry {T : Type} (G : CF_grammar T) {n : ℕ} {p : List (symbol T G.nt)} {A : G.nt} {s : List T} (h : G.DerivesRightmostIn n [symbol.nonterminal G.initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal s)) : p = [] ∧ A = G.initial ∧ s = [] ∨ ∃ (m : ℕ), ∃ r ∈ G.rules, ∃ (p₀ : List (symbol T G.nt)) (α : List (symbol T G.nt)) (β : List (symbol T G.nt)) (t : List T) (z : List T), m < n ∧ r.2 = α ++ [symbol.nonterminal A] ++ β ∧ p = p₀ ++ α ∧ s = z ++ t ∧ G.DerivesRightmostIn m [symbol.nonterminal G.initial] (p₀ ++ [symbol.nonterminal r.1] ++ List.map symbol.terminal t) ∧ G.DerivesRightmost β (List.map symbol.terminal z)

Counted form of derivesRightmost_nonterminal_ancestry. In the non-base case the parent prehandle is reached in strictly fewer steps than the displayed surviving configuration. This strict measure supports terminating reverse item-closure and ancestry arguments even when the grammar contains cycles.

Equivalence with unrestricted scheduling on terminal results

theorem CF_grammar.transforms_of_producesRightmost {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} (h : G.ProducesRightmost u v) : CF_transforms G u v

theorem CF_grammar.derives_of_derivesRightmost {T : Type} {G : CF_grammar T} {u v : List (symbol T G.nt)} (h : G.DerivesRightmost u v) : CF_derives G u v

theorem CF_grammar.derivesRightmost_of_derives {T : Type} {G : CF_grammar T} {u : List (symbol T G.nt)} {w : List T} (h : CF_derives G u (List.map symbol.terminal w)) : G.DerivesRightmost u (List.map symbol.terminal w)

Every context-free derivation ending in terminals has a rightmost scheduling.

theorem CF_grammar.derivesRightmost_iff {T : Type} {G : CF_grammar T} {u : List (symbol T G.nt)} {w : List T} : G.DerivesRightmost u (List.map symbol.terminal w) ↔ CF_derives G u (List.map symbol.terminal w)