feat: context-free languages closure reversal #7666
Conversation
madvorak
commented
Oct 13, 2023
madvorak
commented
| cases g with | ||
| | mk => simp [reverseGrammar, dual_reverseRule, List.map_map, List.map_id] | ||
|
|
||
| private lemma derives_reverse {g : ContextFreeGrammar T} {s : List (Symbol T g.NT)} |
There was a problem hiding this comment.
I'm not sure all of these things should be private, making things private generally just makes it harder for other people to prove things about them
There was a problem hiding this comment.
I guess the question is if there are any possible other results whose proof would make use of reverseGrammar?
There was a problem hiding this comment.
I don't think so.
| ∃ g : ContextFreeGrammar.{uT} T, g.language = L | ||
|
|
||
| /-- `L.reverse` is a language that contains exactly all words from `L` backwards. -/ | ||
| def Language.reverse (L : Language T) : Language T := { w : List T | w.reverse ∈ L } |
There was a problem hiding this comment.
should go in Mathlib.Computability.Language
There was a problem hiding this comment.
and we should add the basic lemmas for it, i.e. the reverse of the zero and 1 language, reverse of union of two languages, concatenation etc
There was a problem hiding this comment.
Done. Please check the names of Language.reverse_something lemmas.
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
madvorak
added
awaiting-author
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
madvorak
removed
the
awaiting-author
leanprover-community-mathlib4-bot
added
the
merge-conflict
|
I'll split it into two PRs. |
|
-> #8629 |
