Skip to content

Commit 882f606

Browse files
ctchouctchou
committed
feat: prove that the Buchi congruence has the saturation property
1 parent e8dd2a0 commit 882f606

4 files changed

Lines changed: 173 additions & 14 deletions

File tree

‎Cslib/Computability/Languages/Congruences/BuchiCongruence.lean‎

Lines changed: 128 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ module
88

99
public import Cslib.Computability.Automata.NA.Pair
1010
public import Cslib.Computability.Languages.Congruences.RightCongruence
11+
public import Cslib.Computability.Languages.OmegaLanguage
12+
public import Cslib.Foundations.Data.Set.Saturation
1113

1214
@[expose] public section
1315

@@ -20,7 +22,7 @@ of ω-regular languages under complementation.
2022

2123
namespace Cslib.Automata.NA.Buchi
2224

23-
open Function
25+
open Function Set Filter ωAcceptor ωLanguage ωSequence
2426

2527
variable {Symbol : Type*} {State : Type}
2628

@@ -32,7 +34,7 @@ following two conditions hold:
3234
from `s` to `t` via an acceptingg states. -/
3335
def BuchiCongruence (na : Buchi State Symbol) : RightCongruence Symbol where
3436
eq.r u v :=
35-
∀ {s t}, (u ∈ na.pairLang s t ↔ v ∈ na.pairLang s t) ∧
37+
∀ s t, (u ∈ na.pairLang s t ↔ v ∈ na.pairLang s t) ∧
3638
(u ∈ na.pairViaLang na.accept s t ↔ v ∈ na.pairViaLang na.accept s t)
3739
eq.iseqv.refl := by grind
3840
eq.iseqv.symm := by grind
@@ -72,4 +74,128 @@ lemma buchiCongrParam_surjective : Surjective na.BuchiCongrParam := by
7274
theorem buchiCongruence_fin_index [Finite State] : Finite (Quotient na.BuchiCongruence.eq) :=
7375
Finite.of_surjective na.BuchiCongrParam buchiCongrParam_surjective
7476

77+
/-- If `xl` and `yl` belong to the same equivalence class of `na.BuchiCongruence`
78+
and `xl` can move `na` from state `s` to state `t`, then so can `yl` and, furthermore,
79+
if `xl` makes `na` go through an accepting state of `na`, then so can `yl`. -/
80+
lemma buchiCongruence_transfer
81+
{a : Quotient na.BuchiCongruence.eq} {xl yl : List Symbol} {s t : State}
82+
(hc : xl ∈ na.BuchiCongruence.eqvCls a) (hc' : yl ∈ na.BuchiCongruence.eqvCls a)
83+
(hp : xl ∈ na.pairLang s t) : ∃ sl, na.IsExecution s yl t sl ∧
84+
( xl ∈ na.pairViaLang na.accept s t → ∃ r ∈ na.accept, r ∈ sl ) := by
85+
have h_eq : na.BuchiCongruence.eq xl yl := by
86+
apply Quotient.exact
87+
grind
88+
have := h_eq s t
89+
by_cases h_xl : xl ∈ na.pairViaLang na.accept s t
90+
· have h_yl : yl ∈ na.pairViaLang na.accept s t := by grind
91+
obtain ⟨r, _, yl1, yl2, h_yl1, h_yl2, rfl⟩ := LTS.mem_pairViaLang.mp h_yl
92+
obtain ⟨sl1, h_yl1⟩ := LTS.mTr_isExecution h_yl1
93+
obtain ⟨sl2, h_yl2⟩ := LTS.mTr_isExecution h_yl2
94+
have := LTS.IsExecution.comp h_yl1 h_yl2
95+
grind [LTS.IsExecution]
96+
· have h_yl : yl ∈ na.pairLang s t := by grind
97+
grind [LTS.mTr_isExecution h_yl]
98+
99+
/-- `na.buchiFamily` is a family of ω-languages indexed by a pair of equivalence classes
100+
of `na.BuchiCongruence` which will turn out to saturate the ω-language accepted by `na`
101+
and cover all possible ω-sequences. -/
102+
def buchiFamily [Inhabited Symbol] (na : Buchi State Symbol) :
103+
Quotient na.BuchiCongruence.eq × Quotient na.BuchiCongruence.eq → ωLanguage Symbol
104+
| (a, b) => na.BuchiCongruence.eqvCls a * (na.BuchiCongruence.eqvCls b)^ω
105+
106+
theorem mem_buchiFamily [Inhabited Symbol]
107+
{xs : ωSequence Symbol} {a b : Quotient na.BuchiCongruence.eq} :
108+
xs ∈ na.buchiFamily (a, b) ↔ ∃ xl, ∃ xls : ωSequence (List Symbol),
109+
xl ∈ na.BuchiCongruence.eqvCls a ∧ (∀ k, xls k ∈ na.BuchiCongruence.eqvCls b - 1) ∧
110+
xl ++ω xls.flatten = xs := by
111+
grind [buchiFamily]
112+
113+
-- This intermediate result is split out of the proof of `buchiCongruence_saturation` below
114+
-- because that proof was too big and kept exceeding the default `maxHeartbeats`.
115+
private lemma frequently_via_accept [Inhabited Symbol]
116+
{xl : List Symbol} {xls : ωSequence (List Symbol)} {ss : ωSequence State}
117+
(h_acc : ∃ᶠ (k : ℕ) in atTop, ss k ∈ na.accept) (h_exec : na.ωTr ss (xl ++ω xls.flatten))
118+
(h_xls_p : ∀ (k : ℕ), (xls k).length > 0)
119+
(f : ℕ → ℕ) (h_f : f = fun k => xl.length + xls.cumLen k)
120+
(ts : ωSequence State) (h_ts : ts = ωSequence.mk (fun k ↦ ss (f k))) :
121+
∃ᶠ (k : ℕ) in atTop, xls k ∈ na.pairViaLang na.accept (ts k) (ts (k + 1)) := by
122+
have hm : StrictMono f := by
123+
intro m n h_mn
124+
grind [cumLen_strictMono h_xls_p h_mn]
125+
apply Frequently.mono <| frequently_in_strictMono hm h_acc
126+
rintro n ⟨k, _, _⟩
127+
apply LTS.mem_pairViaLang.mpr
128+
use ss (f n + k), by grind
129+
use (xls n).take k, (xls n).drop k
130+
split_ands
131+
· have := LTS.isExecution_mTr na.toLTS <|
132+
LTS.ωTr_isExecution h_exec (show f n ≤ f n + k by grind)
133+
suffices (xl ++ω xls.flatten).extract (f n) (f n + k) = (xls n).take k by grind
134+
have : xls.flatten.extract (xls.cumLen n) (xls.cumLen n + k) = (xls n).take k := by
135+
grind [extract_flatten h_xls_p n]
136+
grind only [extract_apppend_right_right]
137+
· have := LTS.isExecution_mTr na.toLTS <|
138+
LTS.ωTr_isExecution h_exec (show f n + k ≤ f (n + 1) by grind)
139+
suffices (xl ++ω xls.flatten).extract (f n + k) (f (n + 1)) = (xls n).drop k by grind
140+
have : xls.flatten.extract (xls.cumLen n + k) (xls.cumLen (n + 1)) = (xls n).drop k := by
141+
grind [extract_flatten h_xls_p n]
142+
grind only [= cumLen_succ, extract_apppend_right_right]
143+
· grind only [!List.take_append_drop]
144+
145+
/-- `na.buchiFamily` saturates the ω-language accepted by `na`. -/
146+
theorem buchiCongruence_saturation [Inhabited Symbol] :
147+
Saturates na.buchiFamily (language na) := by
148+
rintro ⟨a, b⟩ ⟨xs, h_xs, h_lang⟩ ys h_ys
149+
obtain ⟨xl, xls, h_xl_c, h_xls_c, rfl⟩ := mem_buchiFamily.mp h_xs
150+
obtain ⟨yl, yls, h_yl_c, h_yls_c, rfl⟩ := mem_buchiFamily.mp h_ys
151+
obtain ⟨ss, ⟨h_init, h_exec⟩, h_acc⟩ := h_lang
152+
have h_xls_p (k : ℕ) : (xls k).length > 0 := by
153+
grind [Language.mem_sub_one, List.ne_nil_iff_length_pos]
154+
have h_yls_p (k : ℕ) : (yls k).length > 0 := by
155+
grind [Language.mem_sub_one, List.ne_nil_iff_length_pos]
156+
let f (k : ℕ) := xl.length + xls.cumLen k
157+
let ts := ωSequence.mk (fun k ↦ ss (f k))
158+
have h_xl_e : xl ∈ na.pairLang (ss 0) (ts 0) := by
159+
have := LTS.ωTr_mTr h_exec (show 0 ≤ xl.length by grind)
160+
grind [extract_append_zero_right, LTS.mem_pairLang]
161+
have h_xls_e (k : ℕ) : (xls k) ∈ na.pairLang (ts k) (ts (k + 1)) := by
162+
have := LTS.ωTr_mTr h_exec (show f k ≤ f (k + 1) by grind)
163+
suffices (xl ++ω xls.flatten).extract (f k) (f (k + 1)) = xls k by grind [LTS.mem_pairLang]
164+
simp (disch := grind) [extract_apppend_right_right, f]
165+
have h_yl_e : yl ∈ na.pairLang (ss 0) (ts 0) := by
166+
obtain ⟨sl, h_e, _⟩ := buchiCongruence_transfer h_xl_c h_yl_c h_xl_e
167+
grind [LTS.mem_pairLang, LTS.isExecution_mTr (lts := na.toLTS) h_e]
168+
have h_yls (k : ℕ) : ∃ sl, na.IsExecution (ts k) (yls k) (ts (k + 1)) sl ∧
169+
( (xls k) ∈ na.pairViaLang na.accept (ts k) (ts (k + 1)) → ∃ s ∈ na.accept, s ∈ sl ) := by
170+
exact buchiCongruence_transfer ((h_xls_c k).left) ((h_yls_c k).left) (h_xls_e k)
171+
choose sls h_yls_e h_yls_a using h_yls
172+
obtain ⟨ss1, h_ss1_run, h_ss1_seg⟩ := LTS.IsExecution.flatten h_yls_e h_yls_p
173+
obtain ⟨ss2, _, _, _, _⟩ := LTS.ωTr.append h_yl_e h_ss1_run (by
174+
have : ss1 0 = (sls 0)[0]'(by grind) := by
175+
grind [get_extract (xs := ss1) (show 0 < yls.cumLen 1 - yls.cumLen 0 by grind)]
176+
have : ts 0 = (sls 0)[0]'(by grind) := by grind [LTS.IsExecution]
177+
grind)
178+
use ss2, by grind [Run.mk]
179+
suffices ∃ᶠ (k : ℕ) in Filter.atTop, ss1 k ∈ na.accept by
180+
apply (drop_frequently_iff_frequently yl.length).mp
181+
grind
182+
have h_acc' := frequently_via_accept h_acc h_exec h_xls_p f rfl ts rfl
183+
have h_mono : StrictMono yls.cumLen := cumLen_strictMono h_yls_p
184+
apply frequently_atTop.mpr
185+
intro n
186+
obtain ⟨m, _, s, _, h_mem⟩ := frequently_atTop.mp (Frequently.mono h_acc' h_yls_a) n
187+
have : m ≤ yls.cumLen m := by grind [StrictMono.add_le_nat h_mono m 0]
188+
obtain ⟨k, _, _⟩ := List.mem_iff_getElem.mp h_mem
189+
use yls.cumLen m + k, by grind
190+
suffices ss1 (yls.cumLen m + k) = (sls m)[k] by grind
191+
by_cases k < (yls m).length
192+
· have h1 : k < yls.cumLen (m + 1) - yls.cumLen m := by grind only [= cumLen_succ]
193+
simp [← get_extract (xs := ss1) h1, h_ss1_seg m]
194+
· obtain ⟨_, _, _, _⟩ := h_yls_e m
195+
obtain ⟨_, _, _, _⟩ := h_yls_e (m + 1)
196+
have := h_mono (show m + 1 < m + 2 by omega)
197+
have h1 : 0 < yls.cumLen (m + 2) - yls.cumLen (m + 1) := by omega
198+
have h2 := get_extract (xs := ss1) h1
199+
grind only [= cumLen_succ, = get_fun, = List.getElem_take]
200+
75201
end Cslib.Automata.NA.Buchi

‎Cslib/Foundations/Data/OmegaSequence/InfOcc.lean‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@ Authors: Ching-Tsun Chou
66

77
module
88

9+
public import Cslib.Foundations.Data.Nat.Segment
910
public import Cslib.Foundations.Data.OmegaSequence.Defs
1011
public import Mathlib.Data.Fintype.Pigeonhole
11-
public import Mathlib.Order.Filter.AtTopBot.Basic
1212
public import Mathlib.Order.Filter.Cofinite
1313

1414
@[expose] public section
@@ -59,6 +59,24 @@ theorem frequently_in_finite_type [Finite α] {s : Set α} {xs : ωSequence α}
5959
apply Frequently.mono h_inf
6060
grind
6161

62+
open Nat in
63+
/-- If `p` is true infinitely often, then `p` is true in infinitely many segments
64+
of any strictly monotonic function `f`. -/
65+
theorem frequently_in_strictMono {p : ℕ → Prop} {f : ℕ → ℕ}
66+
(hm : StrictMono f) (hf : ∃ᶠ k in atTop, p k) :
67+
∃ᶠ n in atTop, ∃ k, k < f (n + 1) - f n ∧ p (f n + k) := by
68+
apply frequently_atTop.mpr
69+
intro m
70+
obtain ⟨k, _, _⟩ := frequently_atTop.mp hf (f m)
71+
use segment f k
72+
have h0 : f 0 ≤ k := by grind [StrictMono.monotone hm (show 0 ≤ m by grind)]
73+
split_ands
74+
· by_contra
75+
have h1 : segment f k + 1 ≤ m := by grind
76+
grind [(StrictMono.le_iff_le hm).mpr h1, segment_upper_bound' hm h0]
77+
· use k - f (segment f k)
78+
grind [segment_lower_bound' hm h0, segment_upper_bound' hm h0]
79+
6280
end ωSequence
6381

6482
end Cslib

‎Cslib/Foundations/Data/OmegaSequence/Init.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -508,6 +508,17 @@ theorem extract_0u_extract_l {xs : ωSequence α} {n i : ℕ} :
508508
(xs.extract 0 n).extract i = xs.extract i n := by
509509
grind
510510

511+
@[simp, scoped grind =]
512+
theorem take_extract {xs : ωSequence α} {m n k : ℕ} (h : k ≤ n - m) :
513+
(xs.extract m n).take k = xs.extract m (m + k) := by
514+
grind [extract_lu_extract_lu (xs := xs) (i := 0) h]
515+
516+
@[simp, scoped grind =]
517+
theorem drop_extract {xs : ωSequence α} {m n k : ℕ} (h : k ≤ n - m) :
518+
(xs.extract m n).drop k = xs.extract (m + k) n := by
519+
have := extract_lu_extract_lu (xs := xs) (m := m) (n := n) (i := k) (j := n - m)
520+
grind [length_extract, List.take_length]
521+
511522
end ωSequence
512523

513524
end Cslib

‎Cslib/Foundations/Semantics/LTS/Basic.lean‎

Lines changed: 15 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -215,6 +215,13 @@ theorem LTS.mTr_isExecution_iff : lts.MTr s1 μs s2 ↔
215215
∃ ss : List State, lts.IsExecution s1 μs s2 ss := by
216216
grind
217217

218+
/-- The composition of two executions is an execution. -/
219+
theorem LTS.IsExecution.comp
220+
{lts : LTS State Label} {s r t : State} {μs1 μs2 : List Label} {ss1 ss2 : List State}
221+
(h1 : lts.IsExecution s μs1 r ss1) (h2 : lts.IsExecution r μs2 t ss2) :
222+
lts.IsExecution s (μs1 ++ μs2) t (ss1 ++ ss2.drop 1) := by
223+
use by grind, by grind, by grind, by grind
224+
218225
/-- An execution can be split at any intermediate state into two executions. -/
219226
theorem LTS.IsExecution.split
220227
{lts : LTS State Label} {s t : State} {μs : List Label} {ss : List State}
@@ -317,20 +324,17 @@ def LTS.ωTr (lts : LTS State Label) (ss : ωSequence State) (μs : ωSequence L
317324

318325
variable {lts : LTS State Label}
319326

320-
open scoped ωSequence in
327+
open ωSequence
328+
321329
/-- Any finite execution extracted from an infinite execution is valid. -/
330+
theorem LTS.ωTr_isExecution (h : lts.ωTr ss μs) {n m : ℕ} (hnm : n ≤ m) :
331+
lts.IsExecution (ss n) (μs.extract n m) (ss m) (ss.extract n (m + 1)) := by
332+
grind
333+
334+
/-- Any multistep transition extracted from an infinite execution is valid. -/
322335
theorem LTS.ωTr_mTr (h : lts.ωTr ss μs) {n m : ℕ} (hnm : n ≤ m) :
323336
lts.MTr (ss n) (μs.extract n m) (ss m) := by
324-
by_cases heq : n = m
325-
case pos => grind
326-
case neg =>
327-
cases m
328-
case zero => grind
329-
case succ m =>
330-
have : lts.MTr (ss n) (μs.extract n m) (ss m) := ωTr_mTr (hnm := by grind) h
331-
grind [MTr.comp]
332-
333-
open ωSequence
337+
grind [LTS.ωTr_isExecution h hnm]
334338

335339
/-- Prepends an infinite execution with a transition. -/
336340
theorem LTS.ωTr.cons (htr : lts.Tr s μ t) (hωtr : lts.ωTr ss μs) (hm : ss 0 = t) :

0 commit comments

Comments
 (0)