From b99ac09209ec9d7999556d426ea3e6b6e6ba8c58 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Mon, 5 Jan 2026 16:24:31 -0800 Subject: [PATCH 1/3] feat: prove that an omega-language is regular iff it is a finite union of omega-languages of a special form --- Cslib.lean | 1 + Cslib/Computability/Automata/NA/Loop.lean | 30 ++----- Cslib/Computability/Automata/NA/Pair.lean | 81 +++++++++++++++++++ .../Languages/OmegaRegularLanguage.lean | 33 +++++++- Cslib/Foundations/Data/Nat/Segment.lean | 2 +- .../Data/OmegaSequence/InfOcc.lean | 19 +++++ Cslib/Foundations/Semantics/LTS/Basic.lean | 50 ++++++++++-- 7 files changed, 182 insertions(+), 34 deletions(-) create mode 100644 Cslib/Computability/Automata/NA/Pair.lean diff --git a/Cslib.lean b/Cslib.lean index 8c6984eb..d4260163 100644 --- a/Cslib.lean +++ b/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 diff --git a/Cslib/Computability/Automata/NA/Loop.lean b/Cslib/Computability/Automata/NA/Loop.lean index ddd19610..acc9983a 100644 --- a/Cslib/Computability/Automata/NA/Loop.lean +++ b/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 diff --git a/Cslib/Computability/Automata/NA/Pair.lean b/Cslib/Computability/Automata/NA/Pair.lean new file mode 100644 index 00000000..20b9915a --- /dev/null +++ b/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 diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean index 35072807..6527e658 100644 --- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean +++ b/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 ↔ diff --git a/Cslib/Foundations/Data/Nat/Segment.lean b/Cslib/Foundations/Data/Nat/Segment.lean index b6b7a49d..be061363 100644 --- a/Cslib/Foundations/Data/Nat/Segment.lean +++ b/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 diff --git a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean index 8dc76adf..16cd8260 100644 --- a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean +++ b/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 diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 59b0f16a..6b7ce0e3 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/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 From 84d9c5f685d5059c09935c2e99795e0fd14b5a46 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Sat, 17 Jan 2026 15:06:10 -0800 Subject: [PATCH 2/3] incorporate Chris Henson's comments --- Cslib/Computability/Automata/NA/Pair.lean | 23 +++++++++++++--------- Cslib/Foundations/Semantics/LTS/Basic.lean | 17 +++++++++------- 2 files changed, 24 insertions(+), 16 deletions(-) diff --git a/Cslib/Computability/Automata/NA/Pair.lean b/Cslib/Computability/Automata/NA/Pair.lean index 20b9915a..57d91e2b 100644 --- a/Cslib/Computability/Automata/NA/Pair.lean +++ b/Cslib/Computability/Automata/NA/Pair.lean @@ -34,7 +34,8 @@ theorem LTS.pairLang_regular [Finite State] (lts : LTS State Symbol) (s t : Stat (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] + ext + simp namespace NA.Buchi @@ -50,16 +51,20 @@ theorem language_eq_fin_iSup_hmul_omegaPow ω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 ⟨t, h_acc, h_t⟩ := frequently_in_finite_type.mp h_inf + use ss 0, by grind [NA.Run], t, h_acc 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))] + · have : na.MTr (ss 0) (xs.extract 0 (f 0)) (ss (f 0)) := by grind [LTS.ωTr_mTr, NA.Run] + grind [extract_eq_drop_take] · 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)] + use (f · - f 0) + split_ands + · grind [Nat.base_zero_strictMono] + · simp + · intro n + have mono_f (k : ℕ) : f 0 ≤ f (n + k) := h_mono.monotone (by grind) + grind [extract_drop, mono_f 0, LTS.ωTr_mTr h_run.trans <| h_mono.monotone (?_ : n ≤ n + 1)] · 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 @@ -70,7 +75,7 @@ theorem language_eq_fin_iSup_hmul_omegaPow 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], ?_⟩ + use xss, by grind [NA.Run] apply (drop_frequently_iff_frequently yl.length).mp apply frequently_iff_strictMono.mpr use zls.cumLen diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 6b7ce0e3..27851709 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -268,14 +268,17 @@ 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.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 + use sl.take μl.length ++ω ss + split_ands + · intro n + by_cases n < μl.length + · grind [get_append_left] + · by_cases n = μl.length + · grind [get_append_left, get_append_right'] + · grind [get_append_right', hωtr (n - μl.length - 1)] + · grind [get_append_left] · grind [get_append_left] - · by_cases n = μl.length - · grind [get_append_left, get_append_right'] - · grind [get_append_right', hωtr (n - μl.length - 1)] + · grind [drop_append_of_ge_length] open Nat in /-- Concatenating an infinite sequence of finite executions that connect an infinite sequence From 77e4fc9eb599e94b913bc756f3e055cb6bde60f3 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Sat, 17 Jan 2026 18:15:34 -0800 Subject: [PATCH 3/3] minor modification --- Cslib/Computability/Automata/NA/Pair.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Cslib/Computability/Automata/NA/Pair.lean b/Cslib/Computability/Automata/NA/Pair.lean index 57d91e2b..376052dd 100644 --- a/Cslib/Computability/Automata/NA/Pair.lean +++ b/Cslib/Computability/Automata/NA/Pair.lean @@ -37,17 +37,17 @@ theorem LTS.pairLang_regular [Finite State] (lts : LTS State Symbol) (s t : Stat ext simp -namespace NA.Buchi +namespace Automata.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) : + [Inhabited Symbol] [Finite State] (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, + simp only [Buchi.instωAcceptor, ωAcceptor.mem_language, ωLanguage.mem_iSup, ωLanguage.mem_hmul, LTS.mem_pairLang] constructor · rintro ⟨ss, h_run, h_inf⟩ @@ -81,6 +81,6 @@ theorem language_eq_fin_iSup_hmul_omegaPow use zls.cumLen grind [cumLen_strictMono] -end NA.Buchi +end Automata.NA.Buchi end Cslib