From fbf096510d09468dea406d712cc374828b57c135 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Aug 2025 20:38:47 -0700 Subject: [PATCH] chore: minimize number of public imports in `grind` (#10180) --- src/Lean/Meta/Tactic/Grind/AC/Proof.lean | 1 + src/Lean/Meta/Tactic/Grind/AC/Util.lean | 1 + .../Tactic/Grind/Arith/CommRing/EqCnstr.lean | 15 +++++++------- .../Grind/Arith/CommRing/Internalize.lean | 9 +++------ .../Meta/Tactic/Grind/Arith/CommRing/Inv.lean | 6 ++---- .../Tactic/Grind/Arith/CommRing/Poly.lean | 2 -- .../Tactic/Grind/Arith/CommRing/Proof.lean | 15 +++++++------- .../Tactic/Grind/Arith/CommRing/Reify.lean | 4 +--- .../Tactic/Grind/Arith/CommRing/RingId.lean | 14 ++++++------- .../Tactic/Grind/Arith/CommRing/RingM.lean | 2 +- .../Tactic/Grind/Arith/CommRing/SafePoly.lean | 1 + .../Grind/Arith/CommRing/SemiringM.lean | 4 ++-- .../Tactic/Grind/Arith/CommRing/Types.lean | 6 ++---- .../Tactic/Grind/Arith/Cutsat/CommRing.lean | 15 +++++++------- .../Tactic/Grind/Arith/Cutsat/DvdCnstr.lean | 4 ++-- .../Tactic/Grind/Arith/Cutsat/EqCnstr.lean | 18 ++++++++++------- .../Meta/Tactic/Grind/Arith/Cutsat/Inv.lean | 8 +++----- .../Tactic/Grind/Arith/Cutsat/LeCnstr.lean | 19 ++++++++---------- .../Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean | 8 ++++---- .../Meta/Tactic/Grind/Arith/Cutsat/Model.lean | 7 ++----- .../Meta/Tactic/Grind/Arith/Cutsat/Nat.lean | 11 +++++----- .../Meta/Tactic/Grind/Arith/Cutsat/Norm.lean | 3 --- .../Meta/Tactic/Grind/Arith/Cutsat/Proof.lean | 4 ++++ .../Grind/Arith/Cutsat/ReorderVars.lean | 11 +++++----- .../Tactic/Grind/Arith/Cutsat/Search.lean | 20 +++++++++---------- .../Tactic/Grind/Arith/Cutsat/SearchM.lean | 6 ++---- .../Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean | 13 ++++++------ .../Tactic/Grind/Arith/Cutsat/ToIntInfo.lean | 4 +--- .../Meta/Tactic/Grind/Arith/Cutsat/Types.lean | 9 +++------ .../Meta/Tactic/Grind/Arith/Cutsat/Util.lean | 6 ++---- .../Meta/Tactic/Grind/Arith/Cutsat/Var.lean | 14 ++++++------- .../Tactic/Grind/Arith/Linear/StructId.lean | 1 + 32 files changed, 118 insertions(+), 143 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/AC/Proof.lean b/src/Lean/Meta/Tactic/Grind/AC/Proof.lean index d2962d88f2..b325eee223 100644 --- a/src/Lean/Meta/Tactic/Grind/AC/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/AC/Proof.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura module prelude public import Lean.Meta.Tactic.Grind.AC.Util +import Lean.Data.RArray import Lean.Meta.Tactic.Grind.Diseq import Lean.Meta.Tactic.Grind.ProofUtil import Lean.Meta.Tactic.Grind.AC.ToExpr diff --git a/src/Lean/Meta/Tactic/Grind/AC/Util.lean b/src/Lean/Meta/Tactic/Grind/AC/Util.lean index 49131bd170..224b62823c 100644 --- a/src/Lean/Meta/Tactic/Grind/AC/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/AC/Util.lean @@ -9,6 +9,7 @@ public import Lean.Meta.Tactic.Grind.Types public import Lean.Meta.Tactic.Grind.ProveEq public import Lean.Meta.Tactic.Grind.SynthInstance public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId +import Lean.Meta.Tactic.Grind.Simp public section namespace Lean.Meta.Grind.AC open Lean.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean index 2bf9e59b5c..efe4fd1243 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean @@ -4,18 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude -public import Lean.Meta.Tactic.Grind.ProveEq public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId -public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof -public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr -public import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv -public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify +import Lean.Meta.Tactic.Grind.ProveEq +import Lean.Meta.Tactic.Grind.Diseq +import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof +import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr +import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv +import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify +import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions - public section - namespace Lean.Meta.Grind.Arith.CommRing /-- Returns `some ringId` if `a` and `b` are elements of the same ring. -/ private def inSameRing? (a b : Expr) : GoalM (Option Nat) := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean index 8af4a4484f..9a7911431f 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.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 Lean.Meta.Tactic.Grind.Simp public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId -public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify -public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr +import Lean.Meta.Tactic.Grind.Simp +import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify +import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions - public section - namespace Lean.Meta.Grind.Arith.CommRing /-- If `e` is a function application supported by the `CommRing` module, return its type. -/ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean index 4d810066db..80eecd6ea0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.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.Grind.Arith.CommRing.RingM -public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly - +import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly +import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet public section - namespace Lean.Meta.Grind.Arith.CommRing private def checkVars : RingM Unit := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean index da4f18cd38..a7e2056ebd 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean @@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Init.Grind.Ring.Poly - public section namespace Lean.Grind.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean index a7747f0fb4..73d4824ca1 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean @@ -5,15 +5,16 @@ Authors: Leonardo de Moura -/ module prelude -public import Init.Grind.Ring.OfSemiring -public import Lean.Meta.Tactic.Grind.Diseq -public import Lean.Meta.Tactic.Grind.ProofUtil public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId -public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr -public import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly -public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM -public import Lean.Meta.Tactic.Grind.VarRename +import Init.Grind.Ring.OfSemiring +import Lean.Data.RArray +import Lean.Meta.Tactic.Grind.Diseq +import Lean.Meta.Tactic.Grind.ProofUtil +import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr +import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly +import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr +import Lean.Meta.Tactic.Grind.VarRename import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions public section diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean index 53b6756d95..1f7c9a3bd0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean @@ -4,14 +4,12 @@ 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.CommRing.RingM public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM +import Lean.Meta.Tactic.Grind.Simp import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions public section - namespace Lean.Meta.Grind.Arith.CommRing def isAddInst (inst : Expr) : RingM Bool := diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean index 942ae05db8..972035c79f 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean @@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude -public import Init.Grind.Ring.Field -public import Init.Grind.Ring.Envelope -public import Lean.Meta.Tactic.Grind.Simp -public import Lean.Meta.Tactic.Grind.SynthInstance -public import Lean.Meta.Tactic.Grind.Arith.Insts public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM - +import Init.Grind.Ring.Field +import Init.Grind.Ring.Envelope +import Lean.Meta.Tactic.Grind.Simp +import Lean.Meta.Tactic.Grind.SynthInstance +import Lean.Meta.Tactic.Grind.Arith.Insts +import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet public section - namespace Lean.Meta.Grind.Arith.CommRing /-- diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean index 3a4310a702..735a750651 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean @@ -8,7 +8,7 @@ prelude public import Lean.Meta.Tactic.Grind.Types public import Lean.Meta.Tactic.Grind.SynthInstance public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing -public import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet +import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly public section diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean index 6e125fc316..4fbfad2c24 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura module prelude public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM +public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly public section namespace Lean.Meta.Grind.Arith.CommRing /-! diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean index 99a2568c9f..899b04f7c1 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean @@ -5,12 +5,12 @@ Authors: Leonardo de Moura -/ module prelude -public import Init.Grind.Ring.OfSemiring public import Lean.Meta.Tactic.Grind.Types public import Lean.Meta.Tactic.Grind.SynthInstance public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing public import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet -public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr +import Init.Grind.Ring.OfSemiring +import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions public section namespace Lean.Meta.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean index 462d54ecbe..b8eb8f9b70 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean @@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Init.Grind.Ring.OfSemiring -public import Lean.Data.PersistentArray public import Lean.Meta.Tactic.Grind.ExprPtr public import Lean.Meta.Tactic.Grind.Arith.Util -public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly - +import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly +import Lean.Data.PersistentArray public section namespace Lean.Meta.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean index 4c7e9c1ed7..2e2d25896c 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean @@ -4,22 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude -public import Lean.Meta.Tactic.Grind.ProveEq public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId -public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify -public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr -import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions +import Lean.Meta.Tactic.Grind.ProveEq +import Lean.Meta.Tactic.Grind.Simp +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var +import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions +import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify +import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr public section - +namespace Lean.Meta.Grind.Arith.Cutsat /-! CommRing interface for cutsat. We use it to normalize nonlinear polynomials. -/ -namespace Lean.Meta.Grind.Arith.Cutsat - /-- Returns `true` if `p` contains a nonlinear monomial. -/ def _root_.Int.Linear.Poly.isNonlinear (p : Poly) : GoalM Bool := do let .add _ x p := p | return false diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean index a135a83ba0..9d1b8b2be6 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean @@ -7,16 +7,16 @@ module prelude public import Lean.Meta.Tactic.Grind.Types import Lean.Meta.Tactic.Simp.Arith.Int +import Lean.Meta.Tactic.Grind.Simp import Lean.Meta.Tactic.Grind.PropagatorAttr import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat 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 - namespace Lean.Meta.Grind.Arith.Cutsat def DvdCnstr.norm (c : DvdCnstr) : DvdCnstr := diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean index 98d4b49843..9e7fed6d46 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean @@ -5,15 +5,19 @@ Authors: Leonardo de Moura -/ module prelude -public import Lean.Meta.Tactic.Grind.Simp -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var -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 +public import Lean.Meta.Tactic.Grind.Types +import Init.Data.Int.OfNat +import Lean.Meta.Tactic.Grind.Simp +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var +import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat +import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt +import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm import Lean.Meta.NatInstTesters public section - namespace Lean.Meta.Grind.Arith.Cutsat private def _root_.Int.Linear.Poly.substVar (p : Poly) : GoalM (Option (Var × EqCnstr × Poly)) := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.lean index 408309d84c..08bd9fe606 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.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.Grind.Arith.Cutsat.Util -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var - +public import Lean.Meta.Tactic.Grind.Types +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var public section - namespace Int.Linear /-- Returns `true` if all coefficients are not `0`. -/ def Poly.checkCoeffs : Poly → Bool diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean index 069e6f39d7..ca4266309f 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean @@ -4,20 +4,17 @@ 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.Int -public import Lean.Meta.Tactic.Grind.PropagatorAttr -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing - +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util +import Lean.Meta.Tactic.Simp.Arith.Int +import Lean.Meta.Tactic.Grind.PropagatorAttr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm +import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing public section - namespace Lean.Meta.Grind.Arith.Cutsat def LeCnstr.norm (c : LeCnstr) : LeCnstr := diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean index a48b09c79d..13f18548ec 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean @@ -5,11 +5,11 @@ Authors: Leonardo de Moura -/ module prelude -public import Lean.Meta.Tactic.Grind.MBTC -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model - +public import Lean.Meta.Tactic.Grind.Types +import Lean.Meta.Tactic.Grind.MBTC +import Lean.Meta.Tactic.Grind.Arith.ModelUtil +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model public section - namespace Lean.Meta.Grind.Arith.Cutsat private def getAssignmentExt? (e : Expr) : GoalM (Option Rat) := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean index 6ba2c96e9b..2113402051 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean @@ -4,14 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude -public import Init.Grind.ToInt public import Lean.Meta.Tactic.Grind.Types -public import Lean.Meta.Tactic.Grind.Arith.ModelUtil - +import Init.Grind.ToInt +import Lean.Meta.Tactic.Grind.Arith.ModelUtil public section - namespace Lean.Meta.Grind.Arith.Cutsat private def isIntNatENode (n : ENode) : MetaM Bool := diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean index 940c5921dc..2172299435 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean @@ -5,11 +5,12 @@ 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 +public import Lean.Meta.Tactic.Grind.Types +import Init.Data.Int.OfNat +import Lean.Meta.Tactic.Grind.Simp +import Lean.Meta.Tactic.Simp.Arith.Nat.Basic +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm +import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt import Lean.Meta.NatInstTesters public section namespace Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean index 8b04b01186..7aed742667 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean @@ -4,13 +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.Arith.Cutsat.Util import Lean.Meta.IntInstTesters - public section - namespace Lean.Meta.Grind.Arith.Cutsat /-! `Int` expressions are normalized by the `grind` preprocessor, but we diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean index c03ef11ae3..f84d00d343 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean @@ -7,9 +7,13 @@ module prelude public import Init.Grind.Ring.Poly public import Lean.Meta.Tactic.Grind.Types +import Init.Data.Int.OfNat +import Lean.Data.RArray import Lean.Meta.Tactic.Grind.Diseq import Lean.Meta.Tactic.Grind.ProofUtil import Lean.Meta.Tactic.Grind.VarRename +import Lean.Meta.Tactic.Simp.Arith.Int.Basic +import Lean.Meta.Tactic.Simp.Arith.Int.Simp import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ReorderVars.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ReorderVars.lean index 159ea06a0e..1ba9b63140 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ReorderVars.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ReorderVars.lean @@ -4,15 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv - +public import Lean.Meta.Tactic.Grind.Types +import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv public section - namespace Lean.Meta.Grind.Arith.Cutsat - /-! Collect variable information -/ structure VarInfo where diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean index 1da2e5660a..7bc523c130 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean @@ -4,19 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util -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.EqCnstr +public import Lean.Meta.Tactic.Grind.Types public import Lean.Meta.Tactic.Grind.Arith.Cutsat.SearchM -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars - +import Lean.Meta.Tactic.Simp.Arith.Int.Simp +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util +import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model +import Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof public section - namespace Lean.Meta.Grind.Arith.Cutsat /-- Asserts constraints implied by a `CooperSplit`. -/ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean index 543c824a3a..0650d87995 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean @@ -4,12 +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.Arith.Cutsat.Util - +public import Lean.Meta.Tactic.Grind.Types +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util public section - namespace Lean.Meta.Grind.Arith.Cutsat /-- In principle, we only need to support two kinds of case split. diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean index 1ff9d081e8..b27b88a04f 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean @@ -4,16 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude -public import Init.Grind.ToIntLemmas -public import Lean.Meta.Tactic.Grind.SynthInstance -public import Lean.Meta.Tactic.Grind.Simp +public import Lean.Meta.Tactic.Grind.Types public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util -public import Lean.Meta.Tactic.Grind.Arith.EvalNum -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm +import Init.Grind.ToIntLemmas +import Lean.Meta.Tactic.Grind.SynthInstance +import Lean.Meta.Tactic.Grind.Simp +import Lean.Meta.Tactic.Grind.Arith.EvalNum +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm public section - namespace Lean.Meta.Grind.Arith.Cutsat private def reportMissingToIntAdapter (type : Expr) (instType : Expr) : MetaM Unit := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean index b56d928975..924139c282 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean @@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude -public import Init.Grind.ToInt public import Lean.Meta.Tactic.Grind.Arith.Util - +import Init.Grind.ToInt public section namespace Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean index 35eaef4e8a..4e108b3fe6 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.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 Init.Data.Int.Linear -public import Lean.Data.PersistentArray -public import Lean.Meta.Tactic.Grind.ExprPtr -public import Lean.Meta.Tactic.Grind.Arith.Util public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types - +import Lean.Data.PersistentArray +import Lean.Meta.Tactic.Grind.ExprPtr +import Lean.Meta.Tactic.Grind.Arith.Util public section - namespace Lean.Meta.Grind.Arith.Cutsat export Int.Linear (Var Poly) diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean index 75b88d3d36..ee054a5ddb 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean @@ -4,15 +4,13 @@ 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 -public import Lean.Meta.Tactic.Grind.Arith.Util +import Lean.Meta.Tactic.Grind.Arith.Util import Lean.Meta.Tactic.Simp.Arith.Int.Simp - public section - namespace Int.Linear + def Poly.isZero : Poly → Bool | .num 0 => true | _ => false diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean index 7d7b7f388f..4662755f4f 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.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 Lean.Meta.IntInstTesters -public import Lean.Meta.Tactic.Grind.Simp -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat -public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt - +public import Lean.Meta.Tactic.Grind.Types +import Lean.Meta.IntInstTesters +import Lean.Meta.Tactic.Grind.Simp +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat +import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt public section - namespace Lean.Meta.Grind.Arith.Cutsat @[extern "lean_cutsat_propagate_nonlinear"] diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean index 66f7bf3d13..92d4a0f159 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean @@ -14,6 +14,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM public import Lean.Meta.Tactic.Grind.Arith.Linear.Util public import Lean.Meta.Tactic.Grind.Arith.Linear.Var +import Lean.Meta.Tactic.Grind.Arith.Insts public section