From 932efb697a7d9c4cea60215b6cf950735c9c182f Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Mon, 12 Jan 2026 10:25:16 -0800 Subject: [PATCH 1/4] feat: define right congruence and prove its basic properties --- Cslib.lean | 2 + Cslib/Computability/Automata/DA/Congr.lean | 68 +++++++++++++++++++ .../Congruences/RightCongruence.lean | 50 ++++++++++++++ .../Languages/RegularLanguage.lean | 9 +++ Cslib/Foundations/Semantics/FLTS/Basic.lean | 7 +- 5 files changed, 135 insertions(+), 1 deletion(-) create mode 100644 Cslib/Computability/Automata/DA/Congr.lean create mode 100644 Cslib/Computability/Languages/Congruences/RightCongruence.lean diff --git a/Cslib.lean b/Cslib.lean index 8c6984eb..cb410fda 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -6,6 +6,7 @@ public import Cslib.Computability.Automata.Acceptors.Acceptor public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor public import Cslib.Computability.Automata.DA.Basic public import Cslib.Computability.Automata.DA.Buchi +public import Cslib.Computability.Automata.DA.Congr public import Cslib.Computability.Automata.DA.Prod public import Cslib.Computability.Automata.DA.ToNA public import Cslib.Computability.Automata.EpsilonNA.Basic @@ -20,6 +21,7 @@ public import Cslib.Computability.Automata.NA.Prod public import Cslib.Computability.Automata.NA.Sum public import Cslib.Computability.Automata.NA.ToDA public import Cslib.Computability.Automata.NA.Total +public import Cslib.Computability.Languages.Congruences.RightCongruence public import Cslib.Computability.Languages.ExampleEventuallyZero public import Cslib.Computability.Languages.Language public import Cslib.Computability.Languages.OmegaLanguage diff --git a/Cslib/Computability/Automata/DA/Congr.lean b/Cslib/Computability/Automata/DA/Congr.lean new file mode 100644 index 00000000..792dfa5b --- /dev/null +++ b/Cslib/Computability/Automata/DA/Congr.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2026 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +module + +public import Cslib.Computability.Automata.DA.Basic +public import Cslib.Computability.Languages.Congruences.RightCongruence + +@[expose] public section + +/-! # Deterministic automaton corresponding to a right congruence. -/ + +namespace Cslib + +open scoped FLTS RightCongruence + +variable {Symbol : Type*} + +/-- Every right congruence gives rise to a DA whose states are the euqivalence classes of +the right congruence, whose start state is the empty word, and whose transition functiuon +is concatenation on the right of the input symbol. Note that the transition function is +well-defined only because `c` is a right congruence. -/ +@[scoped grind =] +def RightCongruence.toDA (c : RightCongruence Symbol) : Automata.DA c.QuotType Symbol where + tr s x := Quotient.lift (fun u ↦ ⟦ u ++ [x] ⟧) (by + intro u v h_eq + apply Quotient.sound + exact RightCongruence.right_congr u v h_eq [x] + ) s + start := ⟦ [] ⟧ + +namespace Automata.DA + +variable [c : RightCongruence Symbol] + +/-- After consuming a finite word `xs`, `c.toDA` reaches the state `⟦ xs ⟧` which is +the equivalence class of `xs`. -/ +@[simp, scoped grind =] +theorem congr_mtr_eq {xs : List Symbol} : + c.toDA.mtr c.toDA.start xs = ⟦ xs ⟧ := by + generalize h_rev : xs.reverse = ys + induction ys generalizing xs + case nil => grind [List.reverse_eq_nil_iff] + case cons y ys h_ind => + obtain ⟨rfl⟩ := List.reverse_eq_cons_iff.mp h_rev + specialize h_ind (xs := ys.reverse) (by grind) + grind [Quotient.lift_mk] + +namespace FinAcc + +open Acceptor + +/-- The language of `c.toDA` with a single accepting state `s` is exactly +the equivalence class corresponding to `s`. -/ +@[simp] +theorem congr_language_eq {s : c.QuotType} : + language (FinAcc.mk c.toDA {s}) = c.eqvCls s := by + ext xs + grind + +end FinAcc + +end Automata.DA + +end Cslib diff --git a/Cslib/Computability/Languages/Congruences/RightCongruence.lean b/Cslib/Computability/Languages/Congruences/RightCongruence.lean new file mode 100644 index 00000000..a4cacd74 --- /dev/null +++ b/Cslib/Computability/Languages/Congruences/RightCongruence.lean @@ -0,0 +1,50 @@ +/- +Copyright (c) 2026 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +module + +public import Cslib.Computability.Languages.Language + +@[expose] public section + +/-! +# Right RightCongruence + +This file contains basic definitions about right congruences on finite sequences. + +NOTE: Left congruences and two-sided congruences can be similarly defined. +But they are left to future work because they are not needed for now. +-/ + +namespace Cslib + +/-- A right congruence is an equivalence relation on finite sequences (represented by lists) +that is preserved by concatenation on the right. The equivalence relation is represented +by a setoid to to enable ready access to the quotient construction. -/ +class RightCongruence (α : Type*) extends eq : Setoid (List α) where + /-- If `u` an `v` are congruent, then `u ++ w` and `v ++ w` are also congruent for any `w`. -/ + right_congr : ∀ u v, eq u v → ∀ w, eq (u ++ w) (v ++ w) + +/-- The `≃` notation is supported for right congruences. -/ +instance {α : Type*} [RightCongruence α] : HasEquiv (List α) := + ⟨RightCongruence.eq⟩ + +namespace RightCongruence + +variable {α : Type*} + +/-- The quotient type of a RightCongruence relation. -/ +@[scoped grind =] +def QuotType (c : RightCongruence α) := Quotient c.eq + +/-- The equivalence class (as a language) corresponding to an element of the quotient type. -/ +@[scoped grind =] +def eqvCls [c : RightCongruence α] (s : c.QuotType) : Language α := + (Quotient.mk c.eq) ⁻¹' {s} + +end RightCongruence + +end Cslib diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean index c35951bc..0aa05469 100644 --- a/Cslib/Computability/Languages/RegularLanguage.lean +++ b/Cslib/Computability/Languages/RegularLanguage.lean @@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou module +public import Cslib.Computability.Automata.DA.Congr public import Cslib.Computability.Automata.DA.Prod public import Cslib.Computability.Automata.DA.ToNA public import Cslib.Computability.Automata.NA.Concat @@ -159,4 +160,12 @@ theorem IsRegular.kstar [Inhabited Symbol] {l : Language Symbol} obtain ⟨State, h_fin, nfa, rfl⟩ := h use Unit ⊕ (State ⊕ Unit), inferInstance, ⟨finLoop nfa, {inl ()}⟩, loop_language_eq h_l +/-- If a right congruence is of finite index, then each of its equivalence classes is regular. -/ +@[simp] +theorem IsRegular.congr_fin_index {Symbol : Type} [c : RightCongruence Symbol] [Finite c.QuotType] + (s : c.QuotType) : (c.eqvCls s).IsRegular := by + rw [IsRegular.iff_dfa] + use c.QuotType, inferInstance, ⟨c.toDA, {s}⟩ + exact DA.FinAcc.congr_language_eq + end Cslib.Language diff --git a/Cslib/Foundations/Semantics/FLTS/Basic.lean b/Cslib/Foundations/Semantics/FLTS/Basic.lean index c06cb59f..17f54aa1 100644 --- a/Cslib/Foundations/Semantics/FLTS/Basic.lean +++ b/Cslib/Foundations/Semantics/FLTS/Basic.lean @@ -45,9 +45,14 @@ from the left (instead of the right), in order to match the way lists are constr @[scoped grind =] def mtr (flts : FLTS State Label) (s : State) (μs : List Label) := μs.foldl flts.tr s -@[scoped grind =] +@[simp, scoped grind =] theorem mtr_nil_eq {flts : FLTS State Label} {s : State} : flts.mtr s [] = s := rfl +@[simp, scoped grind =] +theorem mtr_concat_eq {flts : FLTS State Label} {s : State} {μs : List Label} {μ : Label} : + flts.mtr s (μs ++ [μ]) = flts.tr (flts.mtr s μs) μ := by + grind + end FLTS end Cslib From 76693286fb66868d956c3911d52eeeaef04e4ee5 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Sat, 17 Jan 2026 15:31:31 -0800 Subject: [PATCH 2/4] incorporate Chris Henson's comments --- Cslib/Computability/Automata/DA/Congr.lean | 2 +- Cslib/Computability/Languages/Congruences/RightCongruence.lean | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Cslib/Computability/Automata/DA/Congr.lean b/Cslib/Computability/Automata/DA/Congr.lean index 792dfa5b..fa0077e2 100644 --- a/Cslib/Computability/Automata/DA/Congr.lean +++ b/Cslib/Computability/Automata/DA/Congr.lean @@ -19,7 +19,7 @@ open scoped FLTS RightCongruence variable {Symbol : Type*} -/-- Every right congruence gives rise to a DA whose states are the euqivalence classes of +/-- Every right congruence gives rise to a DA whose states are the equivalence classes of the right congruence, whose start state is the empty word, and whose transition functiuon is concatenation on the right of the input symbol. Note that the transition function is well-defined only because `c` is a right congruence. -/ diff --git a/Cslib/Computability/Languages/Congruences/RightCongruence.lean b/Cslib/Computability/Languages/Congruences/RightCongruence.lean index a4cacd74..76723492 100644 --- a/Cslib/Computability/Languages/Congruences/RightCongruence.lean +++ b/Cslib/Computability/Languages/Congruences/RightCongruence.lean @@ -6,7 +6,8 @@ Authors: Ching-Tsun Chou module -public import Cslib.Computability.Languages.Language +public import Cslib.Init +public import Mathlib.Computability.Language @[expose] public section From 9ced6e8b5b3d20fc37c3bf2a8c4d990fe25d69ed Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Sat, 17 Jan 2026 18:37:35 -0500 Subject: [PATCH 3/4] right_congr definition --- Cslib/Computability/Automata/DA/Congr.lean | 2 +- Cslib/Computability/Languages/Congruences/RightCongruence.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Cslib/Computability/Automata/DA/Congr.lean b/Cslib/Computability/Automata/DA/Congr.lean index fa0077e2..dcaaf7f5 100644 --- a/Cslib/Computability/Automata/DA/Congr.lean +++ b/Cslib/Computability/Automata/DA/Congr.lean @@ -28,7 +28,7 @@ def RightCongruence.toDA (c : RightCongruence Symbol) : Automata.DA c.QuotType S tr s x := Quotient.lift (fun u ↦ ⟦ u ++ [x] ⟧) (by intro u v h_eq apply Quotient.sound - exact RightCongruence.right_congr u v h_eq [x] + exact right_congr h_eq [x] ) s start := ⟦ [] ⟧ diff --git a/Cslib/Computability/Languages/Congruences/RightCongruence.lean b/Cslib/Computability/Languages/Congruences/RightCongruence.lean index 76723492..7af6b4dc 100644 --- a/Cslib/Computability/Languages/Congruences/RightCongruence.lean +++ b/Cslib/Computability/Languages/Congruences/RightCongruence.lean @@ -27,7 +27,7 @@ that is preserved by concatenation on the right. The equivalence relation is re by a setoid to to enable ready access to the quotient construction. -/ class RightCongruence (α : Type*) extends eq : Setoid (List α) where /-- If `u` an `v` are congruent, then `u ++ w` and `v ++ w` are also congruent for any `w`. -/ - right_congr : ∀ u v, eq u v → ∀ w, eq (u ++ w) (v ++ w) + right_congr {u v} (huv : u ≈ v) (w : List α) : u ++ w ≈ v ++ w /-- The `≃` notation is supported for right congruences. -/ instance {α : Type*} [RightCongruence α] : HasEquiv (List α) := From 57918b64f8ed93c6c09a9db663d62728a36569a8 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Sat, 17 Jan 2026 18:11:21 -0800 Subject: [PATCH 4/4] fix a typo --- Cslib/Computability/Languages/Congruences/RightCongruence.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Computability/Languages/Congruences/RightCongruence.lean b/Cslib/Computability/Languages/Congruences/RightCongruence.lean index 7af6b4dc..981aa5d0 100644 --- a/Cslib/Computability/Languages/Congruences/RightCongruence.lean +++ b/Cslib/Computability/Languages/Congruences/RightCongruence.lean @@ -12,7 +12,7 @@ public import Mathlib.Computability.Language @[expose] public section /-! -# Right RightCongruence +# Right Congruence This file contains basic definitions about right congruences on finite sequences.