leanprover · kim-em · Sep 16, 2025 · Oct 14, 2025 · Oct 14, 2025 · Oct 17, 2025
@@ -18,3 +18,6 @@ jobs:
         with:
           build-args: "--wfail"
           mk_all-check: "true"
+      - run: |
+          set -e
+          lake exe shake Cslib
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Computability.Languages.Language
+import Cslib.Init
+import Mathlib.Computability.Language
 
 namespace Cslib.Automata
 

@@ -6,7 +6,6 @@ Authors: Fabrizio Montesi, Ching-Tsun Chou
 
 import Cslib.Computability.Automata.Acceptor
 import Cslib.Computability.Automata.OmegaAcceptor
-import Cslib.Foundations.Data.OmegaSequence.InfOcc
 import Cslib.Foundations.Semantics.LTS.FLTS
 
 /-! # Deterministic Automata

@@ -5,7 +5,6 @@ Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
 import Cslib.Computability.Automata.NA
-import Cslib.Computability.Automata.Acceptor
 
 /-! # Nondeterministic automata with ε-transitions. -/
 

@@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
-import Cslib.Foundations.Data.OmegaSequence.InfOcc
-import Cslib.Foundations.Semantics.LTS.Basic
 import Cslib.Computability.Automata.Acceptor
 import Cslib.Computability.Automata.OmegaAcceptor
+import Cslib.Foundations.Semantics.LTS.Basic
 
 /-! # Nondeterministic Automaton
 

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
-import Mathlib.Computability.Language
-import Mathlib.Tactic
 import Cslib.Init
+import Mathlib.Computability.Language
 
 /-!
 # Language (additional definitions and theorems)

@@ -8,7 +8,6 @@ import Cslib.Computability.Languages.Language
 import Cslib.Foundations.Data.OmegaSequence.Flatten
 import Mathlib.Computability.Language
 import Mathlib.Order.Filter.AtTopBot.Defs
-import Mathlib.Tactic
 
 /-!
 # ωLanguage

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.DABuchi
-import Cslib.Computability.Languages.ExampleEventuallyZero
-import Cslib.Computability.Languages.RegularLanguage
+import Cslib.Computability.Automata.DA
+import Cslib.Computability.Automata.NA
 
 /-!
 # ω-Regular languages

@@ -7,9 +7,9 @@ Authors: Ching-Tsun Chou
 import Cslib.Computability.Automata.DAToNA
 import Cslib.Computability.Automata.NAToDA
 import Cslib.Computability.Automata.Prod
-import Cslib.Computability.Automata.Acceptor
 import Mathlib.Computability.DFA
-import Mathlib.Tactic
+import Mathlib.Data.Set.Card
+import Mathlib.Tactic.Common
 
 /-!
 # Regular languages

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tanner Duve, Eric Wieser
 -/
 import Cslib.Init
-import Mathlib.Tactic.Lemma
-import Mathlib.Tactic.SimpRw
 
 /-!
 # Free Monad

@@ -3,9 +3,8 @@ Copyright (c) 2025 Tanner Duve. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tanner Duve
 -/
-import Mathlib.Control.Monad.Cont
 import Cslib.Foundations.Control.Monad.Free
-import Mathlib.Control.Monad.Writer
+import Mathlib.Control.Monad.Cont
 
 /-!
 # Free Monad

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Xueying Qin
 -/
 
--- TODO: Notation conflict with Mathlib.Finsupp (both use →₀)
--- import Cslib.Init
-import Mathlib.Data.Finset.Basic
+import Cslib.Init
+import Mathlib.Data.Finset.Filter
+import Mathlib.Data.Finset.Lattice.Basic
 
 /-! # Finite functions
 
@@ -126,7 +126,8 @@ theorem fromFun_inter [Zero β] [DecidableEq α]
 @[scoped grind =]
 theorem fromFun_comm [Zero β] [DecidableEq α]
     [∀ y : β, Decidable (y = 0)] {f : α → β} {support1 support2 : Finset α} :
-    (f ↾₀ support1) ↾₀ support2 = (f ↾₀ support2) ↾₀ support1 := by grind
+    (f ↾₀ support1) ↾₀ support2 = (f ↾₀ support2) ↾₀ support1 := by
+  grind only [= coe_eq_fn, = fromFun_fn, ←= ext]
 
 end FinFun
 

@@ -5,14 +5,7 @@ Authors: Fabrizio Montesi, Kenny Lau
 -/
 
 import Cslib.Init
-import Mathlib.Algebra.Field.Rat
-import Mathlib.Algebra.Ring.CharZero
-import Mathlib.Algebra.Ring.Int.Defs
-import Mathlib.Data.Finset.Max
-import Mathlib.Data.Finset.Preimage
-import Mathlib.Data.Fintype.EquivFin
-import Mathlib.Data.Nat.SuccPred
-import Mathlib.Order.SuccPred.WithBot
+import Mathlib.Analysis.Normed.Field.Lemmas
 
 universe u
 

@@ -7,7 +7,6 @@ Authors: Ching-Tsun Chou
 import Cslib.Init
 import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Data.Nat.Nth
-import Mathlib.Tactic
 
 open Function Set
 
@@ -196,21 +195,20 @@ theorem segment'_eq_segment (hm : StrictMono f) :
   classical
   ext k ; unfold segment'
   rcases (show k < f 0 ∨ k ≥ f 0 by omega) with h_k | h_k
-  · have : k - f 0 = 0 := by grind
-    grind
-  unfold segment; congr 1
+  · grind
+  unfold segment ; congr 1
   simp only [count_eq_card_filter_range]
   suffices h : ∃ g, BijOn g
       ({x ∈ Finset.range (k - f 0 + 1) | x ∈ range fun x => f x - f 0})
       ({x ∈ Finset.range (k + 1) | x ∈ range f}) by
     grind [BijOn.finsetCard_eq, Finset.coe_filter]
   refine ⟨fun n ↦ n + f 0, ?_, ?_, ?_⟩
-  · intro n; simp only [mem_range, Finset.mem_range, mem_setOf_eq]
+  · intro n ; simp only [mem_range, Finset.mem_range, mem_setOf_eq]
     rintro ⟨h_n, i, rfl⟩
     have := StrictMono.monotone hm <| zero_le i
     refine ⟨?_, i, ?_⟩ <;> omega
   · grind [injOn_of_injective, Injective]
-  · intro n; simp only [mem_range, Finset.mem_range, mem_setOf_eq, mem_image]
+  · intro n ; simp only [mem_range, Finset.mem_range, mem_setOf_eq, mem_image]
     rintro ⟨h_n, i, rfl⟩
     have := StrictMono.monotone hm <| zero_le i
     grind

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou, Fabrizio Montesi
 -/
 import Cslib.Init
-import Mathlib.Data.FunLike.Basic
-import Mathlib.Logic.Function.Iterate
+import Mathlib.Order.Filter.AtTopBot.Defs
 
 /-!
 # Definition of `ωSequence` and functions on infinite sequences

@@ -6,7 +6,6 @@ Authors: Ching-Tsun Chou
 
 import Cslib.Foundations.Data.Nat.Segment
 import Cslib.Foundations.Data.OmegaSequence.Init
-import Mathlib.Tactic
 
 /-!
 # Flattening an infinite sequence of lists

@@ -5,6 +5,8 @@ Authors: Ching-Tsun Chou
 -/
 
 import Cslib.Foundations.Data.OmegaSequence.Defs
+import Mathlib.Order.Filter.AtTopBot.Basic
+import Mathlib.Order.Filter.Cofinite
 
 /-!
 # Infinite occurrences

@@ -3,11 +3,11 @@ Copyright (c) 2025 Ching-Tsun Chou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou, Fabrizio Montesi
 -/
+
 import Cslib.Foundations.Data.OmegaSequence.Defs
-import Mathlib.Logic.Function.Basic
-import Mathlib.Data.List.OfFn
-import Mathlib.Data.Nat.Basic
-import Mathlib.Tactic
+import Mathlib.Algebra.Order.Ring.Nat
+import Mathlib.Algebra.Order.Sub.Basic
+import Mathlib.Data.Nat.Lattice
 
 /-!
 # ω-sequences a.k.a. infinite sequences

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Mathlib
+import Batteries.Tactic.Lint.Basic
+import Lean.Meta.GlobalInstances
 
 namespace Cslib.Lint
 

@@ -5,14 +5,9 @@ Authors: Fabrizio Montesi
 -/
 
 import Cslib.Init
-import Mathlib.Tactic.Lemma
-import Mathlib.Data.Finite.Defs
-import Mathlib.Data.Fintype.Basic
-import Mathlib.Logic.Function.Defs
 import Mathlib.Data.Set.Finite.Basic
 import Mathlib.Data.Stream.Defs
-import Mathlib.Util.Notation3
-import Mathlib.Order.SetNotation
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
 
 /-!
 # Labelled Transition System (LTS)

@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.LTS.Basic
-import Cslib.Foundations.Semantics.LTS.TraceEq
 import Cslib.Foundations.Data.Relation
 import Cslib.Foundations.Semantics.LTS.Simulation
-import Mathlib.Order.CompleteLattice.Defs
+import Cslib.Foundations.Semantics.LTS.TraceEq
 
 /-! # Bisimulation and Bisimilarity
 

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.LTS.FLTS
 import Cslib.Foundations.Semantics.LTS.Basic
+import Cslib.Foundations.Semantics.LTS.FLTS
 
 variable {State : Type _} {Label : Type _}
 

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.LTS.FLTS
 import Cslib.Foundations.Semantics.LTS.Basic
+import Cslib.Foundations.Semantics.LTS.FLTS
 
 variable {State : Type _} {Label : Type _}
 

@@ -5,7 +5,6 @@ Authors: Fabrizio Montesi
 -/
 
 import Cslib.Foundations.Semantics.LTS.Basic
-import Cslib.Foundations.Data.Relation
 
 /-! # Simulation and Similarity
 

@@ -5,7 +5,6 @@ Authors: Fabrizio Montesi
 -/
 
 import Cslib.Foundations.Semantics.LTS.Basic
-import Mathlib.Data.Set.Finite.Basic
 
 /-!
 # Trace Equivalence

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jesse Alama
 -/
 
-import Mathlib.Init
 import Cslib.Foundations.Lint.Basic
+import Mathlib.Init
+import Mathlib.Tactic.Common
 
 /-!
 # CSLib Initialization

@@ -5,7 +5,6 @@ Authors: Fabrizio Montesi
 -/
 
 import Cslib.Init
-import Mathlib.Init
 
 /-! # Calculus of Communicating Systems (CCS)
 

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.LTS.Basic
 import Cslib.Foundations.Semantics.LTS.Bisimulation
-import Cslib.Languages.CCS.Basic
 import Cslib.Languages.CCS.Semantics
 
 /-! # Behavioural theory of CCS

@@ -3,8 +3,9 @@ Copyright (c) 2025 Thomas Waring. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring
 -/
-import Cslib.Languages.CombinatoryLogic.Defs
+
 import Cslib.Foundations.Data.Relation
+import Cslib.Languages.CombinatoryLogic.Defs
 
 /-!
 # SKI reduction is confluent

@@ -3,9 +3,8 @@ Copyright (c) 2025 Thomas Waring. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring
 -/
-import Mathlib.Logic.Relation
+
 import Cslib.Foundations.Semantics.ReductionSystem.Basic
-import Cslib.Foundations.Data.Relation
 
 /-!
 # SKI Combinatory Logic

@@ -3,11 +3,9 @@ Copyright (c) 2025 Thomas Waring. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring
 -/
-import Cslib.Languages.CombinatoryLogic.Defs
-import Cslib.Languages.CombinatoryLogic.Basic
+
 import Cslib.Languages.CombinatoryLogic.Confluence
 import Cslib.Languages.CombinatoryLogic.Recursion
-import Mathlib.Tactic.Common
 
 /-!
 # Evaluation results

@@ -3,7 +3,7 @@ Copyright (c) 2025 Thomas Waring. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring
 -/
-import Cslib.Languages.CombinatoryLogic.Defs
+
 import Cslib.Languages.CombinatoryLogic.Basic
 
 /-!

@@ -5,7 +5,6 @@ Authors: Chris Henson
 -/
 
 import Cslib.Foundations.Syntax.HasWellFormed
-import Mathlib.Data.Finset.Defs
 import Mathlib.Data.Finset.Dedup
 import Mathlib.Data.List.Sigma
 

@@ -5,7 +5,6 @@ Authors: Chris Henson
 -/
 
 import Cslib.Foundations.Data.HasFresh
-import Cslib.Foundations.Syntax.HasSubstitution
 import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
 
 /-! # λ-calculus

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
+import Cslib.Foundations.Syntax.HasSubstitution
 import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
 
-
 /-! # λ-calculus
 
 The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax.
-Original file line number
+Diff line change
@@ Expand Up / @@ -5,7 +5,6 @@ Authors: Fabrizio Montesi, Ching-Tsun Chou @@
     -/
     import Cslib.Computability.Automata.NA
-    import Cslib.Computability.Automata.Acceptor
     /-! # Nondeterministic automata with ε-transitions. -/
@@ Expand Down @@