feat: prove that the Buchi congruence has the saturation property

Cslib/Computability/Languages/Congruences/BuchiCongruence.lean

@@ -8,6 +8,8 @@ module
 
 public import Cslib.Computability.Automata.NA.Pair
 public import Cslib.Computability.Languages.Congruences.RightCongruence
+public import Cslib.Computability.Languages.OmegaLanguage
+public import Cslib.Foundations.Data.Set.Saturation
 
 @[expose] public section
 
@@ -20,7 +22,7 @@ of ω-regular languages under complementation.
 
 namespace Cslib.Automata.NA.Buchi
 
-open Function
+open Function Set Filter ωAcceptor ωLanguage ωSequence
 
 variable {Symbol : Type*} {State : Type}
 
@@ -32,7 +34,7 @@ following two conditions hold:
 from `s` to `t` via an acceptingg states. -/
 def BuchiCongruence (na : Buchi State Symbol) : RightCongruence Symbol where
   eq.r u v :=
-    ∀ {s t}, (u ∈ na.pairLang s t ↔ v ∈ na.pairLang s t) ∧
+    ∀ s t, (u ∈ na.pairLang s t ↔ v ∈ na.pairLang s t) ∧
       (u ∈ na.pairViaLang na.accept s t ↔ v ∈ na.pairViaLang na.accept s t)
   eq.iseqv.refl := by grind
   eq.iseqv.symm := by grind
@@ -72,4 +74,118 @@ lemma buchiCongrParam_surjective : Surjective na.BuchiCongrParam := by
 theorem buchiCongruence_fin_index [Finite State] : Finite (Quotient na.BuchiCongruence.eq) :=
   Finite.of_surjective na.BuchiCongrParam buchiCongrParam_surjective
 
+/-- If `xl` and `yl` belong to the same equivalence class of `na.BuchiCongruence`
+and `xl` can move `na` from state `s` to state `t`, then so can `yl` and, furthermore,
+if `xl` makes `na` go through an accepting state of `na`, then so can `yl`. -/
+lemma buchiCongruence_transfer
+    {a : Quotient na.BuchiCongruence.eq} {xl yl : List Symbol} {s t : State}
+    (hc : xl ∈ na.BuchiCongruence.eqvCls a) (hc' : yl ∈ na.BuchiCongruence.eqvCls a)
+    (hp : xl ∈ na.pairLang s t) : ∃ sl, na.IsExecution s yl t sl ∧
+      ( xl ∈ na.pairViaLang na.accept s t → ∃ r ∈ na.accept, r ∈ sl ) := by
+  have h_eq : na.BuchiCongruence.eq xl yl := by
+    apply Quotient.exact
+    grind
+  have := h_eq s t
+  have h_yl : yl ∈ na.pairLang s t := by grind
+  have := LTS.mTr_isExecution h_yl
+  grind [LTS.mem_pairViaLang, LTS.IsExecution, → LTS.IsExecution.comp, → LTS.mTr_isExecution]
+
+/-- `na.buchiFamily` is a family of ω-languages indexed by a pair of equivalence classes
+of `na.BuchiCongruence` which will turn out to saturate the ω-language accepted by `na`
+and cover all possible ω-sequences. -/
+def buchiFamily [Inhabited Symbol] (na : Buchi State Symbol) :
+    Quotient na.BuchiCongruence.eq × Quotient na.BuchiCongruence.eq → ωLanguage Symbol
+  | (a, b) => na.BuchiCongruence.eqvCls a * (na.BuchiCongruence.eqvCls b)^ω
+
+theorem mem_buchiFamily [Inhabited Symbol]
+    {xs : ωSequence Symbol} {a b : Quotient na.BuchiCongruence.eq} :
+    xs ∈ na.buchiFamily (a, b) ↔ ∃ xl, ∃ xls : ωSequence (List Symbol),
+      xl ∈ na.BuchiCongruence.eqvCls a ∧ (∀ k, xls k ∈ na.BuchiCongruence.eqvCls b - 1) ∧
+      xl ++ω xls.flatten = xs := by
+  grind [buchiFamily]
+
+-- This intermediate result is split out of the proof of `buchiCongruence_saturation` below
+-- because that proof was too big and kept exceeding the default `maxHeartbeats`.
+private lemma frequently_via_accept [Inhabited Symbol]
+    {xl : List Symbol} {xls : ωSequence (List Symbol)} {ss : ωSequence State}
+    (h_acc : ∃ᶠ (k : ℕ) in atTop, ss k ∈ na.accept) (h_exec : na.ωTr ss (xl ++ω xls.flatten))
+    (h_xls_p : ∀ (k : ℕ), (xls k).length > 0)
+    (f : ℕ → ℕ) (h_f : f = fun k => xl.length + xls.cumLen k)
+    (ts : ωSequence State) (h_ts : ts = ωSequence.mk (fun k ↦ ss (f k))) :
+    ∃ᶠ (k : ℕ) in atTop, xls k ∈ na.pairViaLang na.accept (ts k) (ts (k + 1)) := by
+  have hm : StrictMono f := by grind [StrictMono, cumLen_strictMono]
+  apply Frequently.mono <| frequently_in_strictMono hm h_acc
+  rintro n ⟨k, _, _⟩
+  apply LTS.mem_pairViaLang.mpr
+  use ss (f n + k), by grind, (xls n).take k, (xls n).drop k
+  have := extract_flatten h_xls_p n
+  have exec {m n} (h : m ≤ n) := LTS.isExecution_mTr na.toLTS <| LTS.ωTr_isExecution h_exec h
+  split_ands
+  · have h : f n ≤ f n + k := by lia
+    specialize exec h
+    grind [extract_apppend_right_right]
+  · have h : f n + k ≤ f (n + 1) := by lia
+    specialize exec h
+    grind [extract_apppend_right_right]
+  · grind only [!List.take_append_drop]
+
+/-- `na.buchiFamily` saturates the ω-language accepted by `na`. -/
+theorem buchiFamily_saturation [Inhabited Symbol] :
+    Saturates na.buchiFamily (language na) := by
+  rintro ⟨a, b⟩ ⟨xs, h_xs, h_lang⟩ ys h_ys
+  obtain ⟨xl, xls, h_xl_c, h_xls_c, rfl⟩ := mem_buchiFamily.mp h_xs
+  obtain ⟨yl, yls, h_yl_c, h_yls_c, rfl⟩ := mem_buchiFamily.mp h_ys
+  obtain ⟨ss, ⟨h_init, h_exec⟩, h_acc⟩ := h_lang
+  have h_xls_p (k : ℕ) : (xls k).length > 0 := by
+    grind [Language.mem_sub_one, List.ne_nil_iff_length_pos]
+  have h_yls_p (k : ℕ) : (yls k).length > 0 := by
+    grind [Language.mem_sub_one, List.ne_nil_iff_length_pos]
+  let f (k : ℕ) := xl.length + xls.cumLen k
+  let ts := ωSequence.mk (fun k ↦ ss (f k))
+  have h_xl_l : 0 ≤ xl.length := by grind
+  have h_xl_e : xl ∈ na.pairLang (ss 0) (ts 0) := by
+    have := LTS.ωTr_mTr h_exec h_xl_l
+    grind [extract_append_zero_right, LTS.mem_pairLang]
+  have h_xls_e (k : ℕ) : (xls k) ∈ na.pairLang (ts k) (ts (k + 1)) := by
+    have := LTS.ωTr_mTr h_exec (show f k ≤ f (k + 1) by grind)
+    suffices (xl ++ω xls.flatten).extract (f k) (f (k + 1)) = xls k by grind [LTS.mem_pairLang]
+    simp (disch := grind) [extract_apppend_right_right, f]
+  have h_yl_e : yl ∈ na.pairLang (ss 0) (ts 0) := by
+    obtain ⟨sl, h_e, _⟩ := buchiCongruence_transfer h_xl_c h_yl_c h_xl_e
+    grind [LTS.mem_pairLang, LTS.isExecution_mTr (lts := na.toLTS) h_e]
+  have h_yls (k : ℕ) : ∃ sl, na.IsExecution (ts k) (yls k) (ts (k + 1)) sl ∧
+      ( (xls k) ∈ na.pairViaLang na.accept (ts k) (ts (k + 1)) → ∃ s ∈ na.accept, s ∈ sl ) := by
+    exact buchiCongruence_transfer ((h_xls_c k).left) ((h_yls_c k).left) (h_xls_e k)
+  choose sls h_yls_e h_yls_a using h_yls
+  obtain ⟨ss1, h_ss1_run, h_ss1_seg⟩ := LTS.IsExecution.flatten h_yls_e h_yls_p
+  have h_ss1_ts : ss1 0 = ts 0 := by
+    have h : 0 < yls.cumLen 1 - yls.cumLen 0 := by grind
+    have : 0 < (sls 0).length := by grind
+    have : ss1 0 = (sls 0)[0] := by grind [get_extract (xs := ss1) h]
+    have : ts 0 = (sls 0)[0] := by grind [LTS.IsExecution]
+    grind
+  obtain ⟨ss2, _, _, _, _⟩ := LTS.ωTr.append h_yl_e h_ss1_run h_ss1_ts
+  use ss2, by grind [Run.mk]
+  suffices ∃ᶠ (k : ℕ) in Filter.atTop, ss1 k ∈ na.accept by
+    apply (drop_frequently_iff_frequently yl.length).mp
+    grind
+  have h_acc' := frequently_via_accept h_acc h_exec h_xls_p f rfl ts rfl
+  have h_mono : StrictMono yls.cumLen := cumLen_strictMono h_yls_p
+  apply frequently_atTop.mpr
+  intro n
+  obtain ⟨m, _, s, _, h_mem⟩ := frequently_atTop.mp (Frequently.mono h_acc' h_yls_a) n
+  have : m ≤ yls.cumLen m := by grind [StrictMono.add_le_nat h_mono m 0]
+  obtain ⟨k, _, _⟩ := List.mem_iff_getElem.mp h_mem
+  use yls.cumLen m + k, by grind
+  suffices ss1 (yls.cumLen m + k) = (sls m)[k] by grind
+  by_cases k < (yls m).length
+  · have h1 : k < yls.cumLen (m + 1) - yls.cumLen m := by grind only [= cumLen_succ]
+    simp [← get_extract (xs := ss1) h1, h_ss1_seg m]
+  · obtain ⟨_, _, _, _⟩ := h_yls_e m
+    obtain ⟨_, _, _, _⟩ := h_yls_e (m + 1)
+    have := h_mono (show m + 1 < m + 2 by omega)
+    have h1 : 0 < yls.cumLen (m + 2) - yls.cumLen (m + 1) := by omega
+    have h2 := get_extract (xs := ss1) h1
+    grind only [= cumLen_succ, = get_fun, = List.getElem_take]
+
 end Cslib.Automata.NA.Buchi

Cslib/Foundations/Data/OmegaSequence/InfOcc.lean

@@ -6,9 +6,9 @@ Authors: Ching-Tsun Chou
 
 module
 
+public import Cslib.Foundations.Data.Nat.Segment
 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
 
 @[expose] public section
@@ -59,6 +59,24 @@ theorem frequently_in_finite_type [Finite α] {s : Set α} {xs : ωSequence α}
     apply Frequently.mono h_inf
     grind
 
+open Nat in
+/-- If `p` is true infinitely often, then `p` is true in infinitely many segments
+of any strictly monotonic function `f`. -/
+theorem frequently_in_strictMono {p : ℕ → Prop} {f : ℕ → ℕ}
+    (hm : StrictMono f) (hf : ∃ᶠ k in atTop, p k) :
+    ∃ᶠ n in atTop, ∃ k, k < f (n + 1) - f n ∧ p (f n + k) := by
+  apply frequently_atTop.mpr
+  intro m
+  obtain ⟨k, _, _⟩ := frequently_atTop.mp hf (f m)
+  use segment f k
+  have h0 : f 0 ≤ k := by grind [StrictMono.monotone hm (show 0 ≤ m by grind)]
+  split_ands
+  · by_contra
+    have h1 : segment f k + 1 ≤ m := by grind
+    grind [(StrictMono.le_iff_le hm).mpr h1, segment_upper_bound' hm h0]
+  · use k - f (segment f k)
+    grind [segment_lower_bound' hm h0, segment_upper_bound' hm h0]
+
 end ωSequence
 
 end Cslib

Cslib/Foundations/Data/OmegaSequence/Init.lean

@@ -508,6 +508,17 @@ theorem extract_0u_extract_l {xs : ωSequence α} {n i : ℕ} :
     (xs.extract 0 n).extract i = xs.extract i n := by
   grind
 
+@[simp, scoped grind =]
+theorem take_extract {xs : ωSequence α} {m n k : ℕ} (h : k ≤ n - m) :
+    (xs.extract m n).take k = xs.extract m (m + k) := by
+  grind [extract_lu_extract_lu (xs := xs) (i := 0) h]
+
+@[simp, scoped grind =]
+theorem drop_extract {xs : ωSequence α} {m n k : ℕ} (h : k ≤ n - m) :
+    (xs.extract m n).drop k = xs.extract (m + k) n := by
+  have := extract_lu_extract_lu (xs := xs) (m := m) (n := n) (i := k) (j := n - m)
+  grind [length_extract, List.take_length]
+
 end ωSequence
 
 end Cslib

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -215,6 +215,36 @@ theorem LTS.mTr_isExecution_iff : lts.MTr s1 μs s2 ↔
     ∃ ss : List State, lts.IsExecution s1 μs s2 ss := by
   grind
 
+lemma LTS.IsExecution.comp_seg2
+    {lts : LTS State Label} {s r t : State} {μs1 μs2 : List Label} {ss1 ss2 : List State}
+    (h1 : lts.IsExecution s μs1 r ss1) (h2 : lts.IsExecution r μs2 t ss2)
+    (k : ℕ) (h_k : k < ss2.length) :
+    (ss1 ++ ss2.tail)[μs1.length + k]'(by grind) = ss2[k] := by
+  by_cases h : k = 0
+  · simp (disch := grind) only [h, add_zero, List.getElem_append_left]
+    grind
+  · simp (disch := grind) only [List.getElem_append_right, List.getElem_tail]
+    have : μs1.length + k - ss1.length + 1 = k := by grind
+    grind
+
+/-- The composition of two executions is an execution. -/
+theorem LTS.IsExecution.comp
+    {lts : LTS State Label} {s r t : State} {μs1 μs2 : List Label} {ss1 ss2 : List State}
+    (h1 : lts.IsExecution s μs1 r ss1) (h2 : lts.IsExecution r μs2 t ss2) :
+    lts.IsExecution s (μs1 ++ μs2) t (ss1 ++ ss2.tail) := by
+  have h0 : (ss1 ++ ss2.tail).length = (μs1 ++ μs2).length + 1 := by grind
+  use h0
+  split_ands
+  · grind
+  · have := LTS.IsExecution.comp_seg2 h1 h2 μs2.length
+    grind only [IsExecution, = List.length_append]
+  · intro k h_k
+    by_cases k < μs1.length
+    · grind only [IsExecution, = List.getElem_append]
+    · have := LTS.IsExecution.comp_seg2 h1 h2 (k - μs1.length)
+      have := LTS.IsExecution.comp_seg2 h1 h2 (k - μs1.length + 1)
+      grind
+
 /-- An execution can be split at any intermediate state into two executions. -/
 theorem LTS.IsExecution.split
     {lts : LTS State Label} {s t : State} {μs : List Label} {ss : List State}
@@ -317,20 +347,17 @@ def LTS.ωTr (lts : LTS State Label) (ss : ωSequence State) (μs : ωSequence L
 
 variable {lts : LTS State Label}
 
-open scoped ωSequence in
+open ωSequence
+
 /-- Any finite execution extracted from an infinite execution is valid. -/
+theorem LTS.ωTr_isExecution (h : lts.ωTr ss μs) {n m : ℕ} (hnm : n ≤ m) :
+    lts.IsExecution (ss n) (μs.extract n m) (ss m) (ss.extract n (m + 1)) := by
+  grind
+
+/-- Any multistep transition extracted from an infinite execution is valid. -/
 theorem LTS.ωTr_mTr (h : lts.ωTr ss μs) {n m : ℕ} (hnm : n ≤ m) :
     lts.MTr (ss n) (μs.extract n m) (ss m) := by
-  by_cases heq : n = m
-  case pos => grind
-  case neg =>
-    cases m
-    case zero => grind
-    case succ m =>
-      have : lts.MTr (ss n) (μs.extract n m) (ss m) := ωTr_mTr (hnm := by grind) h
-      grind [MTr.comp]
-
-open ωSequence
+  grind [LTS.ωTr_isExecution h hnm]
 
 /-- Prepends an infinite execution with a transition. -/
 theorem LTS.ωTr.cons (htr : lts.Tr s μ t) (hωtr : lts.ωTr ss μs) (hm : ss 0 = t) :