feat: prove that omega-regular languages are closed under finite intersection

[ctchou]

Proving that omega-regular languages are closed under finite intersection is harder than doing so for regular languages and requires the following ingredients:

• NAProd.lean: product construction for NA.
• NAHist.lean: adding history state to NA.
• NABuchiInter: the intersection construction that uses both NAProd and NAHist constructions.
• Temporal.lean: temporal reasoning over infinite sequences that is needed to show that NABuchiInter actually works.

I also renamed {Sum,Prod}.lean to {NASum,DAProd}.lean to keep the file naming scheme consistent.

[chenson2018]

Before I review, I've been meaning to ask about the naming scheme. As you add more files, I think it would be easier to navigate if we organized into subdirectories. What do you think about something like the structure below?

├── Automata
    ├── Acceptor.lean
    ├── DA
    │   ├── Basic.lean
    │   ├── Buchi.lean
    │   ├── Prod.lean
    │   └── ToNA.lean
    ├── NA
    │   ├── Basic.lean
    │   ├── Buchi
    │   │   ├── Equiv.lean
    │   │   └── Inter.lean
    │   ├── Epsilon
    │   │   ├── Basic.lean
    │   │   └── ToNA.lean
    │   ├── Hist.lean
    │   ├── Prod.lean
    │   ├── Sum.lean
    │   └── ToDA.lean
    └── OmegaAcceptor.lean

The details of exactly what directories can be changed as you see fit, I just think in general it could be nicer than the flat structure.

[ctchou]

Actually I like a flat directory better. I really hate the hassle of having to climb up and down in a directory tree when I need to open a file. I'm also not sure a tree structure is any more "rational" than the current naming scheme, which already groups the files in a natural way by the alphabetical order. For example, NABuchiIInter.lean contains a construction that is a composition of the constructions in NAProd.lean and NAHist.lean. There seems to me no good reason why the first file should be placed in a subdirectory while the latter two are not. Also note that if you pursue your logic to its conclusion, you probably should split NA.lean into NA/Basic.lean, NA/FinAcc/Basic.lean, NA/Buchi/Basic.lean, and NA/Muller/Basic.lean. I'm really not sure what that would buy you.

I think we will end up with around 20 files in this directory, which I don't think is excessive.

[chenson2018]

This is not critical at the moment, we can always revisit later. I don't want to introduce too much churn while you are still actively developing the library. Let's table this and I'll just review the PR.

Just to write it down for future reference however, the benefits I see and response to your concerns:

• subdirectories make easier to read names, especially with capitalization e.g. NAHist.lean versus NA/Hist.lean
• subdirectories make it easier to see which files are related to each other. 20 files is not inherently excessive, but it is harder at a glance to see what the overarching areas there are versus just a few things at the top level
• I find your closing argument a bit of a strawman, nothing requires the directory structure to be overly granular
• I don't understand the "hassle of having to climb up and down in a directory tree" argument, as you are still free to work from the top level directory

[ctchou]

I'll do a PR after this one to add four subdirectories under Automata:

• Acceptors
• DA
• NA
• EpsilonNA

and spread the current files among the four. I don't think adding more levels makes sense.