feat: prove that regular languages are closed under Kleene star

Cslib/Computability/Automata/NA/Loop.lean

@@ -4,14 +4,14 @@ 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
 
 /-! # Loop construction on nondeterministic automata. -/
 
 namespace Cslib.Automata.NA
 
-open Nat List Sum ωSequence Acceptor Language
+open Nat Set Sum ωSequence Acceptor Language
 open scoped Run LTS
 
 variable {Symbol State : Type*}
@@ -77,23 +77,24 @@ lemma loop_run_from_left {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ Sta
 
 /-- A run of `na.loop` containing at least one non-initial `()` state is the concatenation
 of a nonempty finite run of `na` followed by a run of `na.loop`. -/
-theorem loop_run_one_iter {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)}
-    (h : na.loop.Run xs ss) (h1 : ∃ k, 0 < k ∧ (ss k).isLeft) :
-    ∃ n, xs.take n ∈ language na - 1 ∧ na.loop.Run (xs.drop n) (ss.drop n) := by
-  let n := Nat.find h1
-  have : 0 < n ∧ (ss n).isLeft := Nat.find_spec h1
-  have : ∀ k, 0 < k → k < n → (ss k).isRight := by grind [Nat.find_min h1]
-  refine ⟨n, ⟨?_, ?_⟩, ?_⟩
+theorem loop_run_one_iter {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)} {k : ℕ}
+    (h : na.loop.Run xs ss) (h1 : 0 < k) (h2 : (ss k).isLeft) :
+    ∃ n, n ≤ k ∧ xs.take n ∈ language na - 1 ∧ na.loop.Run (xs.drop n) (ss.drop n) := by
+  have h1' : ∃ k, 0 < k ∧ (ss k).isLeft := by grind
+  let n := Nat.find h1'
+  have : 0 < n ∧ (ss n).isLeft := Nat.find_spec h1'
+  have : ∀ k, 0 < k → k < n → (ss k).isRight := by grind [Nat.find_min h1']
+  refine ⟨n, by grind, ⟨?_, ?_⟩, ?_⟩
   · grind [loop_run_left_right_left]
   · have neq : (ωSequence.take n xs).length ≠ 0 := by grind
-    exact neq.imp (congrArg length)
+    exact neq.imp (congrArg List.length)
   · grind [loop_run_from_left]
 
 /-- For any finite word in `language na`, there is a corresponding finite run of `na.loop`. -/
 theorem loop_fin_run_exists {xl : List Symbol} (h : xl ∈ language na) :
     ∃ sl : List (Unit ⊕ State), ∃ _ : sl.length = xl.length + 1,
     sl[0] = inl () ∧ sl[xl.length] = inl () ∧
-    ∀ k, ∀ _ : k < xl.length, na.loop.Tr sl[k] xl[k] sl[k + 1] := by
+    ∀ k, (_ : k < xl.length) → na.loop.Tr sl[k] xl[k] sl[k + 1] := by
   obtain ⟨_, _, _, _, h_mtr⟩ := h
   obtain ⟨sl, _, _, _, _⟩ := LTS.MTr.exists_states h_mtr
   by_cases xl.length = 0
@@ -102,6 +103,15 @@ theorem loop_fin_run_exists {xl : List Symbol} (h : xl ∈ language na) :
   · use [inl ()] ++ (sl.extract 1 xl.length).map inr ++ [inl ()]
     grind [FinAcc.loop]
 
+/-- For any finite word in `language na`, there is a corresponding multistep transition
+of `na.loop`. -/
+theorem loop_fin_run_mtr {xl : List Symbol} (h : xl ∈ language na) :
+    na.loop.MTr (inl ()) xl (inl ()) := by
+  obtain ⟨sl, _, _, _, h_run⟩ := loop_fin_run_exists h
+  suffices ∀ k, (_ : k ≤ xl.length) → na.loop.MTr (inl ()) (xl.take k) sl[k] by grind
+  intro k
+  induction k <;> grind [LTS.MTr.stepR, List.take_add_one]
+
 /-- For any infinite sequence `xls` of nonempty finite words from `language na`,
 there is an infinite run of `na.loop` corresponding to `xls.flatten` in which
 the state `()` marks the boundaries between the finite words in `xls`. -/
@@ -114,7 +124,7 @@ theorem loop_run_exists [Inhabited Symbol] {xls : ωSequence (List Symbol)}
   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 [eq_nil_iff_length_eq_zero]
+  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
@@ -144,8 +154,9 @@ theorem loop_language_eq [Inhabited Symbol] :
   apply le_antisymm
   · apply omegaPow_coind
     rintro xs ⟨ss, h_run, h_acc⟩
-    have h1 : ∃ k > 0, (ss k).isLeft := by grind [FinAcc.loop, frequently_atTop'.mp h_acc 0]
-    obtain ⟨n, _⟩ := loop_run_one_iter h_run h1
+    obtain ⟨k, h1, h2⟩ : ∃ k > 0, (ss k).isLeft :=
+      by grind [FinAcc.loop, frequently_atTop'.mp h_acc 0]
+    obtain ⟨n, _⟩ := loop_run_one_iter h_run h1 h2
     refine ⟨xs.take n, by grind, xs.drop n, ?_, by simp⟩
     refine ⟨ss.drop n, by grind, ?_⟩
     apply (drop_frequently_iff_frequently n).mpr
@@ -156,8 +167,62 @@ theorem loop_language_eq [Inhabited Symbol] :
     use ss, h_run
     apply frequently_iff_strictMono.mpr
     use xls.cumLen, ?_, by grind
-    grind [cumLen_strictMono, eq_nil_iff_length_eq_zero]
+    grind [cumLen_strictMono, List.eq_nil_iff_length_eq_zero]
 
 end Buchi
 
+namespace FinAcc
+
+open scoped Computability
+
+/-- `finLoop na` is the loop construction applied to the "totalized" version of `na`. -/
+def finLoop (na : FinAcc State Symbol) : NA (Unit ⊕ (State ⊕ Unit)) Symbol :=
+  FinAcc.loop ⟨na.totalize, inl '' na.accept⟩
+
+/-- `finLoop na` is total, assuming that `na` has at least one start state. -/
+instance [h : Nonempty na.start] : na.finLoop.Total where
+  total s x := match s with
+    | inl _ => ⟨inr (inr ()), by simpa [finLoop, loop, NA.totalize, LTS.totalize] using h⟩
+    | inr _ => ⟨inr (inr ()), by grind [finLoop, loop, NA.totalize, LTS.totalize]⟩
+
+/-- `finLoop na` accepts the Kleene star of the language of `na`, assuming that
+the latter is nonempty. -/
+theorem loop_language_eq [Inhabited Symbol] (h : ¬ language na = 0) :
+    language (FinAcc.mk na.finLoop {inl ()}) = (language na)∗ := by
+  rw [Language.kstar_iff_mul_add]
+  ext xl; constructor
+  · rintro ⟨s, _, t, h_acc, h_mtr⟩
+    by_cases h_xl : xl = []
+    · grind [mem_add, mem_one]
+    · have : Nonempty na.start := by
+        obtain ⟨_, s0, _, _⟩ := nonempty_iff_ne_empty.mpr h
+        use s0
+      obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.mTr_ωTr h_mtr
+      have h_run : na.finLoop.Run (xl ++ω xs) ss := by grind [Run]
+      obtain ⟨h1, h2⟩ : 0 < xl.length ∧ (ss xl.length).isLeft := by
+        simp only [mem_singleton_iff] at h_acc
+        grind
+      obtain ⟨n, h_n, _, _, h_ωtr'⟩ := loop_run_one_iter h_run h1 h2
+      left; refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩
+      · grind [totalize_language_eq, take_append_of_le_length]
+      · refine ⟨ss n, by grind, ss xl.length, by grind, ?_⟩
+        have := LTS.ωTr_mTr h_ωtr' (show 0 ≤ xl.length - n by grind)
+        have : n + (xl.length - n) = xl.length := by grind
+        have : ((xl ++ω xs).drop n).extract 0 (xl.length - n) = xl.drop n := by
+          grind [extract_eq_take, drop_append_of_le_length, take_append_of_le_length]
+        grind [finLoop]
+      · exact xl.take_append_drop n
+  · rintro (h | h)
+    · obtain ⟨xl1, ⟨h_xl1, _⟩, xl2, h_xl2, rfl⟩ := h
+      rw [← totalize_language_eq] at h_xl1
+      have := loop_fin_run_mtr h_xl1
+      obtain ⟨s1, _, s2, _, _⟩ := h_xl2
+      obtain ⟨rfl⟩ : s1 = inl () := by grind [finLoop, loop]
+      obtain ⟨rfl⟩ : s2 = inl () := by grind [finLoop, loop]
+      refine ⟨inl (), ?_, inl (), ?_, LTS.MTr.comp _ this ?_⟩ <;> assumption
+    · obtain ⟨rfl⟩ := (Language.mem_one xl).mp h
+      refine ⟨inl (), ?_, inl (), ?_, ?_⟩ <;> grind [finLoop, loop]
+
+end FinAcc
+
 end Cslib.Automata.NA

Cslib/Computability/Languages/Language.lean

@@ -82,4 +82,14 @@ theorem kstar_sub_one : l∗ - 1 = (l - 1) * l∗ := by
       exact ⟨y, h_y, z, h_z, rfl⟩
     · grind [one_def, append_eq_nil_iff]
 
+@[scoped grind =]
+theorem sub_one_kstar : (l - 1)∗ = l∗ := by
+  ext x
+  grind [mem_kstar, mem_kstar_iff_exists_nonempty]
+
+@[scoped grind .]
+theorem kstar_iff_mul_add : m = l∗ ↔ m = (l - 1) * m + 1 := by
+  rw [self_eq_mul_add_iff, mul_one, sub_one_kstar]
+  grind
+
 end Language

Cslib/Computability/Languages/RegularLanguage.lean

@@ -7,6 +7,7 @@ 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.Loop
 import Cslib.Computability.Automata.NA.ToDA
 import Mathlib.Computability.DFA
 import Mathlib.Data.Finite.Sum
@@ -143,4 +144,15 @@ theorem IsRegular.mul [Inhabited Symbol] {l1 l2 : Language Symbol}
     ⟨finConcat nfa1 nfa2, inr '' (inl '' nfa2.accept)⟩
   exact finConcat_language_eq
 
+open NA.FinAcc Sum in
+/-- The Kleene star of a regular language is regular. -/
+@[simp]
+theorem IsRegular.kstar [Inhabited Symbol] {l : Language Symbol}
+    (h : l.IsRegular) : (l∗).IsRegular := by
+  by_cases h_l : l = 0
+  · simp [h_l]
+  · rw [IsRegular.iff_nfa] at h ⊢
+    obtain ⟨State, h_fin, nfa, rfl⟩ := h
+    use Unit ⊕ (State ⊕ Unit), inferInstance, ⟨finLoop nfa, {inl ()}⟩, loop_language_eq h_l
+
 end Cslib.Language

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -144,7 +144,7 @@ theorem LTS.MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by
 which satisfies the single-step transition at every step. -/
 theorem LTS.MTr.exists_states {lts : LTS State Label} {s1 s2 : State} {μs : List Label}
     (h : lts.MTr s1 μs s2) : ∃ ss : List State, ∃ _ : ss.length = μs.length + 1,
-    ss[0] = s1 ∧ ss[μs.length] = s2 ∧ ∀ k, ∀ _ : k < μs.length, lts.Tr ss[k] μs[k] ss[k + 1] := by
+    ss[0] = s1 ∧ ss[μs.length] = s2 ∧ ∀ k, (_ : k < μs.length) → lts.Tr ss[k] μs[k] ss[k + 1] := by
   induction h
   case refl t =>
     use [t]