refactor: introduce grind sets for Automata (see issue #308)

Cslib/Computability/Automata/Acceptors/Acceptor.lean

@@ -23,12 +23,12 @@ namespace Acceptor
 variable {Symbol : Type v}
 
 /-- The language of an `Acceptor` is the set of strings it `Accepts`. -/
-@[scoped grind .]
+@[automata .]
 def language [Acceptor A Symbol] (a : A) : Language Symbol :=
   { xs | Accepts a xs }
 
 /-- A string is in the language of an acceptor iff the acceptor accepts it. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem mem_language [Acceptor A Symbol] (a : A) (xs : List Symbol) :
   xs ∈ language a ↔ Accepts a xs := Iff.rfl
 

Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean

@@ -22,12 +22,12 @@ namespace ωAcceptor
 variable {Symbol : Type v}
 
 /-- The language of an `ωAcceptor` is the set of sequences it `Accepts`. -/
-@[scoped grind .]
+@[automata .]
 def language [ωAcceptor A Symbol] (a : A) : ωLanguage Symbol :=
   { xs | Accepts a xs }
 
 /-- A string is in the language of an acceptor iff the acceptor accepts it. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem mem_language [ωAcceptor A Symbol] (a : A) (xs : ωSequence Symbol) :
   xs ∈ language a ↔ Accepts a xs := Iff.rfl
 

Cslib/Computability/Automata/DA/Basic.lean

@@ -29,7 +29,7 @@ finiteness assumptions), deterministic Buchi automata, and deterministic Muller
 -/
 
 open List Filter Cslib.ωSequence
-open scoped Cslib.FLTS
+open Cslib.FLTS
 
 namespace Cslib.Automata
 
@@ -43,31 +43,31 @@ namespace DA
 variable {State Symbol : Type*}
 
 /-- Helper function for defining `run` below. -/
-@[scoped grind =]
+@[automata =]
 def run' (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State
   | 0 => da.start
   | n + 1 => da.tr (run' da xs n) (xs n)
 
 /-- Infinite run. -/
-@[scoped grind =]
+@[automata =]
 def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs
 
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem run_zero {da : DA State Symbol} {xs : ωSequence Symbol} :
     da.run xs 0 = da.start :=
   rfl
 
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem run_succ {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} :
     da.run xs (n + 1) = da.tr (da.run xs n) (xs n) := by
   rfl
 
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem mtr_extract_eq_run {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} :
     da.mtr da.start (xs.extract 0 n) = da.run xs n := by
   induction n
   case zero => rfl
-  case succ n h_ind => grind
+  case succ n h_ind => grind [automata]
 
 /-- A deterministic automaton that accepts finite strings (lists of symbols). -/
 structure FinAcc (State Symbol : Type*) extends DA State Symbol where

Cslib/Computability/Automata/DA/Buchi.lean

@@ -17,15 +17,15 @@ open Filter
 
 namespace Cslib.Automata.DA
 
-open scoped FinAcc Buchi
+open FinAcc Buchi
 
 variable {State Symbol : Type*}
 
 open Acceptor ωAcceptor in
 /-- The ω-language accepted by a deterministic Buchi automaton is the ω-limit
 of the language accepted by the same automaton.
 -/
-@[scoped grind =]
+@[automata =]
 theorem buchi_eq_finAcc_omegaLim {da : DA State Symbol} {acc : Set State} :
     language (Buchi.mk da acc) = (language (FinAcc.mk da acc))↗ω := by
   ext xs

Cslib/Computability/Automata/DA/Congr.lean

@@ -15,7 +15,7 @@ public import Cslib.Computability.Languages.Congruences.RightCongruence
 
 namespace Cslib
 
-open scoped FLTS RightCongruence
+open FLTS RightCongruence
 
 variable {Symbol : Type*}
 
@@ -58,7 +58,7 @@ the equivalence class corresponding to `s`. -/
 @[simp]
 theorem congr_language_eq {a : Quotient c.eq} : language (FinAcc.mk c.toDA {a}) = eqvCls a := by
   ext
-  grind
+  grind [automata]
 
 end FinAcc
 

Cslib/Computability/Automata/DA/Prod.lean

@@ -16,21 +16,21 @@ public import Cslib.Foundations.Semantics.FLTS.Prod
 namespace Cslib.Automata
 
 open List
-open scoped FLTS
+open FLTS
 
 variable {State1 State2 Symbol : Type*}
 
 namespace DA
 
 /-- The product of two deterministic automata. -/
-@[scoped grind =]
+@[automata =]
 def prod (da1 : DA State1 Symbol) (da2 : DA State2 Symbol) : DA (State1 × State2) Symbol where
   toFLTS := da1.toFLTS.prod da2.toFLTS
   start := (da1.start, da2.start)
 
 /-- A state is reachable by the product automaton iff its components are reachable by
 the respective automaton components. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem prod_mtr_eq (da1 : DA State1 Symbol) (da2 : DA State2 Symbol)
     (s : State1 × State2) (xs : List Symbol) :
     (da1.prod da2).mtr s xs = (da1.mtr s.fst xs, da2.mtr s.snd xs) :=

Cslib/Computability/Automata/DA/ToNA.lean

@@ -23,63 +23,61 @@ variable {State Symbol : Type*}
 section NA
 
 /-- `DA` is a special case of `NA`. -/
-@[scoped grind =]
+@[automata =]
 def toNA (a : DA State Symbol) : NA State Symbol :=
   { a.toLTS with start := {a.start} }
 
 instance : Coe (DA State Symbol) (NA State Symbol) where
   coe := toNA
 
-open scoped FLTS NA NA.Run LTS in
-@[simp, scoped grind =]
+open FLTS NA NA.Run LTS in
+@[simp, automata =]
 theorem toNA_run {a : DA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} :
     a.toNA.Run xs ss ↔ a.run xs = ss := by
   constructor
   · rintro _
     ext n
-    induction n <;> grind [NA.Run]
-  · grind [NA.Run]
+    induction n <;> grind [automata, NA.Run]
+  · grind [automata, NA.Run]
 
 namespace FinAcc
 
 /-- `DA.FinAcc` is a special case of `NA.FinAcc`. -/
-@[scoped grind =]
+@[automata =]
 def toNAFinAcc (a : DA.FinAcc State Symbol) : NA.FinAcc State Symbol :=
   { a.toNA with accept := a.accept }
 
-open Acceptor in
-open scoped FLTS NA.FinAcc in
+open Acceptor FLTS NA.FinAcc in
 /-- The `NA.FinAcc` constructed from a `DA.FinAcc` has the same language. -/
-@[simp, scoped grind _=_]
+@[simp, automata _=_]
 theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} :
     language a.toNAFinAcc = language a := by
   ext xs
   constructor
-  · grind
+  · grind [automata]
   · intro _
     use a.start
-    grind
+    grind [automata]
 
 end FinAcc
 
 namespace Buchi
 
 /-- `DA.Buchi` is a special case of `NA.Buchi`. -/
-@[scoped grind =]
+@[automata =]
 def toNABuchi (a : DA.Buchi State Symbol) : NA.Buchi State Symbol :=
   { a.toNA with accept := a.accept }
 
-open ωAcceptor in
-open scoped NA.Buchi in
+open ωAcceptor NA.Buchi in
 /-- The `NA.Buchi` constructed from a `DA.Buchi` has the same ω-language. -/
-@[simp, scoped grind _=_]
+@[simp, automata _=_]
 theorem toNABuchi_language_eq {a : DA.Buchi State Symbol} :
     language a.toNABuchi = language a := by
   ext xs; constructor
-  · grind
+  · grind [automata]
   · intro _
     use (a.run xs)
-    grind
+    grind [automata]
 
 end Buchi
 

Cslib/Computability/Automata/EpsilonNA/Basic.lean

@@ -43,7 +43,7 @@ namespace FinAcc
 
 /-- An `εNA.FinAcc` accepts a string if there is a saturated multistep accepting derivative with
 that trace from the start state. -/
-@[scoped grind =]
+@[automata =]
 instance : Acceptor (FinAcc State Symbol) Symbol where
   Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
     ∃ s ∈ a.εClosure a.start, ∃ s' ∈ a.accept,

Cslib/Computability/Automata/EpsilonNA/ToNA.lean

@@ -26,7 +26,7 @@ private lemma LTS.noε_saturate_tr
   lts.saturate.Tr s μ s' ↔ lts.saturate.noε.Tr s μ' s' := by
   grind
 
-@[scoped grind =]
+@[automata =]
 lemma LTS.noε_saturate_mTr {lts : LTS State (Option Label)} :
   lts.saturate.MTr s (μs.map some) = lts.saturate.noε.MTr s μs := by
   ext s'
@@ -37,22 +37,21 @@ namespace Automata.εNA.FinAcc
 variable {State Symbol : Type*}
 
 /-- Any `εNA.FinAcc` can be converted into an `NA.FinAcc` that does not use ε-transitions. -/
-@[scoped grind]
+@[automata]
 def toNAFinAcc (a : εNA.FinAcc State Symbol) : NA.FinAcc State Symbol where
   start := a.εClosure a.start
   accept := a.accept
   Tr := a.saturate.noε.Tr
 
-open Acceptor in
-open scoped NA.FinAcc in
+open Acceptor NA.FinAcc in
 /-- Correctness of `toNAFinAcc`. -/
-@[scoped grind _=_]
+@[automata _=_]
 theorem toNAFinAcc_language_eq {ena : εNA.FinAcc State Symbol} :
     language ena.toNAFinAcc = language ena := by
   ext xs
   have : ∀ s s', ena.saturate.MTr s (xs.map some) s' = ena.saturate.noε.MTr s xs s' := by
     simp [LTS.noε_saturate_mTr]
-  grind
+  grind [automata]
 
 end Automata.εNA.FinAcc
 

Cslib/Computability/Automata/NA/Basic.lean

@@ -60,7 +60,7 @@ namespace FinAcc
 accept state.
 
 This is the standard string recognition performed by NFAs in the literature. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 instance : Acceptor (FinAcc State Symbol) Symbol where
   Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
     ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTr s xs s'
@@ -75,7 +75,7 @@ structure Buchi (State Symbol : Type*) extends NA State Symbol where
 namespace Buchi
 
 /-- An infinite run is accepting iff accepting states occur infinitely many times. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 instance : ωAcceptor (Buchi State Symbol) Symbol where
   Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) :=
     ∃ ss, a.Run xs ss ∧ ∃ᶠ k in atTop, ss k ∈ a.accept
@@ -91,7 +91,7 @@ namespace Muller
 
 /-- An infinite run is accepting iff the set of states that occur infinitely many times
 is one of the sets in `accept`. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 instance : ωAcceptor (Muller State Symbol) Symbol where
   Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) :=
     ∃ ss, a.Run xs ss ∧ ss.infOcc ∈ a.accept

Cslib/Computability/Automata/NA/BuchiEquiv.lean

@@ -13,7 +13,7 @@ public import Cslib.Computability.Automata.NA.Basic
 /-! # Equivalence of nondeterministic Buchi automata (NBAs). -/
 
 open Set Function Filter Cslib.ωSequence
-open scoped Cslib.LTS
+open Cslib.LTS
 
 universe u v w
 
@@ -24,7 +24,7 @@ open ωAcceptor
 variable {Symbol : Type u} {State : Type v} {State' : Type w}
 
 /-- Lifts an equivalence on states to an equivalence on NBAs. -/
-@[scoped grind =]
+@[automata =]
 def reindex (f : State ≃ State') : Buchi State Symbol ≃ Buchi State' Symbol where
   toFun nba := {
     Tr s x t := nba.Tr (f.symm s) x (f.symm t)
@@ -54,15 +54,15 @@ theorem reindex_run_iff' {f : State ≃ State'} {nba : Buchi State Symbol}
     (nba.reindex f).Run xs (ss.map f) ↔ nba.Run xs ss := by
   simp [reindex_run_iff]
 
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem reindex_language_eq {f : State ≃ State'} {nba : Buchi State Symbol} :
     language (nba.reindex f) = language nba := by
   ext xs
   constructor
   · rintro ⟨ss', h_run', h_acc'⟩
-    grind [reindex_run_iff]
+    grind [automata, reindex_run_iff]
   · rintro ⟨ss, h_run, h_acc⟩
     use ss.map f
-    constructor <;> grind [reindex_run_iff']
+    constructor <;> grind [automata, reindex_run_iff']
 
 end Cslib.Automata.NA.Buchi