feat: prove that an omega-language is regular iff it is a finite union of omega-languages of a special form #249
Conversation
|
Rebase on #241. |
|
Rebase on #241. |
ctchou
force-pushed
the
na-pair
branch
4 times, most recently
from
60317ee to
558cd6e
Compare
|
Rebase on #241 . |
|
Rebase on #241, which includes the move to the new module system. |
…n of omega-languages of a special form
|
Rebase on upstream/main. |
|
|
||
| /-- The ω-language accepted by a finite-state Büchi automaton is the finite union of ω-languages | ||
| of the form `L * M^ω`, where all `L`s and `M`s are regular languages. -/ | ||
| theorem language_eq_fin_iSup_hmul_omegaPow |
There was a problem hiding this comment.
If you try to open the LTS scope here, grind times out on some proofs, which is a bit at odds with us right above adding an annotation for LTS.mem_pairLang.
Soon there will be an equivalent for simp sets for grind, where you can specify custom sets of grind rules as opposed to having everything attached to scopes. I think this could help separate out what I think are problems with the LTS annotations being too costly. It would be helpful for me if you can think a bit about what grind sets you might like for automata once core releases this feature, e.g. one set for all of automata or if more refinement is helpful.
There was a problem hiding this comment.
I'm not even sure what "simp sets" are. Is there an example I can look at?
There was a problem hiding this comment.
Ah sorry. There is documentation here and you can find some examples in Mathlib.
It is just a way of organizing simp rules past them all being in one default set. So when this feature is released we can specify which grind rules should run for automata. The benefit should be nicer syntax because you'll have less open scoped and performance by not having to bring in every annotation that LTS uses.
| (hm : ss 0 = t) : ∃ ss', lts.ωTr ss' (μl ++ω μs) ∧ ss' 0 = s ∧ ss' μl.length = t := by | ||
| theorem LTS.ωTr.append | ||
| (hmtr : lts.MTr s μl t) (hωtr : lts.ωTr ss μs) (hm : ss 0 = t) : | ||
| ∃ ss', lts.ωTr ss' (μl ++ω μs) ∧ ss' 0 = s ∧ ss' μl.length = t ∧ ss'.drop μl.length = ss := by |
There was a problem hiding this comment.
Should this new condition have been here from the initial addition of this theorem?
There was a problem hiding this comment.
Not sure what exactly you mean. The new conjunct ss'.drop μl.length = ss asserts that ss' has ss as an infinite suffix. Since ss is among the antecedents of this theorem, this conjunct "anchors" the ss' asserted to exist by the theorem by fixing its suffix.
2 participants
This PR proves that an ω-language is regular iff it is the finite union of ω-languages of the form
L * M^ω, where allLs andMs are regular languages. In addition to being of independent interest, thiss result will also be used in proving that ω-regular languages are closed under complementation, where the complement of an ω-regular language will be given as a finite union of this form. As part of this PR, we prove the theoremLTS.ωTr.flatten, which says that an infinite sequence of finite executions of a LTS connecting an infinite sequence of intermediate states can be concatenated into an infinite execution of the LTS. We also use this theorem to simplify the proof ofloop_run_existsin Loop.lean.