feat: prove that an omega-language is regular iff it is a finite union of omega-languages of a special form

Cslib.lean

@@ -16,6 +16,7 @@ public import Cslib.Computability.Automata.NA.BuchiInter
 public import Cslib.Computability.Automata.NA.Concat
 public import Cslib.Computability.Automata.NA.Hist
 public import Cslib.Computability.Automata.NA.Loop
+public import Cslib.Computability.Automata.NA.Pair
 public import Cslib.Computability.Automata.NA.Prod
 public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA

Cslib/Computability/Automata/NA/Loop.lean

@@ -120,30 +120,12 @@ the state `()` marks the boundaries between the finite words in `xls`. -/
 theorem loop_run_exists [Inhabited Symbol] {xls : ωSequence (List Symbol)}
     (h : ∀ k, (xls k) ∈ language na - 1) :
     ∃ ss, na.loop.Run xls.flatten ss ∧ ∀ k, ss (xls.cumLen k) = inl () := by
-  have : Inhabited State := by
-    choose s0 _ using (h 0).left
-    exact { default := s0 }
-  choose sls h_sls using fun k ↦ loop_fin_run_exists <| (h k).left
-  let segs := ωSequence.mk fun k ↦ (sls k).take (xls k).length
-  have h_len : xls.cumLen = segs.cumLen := by ext k; induction k <;> grind
-  have h_pos (k : ℕ) : (segs k).length > 0 := by grind [List.eq_nil_iff_length_eq_zero]
-  have h_mono := cumLen_strictMono h_pos
-  have h_zero := cumLen_zero (ls := segs)
-  have h_seg0 (k : ℕ) : (segs k)[0]! = inl () := by grind
-  refine ⟨segs.flatten, Run.mk ?_ ?_, ?_⟩
-  · simp [h_seg0, flatten_def, FinAcc.loop]
-  · intro n
-    simp only [h_len, flatten_def]
-    have := segment_lower_bound h_mono h_zero n
-    by_cases h_n : n + 1 < segs.cumLen (segment segs.cumLen n + 1)
-    · grind [segment_range_val h_mono (by grind) h_n]
-    · have h1 : segs.cumLen (segment segs.cumLen n + 1) = n + 1 := by
-        grind [segment_upper_bound h_mono h_zero n]
-      have h2 : segment segs.cumLen (n + 1) = segment segs.cumLen n + 1 := by
-        simp [← h1, segment_idem h_mono]
-      simp [h1, h2, h_seg0]
-      grind
-  · simp [h_len, flatten_def, segment_idem h_mono, h_seg0]
+  let ts := ωSequence.const (inl () : Unit ⊕ State)
+  have h_mtr (k : ℕ) : na.loop.MTr (ts k) (xls k) (ts (k + 1)) := by grind [loop_fin_run_mtr]
+  have h_pos (k : ℕ) : (xls k).length > 0 := by grind
+  obtain ⟨ss, _, _⟩ := LTS.ωTr.flatten h_mtr h_pos
+  use ss
+  grind [Run.mk, FinAcc.loop, cumLen_zero (ls := xls)]
 
 namespace Buchi
 

Cslib/Computability/Automata/NA/Pair.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2025 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.RegularLanguage
+
+@[expose] public section
+
+/-! # Languages determined by pairs of states
+-/
+
+namespace Cslib
+
+open Language Automata Acceptor
+
+variable {Symbol : Type*} {State : Type}
+
+/-- `LTS.pairLang s t` is the language of finite words that can take the LTS
+from state `s` to state `t`. -/
+def LTS.pairLang (lts : LTS State Symbol) (s t : State) : Language Symbol :=
+  { xl | lts.MTr s xl t }
+
+@[simp, scoped grind =]
+theorem LTS.mem_pairLang (lts : LTS State Symbol) (s t : State) (xl : List Symbol) :
+    xl ∈ (lts.pairLang s t) ↔ lts.MTr s xl t := Iff.rfl
+
+/-- `LTS.pairLang s t` is a regular language if there are only finitely many states. -/
+@[simp]
+theorem LTS.pairLang_regular [Finite State] (lts : LTS State Symbol) (s t : State) :
+    (lts.pairLang s t).IsRegular := by
+  rw [IsRegular.iff_nfa]
+  use State, inferInstance, (NA.FinAcc.mk ⟨lts, {s}⟩ {t})
+  ext xl; simp [LTS.mem_pairLang]
+
+namespace NA.Buchi
+
+open Set Filter ωSequence ωLanguage ωAcceptor
+
+/-- The ω-language accepted by a finite-state Büchi automaton is the finite union of ω-languages
+of the form `L * M^ω`, where all `L`s and `M`s are regular languages. -/
+theorem language_eq_fin_iSup_hmul_omegaPow
+    [Inhabited Symbol] [Finite State] (na : NA.Buchi State Symbol) :
+    language na = ⨆ s ∈ na.start, ⨆ t ∈ na.accept, (na.pairLang s t) * (na.pairLang t t)^ω := by
+  ext xs
+  simp only [NA.Buchi.instωAcceptor, ωAcceptor.mem_language,
+    ωLanguage.mem_iSup, ωLanguage.mem_hmul, LTS.mem_pairLang]
+  constructor
+  · rintro ⟨ss, h_run, h_inf⟩
+    obtain ⟨t, _, h_t⟩ := frequently_in_finite_type.mp h_inf
+    refine ⟨ss 0, by grind [h_run.start], t, by assumption, ?_⟩
+    obtain ⟨f, h_mono, h_f⟩ := frequently_iff_strictMono.mp h_t
+    refine ⟨xs.take (f 0), ?_, xs.drop (f 0), ?_, by grind⟩
+    · grind [extract_eq_drop_take, LTS.ωTr_mTr h_run.trans (Nat.zero_le (f 0))]
+    · simp only [omegaPow_seq_prop, LTS.mem_pairLang]
+      refine ⟨(f · - f 0), by grind [Nat.base_zero_strictMono], by simp, ?_⟩
+      intro n
+      grind [extract_drop, h_mono.monotone (Nat.zero_le n), h_mono.monotone (Nat.zero_le (n + 1)),
+        LTS.ωTr_mTr h_run.trans <| h_mono.monotone (show n ≤ n + 1 by grind)]
+  · rintro ⟨s, _, t, _, yl, h_yl, zs, h_zs, rfl⟩
+    obtain ⟨zls, rfl, h_zls⟩ := mem_omegaPow.mp h_zs
+    let ts := ωSequence.const t
+    have h_mtr (n : ℕ) : na.MTr (ts n) (zls n) (ts (n + 1)) := by
+      grind [Language.mem_sub_one, LTS.mem_pairLang]
+    have h_pos (n : ℕ) : (zls n).length > 0 := by
+      grind [Language.mem_sub_one, List.eq_nil_iff_length_eq_zero]
+    obtain ⟨zss, h_zss, _⟩ := LTS.ωTr.flatten h_mtr h_pos
+    have (n : ℕ) : zss (zls.cumLen n) = t := by grind
+    obtain ⟨xss, _, _, _, _⟩ := LTS.ωTr.append h_yl h_zss (by grind [cumLen_zero (ls := zls)])
+    refine ⟨xss, by grind [NA.Run.mk], ?_⟩
+    apply (drop_frequently_iff_frequently yl.length).mp
+    apply frequently_iff_strictMono.mpr
+    use zls.cumLen
+    grind [cumLen_strictMono]
+
+end NA.Buchi
+
+end Cslib

Cslib/Computability/Languages/OmegaRegularLanguage.lean

@@ -9,13 +9,13 @@ module
 public import Cslib.Computability.Automata.DA.Buchi
 public import Cslib.Computability.Automata.NA.BuchiEquiv
 public import Cslib.Computability.Automata.NA.BuchiInter
-public import Cslib.Computability.Automata.NA.Concat
-public import Cslib.Computability.Automata.NA.Loop
+public import Cslib.Computability.Automata.NA.Pair
 public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Languages.ExampleEventuallyZero
 public import Cslib.Computability.Languages.RegularLanguage
+public import Mathlib.Data.Finite.Card
 public import Mathlib.Data.Finite.Sigma
-public import Mathlib.Data.Finite.Sum
+public import Mathlib.Logic.Equiv.Fin.Basic
 
 @[expose] public section
 
@@ -185,6 +185,33 @@ theorem IsRegular.omegaPow [Inhabited Symbol] {l : Language Symbol}
   use Unit ⊕ State, inferInstance, ⟨na.loop, {inl ()}⟩
   exact NA.Buchi.loop_language_eq
 
+/-- An ω-language is regular iff it is the finite union of ω-languages of the form `L * M^ω`,
+where all `L`s and `M`s are regular languages. -/
+theorem IsRegular.eq_fin_iSup_hmul_omegaPow [Inhabited Symbol] (p : ωLanguage Symbol) :
+    p.IsRegular ↔ ∃ n : ℕ, ∃ l m : Fin n → Language Symbol,
+      (∀ i, (l i).IsRegular ∧ (m i).IsRegular) ∧ p = ⨆ i, (l i) * (m i)^ω := by
+  constructor
+  · rintro ⟨State, _, na, rfl⟩
+    rw [NA.Buchi.language_eq_fin_iSup_hmul_omegaPow na]
+    have eq_start := Finite.equivFin ↑na.start
+    have eq_accept := Finite.equivFin ↑na.accept
+    have eq_prod := eq_start.prodCongr eq_accept
+    have eq := (eq_prod.trans finProdFinEquiv).symm
+    refine ⟨Nat.card ↑na.start * Nat.card ↑na.accept,
+      fun i ↦ na.pairLang (eq i).1 (eq i).2,
+      fun i ↦ na.pairLang (eq i).2 (eq i).2,
+      by grind [LTS.pairLang_regular], ?_⟩
+    ext xs
+    simp only [mem_iSup]
+    refine ⟨?_, by grind⟩
+    rintro ⟨s, h_s, t, h_t, h_mem⟩
+    use eq.invFun (⟨s, h_s⟩, ⟨t, h_t⟩)
+    simp [h_mem]
+  · rintro ⟨n, l, m, _, rfl⟩
+    rw [← iSup_univ]
+    apply IsRegular.iSup
+    grind [IsRegular.hmul, IsRegular.omegaPow]
+
 /-- McNaughton's Theorem. -/
 proof_wanted IsRegular.iff_da_muller {p : ωLanguage Symbol} :
     p.IsRegular ↔

Cslib/Foundations/Data/Nat/Segment.lean

@@ -188,7 +188,7 @@ private lemma base_zero_shift (f : ℕ → ℕ) :
     (f · - f 0) 0 = 0 := by
   simp
 
-private lemma base_zero_strictMono (hm : StrictMono f) :
+theorem base_zero_strictMono (hm : StrictMono f) :
     StrictMono (f · - f 0) := by
   intro m n h_m_n; simp
   have := hm h_m_n

Cslib/Foundations/Data/OmegaSequence/InfOcc.lean

@@ -7,6 +7,7 @@ Authors: Ching-Tsun Chou
 module
 
 public import Cslib.Foundations.Data.OmegaSequence.Defs
+public import Mathlib.Data.Fintype.Pigeonhole
 public import Mathlib.Order.Filter.AtTopBot.Basic
 public import Mathlib.Order.Filter.Cofinite
 
@@ -40,6 +41,24 @@ theorem frequently_iff_strictMono {p : ℕ → Prop} :
     have h_range : range f ⊆ {n | p n} := by grind
     grind [Infinite.mono, infinite_range_of_injective, StrictMono.injective]
 
+/-- In a finite type, the elements of a set occurs infinitely often iff
+some element in the set occurs infinitely often. -/
+theorem frequently_in_finite_type [Finite α] {s : Set α} {xs : ωSequence α} :
+    (∃ᶠ k in atTop, xs k ∈ s) ↔ ∃ x ∈ s, ∃ᶠ k in atTop, xs k = x := by
+  constructor
+  · intro h_inf
+    rw [Nat.frequently_atTop_iff_infinite] at h_inf
+    have : Infinite (xs ⁻¹' s) := h_inf.to_subtype
+    let rf := Set.restrictPreimage s xs
+    obtain ⟨⟨x, h_x⟩, h_inf'⟩ := Finite.exists_infinite_fiber rf
+    rw [← Set.infinite_range_iff (Subtype.val_injective.comp Subtype.val_injective)] at h_inf'
+    simp only [range, comp_apply, Subtype.exists, mem_preimage, mem_singleton_iff,
+      restrictPreimage_mk, Subtype.mk.injEq, ← Nat.frequently_atTop_iff_infinite, rf] at h_inf'
+    grind
+  · rintro ⟨_, _, h_inf⟩
+    apply Frequently.mono h_inf
+    grind
+
 end ωSequence
 
 end Cslib

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -7,7 +7,7 @@ Authors: Fabrizio Montesi
 module
 
 public import Cslib.Init
-public import Cslib.Foundations.Data.OmegaSequence.Init
+public import Cslib.Foundations.Data.OmegaSequence.Flatten
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Mathlib.Data.Set.Finite.Basic
 public import Mathlib.Order.ConditionallyCompleteLattice.Basic
@@ -264,17 +264,54 @@ theorem LTS.ωTr.cons (htr : lts.Tr s μ t) (hωtr : lts.ωTr ss μs) (hm : ss 0
   induction i <;> grind
 
 /-- Prepends an infinite execution with a finite execution. -/
-theorem LTS.ωTr.append (hmtr : lts.MTr s μl t) (hωtr : lts.ωTr ss μs)
-    (hm : ss 0 = t) : ∃ ss', lts.ωTr ss' (μl ++ω μs) ∧ ss' 0 = s ∧ ss' μl.length = t := by
+theorem LTS.ωTr.append
+    (hmtr : lts.MTr s μl t) (hωtr : lts.ωTr ss μs) (hm : ss 0 = t) :
+    ∃ ss', lts.ωTr ss' (μl ++ω μs) ∧ ss' 0 = s ∧ ss' μl.length = t ∧ ss'.drop μl.length = ss := by
   obtain ⟨sl, _, _, _, _⟩ := LTS.MTr.exists_states hmtr
-  refine ⟨sl ++ω ss.drop 1, ?_, by grind [get_append_left], by grind [get_append_left]⟩
+  refine ⟨sl.take μl.length ++ω ss, ?_,
+    by grind [get_append_left], by grind [get_append_left], by grind [drop_append_of_ge_length]⟩
   intro n
   by_cases n < μl.length
   · grind [get_append_left]
   · by_cases n = μl.length
-    · grind [get_append_left]
+    · grind [get_append_left, get_append_right']
     · grind [get_append_right', hωtr (n - μl.length - 1)]
 
+open Nat in
+/-- Concatenating an infinite sequence of finite executions that connect an infinite sequence
+of intermediate states. -/
+theorem LTS.ωTr.flatten [Inhabited Label] {ts : ωSequence State} {μls : ωSequence (List Label)}
+    (hmtr : ∀ k, lts.MTr (ts k) (μls k) (ts (k + 1))) (hpos : ∀ k, (μls k).length > 0) :
+    ∃ ss, lts.ωTr ss μls.flatten ∧ ∀ k, ss (μls.cumLen k) = ts k := by
+  have : Inhabited State := by exact {default := ts 0}
+  choose sls h_sls using fun k ↦ LTS.MTr.exists_states (hmtr k)
+  let segs := ωSequence.mk fun k ↦ (sls k).take (μls k).length
+  have h_len : μls.cumLen = segs.cumLen := by ext k; induction k <;> grind
+  have h_pos (k : ℕ) : (segs k).length > 0 := by grind [List.eq_nil_iff_length_eq_zero]
+  have h_mono := cumLen_strictMono h_pos
+  have h_zero := cumLen_zero (ls := segs)
+  have h_seg0 (k : ℕ) : (segs k)[0]! = ts k := by grind
+  refine ⟨segs.flatten, ?_, by simp [h_len, flatten_def, segment_idem h_mono, h_seg0]⟩
+  intro n
+  simp only [h_len, flatten_def]
+  have := segment_lower_bound h_mono h_zero n
+  by_cases h_n : n + 1 < segs.cumLen (segment segs.cumLen n + 1)
+  · have := segment_range_val h_mono (by grind) h_n
+    have : n + 1 - segs.cumLen (segment segs.cumLen n) < (μls (segment segs.cumLen n)).length := by
+      grind
+    grind
+  · have h1 : segs.cumLen (segment segs.cumLen n + 1) = n + 1 := by
+      grind [segment_upper_bound h_mono h_zero n]
+    have h2 : segment segs.cumLen (n + 1) = segment segs.cumLen n + 1 := by
+      simp [← h1, segment_idem h_mono]
+    have : n + 1 - segs.cumLen (segment segs.cumLen n) = (μls (segment segs.cumLen n)).length := by
+      grind
+    have h3 : ts (segment segs.cumLen n + 1) =
+        (sls (segment segs.cumLen n))[n + 1 - segs.cumLen (segment segs.cumLen n)]! := by
+      grind
+    simp [h1, h2, h_seg0, h3]
+    grind
+
 end ωMultiStep
 
 section Total
@@ -319,7 +356,8 @@ theorem LTS.Total.mTr_ωTr [Inhabited Label] [ht : lts.Total] {μl : List Label}
     (hm : lts.MTr s μl t) : ∃ μs ss, lts.ωTr ss (μl ++ω μs) ∧ ss 0 = s ∧ ss μl.length = t := by
   let μs : ωSequence Label := .const default
   obtain ⟨ss', ho, h0⟩ := LTS.Total.ωTr_exists (h := ht) t μs
-  refine ⟨μs, LTS.ωTr.append hm ho h0⟩
+  use μs
+  grind [LTS.ωTr.append hm ho h0]
 
 /-- `LTS.totalize` constructs a total LTS from any given LTS by adding a sink state. -/
 def LTS.totalize (lts : LTS State Label) : LTS (State ⊕ Unit) Label where