|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Ching-Tsun Chou. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Ching-Tsun Chou |
| 5 | +-/ |
| 6 | + |
| 7 | +import Cslib.Computability.Automata.DA |
| 8 | +import Cslib.Computability.Automata.NA |
| 9 | +import Cslib.Foundations.Data.OmegaSequence.InfOcc |
| 10 | +import Mathlib.Tactic |
| 11 | + |
| 12 | +/-! |
| 13 | +# ω-Regular languages |
| 14 | +
|
| 15 | +This file defines ω-regular languages and proves some properties of them. |
| 16 | +-/ |
| 17 | + |
| 18 | +open Set Function Filter Cslib.ωSequence Cslib.Automata ωAcceptor |
| 19 | +open scoped Computability |
| 20 | + |
| 21 | +namespace Cslib.ωLanguage.Example |
| 22 | + |
| 23 | +section EventuallyZero |
| 24 | + |
| 25 | +/-- A sequence `xs` is in `eventually_zero` iff `xs k = 0` for all large `k`. -/ |
| 26 | +@[scoped grind =] |
| 27 | +def eventually_zero : ωLanguage (Fin 2) := |
| 28 | + { xs : ωSequence (Fin 2) | ∀ᶠ k in atTop, xs k = 0 } |
| 29 | + |
| 30 | +/-- `eventually_zero` is accepted by a 2-state nondeterministic Buchi automaton. -/ |
| 31 | +theorem eventually_zero_accepted_by_na_buchi : |
| 32 | + ∃ a : NA.Buchi (Fin 2) (Fin 2), language a = eventually_zero := by |
| 33 | + let a : NA.Buchi (Fin 2) (Fin 2) := { |
| 34 | + -- Once state 1 is reached, only symbol 0 is accepted and the next state is still 1 |
| 35 | + Tr s x s' := s = 1 → x = 0 ∧ s' = 1 |
| 36 | + start := {0} |
| 37 | + accept := {1} } |
| 38 | + use a ; ext xs ; constructor |
| 39 | + · rintro ⟨ss, h_run, h_acc⟩ |
| 40 | + obtain ⟨m, h_m⟩ := Frequently.exists h_acc |
| 41 | + apply eventually_atTop.mpr |
| 42 | + use m ; intro n h_n |
| 43 | + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h_n |
| 44 | + suffices h1 : xs (m + k) = 0 ∧ ss (m + k) = 1 by grind |
| 45 | + induction k |
| 46 | + case zero => |
| 47 | + have := h_run.2 m |
| 48 | + grind |
| 49 | + case succ k h_ind => |
| 50 | + have := h_run.2 (m + k) |
| 51 | + have := h_run.2 (m + k + 1) |
| 52 | + grind |
| 53 | + · intro h |
| 54 | + obtain ⟨m, h_m⟩ := eventually_atTop.mp h |
| 55 | + let ss : ωSequence (Fin 2) := fun k ↦ if k ≤ m then (0 : Fin 2) else 1 |
| 56 | + refine ⟨ss, ?_, ?_⟩ |
| 57 | + · simp [a, ss, NA.Run] |
| 58 | + grind |
| 59 | + · apply Eventually.frequently |
| 60 | + apply eventually_atTop.mpr |
| 61 | + use (m + 1) ; intro k _ |
| 62 | + simp [a, ss, show m < k by omega] |
| 63 | + |
| 64 | +private lemma extend_by_zero (u : List (Fin 2)) : |
| 65 | + u ++ω const 0 ∈ eventually_zero := by |
| 66 | + apply eventually_atTop.mpr |
| 67 | + use u.length |
| 68 | + intro k h_k |
| 69 | + rw [get_append_right' h_k] |
| 70 | + simp |
| 71 | + |
| 72 | +private lemma extend_by_one (u : List (Fin 2)) : |
| 73 | + ∃ v, 1 ∈ v ∧ u ++ v ++ω const 0 ∈ eventually_zero := by |
| 74 | + refine ⟨[1], ?_, ?_⟩ |
| 75 | + · simp |
| 76 | + · apply extend_by_zero |
| 77 | + |
| 78 | +private lemma extend_by_hyp {l : Language (Fin 2)} (h : l↗ω = eventually_zero) |
| 79 | + (u : List (Fin 2)) : ∃ v, 1 ∈ v ∧ u ++ v ∈ l := by |
| 80 | + obtain ⟨v, _, h_pfx⟩ := extend_by_one u |
| 81 | + rw [← h] at h_pfx |
| 82 | + obtain ⟨m, h_m, h_uv⟩ := frequently_atTop.mp h_pfx (u ++ v).length |
| 83 | + use (v ++ω ωSequence.const 0).extract 0 (m - u.length) |
| 84 | + rw [extract_append_zero_right (show v.length ≤ m - u.length by grind)] |
| 85 | + constructor |
| 86 | + · simp_all |
| 87 | + · rw [extract_append_zero_right h_m] at h_uv |
| 88 | + grind |
| 89 | + |
| 90 | +private noncomputable def oneSegs {l : Language (Fin 2)} (h : l↗ω = eventually_zero) (n : ℕ) := |
| 91 | + Classical.choose <| extend_by_hyp h (List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten |
| 92 | + |
| 93 | +private lemma oneSegs_lemma {l : Language (Fin 2)} (h : l↗ω = eventually_zero) (n : ℕ) : |
| 94 | + 1 ∈ oneSegs h n ∧ (List.ofFn (fun k : Fin (n + 1) ↦ oneSegs h k)).flatten ∈ l := by |
| 95 | + let P u v := 1 ∈ v ∧ u ++ v ∈ l |
| 96 | + have : P ((List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten) (oneSegs h n) := by |
| 97 | + unfold oneSegs |
| 98 | + exact Classical.choose_spec <| extend_by_hyp h (List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten |
| 99 | + obtain ⟨h1, h2⟩ := this |
| 100 | + refine ⟨h1, ?_⟩ |
| 101 | + rw [List.ofFn_succ_last] |
| 102 | + simpa |
| 103 | + |
| 104 | +theorem eventually_zero_not_omegaLim : |
| 105 | + ¬ ∃ l : Language (Fin 2), l↗ω = eventually_zero := by |
| 106 | + rintro ⟨l, h⟩ |
| 107 | + let ls := ωSequence.mk (oneSegs h) |
| 108 | + have h_segs := oneSegs_lemma h |
| 109 | + have h_pos : ∀ k, (ls k).length > 0 := by grind |
| 110 | + have h_ev : ls.flatten ∈ eventually_zero := by |
| 111 | + rw [← h, mem_omegaLim, frequently_iff_strictMono] |
| 112 | + use (fun k ↦ ls.cumLen (k + 1)) |
| 113 | + constructor |
| 114 | + · intro j k h_jk |
| 115 | + have := cumLen_strictMono h_pos (show j + 1 < k + 1 by omega) |
| 116 | + grind |
| 117 | + · intro n |
| 118 | + rw [extract_eq_take, ← flatten_take h_pos] |
| 119 | + suffices _ : ls.take (n + 1) = List.ofFn (fun k : Fin (n + 1) ↦ oneSegs h k) by grind |
| 120 | + simp [← extract_eq_take, extract_eq_ofFn, ls] |
| 121 | + obtain ⟨m, _⟩ := eventually_atTop.mp h_ev |
| 122 | + have h_inf : ∃ᶠ n in atTop, n ∈ range ls.cumLen := by |
| 123 | + apply frequently_iff_strictMono.mpr |
| 124 | + have := cumLen_strictMono h_pos |
| 125 | + grind |
| 126 | + obtain ⟨n, h_n, k, rfl⟩ := frequently_atTop.mp h_inf m |
| 127 | + have h_k : 1 ∈ ls k := by grind |
| 128 | + simp only [← extract_flatten h_pos k, List.mem_iff_getElem, length_extract] at h_k |
| 129 | + grind |
| 130 | + |
| 131 | +end EventuallyZero |
| 132 | + |
| 133 | +end Cslib.ωLanguage.Example |
0 commit comments