feat(Computability/Languages): languages matching regular expressions are regular

Cslib/Computability/Languages/Language.lean

@@ -41,6 +41,10 @@ theorem mem_biSup {I : Type*} (s : Set I) (l : I → Language α) (x : List α)
 theorem le_one_iff_eq : l ≤ 1 ↔ l = 0 ∨ l = 1 :=
   subset_singleton_iff_eq
 
+@[simp, scoped grind =]
+theorem mem_singleton (x y : List α) : x ∈ ({y} : Language α) ↔ x = y :=
+  Iff.rfl
+
 @[simp, scoped grind =]
 theorem mem_sub_one (x : List α) : x ∈ (l - 1) ↔ x ∈ l ∧ x ≠ [] :=
   Iff.rfl

Cslib/Computability/Languages/RegularLanguage.lean

@@ -13,6 +13,7 @@ public import Cslib.Computability.Automata.NA.Concat
 public import Cslib.Computability.Automata.NA.Loop
 public import Cslib.Computability.Automata.NA.ToDA
 public import Mathlib.Computability.DFA
+public import Mathlib.Computability.RegularExpressions
 public import Mathlib.Data.Finite.Sum
 public import Mathlib.Data.Set.Card
 
@@ -184,4 +185,31 @@ theorem IsRegular.congr_fin_index {Symbol : Type}
   use Quotient c.eq, inferInstance, ⟨c.toDA, {a}⟩
   exact DA.FinAcc.congr_language_eq
 
+/-- The language containing only the one character string `a` is regular. -/
+@[simp]
+theorem IsRegular.char (a : Symbol) : ({[a]} : Language Symbol).IsRegular := by
+  rw [IsRegular.iff_dfa]
+  classical
+  let flts := FLTS.mk (fun (s : Fin 3) (x : Symbol) ↦ if (s = 0 ∧ x = a) then 1 else 2)
+  use Fin 3, inferInstance, ⟨DA.mk flts 0, {1}⟩
+  ext xs
+  induction xs using List.reverseRec with
+  | nil => grind [Accepts, Language.mem_singleton]
+  | append_singleton xs x ih =>
+    simp only [mem_language, Accepts, Language.mem_singleton, FLTS.mtr_concat_eq] at ih ⊢
+    constructor
+    · induction xs using List.reverseRec <;> grind
+    · simp_all [flts, List.append_eq_cons_iff]
+
+/-- Languages matching regular expressions are regular. -/
+theorem IsRegular.regex [Inhabited Symbol] {r : RegularExpression Symbol} :
+    r.matches'.IsRegular := by
+  induction r with
+  | zero => simp
+  | epsilon => simp
+  | char a => simp [IsRegular.char a]
+  | plus P Q hP hQ => grind [RegularExpression.matches', IsRegular.add]
+  | comp P Q hP hQ => grind [RegularExpression.matches', IsRegular.mul]
+  | star P hP => grind [RegularExpression.matches', IsRegular.kstar]
+
 end Cslib.Language