feat: prove that regular languages are closed under concatenation

Cslib.lean

@@ -16,6 +16,7 @@ import Cslib.Computability.Automata.NA.Hist
 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,49 @@ 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. -/
+def finConcat_total : (finConcat na1 na2).Total where
+  next s x := match s with
+    | inl s1 => inl (inr ())
+    | inr s2 => inr (inr ())
+  total s x := 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 finConcat_total 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.totalize.total na.toLTS).mTr_ωTr, =_ LTS.totalize.mtr_left_iff]
+
+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

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -239,7 +239,7 @@ variable {lts : LTS State Label}
 
 open scoped ωSequence in
 /-- Any finite execution extracted from an infinite execution is valid. -/
-theorem LTS.ωTr_mTr {n m : ℕ} {hnm : n ≤ m} (h : lts.ωTr ss μs) :
+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
@@ -250,16 +250,119 @@ theorem LTS.ωTr_mTr {n m : ℕ} {hnm : n ≤ m} (h : lts.ωTr ss μs) :
       have : lts.MTr (ss n) (μs.extract n m) (ss m) := ωTr_mTr (hnm := by grind) h
       grind [MTr.comp]
 
-open scoped ωSequence
+open ωSequence
 
 /-- Prepends an infinite execution with a transition. -/
-theorem LTS.ωTr.cons (hmtr : lts.Tr s1 μ s2) (hωtr : lts.ωTr ss μs) (hm : ss 0 = s2) :
-    lts.ωTr (s1 ::ω ss) (μ ::ω μs) := by
+theorem LTS.ωTr.cons (htr : lts.Tr s μ t) (hωtr : lts.ωTr ss μs) (hm : ss 0 = t) :
+    lts.ωTr (s ::ω ss) (μ ::ω μs) := by
   intro i
   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
+  obtain ⟨sl, _, _, _, _⟩ := LTS.MTr.exists_states hmtr
+  refine ⟨sl ++ω ss.drop 1, ?_, by grind [get_append_left], by grind [get_append_left]⟩
+  intro n
+  by_cases n < μl.length
+  · grind [get_append_left]
+  · by_cases n = μl.length
+    · grind [get_append_left]
+    · grind [get_append_right', hωtr (n - μl.length - 1)]
+
 end ωMultiStep
 
+section Total
+
+/-! ## Total LTS
+
+A LTS is total iff every state has a transition for every label.
+-/
+
+open Sum ωSequence
+
+variable {State Label : Type*} {lts : LTS State Label}
+
+/-- `LTS.Total` provides a witness that the LTS is total. -/
+structure LTS.Total (lts : LTS State Label) where
+  /-- `next` rovides a next state for any given starting state and label. -/
+  next : State → Label → State
+  /-- A proof that the state provided by `next` indeed forms a legal transition. -/
+  total s μ : lts.Tr s μ (next s μ)
+
+/-- `LTS.makeωTr` builds an infinite execution of a total LTS from any starting state and
+any infinite sequence of labels. -/
+def LTS.makeωTr (lts : LTS State Label) (h : lts.Total)
+    (s : State) (μs : ωSequence Label) : ℕ → State
+  | 0 => s
+  | n + 1 => h.next (lts.makeωTr h s μs n) (μs n)
+
+/-- If a LTS is total, then there exists an infinite execution from any starting state and
+over any infinite sequence of labels. -/
+theorem LTS.Total.ωTr_exists (h : lts.Total) (s : State) (μs : ωSequence Label) :
+    ∃ ss, lts.ωTr ss μs ∧ ss 0 = s := by
+  use lts.makeωTr h s μs
+  grind [LTS.makeωTr, h.total]
+
+/-- If a LTS is total, then any finite execution can be extended to an infinite execution,
+provided that the label type is inbabited. -/
+theorem LTS.Total.mTr_ωTr [Inhabited Label] (ht : lts.Total) {μl : List Label} {s t : State}
+    (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 ht t μs
+  refine ⟨μs, 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
+  Tr s' μ t' := match s', t' with
+    | inl s, inl t => lts.Tr s μ t
+    | _, inr () => True
+    | inr (), inl _ => False
+
+/-- The LTS constructed by `LTS.totalize` is indeed total. -/
+def LTS.totalize.total (lts : LTS State Label) : lts.totalize.Total where
+  next _ _ := inr ()
+  total _ _ := by simp [LTS.totalize]
+
+/-- In `LTS.totalize`, there is no finite execution from the sink state to any non-sink state. -/
+theorem LTS.totalize.not_right_left {μs : List Label} {t : State} :
+    ¬ lts.totalize.MTr (inr ()) μs (inl t) := by
+  intro h
+  generalize h_s : (inr () : State ⊕ Unit) = s'
+  generalize h_t : (inl t : State ⊕ Unit) = t'
+  rw [h_s, h_t] at h
+  induction h <;> grind [LTS.totalize]
+
+/-- In `LTS.totalize`, the transitions between non-sink states correspond exactly to
+the transitions in the original LTS. -/
+@[simp]
+theorem LTS.totalize.tr_left_iff {μ : Label} {s t : State} :
+    lts.totalize.Tr (inl s) μ (inl t) ↔ lts.Tr s μ t := by
+  simp [LTS.totalize]
+
+/-- In `LTS.totalize`, the multistep transitions between non-sink states correspond exactly to
+the multistep transitions in the original LTS. -/
+@[simp]
+theorem LTS.totalize.mtr_left_iff {μs : List Label} {s t : State} :
+    lts.totalize.MTr (inl s) μs (inl t) ↔ lts.MTr s μs t := by
+  constructor <;> intro h
+  · generalize h_s : (inl s : State ⊕ Unit) = s'
+    generalize h_t : (inl t : State ⊕ Unit) = t'
+    rw [h_s, h_t] at h
+    induction h generalizing s
+    case refl _ => grind [LTS.MTr]
+    case stepL t1' μ t2' μs t3' h_tr h_mtr h_ind =>
+      obtain ⟨rfl⟩ := h_s
+      cases t2'
+      case inl t2 => grind [LTS.MTr, totalize.tr_left_iff.mp h_tr]
+      case inr t2 => grind [totalize.not_right_left]
+  · induction h
+    case refl _ => grind [LTS.MTr]
+    case stepL t1 μ t2 μs t3 h_tr h_mtr h_ind =>
+      grind [LTS.MTr, totalize.tr_left_iff.mpr h_tr]
+
+end Total
+
 section Termination
 /-! ## Definitions about termination -/