ContextFreeGrammar.Derives.append_right
theorem ContextFreeGrammar.Derives.append_right :
∀ {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)},
g.Derives v w → ∀ (p : List (Symbol T g.NT)), g.Derives (v ++ p) (w ++ p)
This theorem states that for any given context-free grammar `g` and any types `T`, `v`, and `w` that are lists of symbols in `g`, if `g` derives `v` from `w`, then for any list `p` of symbols in `g`, `g` also derives `v` concatenated with `p` from `w` concatenated with `p`. In other words, adding the same suffix to both sides of a derivation in a context-free grammar doesn't affect the derivation relation.
More concisely: If a context-free grammar derives `v` from `w`, then for any suffix `p`, it also derives `v`concatenated with `p` from `w` concatenated with `p`.
|
ContextFreeRule.Rewrites.append_right
theorem ContextFreeRule.Rewrites.append_right :
∀ {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {v w : List (Symbol T N)},
r.Rewrites v w → ∀ (p : List (Symbol T N)), r.Rewrites (v ++ p) (w ++ p)
This theorem states that for any types `T` and `N`, any context-free rule `r`, and any lists `v` and `w` of symbols from `T` and `N`, if `r` rewrites `v` to `w`, then for any list `p` of symbols from `T` and `N`, `r` also rewrites the concatenation of `v` and `p` to the concatenation of `w` and `p`. Essentially, this theorem ensures that adding extra postfixes to both sides of a context-free rewriting rule does not alter the rule's validity.
More concisely: If `r` is a context-free rule that rewrites `v` to `w`, then `r` rewrites `vxi` to `wick` for any lists `xi` of symbols from the same types as `v` and `w`.
|
ContextFreeRule.rewrites_iff
theorem ContextFreeRule.rewrites_iff :
∀ {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} (u v : List (Symbol T N)),
r.Rewrites u v ↔ ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
The theorem `ContextFreeRule.rewrites_iff` states that, for any types `T` and `N`, and any context-free grammar rule `r` of type `ContextFreeRule T N`, a string `u` can be rewritten to a string `v` by rule `r` if and only if there exist a prefix `p` and a postfix `q` such that `u` is the concatenation of `p`, the nonterminal symbol of `r`'s input, and `q`, and `v` is the concatenation of `p`, the output of `r`, and `q`. This suggests that the rule `r` transforms the substring of `u` that matches its input into its output, while leaving the rest of `u` (the prefix and postfix) untouched.
More concisely: For any context-free grammar rule `r` and strings `u`, `v`, there exists prefix `p` and postfix `q` such that `u = pXq` and `v = pYq` if and only if `X` can be rewritten to `Y` by rule `r`, where `X` is the input symbol of `r` and `Y` is its output.
|
ContextFreeGrammar.Produces.append_right
theorem ContextFreeGrammar.Produces.append_right :
∀ {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)},
g.Produces v w → ∀ (p : List (Symbol T g.NT)), g.Produces (v ++ p) (w ++ p)
This theorem states that for any context-free grammar `g`, if `g` can produce a string `w` from a string `v`, then `g` can also produce the string `w` appended with any other string `p` from the string `v` appended with the same string `p`. Here, `v`, `w`, and `p` are all lists of symbols from the nonterminal set of `g`, denoted as `g.NT`.
More concisely: If a context-free grammar `g` can generate string `w` from string `v`, then it can also generate `w` concatenated with any string `p` that can be generated from `v` concatenated with `p`.
|
ContextFreeGrammar.Produces.append_left
theorem ContextFreeGrammar.Produces.append_left :
∀ {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)},
g.Produces v w → ∀ (p : List (Symbol T g.NT)), g.Produces (p ++ v) (p ++ w)
This theorem states that for any context-free grammar `g`, if `v` produces `w` in `g`, then prepending any list `p` to `v` will also produce the list `p` prepended to `w` in the same context-free grammar. In other words, it says that if a sequence of symbols `v` can be transformed into another sequence `w` using the productions/rules of the context-free grammar, then the same transformation can be applied when `v` and `w` are prefixed with the same sequence of symbols `p`.
More concisely: If a context-free grammar generates sequence `w` from sequence `v`, then it also generates the sequence `p` followed by `w` from the sequence `p` followed by `v`.
|
ContextFreeRule.Rewrites.append_left
theorem ContextFreeRule.Rewrites.append_left :
∀ {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {v w : List (Symbol T N)},
r.Rewrites v w → ∀ (p : List (Symbol T N)), r.Rewrites (p ++ v) (p ++ w)
This theorem states that for any types `T` and `N`, given a context-free rule `r` and two lists `v` and `w` of symbols of these types, if `r` rewrites `v` to `w`, then for any other list `p` of symbols, `r` will also rewrite `p` concatenated with `v` to `p` concatenated with `w`. In other words, you can add an extra prefix to the input and output of context-free rewriting without affecting the ability of the rule to perform the rewriting.
More concisely: If `r` is a context-free rule and `v` and `w` are lists such that `r` rewrites `v` to `w`, then `r` rewrites `p` concatenated with `v` to `p` concatenated with `w` for all lists `p`.
|
ContextFreeGrammar.mem_language_iff
theorem ContextFreeGrammar.mem_language_iff :
∀ {T : Type uT} (g : ContextFreeGrammar T) (w : List T),
w ∈ g.language ↔ g.Derives [Symbol.nonterminal g.initial] (List.map Symbol.terminal w)
This theorem is stating that a specific word `w` is part of the language produced by a context-free grammar `g` if and only if the grammar `g` can derive the word `w` from its initial nonterminal symbol in a certain number of steps. In this context, the word `w` is viewed as a list of symbols, and the `List.map Symbol.terminal w` part is mapping each symbol in `w` to a terminal symbol in the grammar. This theorem provides a formal connection between the membership of a word in a language generated by a context-free grammar and the derivation process of the grammar.
More concisely: A word `w` belongs to the language generated by context-free grammar `g` if and only if `g` can derive `w` from its initial nonterminal symbol in a finite number of steps, where `w` is viewed as a list of terminal symbols in `g`.
|
ContextFreeGrammar.Derives.append_left
theorem ContextFreeGrammar.Derives.append_left :
∀ {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)},
g.Derives v w → ∀ (p : List (Symbol T g.NT)), g.Derives (p ++ v) (p ++ w)
This theorem, `ContextFreeGrammar.Derives.append_left`, states that for any context-free grammar `g`, and for any two lists of symbols `v` and `w` derived from `g`, if `g` derives `v` to `w`, then for any extra prefix `p`, `g` also derives the list `p` appended to `v` to the list `p` appended to `w`. In other words, deriving a string in a context-free grammar can be extended with a common prefix.
More concisely: If a context-free grammar derives a sequence `v` to `w`, then for any prefix `p`, it also derives `p` concatenated with `v` to `p` concatenated with `w`.
|