feat: topological characterization of safety and liveness properties of infinite sequences

[ctchou]

This PR formalizes some results in the following classic paper:

Alpern, Bowen; Schneider, Fred B. (1985). "Defining liveness". Information Processing Letters. 21 (4): 181–185.

To wit:

• By viewing an infinite sequence as an infinite product, we define a topology on infinite sequences using the product topology.
• We identify safety and liveness properties with closed and dense sets in this topology and justify these identifications.
• We prove that every property is the intersection of a safety property and a liveness property and give explicit formulas for both.

Zulip discussion: #CSLib: PR reviews > #704: Topological characterization of safety and liveness

[thomaskwaring]

this mostly looks good to me! the results are very nice.

personally, i would prefer to avoid the definition SafetyLivenessDecomposition unless it is expected to be used elsewhere. i also think results characterising the parts of the definition in the theorem would be nice either way, eg:

theorem isSafety_closure (p : ωLanguage α) : p.closure.IsSafety := sorry

theorem isLiveness_sup_compl_closure (p : ωLanguage α) : (p ⊔ p.closureᶜ).IsLiveness := sorry

and in the presence of these, you could have a lemma saying p = p.closure ⊓ (p ⊔ p.closureᶜ), and replace exists_safetyLivenessDecomposition with an existence statement:

theorem exists_safetyLivenessDecomposition (p : ωLanguage α) : ∃ q r : ωLanguage α, q.IsSafety ∧ r.IsLiveness ∧ p = q ⊓ r := sorry

That being said I don't feel strongly on this and I'm happy to defer to your and other reviewers' preferences.

As I mentioned on Zulip, I think the results of ClosedDenseDecomposition can be inlined — the results are not explicitly used in any statements or definitions (ie they are not user-facing) and the proof of SafetyLivenessDecomposition_exists would not be made longer by omitting the import. I see your point about emphasising the topological fact as independent of the space in question, but I'm not sure the current design actually shows that off — maybe a note in the docstring would be better.

Finally, I think the proofs in OmegaSequence/Topology are good as they are, but it does feel like they ought to be able to be golfed. (In particular, why doesn't mathlib have a result saying you can pull back a topological basis along a homeomorphism??) If you agree I am happy to try, but I have no problem with them being merged as is.

Excuse the essay-length review, on the whole I think the PR is great :)

[thomaskwaring]

maybe the fact that ωSequence α ≃ ℕ → α can be split out (sorry if that already exists) so that this follows from α ≃ WithDiscreteTopology α and a congruence lemma for Equiv (EDIT: the latter equiv doesn't exist in mathlib so ignore this comment until such a time as it does)

[ctchou]

@thomaskwaring I have followed your suggestion and removed the definition SafetyLivenessDecomposition and the file Data/Topology/ClosedDenseDecomposition.lean. Do you want to do the golfing in OmegaSequence/Topology, now that you've found the support in mathlib?
#Is there code for X? > Transporting topological bases

[thomaskwaring]

Great, thanks! I will try to work on those golfs tomorrow, but for now I'll approve — I don't think it warrants stalling the PR any further.

[chenson2018]

I've not read this, but approving to unblock merging since another reviewer has approved. You should be able to add to the queue yourself.

(We'll likely update the CODEOWNERS policy soon to make this a bit easier, but please do ping me in the meantime if something gets stuck when one reviewer has already approved)

[chenson2018]

Network flakiness I think, added back to the queue.

[ctchou]

@thomaskwaring Thanks for the golfing!
@chenson2018 Thanks for taking care of the merge problem!