chore: fix test to reflect recent changes

The goal is to match the new behavior for `Poly.norm`

src/Init/Data/Int/Linear.lean

@@ -87,7 +87,7 @@ def Poly.insert (k : Int) (v : Var) (p : Poly) : Poly :=
   match p with
   | .num k' => .add k v (.num k')
   | .add k' v' p =>
-    bif Nat.blt v v' then
+    bif Nat.blt v' v then
       .add k v <| .add k' v' p
     else bif Nat.beq v v' then
       if Int.add k k' == 0 then
@@ -333,7 +333,7 @@ theorem Poly.denote_insert (ctx : Context) (k : Int) (v : Var) (p : Poly) :
     (p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx := by
   induction p <;> simp [*]
   next k' v' p' ih =>
-    by_cases h₁ : Nat.blt v v' <;> simp [*]
+    by_cases h₁ : Nat.blt v' v <;> simp [*]
     by_cases h₂ : Nat.beq v v' <;> simp [*]
     by_cases h₃ : k + k' = 0 <;> simp [*, Nat.eq_of_beq_eq_true h₂]
     rw [← Int.add_mul]

src/Lean/Meta/Tactic.lean

@@ -27,7 +27,6 @@ import Lean.Meta.Tactic.TryThis
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Unfold
 import Lean.Meta.Tactic.Rename
-import Lean.Meta.Tactic.LinearArith
 import Lean.Meta.Tactic.AC
 import Lean.Meta.Tactic.Refl
 import Lean.Meta.Tactic.Congr

src/Lean/Meta/Tactic/Grind.lean

@@ -48,14 +48,6 @@ builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.split
 builtin_initialize registerTraceClass `grind.split.candidate
 builtin_initialize registerTraceClass `grind.split.resolved
-builtin_initialize registerTraceClass `grind.offset
-builtin_initialize registerTraceClass `grind.offset.dist
-builtin_initialize registerTraceClass `grind.offset.internalize
-builtin_initialize registerTraceClass `grind.offset.internalize.term (inherited := true)
-builtin_initialize registerTraceClass `grind.offset.propagate
-builtin_initialize registerTraceClass `grind.offset.eq
-builtin_initialize registerTraceClass `grind.offset.eq.to (inherited := true)
-builtin_initialize registerTraceClass `grind.offset.eq.from (inherited := true)
 builtin_initialize registerTraceClass `grind.beta
 
 /-! Trace options for `grind` developers -/
@@ -69,8 +61,6 @@ builtin_initialize registerTraceClass `grind.debug.final
 builtin_initialize registerTraceClass `grind.debug.forallPropagator
 builtin_initialize registerTraceClass `grind.debug.split
 builtin_initialize registerTraceClass `grind.debug.canon
-builtin_initialize registerTraceClass `grind.debug.offset
-builtin_initialize registerTraceClass `grind.debug.offset.proof
 builtin_initialize registerTraceClass `grind.debug.ematch.pattern
 builtin_initialize registerTraceClass `grind.debug.beta
 builtin_initialize registerTraceClass `grind.debug.internalize

src/Lean/Meta/Tactic/Grind/Arith.lean

@@ -6,5 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.Types
-import Lean.Meta.Tactic.Grind.Arith.Offset
 import Lean.Meta.Tactic.Grind.Arith.Main
+import Lean.Meta.Tactic.Grind.Arith.Offset
+import Lean.Meta.Tactic.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean

@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Util.Trace
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
+
+namespace Lean
+
+builtin_initialize registerTraceClass `grind.cutsat
+builtin_initialize registerTraceClass `grind.cutsat.internalize
+builtin_initialize registerTraceClass `grind.cutsat.internalize.term (inherited := true)
+
+end Lean

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+
+namespace Lean.Meta.Grind.Arith.Cutsat
+
+def checkDvdCnstrs : GoalM Unit := do
+  let s ← get'
+  assert! s.vars.size == s.dvdCnstrs.size
+  -- TODO: condition maximal variable
+
+def checkVars : GoalM Unit := do
+  let s ← get'
+  let mut num := 0
+  for ({ expr }, var) in s.varMap do
+    if h : var < s.vars.size then
+      let expr' := s.vars[var]
+      assert! isSameExpr expr expr'
+    else
+      unreachable!
+    num := num + 1
+  assert! s.vars.size == num
+
+def checkInvariants : GoalM Unit := do
+  checkVars
+  checkDvdCnstrs
+
+end Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.Int.Linear
+import Lean.Data.PersistentArray
+import Lean.Meta.Tactic.Grind.ENodeKey
+import Lean.Meta.Tactic.Grind.Arith.Util
+
+namespace Lean.Meta.Grind.Arith.Cutsat
+
+export Int.Linear (Var Poly RelCnstr DvdCnstr)
+
+mutual
+/-- A divisibility constraint and its justification/proof. -/
+structure DvdCnstrWithProof where
+  c : DvdCnstr
+  p : DvdCnstrProof
+
+inductive DvdCnstrProof where
+  | expr (h : Expr)
+  | solveCombine (c₁ c₂ : DvdCnstrWithProof) (α β : Int)
+  | solveElim (c₁ c₂ : DvdCnstrWithProof)
+end
+
+/-- State of the cutsat procedure. -/
+structure State where
+  /-- Mapping from variables to their denotations. -/
+  vars : PArray Expr := {}
+  /-- Mapping from `Expr` to a variable representing it. -/
+  varMap  : PHashMap ENodeKey Var := {}
+  /--
+  Mapping from variables to divisibility constraints. Recall that we keep the divisibility constraint in solved form.
+  Thus, we have at most one divisibility per variable. -/
+  dvdCnstrs : PArray (Option DvdCnstrWithProof) := {}
+  deriving Inhabited
+
+end Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind.Arith.Cutsat
+
+def get' : GoalM State := do
+  return (← get).arith.cutsat
+
+@[inline] def modify' (f : State → State) : GoalM Unit := do
+  modify fun s => { s with arith.cutsat := f s.arith.cutsat }
+
+end Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+
+namespace Lean.Meta.Grind.Arith.Cutsat
+
+/-- Creates a new variable in the cutsat module. -/
+def mkVar (expr : Expr) : GoalM Var := do
+  if let some var := (← get').varMap.find? { expr } then
+    return var
+  let var : Var := (← get').vars.size
+  trace[grind.cutsat.internalize.term] "{expr} ↦ #{var}"
+  modify' fun s => { s with
+    vars      := s.vars.push expr
+    varMap    := s.varMap.insert { expr } var
+    dvdCnstrs := s.dvdCnstrs.push none
+  }
+  return var
+
+end Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Inv.lean

@@ -5,10 +5,12 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Offset
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv
 
 namespace Lean.Meta.Grind.Arith
 
-def checkInvariants : GoalM Unit :=
+def checkInvariants : GoalM Unit := do
   Offset.checkInvariants
+  Cutsat.checkInvariants
 
 end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Offset.lean

@@ -8,3 +8,19 @@ import Lean.Meta.Tactic.Grind.Arith.Offset.Main
 import Lean.Meta.Tactic.Grind.Arith.Offset.Proof
 import Lean.Meta.Tactic.Grind.Arith.Offset.Util
 import Lean.Meta.Tactic.Grind.Arith.Offset.Types
+
+namespace Lean
+
+builtin_initialize registerTraceClass `grind.offset
+builtin_initialize registerTraceClass `grind.offset.dist
+builtin_initialize registerTraceClass `grind.offset.internalize
+builtin_initialize registerTraceClass `grind.offset.internalize.term (inherited := true)
+builtin_initialize registerTraceClass `grind.offset.propagate
+builtin_initialize registerTraceClass `grind.offset.eq
+builtin_initialize registerTraceClass `grind.offset.eq.to (inherited := true)
+builtin_initialize registerTraceClass `grind.offset.eq.from (inherited := true)
+
+builtin_initialize registerTraceClass `grind.debug.offset
+builtin_initialize registerTraceClass `grind.debug.offset.proof
+
+end Lean

src/Lean/Meta/Tactic/Grind/Arith/Types.lean

@@ -5,12 +5,14 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Offset.Types
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 
 namespace Lean.Meta.Grind.Arith
 
 /-- State for the arithmetic procedures. -/
 structure State where
   offset : Offset.State := {}
+  cutsat : Cutsat.State := {}
   deriving Inhabited
 
 end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/LinearArith.lean

@@ -1,10 +0,0 @@
-/-
-Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
--/
-prelude
-import Lean.Meta.Tactic.LinearArith.Solver
-import Lean.Meta.Tactic.LinearArith.Nat
-import Lean.Meta.Tactic.LinearArith.Main
-import Lean.Meta.Tactic.LinearArith.Simp

src/Lean/Meta/Tactic/LinearArith/Nat.lean

@@ -1,9 +0,0 @@
-/-
-Copyright (c) 2022 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.LinearArith.Nat.Basic
-import Lean.Meta.Tactic.LinearArith.Nat.Simp
-import Lean.Meta.Tactic.LinearArith.Nat.Solver

src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean

@@ -1,29 +0,0 @@
-/-
-Copyright (c) 2022 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.LinearArith.Solver
-import Lean.Meta.Tactic.LinearArith.Nat.Basic
-
-namespace Lean.Meta.Linear.Nat
-
-namespace Collect
-
-inductive LinearArith
-
-structure Cnstr where
-  cnstr : LinearArith
-  proof : Expr
-
-structure State where
-  cnstrs : Array Cnstr
-
-abbrev M := StateRefT State ToLinear.M
-
--- TODO
-
-end Collect
-
-end Lean.Meta.Linear.Nat

src/Lean/Meta/Tactic/LinearArith/Solver.lean

@@ -1,273 +0,0 @@
-/-
-Copyright (c) 2022 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Data.Ord
-import Init.Data.Array.DecidableEq
-import Std.Internal.Rat
-
-namespace Lean.Meta.Linear
-open Std.Internal
-
-structure Var where
-  id : Nat
-  deriving Inhabited, Ord, DecidableEq, Repr
-
-instance : LT Var where
-  lt a b := a.id < b.id
-
-instance (a b : Var) : Decidable (a < b) :=
-  inferInstanceAs (Decidable (a.id < b.id))
-
-structure Assignment where
-  val : Array Rat := #[]
-  deriving Inhabited
-
-abbrev Assignment.size (a : Assignment) : Nat :=
-  a.val.size
-
-abbrev Assignment.get? (a : Assignment) (x : Var) : Option Rat :=
-  if h : x.id < a.size then
-    some (a.val[x.id])
-  else
-    none
-
-abbrev Assignment.push (a : Assignment) (v : Rat) : Assignment :=
-  { a with val := a.val.push v }
-
-abbrev Assignment.shrink (a : Assignment) (newSize : Nat) : Assignment :=
-  { a with val := a.val.shrink newSize }
-
-structure Poly where
-  val : Array (Int × Var)
-  deriving Inhabited, Repr, DecidableEq
-
-abbrev Poly.size (e : Poly) : Nat :=
-  e.val.size
-
-abbrev Poly.getMaxVarCoeff (e : Poly) : Int :=
-  e.val.back!.1
-
-abbrev Poly.getMaxVar (e : Poly) : Var :=
-  e.val.back!.2
-
-abbrev Poly.get (e : Poly) (i : Fin e.size) : Int × Var :=
-  e.val[i]
-
-def Poly.scale (d : Int) (e : Poly) : Poly :=
-  { e with val := e.val.map fun (c, x) => (c*d, x) }
-
-def Poly.add (e₁ e₂ : Poly) : Poly :=
-  let rec go (i₁ i₂ : Nat) (r : Array (Int × Var)) : Poly :=
-    if h₁ : i₁ < e₁.size then
-      if h₂ : i₂ < e₂.size then
-        let (c₁, x₁) := e₁.get ⟨i₁, h₁⟩
-        let (c₂, x₂) := e₂.get ⟨i₂, h₂⟩
-        if x₁ = x₂ then
-           if c₁ + c₂ = 0 then
-             go (i₁+1) (i₂+1) r
-           else
-             go (i₁+1) (i₂+1) (r.push (c₁+c₂, x₁))
-        else if x₁ < x₂ then
-          go (i₁+1) i₂ (r.push (c₁, x₁))
-        else
-          go i₁ (i₂+1) (r.push (c₂, x₂))
-      else
-        go (i₁+1) i₂ (r.push (e₁.get ⟨i₁, h₁⟩))
-    else
-      if h₂ : i₂ < e₂.size then
-        go i₁ (i₂+1) (r.push (e₂.get ⟨i₂, h₂⟩))
-      else
-        { val := r }
-    termination_by (e₁.size - i₁, e₂.size - i₂)
-    decreasing_by all_goals decreasing_with decreasing_trivial_pre_omega
-  go 0 0 #[]
-
-def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
-  let rec go (i₁ i₂ : Nat) (r : Array (Int × Var)) : Poly :=
-    if h₁ : i₁ < e₁.size then
-      let (c₁, x₁) := e₁.get ⟨i₁, h₁⟩
-      if h₂ : i₂ < e₂.size then
-        let (c₂, x₂) := e₂.get ⟨i₂, h₂⟩
-        if x₁ = x₂ then
-           let c := c₁*d₁ + c₂*d₂
-           if c = 0 then
-             go (i₁+1) (i₂+1) r
-           else
-             go (i₁+1) (i₂+1) (r.push (c, x₁))
-        else if x₁ < x₂ then
-          go (i₁+1) i₂ (r.push (d₁*c₁, x₁))
-        else
-          go i₁ (i₂+1) (r.push (d₂*c₂, x₂))
-      else
-        go (i₁+1) i₂ (r.push (d₁*c₁, x₁))
-    else
-      if h₂ : i₂ < e₂.size then
-        let (c₂, x₂) := e₂.get ⟨i₂, h₂⟩
-        go i₁ (i₂+1) (r.push (d₂*c₂, x₂))
-      else
-        { val := r }
-    termination_by (e₁.size - i₁, e₂.size - i₂)
-    decreasing_by all_goals decreasing_with decreasing_trivial_pre_omega
-  go 0 0 #[]
-
-def Poly.eval? (e : Poly) (a : Assignment) : Option Rat := Id.run do
-  let mut r := 0
-  for (c, x) in e.val do
-    if let some v := a.get? x then
-      r := r + c*v
-    else
-      return none
-  return r
-
-structure AssumptionId where
-  id : Nat := 0
-  deriving Inhabited, DecidableEq, Repr
-
-inductive Justification where
-  | combine (c₁ : Int) (j₁ : Justification) (c₂ : Int) (j₂ : Justification)
-  | assumption (id : AssumptionId)
-  deriving Inhabited, DecidableEq, BEq, Repr
-
-inductive CnstrKind where
-  | eq | div | lt | le
-  deriving Inhabited, DecidableEq, BEq, Repr
-
-structure Cnstr where
-  kind : CnstrKind
-  lhs  : Poly
-  rhs  : Int
-  jst  : Justification
-  deriving Inhabited, DecidableEq, BEq, Repr
-
-abbrev Cnstr.isStrict (c : Cnstr) : Bool :=
-  c.kind matches CnstrKind.lt
-
-def Cnstr.getBound (c : Cnstr) (a : Assignment) : Rat := Id.run do
-  let mut r : Rat := c.rhs
-  -- The maximal variable is in the last position
-  for (c, x) in c.lhs.val[:c.lhs.val.size-1] do
-    if let some v := a.get? x then
-      r := r - c*v
-    else
-      unreachable!
-  let k := c.lhs.val.back!.1
-  return r / k
-
-def Cnstr.isUnsat (c : Cnstr) (a : Assignment) : Bool :=
-  if let some v := c.lhs.eval? a then
-    match c.kind with
-    | CnstrKind.eq => !(v == c.rhs)
-    | CnstrKind.lt => !(v < c.rhs)
-    | CnstrKind.le => !(v <= c.rhs)
-    | CnstrKind.div => unreachable! -- TODO
-  else
-    false
-
-def getBestBound? (cs : Array Cnstr) (a : Assignment) (isLower isInt : Bool) : Option (Rat × Cnstr) :=
-  let adjust (v : Rat) :=
-    if isInt then if isLower then (v.ceil : Rat) else v.floor else v
-  if h : 0 < cs.size then
-    let c0 := cs[0]
-    let b  := adjust <| c0.getBound a
-    some <| cs[1:].foldl (init := (b, c0)) fun r c =>
-      let b' := adjust <| c.getBound a
-      if isLower then
-        if b' > r.1 then (b', c) else r
-      else
-        if b' < r.1 then (b', c) else r
-  else
-    none
-
-inductive Result where
-  | unsat (j : Justification)
-  | unsupported
-  | timeout
-  | sat (a : Assignment)
-
-structure Context where
-  int : Array Bool
-
-structure State where
-  lowers      : Array (Array Cnstr)
-  uppers      : Array (Array Cnstr)
-  int         : Array Bool
-  assignment  : Assignment := {} -- partial assignment
-  deriving Inhabited
-
-abbrev State.getNumVars (s : State) : Nat := s.lowers.size
-
-abbrev State.currVar (s : State) : Nat := s.assignment.size
-
-abbrev State.getBestLowerBound? (s : State) : Option (Rat × Cnstr) :=
-  getBestBound? s.lowers[s.currVar]! s.assignment true s.int[s.currVar]!
-
-abbrev State.getBestUpperBound? (s : State) : Option (Rat × Cnstr) :=
-  getBestBound? s.uppers[s.currVar]! s.assignment false s.int[s.currVar]!
-
-abbrev State.assignCurr (s : State) (v : Rat) : State :=
-  { s with assignment := s.assignment.push v }
-
-def pickAssignment? (lower : Rat) (lowerIsStrict : Bool) (upper : Rat) (upperIsStrict : Bool) : Option Rat :=
-  if lower == upper then
-    if lowerIsStrict || upperIsStrict then none else some lower
-  else if lower < upper then
-    if lowerIsStrict then
-      let c := if lower.isInt then lower + 1 else lower.ceil
-      if c < upper then some c else some ((lower + upper) / 2)
-    else
-      some lower
-  else
-    none
-
-def resolve (s : State) (cl : Cnstr) (cu : Cnstr) : Sum Result State :=
-  let kl : Int := - cl.lhs.getMaxVarCoeff
-  let ku : Int := cu.lhs.getMaxVarCoeff
-  -- Both `kl` and `ku` must be positive
-  let lhs := Poly.combine ku cl.lhs kl cu.lhs
-  -- TODO: normalize coefficients
-  let rhs := ku * cl.rhs + kl * cu.rhs
-  let c   := {
-    lhs, rhs,
-    kind := if cl.isStrict || cu.isStrict then CnstrKind.lt else CnstrKind.le
-    jst  := Justification.combine kl cl.jst ku cu.jst
-    : Cnstr }
-  if !c.isUnsat s.assignment then
-    -- TODO: the naive resolution procedure above may fail for integer constraints
-    Sum.inl Result.unsupported
-  else if lhs.size == 0 then
-    Sum.inl <| Result.unsat c.jst
-  else
-    let maxVarIdx := c.lhs.getMaxVar.id
-    match s with -- Hack: we avoid { s with ... } to make sure we get a destructive update
-    | { lowers, uppers, int, assignment, } =>
-      let assignment := assignment.shrink maxVarIdx
-      if c.lhs.getMaxVarCoeff < 0 then
-        let lowers := lowers.modify maxVarIdx (·.push c)
-        Sum.inr { lowers, uppers, int, assignment }
-      else
-        let uppers := uppers.modify maxVarIdx (·.push c)
-        Sum.inr { lowers, uppers, int, assignment }
-
-def solve (n : Nat) (s : State) : Result :=
-  match n with
-  | 0   => Result.timeout
-  | n+1 =>
-    let i := s.currVar
-    if i = s.getNumVars then
-      Result.sat s.assignment -- all variables have been assigned
-    else
-      match s.getBestLowerBound?, s.getBestUpperBound? with
-      | none,         none         => solve n <| s.assignCurr 0
-      | some (l, cl), none         => solve n <| s.assignCurr (if cl.isStrict then l.ceil + 1 else l.ceil)
-      | none,         some (u, cu) => solve n <| s.assignCurr (if cu.isStrict then u.floor - 1 else u.floor)
-      | some (l, cl), some (u, cu) =>
-        match pickAssignment? l cl.isStrict u cu.isStrict with
-        | some v => solve n <| s.assignCurr v
-        | none => match resolve s cl cu with
-          | Sum.inl r => r
-          | Sum.inr s => solve n s
-
-end Lean.Meta.Linear

src/Lean/Meta/Tactic/Simp.lean

@@ -15,6 +15,7 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 import Lean.Meta.Tactic.Simp.RegisterCommand
 import Lean.Meta.Tactic.Simp.Attr
 import Lean.Meta.Tactic.Simp.Diagnostics
+import Lean.Meta.Tactic.Simp.Arith
 
 namespace Lean
 

src/Lean/Meta/Tactic/Simp/Arith.lean

@@ -1,14 +1,13 @@
 /-
-Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Sebastian Ullrich
 -/
 prelude
-import Lean.Meta.Tactic.LinearArith.Basic
-import Lean.Meta.Tactic.LinearArith.Nat.Simp
-import Lean.Meta.Tactic.LinearArith.Int.Simp
+import Lean.Meta.Tactic.Simp.Arith.Nat
+import Lean.Meta.Tactic.Simp.Arith.Int
 
-namespace Lean.Meta.Linear
+namespace Lean.Meta.Simp.Arith
 
 def parentIsTarget (parent? : Option Expr) : Bool :=
   match parent? with
@@ -16,7 +15,7 @@ def parentIsTarget (parent? : Option Expr) : Bool :=
   | some parent => isLinearTerm parent || isLinearCnstr parent || isDvdCnstr parent
 
 def simp? (e : Expr) (parent? : Option Expr) : MetaM (Option (Expr × Expr)) := do
-  -- TODO: add support for `Int` and arbitrary ordered comm rings
+  -- TODO: invoke `Int` procedures and add support for arbitrary ordered comm rings
   if isLinearCnstr e then
     Nat.simpCnstr? e
   else if isLinearTerm e && !parentIsTarget parent? then
@@ -25,4 +24,4 @@ def simp? (e : Expr) (parent? : Option Expr) : MetaM (Option (Expr × Expr)) :=
   else
     return none
 
-end Lean.Meta.Linear
+end Lean.Meta.Simp.Arith

src/Lean/Meta/Tactic/Simp/Arith/Int.lean

@@ -4,5 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.Tactic.LinearArith.Int.Basic
-import Lean.Meta.Tactic.LinearArith.Int.Simp
+import Lean.Meta.Tactic.Simp.Arith.Int.Basic
+import Lean.Meta.Tactic.Simp.Arith.Int.Simp

src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean

@@ -66,7 +66,7 @@ deriving instance Repr for RawDvdCnstr
 
 end Int.Linear
 
-namespace Lean.Meta.Linear.Int
+namespace Lean.Meta.Simp.Arith.Int
 
 def ofPoly (p : Int.Linear.Poly) : Expr :=
   open Int.Linear.Poly in
@@ -287,7 +287,9 @@ def toRawRelCnstr? (e : Expr) : MetaM (Option (Int.Linear.RawRelCnstr × Array E
   if atoms.size <= 1 then
     return some (c, atoms)
   else
-    let (atoms, perm) := sortExprs atoms
+    -- We use `lt := false` because `Poly.norm` sorts variables in decreasing order.
+    -- It does that because of the cutsat procedure.
+    let (atoms, perm) := sortExprs atoms (lt := false)
     let c := c.applyPerm perm
     return some (c, atoms)
 
@@ -297,7 +299,7 @@ def toRawDvdCnstr? (e : Expr) : MetaM (Option (Int.Linear.RawDvdCnstr × Array E
   if atoms.size <= 1 then
     return some (c, atoms)
   else
-    let (atoms, perm) := sortExprs atoms
+    let (atoms, perm) := sortExprs atoms (lt := false)
     let c := c.applyPerm perm
     return some (c, atoms)
 
@@ -307,4 +309,4 @@ def toContextExpr (ctx : Array Expr) : Expr :=
   else
     RArray.toExpr (mkConst ``Int) id (RArray.leaf (mkIntLit 0))
 
-end Lean.Meta.Linear.Int
+end Lean.Meta.Simp.Arith.Int

src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.Tactic.LinearArith.Basic
-import Lean.Meta.Tactic.LinearArith.Int.Basic
+import Lean.Meta.Tactic.Simp.Arith.Util
+import Lean.Meta.Tactic.Simp.Arith.Int.Basic
 
 def Int.Linear.Poly.gcdAll : Poly → Nat
   | .num k => k.natAbs
@@ -41,7 +41,7 @@ def Int.Linear.RelCnstr.isEq : RelCnstr → Bool
 def Int.Linear.RelCnstr.getConst : RelCnstr → Int
   | .eq p | .le p => p.getConst
 
-namespace Lean.Meta.Linear.Int
+namespace Lean.Meta.Simp.Arith.Int
 
 def simpRelCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   let some (c, atoms) ← toRawRelCnstr? e | return none
@@ -156,4 +156,4 @@ def simpExpr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   else
     return none
 
-end Lean.Meta.Linear.Int
+end Lean.Meta.Simp.Arith.Int

src/Lean/Meta/Tactic/Simp/Arith/Nat.lean

@@ -4,8 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.Tactic.LinearArith.Nat
-
-namespace Lean.Meta.Linear
-
-end Lean.Meta.Linear
+import Lean.Meta.Tactic.Simp.Arith.Nat.Basic
+import Lean.Meta.Tactic.Simp.Arith.Nat.Simp

src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean

@@ -30,7 +30,7 @@ def ExprCnstr.applyPerm (perm : Lean.Perm) : ExprCnstr → ExprCnstr
 
 end Nat.Linear
 
-namespace Lean.Meta.Linear.Nat
+namespace Lean.Meta.Simp.Arith.Nat
 
 deriving instance Repr for Nat.Linear.Expr
 deriving instance Repr for Nat.Linear.ExprCnstr
@@ -185,4 +185,4 @@ def toContextExpr (ctx : Array Expr) : Expr :=
   else
     RArray.toExpr (mkConst ``Nat) id (RArray.leaf (mkNatLit 0))
 
-namespace Lean.Meta.Linear.Nat
+namespace Lean.Meta.Simp.Arith.Nat

src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.Tactic.LinearArith.Basic
-import Lean.Meta.Tactic.LinearArith.Nat.Basic
+import Lean.Meta.Tactic.Simp.Arith.Util
+import Lean.Meta.Tactic.Simp.Arith.Nat.Basic
 
-namespace Lean.Meta.Linear.Nat
+namespace Lean.Meta.Simp.Arith.Nat
 
 def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   let some (c, atoms) ← toLinearCnstr? e
@@ -80,4 +80,4 @@ def simpExpr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   else
     return none
 
-end Lean.Meta.Linear.Nat
+end Lean.Meta.Simp.Arith.Nat

src/Lean/Meta/Tactic/Simp/Arith/Util.lean

@@ -7,7 +7,7 @@ prelude
 import Lean.Meta.Basic
 import Lean.Expr
 
-namespace Lean.Meta.Linear
+namespace Lean.Meta.Simp.Arith
 /-
 To prevent the kernel from accidentially reducing the atoms in the equation while typechecking,
 we abstract over them.
@@ -60,4 +60,4 @@ partial def isLinearCnstr (e : Expr) : Bool :=
 def isDvdCnstr (e : Expr) : Bool :=
   e.isAppOfArity ``Dvd.dvd 4
 
-end Lean.Meta.Linear
+end Lean.Meta.Simp.Arith

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -11,7 +11,7 @@ import Lean.Meta.SynthInstance
 import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Types
-import Lean.Meta.Tactic.LinearArith.Simp
+import Lean.Meta.Tactic.Simp.Arith
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.Attr
 import Lean.Meta.BinderNameHint
@@ -283,25 +283,25 @@ where
 def simpArith (e : Expr) : SimpM Step := do
   unless (← getConfig).arith do
     return .continue
-  if Linear.isLinearCnstr e then
-    if let some (e', h) ← Linear.Nat.simpCnstr? e then
+  if Arith.isLinearCnstr e then
+    if let some (e', h) ← Arith.Nat.simpCnstr? e then
       return .visit { expr := e', proof? := h }
-    else if let some (e', h) ← Linear.Int.simpRelCnstr? e then
+    else if let some (e', h) ← Arith.Int.simpRelCnstr? e then
       return .visit { expr := e', proof? := h }
     else
       return .continue
-  else if Linear.isLinearTerm e then
-    if Linear.parentIsTarget (← getContext).parent? then
+  else if Arith.isLinearTerm e then
+    if Arith.parentIsTarget (← getContext).parent? then
       -- We mark `cache := false` to ensure we do not miss simplifications.
       return .continue (some { expr := e, cache := false })
-    else if let some (e', h) ← Linear.Nat.simpExpr? e then
+    else if let some (e', h) ← Arith.Nat.simpExpr? e then
       return .visit { expr := e', proof? := h }
-    else if let some (e', h) ← Linear.Int.simpExpr? e then
+    else if let some (e', h) ← Arith.Int.simpExpr? e then
       return .visit { expr := e', proof? := h }
     else
       return .continue
-  else if Linear.isDvdCnstr e then
-    if let some (e', h) ← Linear.Int.simpDvdCnstr? e then
+  else if Arith.isDvdCnstr e then
+    if let some (e', h) ← Arith.Int.simpDvdCnstr? e then
       return .visit { expr := e', proof? := h }
     else
       return .continue

src/Lean/Util/SortExprs.lean

@@ -12,10 +12,14 @@ abbrev Perm := Std.HashMap Nat Nat
 
 /--
 Sorts the given expressions using `Expr.lt`, and creates a "permutation map" storing the new position of each expression.
+If `lt := false`, then sorts expressions in decreasing order.
 -/
-def sortExprs (es : Array Expr) : Array Expr × Perm :=
+def sortExprs (es : Array Expr) (lt := true) : Array Expr × Perm :=
   let es := es.mapIdx fun i e => (e, i)
-  let es := es.qsort fun (e₁, _) (e₂, _) => e₁.lt e₂
+  let es := if lt then
+    es.qsort fun (e₁, _) (e₂, _) => e₁.lt e₂
+  else
+    es.qsort fun (e₁, _) (e₂, _) => e₂.lt e₁
   let (_, perm) := es.foldl (init := (0, Std.HashMap.empty)) fun (i, perm) (_, j) => (i+1, perm.insert j i)
   let es := es.map (·.1)
   (es, perm)

tests/lean/run/liaByRefl.lean

@@ -71,15 +71,15 @@ example :
   rfl
 
 example (x₁ x₂ x₃ : Int) : ((x₁ + x₂) + (x₂ + x₃) = x₃ + x₂) = (x₁ + x₂ = 0) :=
-  RawRelCnstr.eq_of_norm_eq #R[x₁, x₂, x₃]
-    (.eq (Expr.add (Expr.add (Expr.var 0) (Expr.var 1)) (Expr.add (Expr.var 1) (Expr.var 2)))
-         (Expr.add (Expr.var 2) (Expr.var 1)))
-    (.eq (.add 1 0 (.add 1 1 (.num 0))))
+  RawRelCnstr.eq_of_norm_eq #R[x₃, x₂, x₁]
+    (.eq (Expr.add (Expr.add (Expr.var 2) (Expr.var 1)) (Expr.add (Expr.var 1) (Expr.var 0)))
+         (Expr.add (Expr.var 0) (Expr.var 1)))
+    (.eq (.add 1 2 (.add 1 1 (.num 0))))
     rfl
 
 example (x₁ x₂ x₃ : Int) : ((x₁ + x₂) + (x₂ + x₃) ≤ x₃ + x₂) = (x₁ + x₂ ≤ 0) :=
-  RawRelCnstr.eq_of_norm_eq #R[x₁, x₂, x₃]
-    (.le (Expr.add (Expr.add (Expr.var 0) (Expr.var 1)) (Expr.add (Expr.var 1) (Expr.var 2)))
-         (Expr.add (Expr.var 2) (Expr.var 1)))
-    (.le (Poly.add 1 0 (.add 1 1 (.num 0))))
+  RawRelCnstr.eq_of_norm_eq #R[x₃, x₂, x₁]
+    (.le (Expr.add (Expr.add (Expr.var 2) (Expr.var 1)) (Expr.add (Expr.var 1) (Expr.var 0)))
+         (Expr.add (Expr.var 0) (Expr.var 1)))
+    (.le (Poly.add 1 2 (.add 1 1 (.num 0))))
     rfl

tests/lean/run/simpCnstr1.lean

@@ -4,7 +4,7 @@ open Lean in open Lean.Meta in
 def test (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   forallTelescope info.type fun _ e => do
-    let some (e', p) ← Linear.simp? e none | throwError "failed to simplify{indentExpr e}"
+    let some (e', p) ← Simp.Arith.simp? e none | throwError "failed to simplify{indentExpr e}"
     check p
     unless (← isDefEq (← inferType p) (← mkEq e e')) do
       throwError "invalid proof"

tests/lean/run/simp_int_arith.lean

@@ -143,18 +143,18 @@ fun x y z =>
   of_eq_true
     (id
       (Int.Linear.RawRelCnstr.eq_true_of_isValid
-        (Lean.RArray.branch 1 (Lean.RArray.leaf x) (Lean.RArray.branch 2 (Lean.RArray.leaf y) (Lean.RArray.leaf z)))
+        (Lean.RArray.branch 1 (Lean.RArray.leaf z) (Lean.RArray.branch 2 (Lean.RArray.leaf y) (Lean.RArray.leaf x)))
         (Int.Linear.RawRelCnstr.le
-          ((((((Int.Linear.Expr.var 0).add (Int.Linear.Expr.var 1)).add (Int.Linear.Expr.num 2)).add
+          ((((((Int.Linear.Expr.var 2).add (Int.Linear.Expr.var 1)).add (Int.Linear.Expr.num 2)).add
                     (Int.Linear.Expr.var 1)).add
-                (Int.Linear.Expr.var 2)).add
-            (Int.Linear.Expr.var 2))
-          (((((((Int.Linear.Expr.var 1).add (Int.Linear.Expr.mulL 3 (Int.Linear.Expr.var 2))).add
+                (Int.Linear.Expr.var 0)).add
+            (Int.Linear.Expr.var 0))
+          (((((((Int.Linear.Expr.var 1).add (Int.Linear.Expr.mulL 3 (Int.Linear.Expr.var 0))).add
                             (Int.Linear.Expr.num 1)).add
                         (Int.Linear.Expr.num 1)).add
-                    (Int.Linear.Expr.var 0)).add
+                    (Int.Linear.Expr.var 2)).add
                 (Int.Linear.Expr.var 1)).sub
-            (Int.Linear.Expr.var 2)))
+            (Int.Linear.Expr.var 0)))
         (Eq.refl true)))
 -/
 #guard_msgs (info) in
@@ -170,18 +170,18 @@ fun x y z f =>
     ((fun x_1 =>
         id
           (Int.Linear.RawRelCnstr.eq_true_of_isValid
-            (Lean.RArray.branch 1 (Lean.RArray.leaf x)
-              (Lean.RArray.branch 2 (Lean.RArray.leaf z) (Lean.RArray.leaf x_1)))
+            (Lean.RArray.branch 1 (Lean.RArray.leaf x_1)
+              (Lean.RArray.branch 2 (Lean.RArray.leaf z) (Lean.RArray.leaf x)))
             (Int.Linear.RawRelCnstr.le
-              ((((((Int.Linear.Expr.var 0).add (Int.Linear.Expr.var 2)).add (Int.Linear.Expr.num 2)).add
-                        (Int.Linear.Expr.var 2)).add
+              ((((((Int.Linear.Expr.var 2).add (Int.Linear.Expr.var 0)).add (Int.Linear.Expr.num 2)).add
+                        (Int.Linear.Expr.var 0)).add
                     (Int.Linear.Expr.var 1)).add
                 (Int.Linear.Expr.var 1))
-              (((((((Int.Linear.Expr.var 2).add (Int.Linear.Expr.mulL 3 (Int.Linear.Expr.var 1))).add
+              (((((((Int.Linear.Expr.var 0).add (Int.Linear.Expr.mulL 3 (Int.Linear.Expr.var 1))).add
                                 (Int.Linear.Expr.num 1)).add
                             (Int.Linear.Expr.num 1)).add
-                        (Int.Linear.Expr.var 0)).add
-                    (Int.Linear.Expr.var 2)).sub
+                        (Int.Linear.Expr.var 2)).add
+                    (Int.Linear.Expr.var 0)).sub
                 (Int.Linear.Expr.var 1)))
             (Eq.refl true)))
       (f y))
@@ -303,13 +303,13 @@ fun a b =>
     (Eq.trans
       (congrArg (fun x => x ↔ 2 ∣ a + 2 * b + 11)
         (id
-          (RawDvdCnstr.eq_of_isEqv (RArray.branch 1 (RArray.leaf a) (RArray.leaf b))
+          (RawDvdCnstr.eq_of_isEqv (RArray.branch 1 (RArray.leaf b) (RArray.leaf a))
             { k := 6,
               e :=
-                (((Expr.var 0).add ((Expr.num 21).sub (Expr.var 0))).add
-                      (Expr.mulL 3 ((Expr.var 0).add (Expr.mulL 2 (Expr.var 1))))).add
+                (((Expr.var 1).add ((Expr.num 21).sub (Expr.var 1))).add
+                      (Expr.mulL 3 ((Expr.var 1).add (Expr.mulL 2 (Expr.var 0))))).add
                   (Expr.num 12) }
-            { k := 2, p := Poly.add 1 0 (Poly.add 2 1 (Poly.num 11)) } 3 (Eq.refl true))))
+            { k := 2, p := Poly.add 1 1 (Poly.add 2 0 (Poly.num 11)) } 3 (Eq.refl true))))
       (iff_self (2 ∣ a + 2 * b + 11)))
 -/
 #guard_msgs (info) in
@@ -326,13 +326,13 @@ fun a b =>
     (Eq.trans
       (congrArg (fun x => x ↔ 2 ∣ a + 2 * b)
         (id
-          (RawDvdCnstr.eq_of_isEqv (RArray.branch 1 (RArray.leaf a) (RArray.leaf b))
+          (RawDvdCnstr.eq_of_isEqv (RArray.branch 1 (RArray.leaf b) (RArray.leaf a))
             { k := 6,
               e :=
-                (((Expr.var 0).add ((Expr.num 11).sub (Expr.var 0))).add
-                      (Expr.mulL 3 ((Expr.var 0).add (Expr.mulL 2 (Expr.var 1))))).sub
+                (((Expr.var 1).add ((Expr.num 11).sub (Expr.var 1))).add
+                      (Expr.mulL 3 ((Expr.var 1).add (Expr.mulL 2 (Expr.var 0))))).sub
                   (Expr.num 11) }
-            { k := 2, p := Poly.add 1 0 (Poly.add 2 1 (Poly.num 0)) } 3 (Eq.refl true))))
+            { k := 2, p := Poly.add 1 1 (Poly.add 2 0 (Poly.num 0)) } 3 (Eq.refl true))))
       (iff_self (2 ∣ a + 2 * b)))
 -/
 #guard_msgs (info) in