Skip to content

Commit a79f1c2

Browse files
ctchoufmontesichenson2018
authored
feat: define BuchiCongruence and prove that it is a right congruence of finite index (#278)
This PR defines the notion of a "right congruence", which is an equivalence relation between finite words that is preserved by concatenation on the right, and proves its basic properties: - There is a natural deterministic automaton corresponding to each right congruence whose states are the equivalence classes of the congruence and whose transitions correspond to concatenation on the right of the input symbols. - If a right congruence is of finite index, then each of its equivalence classes is a regular language. Furthermore, this PR also defines a special type of right congruences introduced by J.R. Buchi and proves that it is of finite index if the underlying Buchi automaton is finite-state. The purpose of Buchi congruence is to prove the closure of ω-regular languages under complementation. But more work will be needed before we reach that goal. The old PR #265 has been absorbed into this PR. --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
1 parent ba0fb9d commit a79f1c2

8 files changed

Lines changed: 321 additions & 27 deletions

File tree

‎Cslib.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ public import Cslib.Computability.Automata.Acceptors.Acceptor
66
public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
77
public import Cslib.Computability.Automata.DA.Basic
88
public import Cslib.Computability.Automata.DA.Buchi
9+
public import Cslib.Computability.Automata.DA.Congr
910
public import Cslib.Computability.Automata.DA.Prod
1011
public import Cslib.Computability.Automata.DA.ToNA
1112
public import Cslib.Computability.Automata.EpsilonNA.Basic
@@ -21,6 +22,8 @@ public import Cslib.Computability.Automata.NA.Prod
2122
public import Cslib.Computability.Automata.NA.Sum
2223
public import Cslib.Computability.Automata.NA.ToDA
2324
public import Cslib.Computability.Automata.NA.Total
25+
public import Cslib.Computability.Languages.Congruences.BuchiCongruence
26+
public import Cslib.Computability.Languages.Congruences.RightCongruence
2427
public import Cslib.Computability.Languages.ExampleEventuallyZero
2528
public import Cslib.Computability.Languages.Language
2629
public import Cslib.Computability.Languages.OmegaLanguage

‎Cslib/Computability/Automata/DA/Congr.lean‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
/-
2+
Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Ching-Tsun Chou
5+
-/
6+
7+
module
8+
9+
public import Cslib.Computability.Automata.DA.Basic
10+
public import Cslib.Computability.Languages.Congruences.RightCongruence
11+
12+
@[expose] public section
13+
14+
/-! # Deterministic automaton corresponding to a right congruence. -/
15+
16+
namespace Cslib
17+
18+
open scoped FLTS RightCongruence
19+
20+
variable {Symbol : Type*}
21+
22+
/-- Every right congruence gives rise to a DA whose states are the equivalence classes of
23+
the right congruence, whose start state is the empty word, and whose transition functiuon
24+
is concatenation on the right of the input symbol. Note that the transition function is
25+
well-defined only because `c` is a right congruence. -/
26+
@[scoped grind =]
27+
def RightCongruence.toDA [c : RightCongruence Symbol] : Automata.DA (Quotient c.eq) Symbol where
28+
tr s x := Quotient.lift (fun u ↦ ⟦ u ++ [x] ⟧) (by
29+
intro u v h_eq
30+
apply Quotient.sound
31+
exact right_cov.elim [x] h_eq
32+
) s
33+
start := ⟦ [] ⟧
34+
35+
namespace Automata.DA
36+
37+
variable [c : RightCongruence Symbol]
38+
39+
/-- After consuming a finite word `xs`, `c.toDA` reaches the state `⟦ xs ⟧` which is
40+
the equivalence class of `xs`. -/
41+
@[simp, scoped grind =]
42+
theorem congr_mtr_eq {xs : List Symbol} :
43+
c.toDA.mtr c.toDA.start xs = ⟦ xs ⟧ := by
44+
generalize h_rev : xs.reverse = ys
45+
induction ys generalizing xs
46+
case nil => grind [List.reverse_eq_nil_iff]
47+
case cons y ys h_ind =>
48+
obtain ⟨rfl⟩ := List.reverse_eq_cons_iff.mp h_rev
49+
specialize h_ind (xs := ys.reverse) (by grind)
50+
grind [Quotient.lift_mk]
51+
52+
namespace FinAcc
53+
54+
open Acceptor RightCongruence
55+
56+
/-- The language of `c.toDA` with a single accepting state `s` is exactly
57+
the equivalence class corresponding to `s`. -/
58+
@[simp]
59+
theorem congr_language_eq {a : Quotient c.eq} : language (FinAcc.mk c.toDA {a}) = eqvCls a := by
60+
ext
61+
grind
62+
63+
end FinAcc
64+
65+
end Automata.DA
66+
67+
end Cslib

‎Cslib/Computability/Automata/NA/Pair.lean‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,67 @@ theorem LTS.pairLang_regular [Finite State] {lts : LTS State Symbol} {s t : Stat
3737
ext
3838
simp
3939

40+
/-- `LTS.pairViaLang via s t` is the language of finite words that can take the LTS
41+
from state `s` to state `t` via a state in `via`. -/
42+
def LTS.pairViaLang (lts : LTS State Symbol) (via : Set State) (s t : State) : Language Symbol :=
43+
⨆ r ∈ via, lts.pairLang s r * lts.pairLang r t
44+
45+
@[simp, scoped grind =]
46+
theorem LTS.mem_pairViaLang {lts : LTS State Symbol} {via : Set State}
47+
{s t : State} {xs : List Symbol} : xs ∈ lts.pairViaLang via s t ↔
48+
∃ r ∈ via, ∃ xs1 xs2, lts.MTr s xs1 r ∧ lts.MTr r xs2 t ∧ xs1 ++ xs2 = xs := by
49+
simp [LTS.pairViaLang, Language.mem_mul]
50+
51+
/-- `LTS.pairViaLang via s t` is a regular language if there are only finitely many states. -/
52+
@[simp]
53+
theorem LTS.pairViaLang_regular [Inhabited Symbol] [Finite State] {lts : LTS State Symbol}
54+
{via : Set State} {s t : State} : (lts.pairViaLang via s t).IsRegular := by
55+
apply IsRegular.iSup
56+
grind [Language.IsRegular.mul, LTS.pairLang_regular]
57+
58+
theorem LTS.pairLang_append {lts : LTS State Symbol} {s0 s1 s2 : State} {xs1 xs2 : List Symbol}
59+
(h1 : xs1 ∈ lts.pairLang s0 s1) (h2 : xs2 ∈ lts.pairLang s1 s2) :
60+
xs1 ++ xs2 ∈ lts.pairLang s0 s2 := by
61+
grind [<= LTS.MTr.comp]
62+
63+
theorem LTS.pairLang_split {lts : LTS State Symbol} {s0 s2 : State} {xs1 xs2 : List Symbol}
64+
(h : xs1 ++ xs2 ∈ lts.pairLang s0 s2) :
65+
∃ s1, xs1 ∈ lts.pairLang s0 s1 ∧ xs2 ∈ lts.pairLang s1 s2 := by
66+
obtain ⟨r, _, _⟩ := LTS.MTr.split <| LTS.mem_pairLang.mp h
67+
use r
68+
grind
69+
70+
theorem LTS.pairViaLang_append_pairLang {lts : LTS State Symbol}
71+
{s0 s1 s2 : State} {xs1 xs2 : List Symbol} {via : Set State}
72+
(h1 : xs1 ∈ lts.pairViaLang via s0 s1) (h2 : xs2 ∈ lts.pairLang s1 s2) :
73+
xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2 := by
74+
obtain ⟨r, _, _, _, _, _, rfl⟩ := LTS.mem_pairViaLang.mp h1
75+
apply LTS.mem_pairViaLang.mpr
76+
use r
77+
grind [<= LTS.MTr.comp]
78+
79+
theorem LTS.pairLang_append_pairViaLang {lts : LTS State Symbol}
80+
{s0 s1 s2 : State} {xs1 xs2 : List Symbol} {via : Set State}
81+
(h1 : xs1 ∈ lts.pairLang s0 s1) (h2 : xs2 ∈ lts.pairViaLang via s1 s2) :
82+
xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2 := by
83+
obtain ⟨r, _, _, _, _, _, rfl⟩ := LTS.mem_pairViaLang.mp h2
84+
apply LTS.mem_pairViaLang.mpr
85+
use r
86+
grind [<= LTS.MTr.comp]
87+
88+
theorem LTS.pairViaLang_split {lts : LTS State Symbol} {s0 s2 : State} {xs1 xs2 : List Symbol}
89+
{via : Set State} (h : xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2) :
90+
∃ s1, xs1 ∈ lts.pairViaLang via s0 s1 ∧ xs2 ∈ lts.pairLang s1 s2 ∨
91+
xs1 ∈ lts.pairLang s0 s1 ∧ xs2 ∈ lts.pairViaLang via s1 s2 := by
92+
obtain ⟨r, h_r, ys1, ys2, h_ys1, h_ys2, h_eq⟩ := LTS.mem_pairViaLang.mp h
93+
obtain ⟨zs1, rfl, rfl⟩ | ⟨zs2, rfl, rfl⟩ := List.append_eq_append_iff.mp h_eq
94+
· obtain ⟨s1, _, _⟩ := LTS.MTr.split h_ys2
95+
use s1
96+
grind
97+
· obtain ⟨s1, _, _⟩ := LTS.MTr.split h_ys1
98+
use s1
99+
grind
100+
40101
namespace Automata.NA.Buchi
41102

42103
open Set Filter ωSequence ωLanguage ωAcceptor

‎Cslib/Computability/Languages/Congruences/BuchiCongruence.lean‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
/-
2+
Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Ching-Tsun Chou
5+
-/
6+
7+
module
8+
9+
public import Cslib.Computability.Automata.NA.Pair
10+
public import Cslib.Computability.Languages.Congruences.RightCongruence
11+
12+
@[expose] public section
13+
14+
/-!
15+
# Buchi Congruence
16+
17+
A special type of right congruences used by J.R. Büchi to prove the closure
18+
of ω-regular languages under complementation.
19+
-/
20+
21+
namespace Cslib.Automata.NA.Buchi
22+
23+
open Function
24+
25+
variable {Symbol : Type*} {State : Type}
26+
27+
/-- Given a Buchi automaton `na`, two finite words `u` and `v` are Buchi-congruent
28+
according to `na` iff for every pair of states `s` and `t` of `na`, both of the
29+
following two conditions hold:
30+
(1) `u` can move `na` from `s` to `t` iff `v` can move `na` from `s` to `t`;
31+
(2) `u` can move `na` from `s` to `t` via an acceptingg states iff `v` can move `na`
32+
from `s` to `t` via an acceptingg states. -/
33+
def BuchiCongruence (na : Buchi State Symbol) : RightCongruence Symbol where
34+
eq.r u v :=
35+
∀ {s t}, (u ∈ na.pairLang s t ↔ v ∈ na.pairLang s t) ∧
36+
(u ∈ na.pairViaLang na.accept s t ↔ v ∈ na.pairViaLang na.accept s t)
37+
eq.iseqv.refl := by grind
38+
eq.iseqv.symm := by grind
39+
eq.iseqv.trans := by grind
40+
right_cov.elim := by
41+
grind [Covariant, → LTS.pairLang_split, <= LTS.pairLang_append, → LTS.pairViaLang_split,
42+
<= LTS.pairViaLang_append_pairLang, <= LTS.pairLang_append_pairViaLang]
43+
44+
open scoped Classical in
45+
/-- `BuchiCongrParam` is a parameterization of the equivalence classes of `na.BuchiCongruence`
46+
using the type `State → State → Prop × Prop`, which is finite if `State` is. -/
47+
noncomputable def BuchiCongrParam (na : Buchi State Symbol)
48+
(f : State → State → Prop × Prop) : Quotient na.BuchiCongruence.eq :=
49+
if h : ∃ u, ∀ s t, ((f s t).1 ↔ u ∈ na.pairLang s t) ∧
50+
((f s t).2 ↔ u ∈ na.pairViaLang na.accept s t)
51+
then ⟦ Classical.choose h ⟧
52+
else ⟦ [] ⟧
53+
54+
variable {na : Buchi State Symbol}
55+
56+
/-- `BuchiCongrParam` is surjective. -/
57+
lemma buchiCongrParam_surjective : Surjective na.BuchiCongrParam := by
58+
intro q
59+
let f s t := (q.out ∈ na.pairLang s t, q.out ∈ na.pairViaLang na.accept s t)
60+
have h : ∃ u, ∀ s t, ((f s t).1 ↔ u ∈ na.pairLang s t) ∧
61+
((f s t).2 ↔ u ∈ na.pairViaLang na.accept s t) := by
62+
use q.out
63+
grind
64+
use f
65+
simp only [BuchiCongrParam, h, ↓reduceDIte]
66+
rw [← Quotient.out_eq q]
67+
apply Quotient.sound
68+
intro s t
69+
grind
70+
71+
/-- `na.BuchiCongruence` is of finite index if `na` has only finitely many states. -/
72+
theorem buchiCongruence_fin_index [Finite State] : Finite (Quotient na.BuchiCongruence.eq) :=
73+
Finite.of_surjective na.BuchiCongrParam buchiCongrParam_surjective
74+
75+
end Cslib.Automata.NA.Buchi

‎Cslib/Computability/Languages/Congruences/RightCongruence.lean‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
/-
2+
Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Ching-Tsun Chou
5+
-/
6+
7+
module
8+
9+
public import Cslib.Init
10+
public import Mathlib.Computability.Language
11+
12+
@[expose] public section
13+
14+
/-!
15+
# Right Congruence
16+
17+
This file contains basic definitions about right congruences on finite sequences.
18+
19+
NOTE: Left congruences and two-sided congruences can be similarly defined.
20+
But they are left to future work because they are not needed for now.
21+
-/
22+
23+
namespace Cslib
24+
25+
/-- A right congruence is an equivalence relation on finite sequences (represented by lists)
26+
that is preserved by concatenation on the right. The equivalence relation is represented
27+
by a setoid to to enable ready access to the quotient construction. -/
28+
class RightCongruence (α : Type*) extends eq : Setoid (List α) where
29+
right_cov : CovariantClass _ _ (fun x y => y ++ x) eq
30+
31+
namespace RightCongruence
32+
33+
variable {α : Type*}
34+
35+
/-- The equivalence class (as a language) corresponding to an element of the quotient type. -/
36+
abbrev eqvCls [c : RightCongruence α] (a : Quotient c.eq) : Language α :=
37+
(Quotient.mk c.eq) ⁻¹' {a}
38+
39+
end RightCongruence
40+
41+
end Cslib

‎Cslib/Computability/Languages/RegularLanguage.lean‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou
66

77
module
88

9+
public import Cslib.Computability.Automata.DA.Congr
910
public import Cslib.Computability.Automata.DA.Prod
1011
public import Cslib.Computability.Automata.DA.ToNA
1112
public import Cslib.Computability.Automata.NA.Concat
@@ -24,7 +25,7 @@ public import Mathlib.Tactic.Common
2425

2526
namespace Cslib.Language
2627

27-
open Set List Prod Automata Acceptor
28+
open Set List Prod Automata Acceptor RightCongruence
2829
open scoped Computability FLTS DA NA DA.FinAcc NA.FinAcc
2930

3031
variable {Symbol : Type*}
@@ -159,4 +160,13 @@ theorem IsRegular.kstar [Inhabited Symbol] {l : Language Symbol}
159160
obtain ⟨State, h_fin, nfa, rfl⟩ := h
160161
use Unit ⊕ (State ⊕ Unit), inferInstance, ⟨finLoop nfa, {inl ()}⟩, loop_language_eq h_l
161162

163+
/-- If a right congruence is of finite index, then each of its equivalence classes is regular. -/
164+
@[simp]
165+
theorem IsRegular.congr_fin_index {Symbol : Type}
166+
[c : RightCongruence Symbol] [Finite (Quotient c.eq)]
167+
(a : Quotient c.eq) : (eqvCls a).IsRegular := by
168+
rw [IsRegular.iff_dfa]
169+
use Quotient c.eq, inferInstance, ⟨c.toDA, {a}⟩
170+
exact DA.FinAcc.congr_language_eq
171+
162172
end Cslib.Language

‎Cslib/Foundations/Semantics/FLTS/Basic.lean‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,9 +45,14 @@ from the left (instead of the right), in order to match the way lists are constr
4545
@[scoped grind =]
4646
def mtr (flts : FLTS State Label) (s : State) (μs : List Label) := μs.foldl flts.tr s
4747

48-
@[scoped grind =]
48+
@[simp, scoped grind =]
4949
theorem mtr_nil_eq {flts : FLTS State Label} {s : State} : flts.mtr s [] = s := rfl
5050

51+
@[simp, scoped grind =]
52+
theorem mtr_concat_eq {flts : FLTS State Label} {s : State} {μs : List Label} {μ : Label} :
53+
flts.mtr s (μs ++ [μ]) = flts.tr (flts.mtr s μs) μ := by
54+
grind
55+
5156
end FLTS
5257

5358
end Cslib

0 commit comments

Comments
 (0)