Merge remote-tracking branch 'upstream/main' into grind-lint

chenson2018 · chenson2018 · commit bb5d6f07e421 · 2025-11-27T15:40:16.000-05:00
diff --git a/Cslib.lean b/Cslib.lean
@@ -64,5 +64,4 @@ import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 import Cslib.Logics.LinearLogic.CLL.Basic
 import Cslib.Logics.LinearLogic.CLL.CutElimination
-import Cslib.Logics.LinearLogic.CLL.MProof
 import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean
@@ -29,6 +29,7 @@ open scoped Cslib.FLTS
 
 namespace Cslib.Automata
 
+/-- A deterministic automaton extends a `FLTS` with a unique initial state. -/
 structure DA (State Symbol : Type*) extends FLTS State Symbol where
   /-- The initial state of the automaton. -/
   start : State
@@ -66,7 +67,7 @@ theorem mtr_extract_eq_run {da : DA State Symbol} {xs : ωSequence Symbol} {n :
 
 /-- A deterministic automaton that accepts finite strings (lists of symbols). -/
 structure FinAcc (State Symbol : Type*) extends DA State Symbol where
-  /-- The accept states. -/
+  /-- The set of accepting states. -/
   accept : Set State
 
 namespace FinAcc
@@ -77,33 +78,39 @@ the string to an accept state.
 This is the standard string recognition performed by DFAs in the literature. -/
 @[simp, scoped grind =]
 instance : Acceptor (DA.FinAcc State Symbol) Symbol where
-  Accepts (a : DA.FinAcc State Symbol) (xs : List Symbol) := a.mtr a.start xs ∈ a.accept
+  Accepts (a : DA.FinAcc State Symbol) (xs : List Symbol) :=
+    a.mtr a.start xs ∈ a.accept
 
 end FinAcc
 
 /-- Deterministic Buchi automaton. -/
 structure Buchi (State Symbol : Type*) extends DA State Symbol where
-  /-- The accept states -/
+  /-- The set of accepting states. -/
   accept : Set State
 
 namespace Buchi
 
+/-- An infinite run is accepting iff accepting states occur infinitely many times. -/
 @[simp, scoped grind =]
 instance : ωAcceptor (Buchi State Symbol) Symbol where
-  Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) := ∃ᶠ k in atTop, a.run xs k ∈ a.accept
+  Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) :=
+    ∃ᶠ k in atTop, a.run xs k ∈ a.accept
 
 end Buchi
 
 /-- Deterministic Muller automaton. -/
 structure Muller (State Symbol : Type*) extends DA State Symbol where
-  /-- The accepting set of sets of states. -/
+  /-- The set of sets of accepting states. -/
   accept : Set (Set State)
 
 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 =]
 instance : ωAcceptor (Muller State Symbol) Symbol where
-  Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) := (a.run xs).infOcc ∈ a.accept
+  Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) :=
+    (a.run xs).infOcc ∈ a.accept
 
 end Muller
 
diff --git a/Cslib/Computability/Automata/EpsilonNA.lean b/Cslib/Computability/Automata/EpsilonNA.lean
@@ -30,7 +30,9 @@ abbrev εNA.εClosure (a : εNA State Symbol) (S : Set State) := a.τClosure S
 
 namespace εNA
 
+/-- The finite-word acceptance condition of an `εNA` is a set of accepting states. -/
 structure FinAcc (State Symbol : Type*) extends εNA State Symbol where
+  /-- The set of accepting states. -/
   accept : Set State
 
 namespace FinAcc
diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean
@@ -31,6 +31,7 @@ open Filter
 
 namespace Cslib.Automata
 
+/-- A nondeterministic automaton extends a `LTS` with a set of initial states. -/
 structure NA (State Symbol : Type*) extends LTS State Symbol where
   /-- The set of initial states of the automaton. -/
   start : Set State
@@ -64,7 +65,7 @@ end NARunGrind
 
 /-- A nondeterministic automaton that accepts finite strings (lists of symbols). -/
 structure FinAcc (State Symbol : Type*) extends NA State Symbol where
-  /-- The accept states. -/
+  /-- The set of accepting states. -/
   accept : Set State
 
 namespace FinAcc
@@ -82,10 +83,12 @@ end FinAcc
 
 /-- Nondeterministic Buchi automaton. -/
 structure Buchi (State Symbol : Type*) extends NA State Symbol where
+  /-- The set of accepting states. -/
   accept : Set State
 
 namespace Buchi
 
+/-- An infinite run is accepting iff accepting states occur infinitely many times. -/
 @[simp, scoped grind =]
 instance : ωAcceptor (Buchi State Symbol) Symbol where
   Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) :=
@@ -95,10 +98,13 @@ end Buchi
 
 /-- Nondeterministic Muller automaton. -/
 structure Muller (State Symbol : Type*) extends NA State Symbol where
+  /-- The set of sets of accepting states. -/
   accept : Set (Set State)
 
 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 =]
 instance : ωAcceptor (Muller State Symbol) Symbol where
   Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) :=
diff --git a/Cslib/Computability/Automata/Prod.lean b/Cslib/Computability/Automata/Prod.lean
@@ -17,14 +17,15 @@ variable {State1 State2 Symbol : Type*}
 
 namespace DA
 
-/-
-TODO: This operation could be generalised to FLTS and lifted here.
--/
+/-- The product of two deterministic automata.
+TODO: This operation could be generalised to FLTS and lifted here. -/
 @[scoped grind =]
 def prod (da1 : DA State1 Symbol) (da2 : DA State2 Symbol) : DA (State1 × State2) Symbol where
   start := (da1.start, da2.start)
   tr := fun (s1, s2) x ↦ (da1.tr s1 x, da2.tr s2 x)
 
+/-- A state is reachable by the product automaton iff its components are reachable by
+the respective component automata. -/
 @[simp, scoped grind =]
 theorem prod_mtr_eq (da1 : DA State1 Symbol) (da2 : DA State2 Symbol)
     (s : State1 × State2) (xs : List Symbol) :
diff --git a/Cslib/Computability/Automata/Sum.lean b/Cslib/Computability/Automata/Sum.lean
@@ -16,11 +16,13 @@ open scoped Run
 
 variable {Symbol I : Type*} {State : I → Type*}
 
+/-- The sum of an indexed family of nondeterministic automata. -/
 @[scoped grind =]
 def iSum (na : (i : I) → NA (State i) Symbol) : NA (Σ i, State i) Symbol where
   start := ⋃ i, Sigma.mk i '' (na i).start
   Tr s x t := ∃ i s_i t_i, (na i).Tr s_i x t_i ∧ ⟨i, s_i⟩ = s ∧ ⟨i, t_i⟩ = t
 
+/-- An infinite run of the sum automaton is an infinite run of one of its component automata. -/
 @[simp, scoped grind =]
 theorem iSum_run_iff {na : (i : I) → NA (State i) Symbol}
     {xs : ωSequence Symbol} {ss : ωSequence (Σ i, State i)} :
@@ -54,6 +56,8 @@ namespace Buchi
 
 open ωAcceptor
 
+/-- The ω-language accepted by the Buchi sum automata is the union of the ω-languages accepted
+by its component automata. -/
 @[simp]
 theorem iSum_language_eq {na : (i : I) → NA (State i) Symbol} {acc : (i : I) → Set (State i)} :
     language (Buchi.mk (iSum na) (⋃ i, Sigma.mk i '' (acc i))) =
diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean
@@ -117,11 +117,13 @@ A.k.a. ω-power.
 def omegaPow [Inhabited α] (l : Language α) : ωLanguage α :=
   { s | ∃ xs : ωSequence (List α), xs.flatten = s ∧ ∀ k, xs k ∈ l - 1 }
 
-/-- Use the postfix notation ^ω` for `omegaPow`. -/
+/-- Notation class for `omegaPow`. -/
 @[notation_class]
 class OmegaPow (α : Type*) (β : outParam (Type*)) where
+  /-- The `omegaPow` operation. -/
   omegaPow : α → β
 
+/-- Use the postfix notation ^ω` for `omegaPow`. -/
 postfix:1024 "^ω" => OmegaPow.omegaPow
 
 instance [Inhabited α] : OmegaPow (Language α) (ωLanguage α) :=
@@ -131,17 +133,18 @@ theorem omegaPow_def [Inhabited α] (l : Language α) :
     l^ω = { s | ∃ xs : ωSequence (List α), xs.flatten = s ∧ ∀ k, xs k ∈ l - 1 }
   := rfl
 
-/- The ω-limit of a language `l` is the ω-language of infinite sequences each of which
-contains infinitely many distinct prefixes in `l`.
--/
+/-- The ω-limit of a language `l` is the ω-language of infinite sequences each of which
+contains infinitely many distinct prefixes in `l`. -/
 def omegaLim (l : Language α) : ωLanguage α :=
   { s | ∃ᶠ m in atTop, s.extract 0 m ∈ l }
 
-/-- Use the postfix notation ↗ω` for `omegaLim`. -/
+/-- Notation class for `omegaLim`. -/
 @[notation_class]
 class OmegaLim (α : Type*) (β : outParam (Type*)) where
+  /-- The `omegaLim` operation. -/
   omegaLim : α → β
 
+/-- Use the postfix notation ↗ω` for `omegaLim`. -/
 postfix:1024 "↗ω" => OmegaLim.omegaLim
 
 instance instOmegaLim : OmegaLim (Language α) (ωLanguage α) :=
diff --git a/Cslib/Foundations/Data/Nat/Segment.lean b/Cslib/Foundations/Data/Nat/Segment.lean
@@ -11,11 +11,15 @@ import Mathlib.Data.Nat.Nth
 open Function Set
 
 /-!
+# Segments defined by a strictly monotonic function on Nat
+
 Given a strictly monotonic function `f : ℕ → ℕ` and `k : ℕ` with `k ≥ f 0`,
 `Nat.segment f k` is the unique `m : ℕ` such that `f m ≤ k < f (k + 1)`.
 `Nat.segment f k` is defined to be 0 for `k < f 0`.
 This file defines `Nat.segment` and proves various properties aboout it.
 -/
+
+/-- The `f`-segment of `k`, where `f : ℕ → ℕ` will be assumed to be at least StrictMono. -/
 @[scoped grind]
 noncomputable def Nat.segment (f : ℕ → ℕ) (k : ℕ) : ℕ :=
   open scoped Classical in
diff --git a/Cslib/Foundations/Data/OmegaSequence/Defs.lean b/Cslib/Foundations/Data/OmegaSequence/Defs.lean
@@ -28,6 +28,7 @@ variable {α : Type u} {β : Type v} {δ : Type w}
 
 /-- An `ωSequence α` is an infinite sequence of elements of `α`. -/
 structure ωSequence (α : Type u) where
+  /-- The function that defines this infinite sequence. -/
   get : ℕ → α
 
 instance : FunLike (ωSequence α) ℕ α where
diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
@@ -52,27 +52,20 @@ theorem Relation.ReflTransGen.diamond_confluence (h : Diamond R) : Confluence R
     exact ⟨D', ⟨B_D', ReflTransGen.trans CD D_D'⟩⟩
 
 -- not sure why this doesn't compile as an "instance" but oh well
+/-- A pair of subrelations lifts to transitivity on the relation. -/
 def trans_of_subrelation {α : Type _} (s s' r : α → α → Prop) (hr : Transitive r)
     (h : ∀ a b : α, s a b → r a b) (h' : ∀ a b : α, s' a b → r a b) : Trans s s' r where
-  trans := by
-    intro a b c hab hbc
-    replace hab := h _ _ hab
-    replace hbc := h' _ _ hbc
-    exact hr hab hbc
+  trans hab hbc := hr (h _ _ hab) (h' _ _ hbc)
 
+/-- A subrelation lifts to transitivity on the left of the relation. -/
 def trans_of_subrelation_left {α : Type _} (s r : α → α → Prop) (hr : Transitive r)
     (h : ∀ a b : α, s a b → r a b) : Trans s r r where
-  trans := by
-    intro a b c hab hbc
-    replace hab := h _ _ hab
-    exact hr hab hbc
+  trans hab hbc := hr (h _ _ hab) hbc
 
+/-- A subrelation lifts to transitivity on the right of the relation. -/
 def trans_of_subrelation_right {α : Type _} (s r : α → α → Prop) (hr : Transitive r)
     (h : ∀ a b : α, s a b → r a b) : Trans r s r where
-  trans := by
-    intro a b c hab hbc
-    replace hbc := h _ _ hbc
-    exact hr hab hbc
+  trans hab hbc := hr hab (h _ _ hbc)
 
 /-- This is a straightforward but useful specialisation of a more general result in
 `Mathlib.Logic.Relation`. -/
diff --git a/Cslib/Foundations/Lint/Basic.lean b/Cslib/Foundations/Lint/Basic.lean
@@ -28,6 +28,6 @@ def topNamespace : Batteries.Tactic.Lint.Linter where
     if top.contains declName.components[0]! then
       return none
     else
-      return m!"{declName} is not namespaced."
+      return m!"is not namespaced."
 
 end Cslib.Lint
diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -370,6 +370,7 @@ section Weak
 
 /-- A type of transition labels that includes a special 'internal' transition `τ`. -/
 class HasTau (Label : Type v) where
+  /-- The internal transition label, also known as τ. -/
   τ : Label
 
 /-- Saturated transition relation. -/
@@ -679,12 +680,16 @@ syntax attrKind "lts_transition_notation" ident (str)? : command
 macro_rules
   | `($kind:attrKind lts_transition_notation $lts $sym) =>
     `(
+      @[nolint docBlame]
       $kind:attrKind notation3 t:39 "["μ"]⭢" $sym:str t':39 => (LTS.Tr.toRelation $lts μ) t t'
+      @[nolint docBlame]
       $kind:attrKind notation3 t:39 "["μs"]↠" $sym:str t':39 => (LTS.MTr.toRelation $lts μs) t t'
      )
   | `($kind:attrKind lts_transition_notation $lts) =>
     `(
+      @[nolint docBlame]
       $kind:attrKind notation3 t:39 "["μ"]⭢" t':39 => (LTS.Tr.toRelation $lts μ) t t'
+      @[nolint docBlame]
       $kind:attrKind notation3 t:39 "["μs"]↠" t':39 => (LTS.MTr.toRelation $lts μs) t t'
      )
 
diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean
@@ -94,12 +94,16 @@ syntax attrKind "reduction_notation" ident (str)? : command
 macro_rules
   | `($kind:attrKind reduction_notation $rs $sym) =>
     `(
+      @[nolint docBlame]
       $kind:attrKind notation3 t:39 " ⭢" $sym:str t':39 => (ReductionSystem.Red  $rs) t t'
+      @[nolint docBlame]
       $kind:attrKind notation3 t:39 " ↠" $sym:str t':39 => (ReductionSystem.MRed $rs) t t'
      )
   | `($kind:attrKind reduction_notation $rs) =>
     `(
+      @[nolint docBlame]
       $kind:attrKind notation3 t:39 " ⭢ " t':39 => (ReductionSystem.Red  $rs) t t'
+      @[nolint docBlame]
       $kind:attrKind notation3 t:39 " ↠ " t':39 => (ReductionSystem.MRed $rs) t t'
      )
 
diff --git a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean
@@ -13,6 +13,7 @@ class HasAlphaEquiv (β : Type u) where
   /-- α-equivalence relation for type β. -/
   AlphaEquiv : β → β → Prop
 
+@[inherit_doc]
 notation m:max " =α " n:max => HasAlphaEquiv.AlphaEquiv m n
 
 end Cslib
diff --git a/Cslib/Languages/CCS/Basic.lean b/Cslib/Languages/CCS/Basic.lean
@@ -75,7 +75,8 @@ theorem Co.symm (h : Act.Co μ μ') : Act.Co μ' μ := by grind
 @[grind →]
 theorem co_isVisible (h : Act.Co μ μ') : μ.IsVisible ∧ μ'.IsVisible := by grind
 
-@[grind]
+/-- Checks that an action is the coaction of another. This is the Boolean version of `Act.Co`. -/
+@[grind =]
 def isCo [DecidableEq Name] (μ μ' : Act Name) : Bool :=
   match μ, μ' with
   | name a, coname b | coname a, name b => a = b
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean
@@ -38,12 +38,14 @@ def openRec (X : ℕ) (δ : Ty Var) : Ty Var → Ty Var
 | all σ τ => all (openRec X δ σ) (openRec (X + 1) δ τ)
 | sum σ τ => sum (openRec X δ σ) (openRec X δ τ)
 
+@[inherit_doc]
 scoped notation:68 γ "⟦" X " ↝ " δ "⟧ᵞ"=> openRec X δ γ
 
 /-- Variable opening (type opening to type) of the closest binding. -/
 @[scoped grind =]
 def open' (γ δ : Ty Var) := openRec 0 δ γ
 
+@[inherit_doc]
 scoped infixr:80 " ^ᵞ " => open'
 
 /-- Locally closed types. -/
@@ -149,12 +151,14 @@ def openRec_ty (X : ℕ) (δ : Ty Var) : Term Var → Term Var
 | inr t₂ => inr (openRec_ty X δ t₂)
 | case t₁ t₂ t₃ => case (openRec_ty X δ t₁) (openRec_ty X δ t₂) (openRec_ty X δ t₃)
 
+@[inherit_doc]
 scoped notation:68 t "⟦" X " ↝ " δ "⟧ᵗᵞ"=> openRec_ty X δ t
 
 /-- Variable opening (term opening to type) of the closest binding. -/
 @[scoped grind =]
 def open_ty (t : Term Var) (δ : Ty Var) := openRec_ty 0 δ t
 
+@[inherit_doc]
 scoped infixr:80 " ^ᵗᵞ " => open_ty
 
 /-- Variable opening (term opening to term) of the ith bound variable. -/
@@ -171,12 +175,14 @@ def openRec_tm (x : ℕ) (s : Term Var) : Term Var → Term Var
 | inr t₂ => inr (openRec_tm x s t₂)
 | case t₁ t₂ t₃ => case (openRec_tm x s t₁) (openRec_tm (x + 1) s t₂) (openRec_tm (x + 1) s t₃)
 
+@[inherit_doc]
 scoped notation:68 t "⟦" x " ↝ " s "⟧ᵗᵗ"=> openRec_tm x s t
 
 /-- Variable opening (term opening to term) of the closest binding. -/
 @[scoped grind =]
 def open_tm (t₁ t₂ : Term Var) := openRec_tm 0 t₂ t₁
 
+@[inherit_doc]
 scoped infixr:80 " ^ᵗᵗ " => open_tm
 
 /-- Locally closed terms. -/
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -36,6 +36,7 @@ inductive Ty (Base : Type v)
   /-- A function type. -/
   | arrow : Ty Base → Ty Base → Ty Base
 
+@[inherit_doc]
 scoped infixr:70 " ⤳ " => Ty.arrow
 
 open Ty Context
@@ -51,6 +52,7 @@ inductive Typing : Context Var (Ty Base) → Term Var → Ty Base → Prop
 
 attribute [scoped grind .] Typing.var Typing.app
 
+@[inherit_doc]
 scoped notation:50 Γ " ⊢ " t " ∶ " τ:arg => Typing Γ t τ
 
 namespace Typing
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
@@ -31,6 +31,7 @@ open Untyped Typing
 
 variable {Var : Type u} {Base : Type v} {R : Term Var → Term Var → Prop}
 
+/-- A relation on terms preserves typing if all related terms have the same type. -/
 def PreservesTyping (R : Term Var → Term Var → Prop) (Base : Type v) :=
   ∀ {Γ t t'} {τ : Ty Base}, Γ ⊢ t ∶ τ → R t t' → Γ ⊢ t' ∶ τ
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean
diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean
diff --git a/Cslib/Logics/LinearLogic/CLL/CutElimination.lean b/Cslib/Logics/LinearLogic/CLL/CutElimination.lean
diff --git a/Cslib/Logics/LinearLogic/CLL/MProof.lean b/Cslib/Logics/LinearLogic/CLL/MProof.lean
diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean
diff --git a/CslibTests.lean b/CslibTests.lean
diff --git a/CslibTests/Lint.lean b/CslibTests/Lint.lean
diff --git a/lakefile.toml b/lakefile.toml
diff --git a/scripts/nolints.json b/scripts/nolints.json
