From 8842bc40326b7cafe8bf85ae680c795744af81db Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Wed, 16 Sep 2026 17:17:08 -0700
Subject: [PATCH] feat(Language): characterizing regular languages as preimages
 of subsets of finite monoids

---
 .../Languages/SyntacticMonoid.lean            | 87 ++++++++++++++++++-
 1 file changed, 86 insertions(+), 1 deletion(-)

diff --git a/Cslib/Computability/Languages/SyntacticMonoid.lean b/Cslib/Computability/Languages/SyntacticMonoid.lean
index 00a89e8f5..8e3412ff3 100644
--- a/Cslib/Computability/Languages/SyntacticMonoid.lean
+++ b/Cslib/Computability/Languages/SyntacticMonoid.lean
@@ -24,7 +24,7 @@ variable {α : Type}
 
 namespace Language
 
-open Cslib.Language
+open Cslib.Language FreeMonoid
 
 /-- Converting a (two-sided) congruence `c` on finite words to a congruence relation
 on the (multiplicative) free monoid. -/
@@ -40,9 +40,94 @@ def Congruence.toCon [c : Congruence α] : Con (FreeMonoid α) where
 by the Myhill congruence of `l`. -/
 abbrev SyntacticMonoid (l : Language α) := l.MyhillCongruence.toCon.Quotient
 
+/-- The natural homomorphism from `FreeMonoid α` to `l.SyntacticMonoid` induced
+by the Myhill congruence of `l`. -/
+abbrev homSyntacticMonoid (l : Language α) := l.MyhillCongruence.toCon.mk'
+
 /-- A language `l` is regular if and only if its syntactic monoid is finite. -/
 theorem IsRegular.iff_finite_syntacticMonoid (l : Language α) :
     l.IsRegular ↔ Finite (l.SyntacticMonoid) :=
   IsRegular.iff_finite_myhillQuotient l
 
+/-- The congruence induced by `homSyntacticMonoid` is the Myhill congruence. -/
+theorem homSyntacticMonoid_myhillCongruence {l : Language α} {x y : List α}
+    (h : l.homSyntacticMonoid (ofList x) = l.homSyntacticMonoid (ofList y)) :
+    l.MyhillCongruence.eq x y := by
+  simp only [Con.coe_mk', Con.eq] at h
+  assumption
+
+/-- Any regular language is the preimage of a subset of a finite monoid `M`
+under a monoid homomorphism from the free monoid on its alphabet to `M`. -/
+theorem IsRegular.exists_finite_monoid {l : Language α} (h : l.IsRegular) :
+    ∃ M : Type, ∃ _ : Monoid M, ∃ _ : Finite M, ∃ f : FreeMonoid α →* M, ∃ s : Set M,
+    (f ∘ ofList) ⁻¹' s = l := by
+  use l.SyntacticMonoid, Con.monoid _, (iff_finite_syntacticMonoid l).mp h,
+    l.homSyntacticMonoid, (l.homSyntacticMonoid ∘ ofList) '' l
+  apply le_antisymm
+  · rintro x ⟨y, hy, heq⟩
+    have heq := homSyntacticMonoid_myhillCongruence heq
+    specialize heq [] []
+    simp only [List.nil_append, List.append_nil] at heq
+    exact heq.mp hy
+  · exact Set.subset_preimage_image _ _
+
+section FiniteMonoid
+
+variable {M : Type*} [Monoid M] (f : FreeMonoid α →* M)
+
+/-- Given a a monoid homomorphism `f` from `FreeMonoid α` to another monoid `M`,
+`inducedCongr f` is the language congruence induced by `f`. -/
+-- NOTE: This is in fact a two-sided congruence, but we need only the `RightCongruence` part here.
+@[implicit_reducible]
+def inducedCongr : RightCongruence α where
+  eq := Setoid.ker (f ∘ ofList)
+  right_cov.elim := by
+    intro x y z
+    simp only [Setoid.ker_def, Function.comp_apply, ofList_append, map_mul]
+    grind
+
+instance [h : Finite M] :
+    Finite (Quotient (inducedCongr f).eq) :=
+  Finite.of_equiv _ (Setoid.quotientKerEquivRange f).symm
+
+theorem inducedCongr_ofList (x : List α) :
+    (f ∘ ofList) ⁻¹' {(f ∘ ofList) x} = (inducedCongr f).eqvCls ⟦ x ⟧ := by
+  ext y
+  simp [Quotient.eq]
+
+theorem IsRegular.of_finite_monoid_singleton [Finite M]
+    (m : M) : IsRegular ((f ∘ ofList) ⁻¹' {m}) := by
+  by_cases h : (f ∘ ofList) ⁻¹' {m} = ∅
+  · rw [h]
+    exact IsRegular.zero
+  · obtain ⟨x, rfl⟩ := Set.nonempty_iff_ne_empty.mpr h
+    rw [inducedCongr_ofList]
+    exact IsRegular.congr_fin_index (c := inducedCongr f) _
+
+/-- The preimage of a subset of a finite monoid `M` under a monoid homomorphism
+from the free monoid to `M` is regular. -/
+theorem IsRegular.of_finite_monoid [Finite M]
+    (s : Set M) : IsRegular ((f ∘ ofList) ⁻¹' s) := by
+  have h : (f ∘ ofList) ⁻¹' s = ⨆ m ∈ s, (f ∘ ofList) ⁻¹' {m} := by
+    simp only [Set.iSup_eq_iUnion, Set.biUnion_preimage_singleton]
+  rw [h]
+  apply IsRegular.iSup
+  simp [IsRegular.of_finite_monoid_singleton]
+
+end FiniteMonoid
+
+/-- A language is regular if and only if it is the preimage of a subset of a finite monoid `M`
+under a monoid homomorphism from the free monoid on its alphabet to `M`. -/
+theorem IsRegular.iff_finite_monoid {l : Language α} :
+    l.IsRegular ↔
+    ∃ M : Type, ∃ _ : Monoid M, ∃ _ : Finite M, ∃ f : FreeMonoid α →* M, ∃ s : Set M,
+    (f ∘ ofList) ⁻¹' s = l := by
+  apply Iff.intro
+  case mp =>
+    intro h
+    exact IsRegular.exists_finite_monoid h
+  case mpr =>
+    rintro ⟨M, _, _, f, s, rfl⟩
+    exact IsRegular.of_finite_monoid f s
+
 end Language