feat: prove that regular languages are closed under concatenation

Cslib.lean

@@ -17,6 +17,7 @@ import Cslib.Computability.Automata.NA.Loop
 import Cslib.Computability.Automata.NA.Prod
 import Cslib.Computability.Automata.NA.Sum
 import Cslib.Computability.Automata.NA.ToDA
+import Cslib.Computability.Automata.NA.Total
 import Cslib.Computability.Languages.ExampleEventuallyZero
 import Cslib.Computability.Languages.Language
 import Cslib.Computability.Languages.OmegaLanguage

Cslib/Computability/Automata/NA/Concat.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.NA.Basic
+import Cslib.Computability.Automata.NA.Total
 import Cslib.Foundations.Data.OmegaSequence.Temporal
 
 /-! # Concatenation of nondeterministic automata. -/
@@ -74,17 +74,18 @@ lemma concat_run_right {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ Sta
 
 /-- A run of `concat na1 na2` containing at least one `na2` state is the concatenation of
 an accepting finite run of `na1` followed by a run of `na2`. -/
-theorem concat_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)}
-    (hc : (concat na1 na2).Run xs ss) (hr : ∃ k, (ss k).isRight) :
-    ∃ n, xs.take n ∈ language na1 ∧ ∃ ss2, na2.Run (xs.drop n) ss2 ∧ ss.drop n = ss2.map inr := by
-  let n := Nat.find hr
-  have hl (k) (h_k : k < n) := not_isRight.mp <| Nat.find_min hr h_k
-  refine ⟨n, ?_, ?_⟩
+theorem concat_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)} {k : ℕ}
+    (hc : (concat na1 na2).Run xs ss) (hr : (ss k).isRight) :
+    ∃ n, n ≤ k ∧ xs.take n ∈ language na1 ∧
+    ∃ ss2, na2.Run (xs.drop n) ss2 ∧ ss.drop n = ss2.map inr := by
+  have hr' : ∃ k, (ss k).isRight := by grind
+  let n := Nat.find hr'
+  have hl (k) (h_k : k < n) := not_isRight.mp <| Nat.find_min hr' h_k
+  refine ⟨n, by grind, ?_, ?_⟩
   · by_cases h_n : n = 0
     · grind [concat_start_right]
     · grind [concat_run_left_right]
-  · have hr : (ss n).isRight := Nat.find_spec hr
-    grind [concat_run_right hc n hl hr]
+  · exact concat_run_right hc n hl (Nat.find_spec hr')
 
 /-- Given an accepting finite run of `na1` and a run of `na2`, there exists a run of
 `concat na1 na2` that is the concatenation of the two runs. -/
@@ -117,8 +118,8 @@ theorem concat_language_eq {acc2 : Set State2} :
   ext xs
   constructor
   · rintro ⟨ss, h_run, h_acc⟩
-    have h_ex2 : ∃ k, (ss k).isRight := by grind [Frequently.exists h_acc]
-    obtain ⟨n, h_acc1, ss2, h_run2, h_map2⟩ := concat_run_proj h_run h_ex2
+    obtain ⟨k, h_k⟩ : ∃ k, (ss k).isRight := by grind [Frequently.exists h_acc]
+    obtain ⟨n, _, h_acc1, ss2, h_run2, h_map2⟩ := concat_run_proj h_run h_k
     use xs.take n, h_acc1, xs.drop n, ?_, by simp
     use ss2, h_run2
     grind [(drop_frequently_iff_frequently n).mpr h_acc]
@@ -130,4 +131,48 @@ theorem concat_language_eq {acc2 : Set State2} :
 
 end Buchi
 
+namespace FinAcc
+
+/-- `finConcat na1 na2` is the concatenation of the "totalized" versions of `na1` and `na2`. -/
+def finConcat (na1 : FinAcc State1 Symbol) (na2 : FinAcc State2 Symbol)
+  : NA ((State1 ⊕ Unit) ⊕ (State2 ⊕ Unit)) Symbol :=
+  concat ⟨na1.totalize, inl '' na1.accept⟩ na2.totalize
+
+variable {na1 : FinAcc State1 Symbol} {na2 : FinAcc State2 Symbol}
+
+/-- `finConcat na1 na2` is total. -/
+instance : (finConcat na1 na2).Total where
+  total s x := match s with
+    | inl _ => ⟨inl (inr ()), by grind [finConcat, concat, NA.totalize, LTS.totalize]⟩
+    | inr _ => ⟨inr (inr ()), by grind [finConcat, concat, NA.totalize, LTS.totalize]⟩
+
+/-- `finConcat na1 na2` accepts the concatenation of the languages of `na1` and `na2`. -/
+theorem finConcat_language_eq [Inhabited Symbol] :
+    language (FinAcc.mk (finConcat na1 na2) (inr '' (inl '' na2.accept))) =
+    language na1 * language na2 := by
+  ext xl
+  constructor
+  · rintro ⟨s, _, t, h_acc, h_mtr⟩
+    obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.mTr_ωTr h_mtr
+    have hc : (finConcat na1 na2).Run (xl ++ω xs) ss := by grind [Run]
+    have hr : (ss xl.length).isRight := by grind
+    obtain ⟨n, _⟩ := concat_run_proj hc hr
+    refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩
+    · grind [totalize_language_eq, take_append_of_le_length]
+    · have : ss xl.length = (ss.drop n) (xl.length - n) := by grind
+      grind [drop_append_of_le_length, take_append_of_le_length, totalize_run_mtr]
+    · exact xl.take_append_drop n
+  · rintro ⟨xl1, h_xl1, xl2, h_xl2, rfl⟩
+    rw [← totalize_language_eq] at h_xl1
+    obtain ⟨_, h_s2, _, _, h_mtr2⟩ := h_xl2
+    obtain ⟨_, _, h_run2, _, _⟩ := totalize_mtr_run h_s2 h_mtr2
+    obtain ⟨ss, ⟨_, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2
+    grind [
+      finConcat, List.length_append, take_append_of_le_length,
+      extract_eq_drop_take, =_ append_append_ωSequence, get_drop xl2.length xl1.length ss,
+      LTS.ωTr_mTr h_ωtr (zero_le (xl1.length + xl2.length))
+    ]
+
+end FinAcc
+
 end Cslib.Automata.NA

Cslib/Computability/Automata/NA/Total.lean

@@ -0,0 +1,57 @@
+/-
+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
+-/
+
+import Cslib.Computability.Automata.NA.Basic
+
+/-! # Making a nondeterministic automaton total.
+-/
+
+namespace Cslib.Automata.NA
+
+open Sum ωSequence Acceptor
+
+variable {Symbol State : Type*}
+
+/-- `NA.totalize` makes the original NA total by replacing its LTS with `LTS.totalize`
+and its starting states with their lifted non-sink versions. -/
+def totalize (na : NA State Symbol) : NA (State ⊕ Unit) Symbol where
+  toLTS := na.toLTS.totalize
+  start := inl '' na.start
+
+variable {na : NA State Symbol}
+
+/-- In an infinite execution of `NA.totalize`, as long as the NA stays in a non-sink state,
+the execution so far corresponds to a finite execution of the original NA. -/
+theorem totalize_run_mtr {xs : ωSequence Symbol} {ss : ωSequence (State ⊕ Unit)} {n : ℕ}
+    (h : na.totalize.Run xs ss) (hl : (ss n).isLeft) :
+    ∃ s t, na.MTr s (xs.take n) t ∧ s ∈ na.start ∧ ss 0 = inl s ∧ ss n = inl t := by
+  obtain ⟨s, _, eq₁⟩ := h.start
+  obtain ⟨t, eq₂⟩ := isLeft_iff.mp hl
+  use s, t
+  refine ⟨?_, by grind⟩
+  -- TODO: `grind` does not use congruence relations with `na.totalize.MTr`
+  rw [← LTS.totalize.mtr_left_iff, ← extract_eq_take, eq₁, ← eq₂]
+  exact LTS.ωTr_mTr h.trans (by grind)
+
+/-- Any finite execution of the original NA can be extended to an infinite execution of
+`NA.totalize`, provided that the alphabet is inbabited. -/
+theorem totalize_mtr_run [Inhabited Symbol] {xl : List Symbol} {s t : State}
+    (hs : s ∈ na.start) (hm : na.MTr s xl t) :
+    ∃ xs ss, na.totalize.Run (xl ++ω xs) ss ∧ ss 0 = inl s ∧ ss xl.length = inl t := by
+  grind [totalize, Run, LTS.Total.mTr_ωTr <| LTS.totalize.mtr_left_iff.mpr hm]
+
+namespace FinAcc
+
+/-- `NA.totalize` and the original NA accept the same language of finite words,
+as long as the accepting states are also lifted in the obvious way. -/
+theorem totalize_language_eq {na : FinAcc State Symbol} :
+    language (FinAcc.mk na.totalize (inl '' na.accept)) = language na := by
+  ext xl
+  simp [totalize]
+
+end FinAcc
+
+end Cslib.Automata.NA

Cslib/Computability/Languages/RegularLanguage.lean

@@ -6,8 +6,10 @@ Authors: Ching-Tsun Chou
 
 import Cslib.Computability.Automata.DA.Prod
 import Cslib.Computability.Automata.DA.ToNA
+import Cslib.Computability.Automata.NA.Concat
 import Cslib.Computability.Automata.NA.ToDA
 import Mathlib.Computability.DFA
+import Mathlib.Data.Finite.Sum
 import Mathlib.Data.Set.Card
 import Mathlib.Tactic.Common
 
@@ -49,19 +51,22 @@ theorem IsRegular.iff_nfa {l : Language Symbol} :
     use Set State, inferInstance, na.toDAFinAcc
     grind
 
+/-- The complementation of a regular language is regular. -/
 theorem IsRegular.compl {l : Language Symbol} (h : l.IsRegular) : (lᶜ).IsRegular := by
   rw [IsRegular.iff_dfa] at h ⊢
   obtain ⟨State, _, ⟨da, acc⟩, rfl⟩ := h
   use State, inferInstance, ⟨da, accᶜ⟩
   grind
 
+/-- The empty language is regular. -/
 @[simp]
 theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by
   rw [IsRegular.iff_dfa]
   let flts := FLTS.mk (fun () (_ : Symbol) ↦ ())
   use Unit, inferInstance, ⟨DA.mk flts (), ∅⟩
   grind
 
+/-- The language containing only the empty word is regular. -/
 @[simp]
 theorem IsRegular.one : (1 : Language Symbol).IsRegular := by
   rw [IsRegular.iff_dfa]
@@ -73,11 +78,13 @@ theorem IsRegular.one : (1 : Language Symbol).IsRegular := by
     grind
   · grind [Language.mem_one]
 
+/-- The language of all finite words is regular. -/
 @[simp]
 theorem IsRegular.top : (⊤ : Language Symbol).IsRegular := by
   have : (⊥ᶜ : Language Symbol).IsRegular := IsRegular.compl <| IsRegular.zero
   rwa [← compl_bot]
 
+/-- The intersection of two regular languages is regular. -/
 @[simp]
 theorem IsRegular.inf {l1 l2 : Language Symbol}
     (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 ⊓ l2).IsRegular := by
@@ -87,6 +94,7 @@ theorem IsRegular.inf {l1 l2 : Language Symbol}
   use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∩ snd ⁻¹' acc2⟩
   ext; grind [Language.mem_inf]
 
+/-- The union of two regular languages is regular. -/
 @[simp]
 theorem IsRegular.add {l1 l2 : Language Symbol}
     (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 + l2).IsRegular := by
@@ -96,6 +104,7 @@ theorem IsRegular.add {l1 l2 : Language Symbol}
   use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∪ snd ⁻¹' acc2⟩
   ext; grind [Language.mem_add]
 
+/-- The intersection of any finite number of regular languages is regular. -/
 @[simp]
 theorem IsRegular.iInf {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol}
     (h : ∀ i ∈ s, (l i).IsRegular) : (⨅ i ∈ s, l i).IsRegular := by
@@ -107,6 +116,7 @@ theorem IsRegular.iInf {I : Type*} [Finite I] {s : Set I} {l : I → Language Sy
     rw [iInf_insert]
     grind [IsRegular.inf]
 
+/-- The union of any finite number of regular languages is regular. -/
 @[simp]
 theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol}
     (h : ∀ i ∈ s, (l i).IsRegular) : (⨆ i ∈ s, l i).IsRegular := by
@@ -121,4 +131,16 @@ theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {l : I → Language Sy
     rw [iSup_insert]
     apply IsRegular.add <;> grind
 
+open NA.FinAcc Sum in
+/-- The concatenation of two regular languages is regular. -/
+@[simp]
+theorem IsRegular.mul [Inhabited Symbol] {l1 l2 : Language Symbol}
+    (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 * l2).IsRegular := by
+  rw [IsRegular.iff_nfa] at h1 h2 ⊢
+  obtain ⟨State1, h_fin1, nfa1, rfl⟩ := h1
+  obtain ⟨State2, h_fin1, nfa2, rfl⟩ := h2
+  use (State1 ⊕ Unit) ⊕ (State2 ⊕ Unit), inferInstance,
+    ⟨finConcat nfa1 nfa2, inr '' (inl '' nfa2.accept)⟩
+  exact finConcat_language_eq
+
 end Cslib.Language