feat: prove that the Buchi congruence has the saturation property

[ctchou]

This PR proves that the Buchi congruence introduced in #278 has the saturation property defined in Cslib.Foundations.Data.Set.Saturation. More precisely, the family of omega-languages of the form U * V^ω, where U and V are equivalence classes of the Buchi congruence, saturates the omega-language accepted by the underlying Buchi automaton. This proof is the hardest step in proving the closure of ω-regular languages under complementation and explains why the Buchi congruence is defined the way it is. Some miscellaneous results about LTS and infinite sequences that are needed by the proof are also added.

[chenson2018]

As I mention I've not fully reviewed buchiFamily_saturation, but here is an initial review.

[fmontesi]

Looks pretty good to me, just minor things.

[chenson2018]

My delay in approving this is because of buchiFamily_saturation. I have looked at this off and on and could make some incremental grind improvements, but I don't have the subject expertise here. Is there anything that can be split off in separate lemmas? The existential from mem_buchiFamily seems to make this awkward, but is there any way this could be reworked more cleanly?

[ctchou]

We can work on this after I get back from my trip on March 12. I don't have my laptop with me now.

[ctchou]

@chenson2018 Could you elaborate on your last comment? I'm not sure I understand it. buchiFamly is an indexed family of omega-regular languages, where each index is a pair of equivalence classes of na.BuchiCongruence. The theorem men_buchiFamily merely relates a member of such a language with the two equivalence classes of its index. I don't think the proof of buchiFamily_saturation can be simplified much. If you still have the survey article by W. Thomas I sent you, this proof is essentially a formalization of the proof of part (a) of lemma 2.2 on page 140.

[chenson2018]

@ctchou Let me take another look and at least add the cleanups to grind usage I'd done locally. My question was essentially if you can rephrase the existentials to be "constructive" so it'd be easier to extract some smaller lemmas.

[ctchou]

I don't think that's possible. In essence, here we are starting with something like x ∈ U * V^ω. Both the concatenation operation * and the omega power operation ^ω are essentially nondeterministic operations. For example, x ∈ U * V^ω merely says that x is the concatenation of some finite sequence from U followed by some infinite sequence from V^ω. We have no other information and no way to avoid the existential quantifiers.