From 1feac1ae92ee49110a346773f1ff40bb1bb4dc7c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Aug 2025 23:34:44 -0700 Subject: [PATCH] chore: simplify `grind` import graph (#10128) --- src/Lean/Meta/Offset.lean | 9 +++------ src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean | 1 + src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean | 3 +-- src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean | 4 +--- src/Lean/Meta/Tactic/Grind/Arith/EvalNum.lean | 3 +-- src/Lean/Meta/Tactic/Grind/Canon.lean | 4 +--- src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean | 11 ++++------- src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean | 4 +--- 8 files changed, 13 insertions(+), 26 deletions(-) diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean index dadaa4f37a..46ae60c8cd 100644 --- a/src/Lean/Meta/Offset.lean +++ b/src/Lean/Meta/Offset.lean @@ -4,16 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Init.Control.Option public import Lean.Data.LBool -public import Lean.Meta.InferType -public import Lean.Meta.NatInstTesters -public import Lean.Util.SafeExponentiation - +public import Lean.Meta.Basic +import Lean.Meta.NatInstTesters +import Lean.Util.SafeExponentiation public section - namespace Lean.Meta private abbrev withInstantiatedMVars (e : Expr) (k : Expr → OptionT MetaM α) : OptionT MetaM α := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean index 46ad56be7b..a135a83ba0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean @@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing +import Lean.Meta.NatInstTesters public section diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean index 148b3f122a..98d4b49843 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Lean.Meta.Tactic.Grind.Simp public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var @@ -12,7 +11,7 @@ public import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr public import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt public import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing - +import Lean.Meta.NatInstTesters public section namespace Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean index 4ae2363f61..940c5921dc 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean @@ -4,16 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Init.Data.Int.OfNat public import Lean.Meta.Tactic.Grind.Simp public import Lean.Meta.Tactic.Simp.Arith.Nat.Basic public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt - +import Lean.Meta.NatInstTesters public section - namespace Lean.Meta.Grind.Arith.Cutsat /-- Given `e`, returns `(NatCast.natCast e, rfl)` -/ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/EvalNum.lean b/src/Lean/Meta/Tactic/Grind/Arith/EvalNum.lean index 378d0abcd7..116809eb99 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/EvalNum.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/EvalNum.lean @@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Lean.Meta.Tactic.Grind.Types import Lean.Meta.IntInstTesters - +import Lean.Meta.NatInstTesters public section namespace Lean.Meta.Grind.Arith diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean index 3e5833f493..e397605666 100644 --- a/src/Lean/Meta/Tactic/Grind/Canon.lean +++ b/src/Lean/Meta/Tactic/Grind/Canon.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Init.Grind.Util public import Lean.Meta.Basic @@ -14,9 +13,8 @@ public import Lean.Util.PtrSet public import Lean.Util.FVarSubset public import Lean.Meta.Tactic.Grind.Types import Lean.Meta.IntInstTesters - +import Lean.Meta.NatInstTesters public section - namespace Lean.Meta.Grind namespace Canon diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean b/src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean index 2dd6bab6af..4f37bdbf4b 100644 --- a/src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean +++ b/src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean @@ -4,17 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Lean.Util.SortExprs -public import Lean.Meta.Check -public import Lean.Meta.Offset -public import Lean.Meta.AppBuilder public import Lean.Meta.KExprMap -public import Lean.Data.RArray - +import Lean.Meta.Offset +import Lean.Data.RArray +import Lean.Meta.AppBuilder +import Lean.Meta.NatInstTesters public section - namespace Nat.Linear /-- Applies the given variable permutation to `e` -/ diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean b/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean index f74ec6614f..5abcc90aff 100644 --- a/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean +++ b/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean @@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Lean.Meta.Tactic.Simp.Arith.Util public import Lean.Meta.Tactic.Simp.Arith.Nat.Basic - +import Lean.Meta.AppBuilder public section - namespace Lean.Meta.Simp.Arith.Nat def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do