Incorporate Chris Henson's and Eric Wieser's comments

Author: ctchou

Cslib/Computability/Automata/DA.lean

@@ -20,21 +20,17 @@ namespace Cslib
 
 open List
 
-structure DA (State : Type _) (Symbol : Type _) where
+structure DA (State : Type*) (Symbol : Type*) where
   /-- The initial state of the automaton. -/
   start : State
   /-- The transition function of the automaton. -/
   tr : State → Symbol → State
 
 namespace DA
 
-variable {State State1 State2 : Type _} {Symbol : Type _}
+variable {State State1 State2 : Type*} {Symbol : Type*}
 
-/-- Extended transition function.
-
-Implementation note: compared to [Hopcroft2006], the definition consumes the input list of symbols
-from the left (instead of the right), in order to match the way lists are constructed.
--/
+/-- Extended transition function. -/
 @[scoped grind =]
 def mtr (DA : DA State Symbol) (s : State) (xs : List Symbol) := xs.foldl DA.tr s
 

Cslib/Computability/Automata/DFA.lean

@@ -21,7 +21,7 @@ open scoped DA Language
 /-- A Deterministic Finite Automaton (DFA) consists of a labelled transition function
 `tr` over finite sets of states and labels (called symbols), a starting state `start` and a finite
 set of accepting states `accept`. -/
-structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where
+structure DFA (State : Type*) (Symbol : Type*) extends DA State Symbol where
   /-- The set of accepting states of the automaton. -/
   accept : Set State
   /-- The automaton is finite-state. -/
@@ -31,7 +31,7 @@ structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where
 
 namespace DFA
 
-variable {State State1 State2 : Type _} {Symbol : Type _}
+variable {State State1 State2 : Type*} {Symbol : Type*}
 
 /-- A DFA accepts a string if there is a multi-step accepting derivative with that trace from
 the start state. -/
@@ -75,12 +75,11 @@ theorem one_lang [Finite Symbol] : one.language = (1 : Language Symbol) := by
   · intro h ; by_contra h'
     have := dropLast_append_getLast h'
     grind
-  · rw [Language.mem_one]
-    grind
+  · grind [Language.mem_one]
 
 @[scoped grind =]
 def compl (dfa : DFA State Symbol) : DFA State Symbol :=
-  { dfa with accept := (dfa.accept)ᶜ }
+  { dfa with accept := dfa.acceptᶜ }
 
 @[simp, scoped grind =]
 theorem compl_lang (dfa : DFA State Symbol) : dfa.compl.language = (dfa.language)ᶜ := by

Cslib/Computability/Automata/DFAToNFA.lean

@@ -15,7 +15,7 @@ open scoped DA
 
 namespace DFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 section NFA
 

Cslib/Computability/Automata/EpsilonNFA.lean

@@ -17,15 +17,15 @@ symbol type. The special symbol ε is represented by the `Option.none` case.
 Internally, ε (`Option.none`) is treated as the `τ` label of the underlying transition system,
 allowing for reusing the definitions and results on saturated transitions of `LTS` to deal with
 ε-closure. -/
-structure εNFA (State : Type _) (Symbol : Type _) extends NA State (Option Symbol) where
+structure εNFA (State : Type*) (Symbol : Type*) extends NA State (Option Symbol) where
   /-- The set of accepting states of the automaton. -/
   accept : Set State
   /-- The automaton is finite-state. -/
   finite_state : Finite State
   /-- The type of symbols (also called 'alphabet') is finite. -/
   finite_symbol : Finite Symbol
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 @[local grind =]
 private instance : HasTau (Option α) := ⟨.none⟩

Cslib/Computability/Automata/EpsilonNFAToNFA.lean

@@ -27,7 +27,7 @@ private lemma LTS.noε_saturate_tr
 
 namespace εNFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 section NFA
 
@@ -41,7 +41,7 @@ def toNFA (enfa : εNFA State Symbol) : NFA State Symbol where
   finite_symbol := enfa.finite_symbol
 
 @[scoped grind =]
-lemma LTS.noε_saturate_mTr {s : State} {Label : Type _} {μs : List Label}
+lemma LTS.noε_saturate_mTr {s : State} {Label : Type*} {μs : List Label}
   {lts : LTS State (Option Label)} :
   lts.saturate.MTr s (μs.map (some ·)) = lts.saturate.noε.MTr s μs := by
   ext s'

Cslib/Computability/Automata/NA.lean

@@ -17,7 +17,7 @@ type `State → Symbol → Set State`; it gets automatically expanded to the for
 
 namespace Cslib
 
-structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where
+structure NA (State : Type*) (Symbol : Type*) extends LTS State Symbol where
   /-- The set of initial states of the automaton. -/
   start : Set State
 

Cslib/Computability/Automata/NFA.lean

@@ -11,7 +11,7 @@ namespace Cslib
 
 /-- A Nondeterministic Finite Automaton (NFA) is a nondeterministic automaton (NA)
 over finite sets of states and symbols. -/
-structure NFA (State : Type _) (Symbol : Type _) extends NA State Symbol where
+structure NFA (State : Type*) (Symbol : Type*) extends NA State Symbol where
   /-- The set of accepting states of the automaton. -/
   accept : Set State
   /-- The automaton is finite-state. -/
@@ -21,7 +21,7 @@ structure NFA (State : Type _) (Symbol : Type _) extends NA State Symbol where
 
 namespace NFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 /-- An NFA accepts a string if there is a multi-step accepting derivative with that trace from
 the start state. -/

Cslib/Computability/Automata/NFAToDFA.lean

@@ -13,7 +13,7 @@ namespace Cslib
 
 namespace NFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 section SubsetConstruction
 

Cslib/Computability/Languages/Language.lean

@@ -20,35 +20,25 @@ namespace Language
 open Set List
 open scoped Computability
 
-variable {α : Type _} {l m : Language α}
+variable {α : Type*} {l m : Language α}
 
 @[simp, scoped grind =]
 theorem mem_inf (x : List α) : x ∈ l ⊓ m ↔ x ∈ l ∧ x ∈ m :=
   Iff.rfl
 
 @[simp]
-theorem mem_biInf {I : Type _} (s : Set I) (l : I → Language α) (x : List α) :
+theorem mem_biInf {I : Type*} (s : Set I) (l : I → Language α) (x : List α) :
     (x ∈ ⨅ i ∈ s, l i) ↔ ∀ i ∈ s, x ∈ l i :=
   mem_iInter₂
 
 @[simp]
-theorem mem_biSup {I : Type _} (s : Set I) (l : I → Language α) (x : List α) :
+theorem mem_biSup {I : Type*} (s : Set I) (l : I → Language α) (x : List α) :
     (x ∈ ⨆ i ∈ s, l i) ↔ ∃ i ∈ s, x ∈ l i := by
-  constructor
-  · intro h
-    obtain ⟨i, h_i, h_x⟩ := mem_iUnion₂.mp h
-    use i
-  · rintro ⟨i, h_i, h_x⟩
-    apply mem_iUnion₂.mpr
-    use i
-
-theorem biInf_insert {I : Type _} (a : I) (s : Set I) (l : I → Language α) :
-    (⨅ i ∈ insert a s, l i) = l a ⊓ ⨅ i ∈ s, l i := by
-  apply biInter_insert
-
-theorem biSup_insert {I : Type _} (a : I) (s : Set I) (l : I → Language α) :
-    (⨆ i ∈ insert a s, l i) = l a ⊔ ⨆ i ∈ s, l i := by
-  apply biUnion_insert
+  constructor <;> intro h
+  · have := mem_iUnion₂.mp h
+    grind
+  · apply mem_iUnion₂.mpr
+    grind
 
 -- This section will be removed once the following PR gets into mathlib:
 -- https://github.com/leanprover-community/mathlib4/pull/30913

Cslib/Computability/Languages/OmegaLanguage.lean

@@ -59,7 +59,7 @@ open scoped Computability
 
 universe v
 
-variable {α β γ : Type _}
+variable {α β γ : Type*}
 
 /-- An ω-language is a set of strings over an alphabet. -/
 def ωLanguage (α) :=