chore: split LTS/Basic.lean into more manageable pieces

[ctchou]

This PR splits Cslib/Foundations/Semantics/LTS/Basic.lean into 7 files with the following dependencies among them:

• Basic.lean
• Execution.lean, which imports Basic.lean
• OmegaExecution.lean, which imports Execution.lean
• Total.lean, which imports OmegaExecution.lean
• HasTau.lean, which imports Basic.lean
• Divergence.lean, which imports HasTau.lean and OmegaExecution.lean
• Union.lean, which imports Basic.lean

Other files which formerly import LTS/Basic.lean now import only the "lowest" necessary file in the above hierarchy. LTS/Basic.lean now imports only Cslib.Init and some mathlib files.

I also took the opportunity to rename a few theorems to more rational and systematic names.

[chenson2018]

Two very small comments, thanks for starting this!

[chenson2018]

One more thought. I think in splitting this up, we should do two more things:

• create a LTS/Defs.lean module that only has definitions
• move the meta section at the bottom into its own module (LTS/Attr.lean, LTS/Meta.lean?). My understanding from discussion on Zulip is that this is preferable for isolating meta imports

[fmontesi]

One more thought. I think in splitting this up, we should do two more things:

• create a LTS/Defs.lean module that only has definitions
• move the meta section at the bottom into its own module (LTS/Attr.lean, LTS/Meta.lean?). My understanding from discussion on Zulip is that this is preferable for isolating meta imports

What would go in LTS/Defs.lean exactly? I'm not sure myself.

[chenson2018]

What would go in LTS/Defs.lean exactly? I'm not sure myself.

I just had the impression that maybe the couple of remaining sections (Termination, Classes) in LTSD/Basic.lean might also be split off. I might be missing how they're interconnected.

[ctchou]

One of my goals is to remove the dependency on OmegaSequence as much as possible from all files that uses LTS (including LTS files themselves). There are quite a few definitions that need OmegaSequence, so I don't think putting all definitions in the single file is a good idea. (BTW, only 3 LTS files uses OmegaSequence now: OmegaExecution.lean, Total.lean, and Divergence.lean. Outside LTS, the first two are imported only by Automata/NA/{Basic,Total}.lean, respectively. Divergence.lean is not used anywhere.)

I'll go ahead with putting Termination and the meta section in its own file. I'm not sure about Classes, because it does not seem to have a coherent theme. Actually I think splitting out Relation related stuff into its own file may make more sense.

[ctchou]

@chenson2018 Thanks for the fix. I'll try to see if I can split out Relation.

[ctchou]

LTS/Relation.lean has been split out. LTS/Basic.lean is now about 300 lines long. This is about as far as I want to go.

[chenson2018]

!radar

[leanprover-radar]

Benchmark results for a8a45a5 against 1119f31 are in. There are no significant changes. @chenson2018

• 🟥 build//instructions: +26.5G (+1.41%)

Small changes (2✅, 11🟥)

• ✅ build/module/Cslib.Foundations.Semantics.LTS.Basic//instructions: -104.6G (-92.17%) (reduced significance based on *//lines)
• ✅ build/module/Cslib.Logics.HML.LogicalEquivalence//instructions: -236.7M (-3.12%)
• 🟥 build/profile/.olean serialization//wall-clock: +425ms (+10.69%)
• 🟥 build/profile/compilation (LCNF base)//wall-clock: +168ms (+15.07%)
• 🟥 build/profile/compilation (LCNF impure)//wall-clock: +38ms (+16.49%)
• 🟥 build/profile/compilation (LCNF mono)//wall-clock: +81ms (+15.82%)
• 🟥 build/profile/elaboration//wall-clock: +974ms (+16.37%)
• 🟥 build/profile/import//wall-clock: +8s (+16.10%)
• 🟥 build/profile/initialization//wall-clock: +300ms (+13.75%)
• 🟥 build/profile/interpretation//wall-clock: +4s (+15.48%)
• 🟥 build/profile/lazy discriminator local search//wall-clock: +0s (+90.00%)
• 🟥 build/profile/parsing//wall-clock: +108ms (+14.43%)
• 🟥 build/profile/process pre-definitions//wall-clock: +155ms (+16.74%)

[chenson2018]

(I think the benchmarking is mostly noise here, just wanted to check to be sure)

[ctchou]

I made the change of using namespace LTS and removing the LTS. prefix as much as possible. Note that some identifiers in TraceEq.lean, Simulation.lean, and Bisimulation.lean were not in the LTS namespace but are now in it. This leads to several other changes elsewhere outside LTS.

[ctchou]

Also, I made the decision of not putting HasTau in the LTS namespace. If you think it should be, let me know.

[fmontesi]

LGTM, thanks!