feat: add Cslib/Computability/Languages/OmegaLanguage.lean

[ctchou]

This is the first version of OmegaLanguage, which is an analogue of Mathlib.Computability.Language, but for infinite sequences. We now have a more satisfactory definition of omegaPow, which enables more algebraic and much shorter proofs of the harder results (see the "main theorems" section of the main comment in OmegaLanguage.lean) than in:
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/Languages/Basic.lean
The results proved so far are sufficient for starting the development of the theory of omega-automata. The main TODOs are results about omegaPow and map, which are not needed for now.

As part of this work, we added several new definitions and theorems about Language and OmegaSequence.flatten. We also took this opportunity to change some infelicitous theorem names in Flatten.lean and Segment.lean and to use namespace Nat to remove the prefix Nat. from many places in Segment.lean.

[ctchou]

Rebase on the current "omega-flatten".

[chenson2018]

I did a little less grind golfing this review. Partly because you'd already done a bit, partly because you used more of simp (which is fine). The places I did make grind suggestions are where I felt it was particularly advantageous or you had some awkwardness in switching back and forth from simp to grind.

[ctchou]

@chenson2018's comments have been incorporated.

[ctchou]

OK, I got rid of Language.le_one and all uses of sdiff on languages. Now the definition of omegaPow uses - instead of \ and all previous occurrences of l.le_one are replaced by l ≤ 1.

I am done reviewing, I will leave for Fabrizio to review/merge. Please open an issue regarding the Mathlib PR dependency, we have a "pending upstream" tag to track these.

[ctchou]

I created a new issue (#132) to track the mathlib PR dependency. But I can't figure out how to assign the label "pending upstream" to the issue. @chenson2018, any idea how?

[chenson2018]

I added the label, maybe a permissions problem.

[ctchou]

Yes, probably a permission issue. There is nothing I can click about labels, thought I see them on the RHS.

[ctchou]

Merge in the current main to make sure that there is no conflict.