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

Cslib.lean

@@ -38,6 +38,7 @@ public import Cslib.Computability.Languages.MyhillNerode
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Languages.SafetyLiveness
 public import Cslib.Computability.Machines.Turing.SingleTape.Defs
 public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
 public import Cslib.Computability.Machines.Turing.SingleTape.NonDeterministic
@@ -72,10 +73,12 @@ public import Cslib.Foundations.Data.OmegaSequence.Flatten
 public import Cslib.Foundations.Data.OmegaSequence.InfOcc
 public import Cslib.Foundations.Data.OmegaSequence.Init
 public import Cslib.Foundations.Data.OmegaSequence.Temporal
+public import Cslib.Foundations.Data.OmegaSequence.Topology
 public import Cslib.Foundations.Data.PFunctor.Free
 public import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Data.StackTape
+public import Cslib.Foundations.Data.Topology.ClosedDenseDecomposition
 public import Cslib.Foundations.Lint.Basic
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence

Cslib/Computability/Automata/NA/Loop.lean

@@ -189,7 +189,7 @@ theorem loop_language_eq [Inhabited Symbol] (h : ¬ language na = 0) :
   ext xl; constructor
   · rintro ⟨s, _, t, h_acc, h_mtr⟩
     by_cases h_xl : xl = []
-    · grind [mem_add, mem_one]
+    · grind [Language.mem_add, Language.mem_one]
     · have : Nonempty na.start := by
         obtain ⟨_, s0, _, _⟩ := nonempty_iff_ne_empty.mpr h
         use s0

Cslib/Computability/Languages/OmegaLanguage.lean

@@ -8,6 +8,7 @@ module
 
 public import Cslib.Computability.Languages.Language
 public import Cslib.Foundations.Data.OmegaSequence.Flatten
+public import Cslib.Foundations.Data.OmegaSequence.Topology
 public import Mathlib.Computability.Language
 public import Mathlib.Order.CompleteBooleanAlgebra
 public import Mathlib.Order.Filter.AtTopBot.Defs
@@ -28,6 +29,8 @@ denote languages (namely, sets of finite sequences of type `List α`).
   universe sets), and the subset relation are denoted using lattice-theoretic
   notations (`p ∪ q`, `p ∩ q`, `pᶜ`, `⊥`, `⊤`, and `≤`) and terminologies in
   definition and theorem names ("inf", "sup", "compl", "bot", "top", "le").
+* `p.closure`: the topological closure of `p`, where `ωLanguage α` inherits the
+  product topology of `TopologicalSpace (ωSequence α)`
 * `l * p`: ω-language of `x ++ω y` where `x ∈ l` and `y ∈ p`; referred to as
   "hmul" in definition and theorem names.
 * `l^ω`: ω-language of infinite sequences each of which is the concatenation of
@@ -137,6 +140,10 @@ lemma iInf_def {ι : Sort v} {p : ι → ωLanguage α} : ⨅ i, p i = ⟨⋂ i,
   ext
   simp [iInf, sInf_def]
 
+/-- The topological closure of an ω-language. -/
+def closure (p : ωLanguage α) : ωLanguage α :=
+  _root_.closure p.toSet
+
 /-- The concatenation of a language l and an ω-language `p` is the ω-language made of
 infinite sequences `x ++ω y` where `x ∈ l` and `y ∈ p`. -/
 instance : HMul (Language α) (ωLanguage α) (ωLanguage α) where

Cslib/Computability/Languages/SafetyLiveness.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+module
+
+public import Cslib.Computability.Languages.OmegaLanguage
+public import Cslib.Foundations.Data.Topology.ClosedDenseDecomposition
+
+/-!
+# Safety and Liveness properties of ω-sequences
+
+This file formalizes the main results of [AlpernSchneider1985].  Namely, given
+an appropriate topology on ω-sequences:
+* Safety properties can be identified with closed sets.
+* Liveness properties can be identified with dense sets.
+* Every property is the intersection of a safety property and a liveness property.
+
+## References
+* [Alpern, Bowen; Schneider, Fred B. (1985). "Defining liveness".
+Information Processing Letters. 21 (4): 181–185.][AlpernSchneider1985]
+-/
+
+@[expose] public section
+
+namespace Cslib.ωLanguage
+
+open Set ωSequence TopologicalSpace
+
+variable {α : Type*}
+
+/-- Safety properties are identified with closed sets. -/
+abbrev IsSafety (p : ωLanguage α) : Prop := IsClosed p.toSet
+
+/-- An alternative characterization of `IsSafety` that justifies its definition:
+if an ω-sequence violates a safety property, then it has a finite prefix all of whose
+infinite extensions also violate the property. -/
+theorem isSafety_iff (p : ωLanguage α) :
+    p.IsSafety ↔ ∀ xs, xs ∉ p → ∃ n, ∀ ys, (xs.take n) ++ω ys ∉ p := by
+  simp [← isOpen_compl_iff, isOpen_iff, mem_def]
+
+/-- Liveness properties are identified with dense sets. -/
+abbrev IsLiveness (p : ωLanguage α) : Prop := Dense p.toSet
+
+/-- An alternative characterization of `IsLiveness` that justifies its definition:
+any finite sequence can be extended to an infinite sequence satisfying a liveness property. -/
+theorem isLiveness_iff (p : ωLanguage α) :
+    p.IsLiveness ↔ ∀ (xs : ωSequence α) (n : ℕ), ∃ ys, (xs.take n) ++ω ys ∈ p := by
+  exact Dense_iff p.toSet
+
+/-- `SafetyLivenessDecomposition p ps pl` means that `ps` is a safety property,
+`pl` is a liveness property, and `ps ⊓ pl = p`. -/
+def SafetyLivenessDecomposition (p ps pl : ωLanguage α) : Prop :=
+  IsSafety ps ∧ IsLiveness pl ∧ ps ⊓ pl = p
+
+/-- Every property `p` is the intersection of the safety property `p.closure` and
+the liveness property `p ⊔ p.closureᶜ`. -/
+theorem SafetyLivenessDecomposition_exists (p : ωLanguage α) :
+    SafetyLivenessDecomposition p p.closure (p ⊔ p.closureᶜ) := by
+  obtain ⟨_, _, _⟩ := ClosedDenseDecomposition_exists p.toSet
+  split_ands
+  · simpa
+  · simpa [sup_def, closure, compl_def]
+  · simpa [ωLanguage.ext_iff, sup_def, closure, compl_def]
+
+end Cslib.ωLanguage

Cslib/Foundations/Data/OmegaSequence/Topology.lean

@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+module
+
+public import Cslib.Foundations.Data.OmegaSequence.Init
+public import Mathlib.Topology.Homeomorph.TransferInstance
+public import Mathlib.Topology.MetricSpace.PiNat
+
+/-!
+# Topology on ω-sequences
+
+The topology on ω-sequences is essentially the product topology when `ωSequence α` is
+viewed as the product space `Π (n : ℕ), α`, where `α` is equipped with the discrete
+topology.  The notion of "cylinders" are also ported from `Π (n : ℕ), α` and they form
+a topological basis.
+-/
+
+@[expose] public section
+
+namespace Cslib.ωSequence
+
+open Set Homeomorph TopologicalSpace ωSequence
+
+variable {α : Type*}
+
+/-- Define the topology on `ωSequence α` using an equivalence from it to the product topology
+`ℕ → WithDiscreteTopology α`. -/
+instance : TopologicalSpace (ωSequence α) :=
+  haveI eqv : ωSequence α ≃ (ℕ → WithDiscreteTopology α) := {
+    toFun xs i := .toTopology ⊥ (xs.get i)
+    invFun f := ωSequence.mk fun i => (f i).ofTopology
+    left_inv _ := rfl
+    right_inv _ := rfl
+  }
+  eqv.topologicalSpace
+
+/-- The homeomorphisim from `ωSequence α` to `ℕ → WithDiscreteTopology α`. -/
+def homeomorph : ωSequence α ≃ₜ (ℕ → WithDiscreteTopology α) := Equiv.homeomorph _
+
+@[simp]
+lemma homeomorph_apply (xs : ωSequence α) (i : Nat) :
+    homeomorph xs i = .toTopology ⊥ (xs i) :=
+  rfl
+
+@[simp]
+lemma homeomorph_symm_apply (f : ℕ → WithDiscreteTopology α) :
+    homeomorph.symm f = ωSequence.mk fun i => (f i).ofTopology :=
+  rfl
+
+/-- Port the notion of "cylinders" from `ℕ → WithDiscreteTopology α` to `ωSequence α`. -/
+def cylinder (xs : ωSequence α) (n : ℕ) : Set (ωSequence α) :=
+  homeomorph ⁻¹' (PiNat.cylinder (homeomorph xs) n)
+
+/-- An alternative characterization of cylinders in terms of `ωSequence α` alone. -/
+theorem cylinder_def (xs : ωSequence α) (n : ℕ) :
+    xs.cylinder n = { ys | ∀ k, k < n → ys k = xs k } := by
+  simp [cylinder, PiNat.cylinder]
+
+/-- Yet another alternative characterization of cylinders in terms of `ωSequence α` alone. -/
+theorem cylinder_eq_prepend_range (xs : ωSequence α) (n : ℕ) :
+    xs.cylinder n = range (xs.take n ++ω ·) := by
+  ext ys
+  simp only [cylinder_def, mem_ofPred_eq, mem_range]
+  constructor
+  · intro h
+    use ys.drop n
+    suffices xs.take n = ys.take n by grind
+    apply List.ext_get <;> grind
+  · grind [get_append_left]
+
+/-- All cylinders are open sets. -/
+theorem isOpen_cylinder (xs : ωSequence α) (n : ℕ) :
+    IsOpen (xs.cylinder n) := by
+  simp [cylinder, PiNat.isOpen_cylinder]
+
+/-- Every ω-sequence in an open set belongs to a cylinder which is contained in the set. -/
+theorem nhds_cylinders {xs : ωSequence α} {s : Set (ωSequence α)} (hx : xs ∈ s) (hs : IsOpen s) :
+    ∃ (ys : ωSequence α) (n : ℕ), xs ∈ ys.cylinder n ∧ ys.cylinder n ⊆ s := by
+  let xs' := homeomorph xs
+  have hx' : xs' ∈ homeomorph '' s := by grind
+  have hs' := (isOpen_image homeomorph).mpr hs
+  have hb := PiNat.isTopologicalBasis_cylinders (fun _ : ℕ ↦ WithDiscreteTopology α)
+  obtain ⟨_, ⟨ys', n, rfl⟩, hmm, hss⟩ := IsTopologicalBasis.exists_subset_of_mem_open hb hx' hs'
+  use homeomorph.symm ys', n
+  split_ands
+  · exact mem_preimage.mp hmm
+  · exact preimage_subset hss <| injOn_of_injective <| Homeomorph.injective homeomorph
+
+/-- The cylinders form a topological basis. -/
+theorem isTopologicalBasis_cylinders :
+    IsTopologicalBasis { s | ∃ (xs : ωSequence α) (n : ℕ), s = xs.cylinder n } := by
+  apply isTopologicalBasis_of_isOpen_of_nhds
+  · grind [isOpen_cylinder]
+  · grind [nhds_cylinders]
+
+/-- A set is open iff any ω-sequence in the set has a finite prefix all of whose infinite
+extensions are also in the set. -/
+theorem isOpen_iff (s : Set (ωSequence α)) :
+    IsOpen s ↔ ∀ xs, xs ∈ s → ∃ n, ∀ ys, (xs.take n) ++ω ys ∈ s := by
+  simp only [IsTopologicalBasis.isOpen_iff isTopologicalBasis_cylinders,
+    cylinder_eq_prepend_range, mem_ofPred_eq, ↓existsAndEq, mem_range, true_and]
+  constructor <;> intro h xs hxs
+  · obtain ⟨_, n, ⟨_, rfl⟩, _⟩ := h xs hxs
+    use n
+    grind [take_append_of_le_length]
+  · obtain ⟨n, _⟩ := h xs hxs
+    use xs, n, ⟨xs.drop n, ?_⟩ <;> grind
+
+/-- A set is dense iff any finite sequence can be extended to an infinite sequence in the set. -/
+theorem Dense_iff (s : Set (ωSequence α)) :
+    Dense s ↔ ∀ (xs : ωSequence α) (n : ℕ), ∃ ys, (xs.take n) ++ω ys ∈ s := by
+  simp only [IsTopologicalBasis.dense_iff isTopologicalBasis_cylinders, cylinder_eq_prepend_range,
+    mem_ofPred_eq, forall_exists_index]
+  constructor
+  · intro h xs n
+    obtain ⟨ys, h1, _⟩ := h (xs.cylinder n) xs n
+      (by simp [cylinder_eq_prepend_range]) (by use xs; simp [cylinder_def])
+    use ys.drop n
+    suffices xs.take n = ys.take n by grind
+    grind [cylinder_eq_prepend_range, take_append_of_le_length]
+  · rintro h c xs n rfl ⟨_, _, rfl⟩
+    obtain ⟨ys, _⟩ := h xs n
+    use xs.take n ++ω ys
+    grind
+
+end Cslib.ωSequence

Cslib/Foundations/Data/Topology/ClosedDenseDecomposition.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Topology.Closure
+
+/-!
+# Closed-dense decomposition
+
+Every set in a topological space is the intersection of a closed set and a dense set.
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+open Set
+
+variable {X : Type*} [TopologicalSpace X]
+
+/-- `ClosedDenseDecomposition s sc sd` means that `sc` is a closed set, `sd` is a dense set,
+and `sc ∩ sd = s`. -/
+def ClosedDenseDecomposition (s sc sd : Set X) : Prop :=
+  IsClosed sc ∧ Dense sd ∧ sc ∩ sd = s
+
+/-- Every set `s` in a topological space is the intersection of the closed set `closure s`
+and the dense set `s ∪ (closure)ᶜ`. -/
+theorem ClosedDenseDecomposition_exists (s : Set X) :
+    ClosedDenseDecomposition s (closure s) (s ∪ (closure s)ᶜ) := by
+  split_ands
+  · exact isClosed_closure
+  · simp only [dense_iff_closure_eq, closure_union, ← compl_subset_iff_union, subset_closure]
+  · simp [inter_union_distrib_left, subset_closure]
+
+end Cslib

references.bib

@@ -19,6 +19,19 @@ @inproceedings{Aceto1999
   bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{AlpernSchneider1985,
+  author    = {Alpern, Bowen and Schneider, Fred B.},
+  title     = {Defining liveness},
+  journal   = {Information Processing Letters},
+  volume    = {21},
+  number    = {4},
+  pages     = {181--185},
+  year      = {1985},
+  issn      = {0020-0190},
+  doi       = {10.1016/0020-0190(85)90056-0},
+  url       = {https://www.sciencedirect.com/science/article/pii/0020019085900560}
+}
+
 @article{AngluinLaird1988,
   author       = {Angluin, Dana and Laird, Philip},
   title        = {Learning from Noisy Examples},