chore: fix test

Goal: avoid converting back to `Expr`

src/Init/Data/Int/Linear.lean

@@ -11,6 +11,7 @@ import Init.Data.Int.LemmasAux
 import Init.Data.Int.DivModLemmas
 import Init.Data.Int.Gcd
 import Init.Data.RArray
+import Init.Data.AC
 
 namespace Int.Linear
 
@@ -51,6 +52,32 @@ def Poly.denote (ctx : Context) (p : Poly) : Int :=
   | .num k => k
   | .add k v p => Int.add (Int.mul k (v.denote ctx)) (denote ctx p)
 
+/--
+Similar to `Poly.denote`, but produces a denotation better for `simp +arith`.
+Remark: we used to convert `Poly` back into `Expr` to achieve that.
+-/
+def Poly.denote' (ctx : Context) (p : Poly) : Int :=
+  match p with
+  | .num k => k
+  | .add 1 v p => go (v.denote ctx) p
+  | .add k v p => go (Int.mul k (v.denote ctx)) p
+where
+  go (r : Int)  (p : Poly) : Int :=
+    match p with
+    | .num 0 => r
+    | .num k => Int.add r k
+    | .add 1 v p => go (Int.add r (v.denote ctx)) p
+    | .add k v p => go (Int.add r (Int.mul k (v.denote ctx))) p
+
+theorem Poly.denote'_go_eq_denote (ctx : Context) (p : Poly) (r : Int) : denote'.go ctx r p = p.denote ctx + r := by
+  induction r, p using denote'.go.induct ctx <;> simp [denote'.go, denote]
+  next => rw [Int.add_comm]
+  next ih => simp [denote'.go] at ih; rw [ih]; ac_rfl
+  next ih => simp [denote'.go] at ih; rw [ih]; ac_rfl
+
+theorem Poly.denote'_eq_denote (ctx : Context) (p : Poly) : p.denote' ctx = p.denote ctx := by
+  unfold denote' <;> split <;> simp [denote, denote'_go_eq_denote] <;> ac_rfl
+
 def Poly.addConst (p : Poly) (k : Int) : Poly :=
   match p with
   | .num k' => .num (k+k')
@@ -105,6 +132,13 @@ def RelCnstr.denote (ctx : Context) : RelCnstr → Prop
   | .eq p => p.denote ctx = 0
   | .le p => p.denote ctx ≤ 0
 
+def RelCnstr.denote' (ctx : Context) : RelCnstr → Prop
+  | .eq p => p.denote' ctx = 0
+  | .le p => p.denote' ctx ≤ 0
+
+theorem RelCnstr.denote'_eq_denote (ctx : Context) (c : RelCnstr) : c.denote' ctx = c.denote ctx := by
+  cases c <;> simp [denote, denote', Poly.denote'_eq_denote]
+
 /--
 Returns the ceiling of the division `a / b`. That is, the result is equivalent to `⌈a / b⌉`.
 Examples:
@@ -202,6 +236,18 @@ def Poly.divCoeffs (k : Int) : Poly → Bool
   | .num _ => true
   | .add k' _ p => k' % k == 0 && divCoeffs k p
 
+/--
+`p.mul k` multiplies all coefficients and constant of the polynomial `p` by `k`.
+-/
+def Poly.mul (p : Poly) (k : Int) : Poly :=
+  match p with
+  | .num k' => .num (k*k')
+  | .add k' v p => .add (k*k') v (mul p k)
+
+@[simp] theorem Poly.denote_mul (ctx : Context) (p : Poly) (k : Int) : (p.mul k).denote ctx = k * p.denote ctx := by
+  induction p <;> simp [mul, denote, *]
+  rw [Int.mul_assoc, Int.mul_add]
+
 /-- Normalizes the polynomial of the given relational constraint. -/
 def RelCnstr.norm : RelCnstr → RelCnstr
   | .eq p => .eq p.norm
@@ -228,6 +274,30 @@ def RelCnstr.div (k : Int) : RelCnstr → RelCnstr
   | .eq p => .eq <| p.div k
   | .le p => .le <| p.div k
 
+/--
+Multiplies all coefficients and constants in the linear polynomial of the given constraint by `k`.
+-/
+def RelCnstr.mul (k : Int) : RelCnstr → RelCnstr
+  | .eq p => .eq <| p.mul k
+  | .le p => .le <| p.mul k
+
+@[simp] theorem RelCnstr.denote_mul (ctx : Context) (c : RelCnstr) (k : Int) (h : k > 0) : (c.mul k).denote ctx = c.denote ctx := by
+  cases c <;> simp [mul, denote]
+  next =>
+    constructor
+    · intro h₁; cases (Int.mul_eq_zero.mp h₁)
+      next hz => simp [hz] at h
+      next => assumption
+    · intro h'; simp [*]
+  next =>
+    constructor
+    · intro h₁
+      conv at h₁ => rhs; rw [← Int.mul_zero k]
+      exact Int.le_of_mul_le_mul_left h₁ h
+    · intro h₂
+      have := Int.mul_le_mul_of_nonneg_left h₂ (Int.le_of_lt h)
+      simp at this; assumption
+
 /-- Raw relational constraint. They are later converted into `RelCnstr`. -/
 inductive RawRelCnstr  where
   | eq (p₁ p₂ : Expr)
@@ -248,8 +318,8 @@ def RawRelCnstr.norm : RawRelCnstr → RelCnstr
   | .le e₁ e₂ => .le (e₁.sub e₂).toPoly.norm
 
 /-- A certificate for normalizing the coefficients of a raw relational constraint. -/
-def divBy (e e' : RawRelCnstr) (k : Int) : Bool :=
-  k > 0 && e.norm.divAll k && e'.norm == e.norm.div k
+def divBy (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : Bool :=
+  k > 0 && c.norm == c'.mul k
 
 attribute [local simp] Int.add_comm Int.add_assoc Int.add_left_comm Int.add_mul Int.mul_add
 attribute [local simp] Poly.insert Poly.denote Poly.norm Poly.addConst
@@ -371,10 +441,10 @@ theorem Expr.eq_of_toPoly_eq (ctx : Context) (e e' : Expr) (h : e.toPoly == e'.t
   simp [Poly.norm] at h
   assumption
 
-theorem RawRelCnstr.eq_of_norm_eq (ctx : Context) (c c' : RawRelCnstr) (h : c.norm == c'.norm) : c.denote ctx = c'.denote ctx := by
+theorem RawRelCnstr.eq_of_norm_eq (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (h : c.norm == c') : c.denote ctx = c'.denote' ctx := by
   have h := congrArg (RelCnstr.denote ctx) (eq_of_beq h)
-  rw [denote_norm, denote_norm] at h
-  assumption
+  rw [denote_norm] at h
+  rw [RelCnstr.denote'_eq_denote, h]
 
 theorem RawRelCnstr.eq_of_norm_eq_var (ctx : Context) (x y : Var) (c : RawRelCnstr) (h : c.norm == .eq (.add 1 x (.add (-1) y (.num 0))))
     : c.denote ctx = (x.denote ctx = y.denote ctx) := by
@@ -411,39 +481,19 @@ private theorem eq_mul_le_zero {a b : Int} : 0 < b → (a ≤ 0 ↔ a * b ≤ 0)
     rw [this] at h'
     exact Int.le_of_mul_le_mul_right h' h
 
-attribute [local simp] RelCnstr.divAll RelCnstr.div
+attribute [local simp] RelCnstr.divAll RelCnstr.div RelCnstr.mul
 
-theorem RawRelCnstr.eq_of_norm_eq_of_divBy' (ctx : Context) (c c' : RawRelCnstr) (p : RelCnstr) (k : Int)
-    : k > 0 → p.divAll k → c.norm = p → c'.norm = p.div k → c.denote ctx = c'.denote ctx := by
-  intro h₀ h₁ h₂ h₃
-  have hz : k ≠ 0 := Int.ne_of_gt h₀
-  cases p <;> simp at h₁
-  next p =>
-    replace h₁ := Poly.denote_div_eq_of_divAll ctx p k h₁
-    replace h₂ := congrArg (RelCnstr.denote ctx) h₂
-    simp only [RelCnstr.denote.eq_1, ← h₁] at h₂
-    replace h₃ := congrArg (RelCnstr.denote ctx) h₃
-    simp only [RelCnstr.denote.eq_1, RelCnstr.div] at h₃
-    rw [mul_eq_zero_iff_eq_zero _ _ hz] at h₂
-    have := Eq.trans h₂ h₃.symm
-    rw [denote_norm, denote_norm] at this
-    exact this
-  next p =>
-    replace h₁ := Poly.denote_div_eq_of_divAll ctx p k h₁
-    replace h₂ := congrArg (RelCnstr.denote ctx) h₂
-    simp only [RelCnstr.denote.eq_2, ← h₁] at h₂
-    replace h₃ := congrArg (RelCnstr.denote ctx) h₃
-    simp only [RelCnstr.denote.eq_2, RelCnstr.div] at h₃
-    rw [eq_mul_le_zero h₀] at h₃
-    have := Eq.trans h₂ h₃.symm
-    rw [denote_norm, denote_norm] at this
-    exact this
+theorem RawRelCnstr.eq_of_norm_eq_mul (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (k : Int) (hz : k > 0) (h : c.norm = c'.mul k) : c.denote ctx = c'.denote ctx := by
+  replace h := congrArg (RelCnstr.denote ctx) h
+  simp only [RawRelCnstr.denote_norm, RelCnstr.denote_mul, *] at h
+  assumption
 
-theorem RawRelCnstr.eq_of_divBy (ctx : Context) (e e' : RawRelCnstr) (k : Int) : divBy e e' k → e.denote ctx = e'.denote ctx := by
+theorem RawRelCnstr.eq_of_divBy (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : divBy c c' k → c.denote ctx = c'.denote' ctx := by
   intro h
+  simp only [RelCnstr.denote'_eq_denote]
   simp only [divBy, Bool.and_eq_true, bne_iff_ne, ne_eq, beq_iff_eq, decide_eq_true_eq] at h
-  have ⟨⟨h₁, h₂⟩, h₃⟩ := h
-  exact eq_of_norm_eq_of_divBy' ctx e e' e.norm k h₁ h₂ rfl h₃
+  have ⟨h₁, h₂⟩ := h
+  exact eq_of_norm_eq_mul ctx c c' k h₁ h₂
 
 private theorem mul_add_cmod_le_iff {a k b : Int} (h : k > 0) : a*k + cmod b k ≤ 0 ↔ a ≤ 0 := by
   constructor
@@ -469,11 +519,11 @@ private theorem mul_add_cmod_le_iff {a k b : Int} (h : k > 0) : a*k + cmod b k
     simp at this
     assumption
 
-theorem RawRelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c c' : RawRelCnstr) (p : RelCnstr) (k : Int)
-    : k > 0 → p.divCoeffs k → p.isLe → c.norm = p → c'.norm = p.div k → c.denote ctx = c'.denote ctx := by
+theorem RawRelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c₁ : RawRelCnstr) (c₂ : RelCnstr) (c₃ : RelCnstr) (k : Int)
+    : k > 0 → c₂.divCoeffs k → c₂.isLe → c₁.norm = c₂ → c₃ = c₂.div k → c₁.denote ctx = c₃.denote ctx := by
   intro h₀ h₁ h₂ h₃ h₄
   have hz : k ≠ 0 := Int.ne_of_gt h₀
-  cases p <;> simp [RelCnstr.isLe] at h₂
+  cases c₂ <;> simp [RelCnstr.isLe] at h₂
   clear h₂
   next p =>
     simp [RelCnstr.divCoeffs] at h₁
@@ -482,24 +532,25 @@ theorem RawRelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c c' : RawRelCns
     simp only [RelCnstr.denote.eq_2, ← h₁] at h₃
     replace h₄ := congrArg (RelCnstr.denote ctx) h₄
     simp only [RelCnstr.denote.eq_2, RelCnstr.div] at h₄
-    rw [denote_norm] at h₃ h₄
+    rw [denote_norm] at h₃
     rw [h₃, h₄]
     apply propext
     apply mul_add_cmod_le_iff
     exact h₀
 
 /-- Certificate for normalizing the coefficients of inequality constraint with bound tightening. -/
-def divByLe (c c' : RawRelCnstr) (k : Int) : Bool :=
-  k > 0 && c.isLe && c.norm.divCoeffs k && c'.norm == c.norm.div k
+def divByLe (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : Bool :=
+  k > 0 && c.isLe && c.norm.divCoeffs k && c' == c.norm.div k
 
-theorem RawRelCnstr.eq_of_divByLe (ctx : Context) (c c' : RawRelCnstr) (k : Int) : divByLe c c' k → c.denote ctx = c'.denote ctx := by
+theorem RawRelCnstr.eq_of_divByLe (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : divByLe c c' k → c.denote ctx = c'.denote' ctx := by
   intro h
+  simp only [RelCnstr.denote'_eq_denote]
   simp only [divByLe, Bool.and_eq_true, bne_iff_ne, ne_eq, beq_iff_eq, decide_eq_true_eq] at h
   have ⟨⟨⟨h₀, h₁⟩, h₂⟩, h₃⟩ := h
   have hle : c.norm.isLe := by
     cases c <;> simp [RawRelCnstr.isLe] at h₁
     simp [RelCnstr.isLe]
-  apply eq_of_norm_eq_of_divCoeffs ctx c c' c.norm k h₀ h₂ hle rfl h₃
+  apply eq_of_norm_eq_of_divCoeffs ctx c c.norm c' k h₀ h₂ hle rfl h₃
 
 def RelCnstr.isUnsat : RelCnstr → Bool
   | .eq (.num k) => k != 0
@@ -606,15 +657,6 @@ theorem Poly.gcd_dvd_const {ctx : Context} {p : Poly} {k : Int} (h : k ∣ p.den
     rw [Int.add_comm] at h
     exact ih (gcd_dvd_step h)
 
-def Poly.mul (p : Poly) (k : Int) : Poly :=
-  match p with
-  | .num k' => .num (k*k')
-  | .add k' v p => .add (k*k') v (mul p k)
-
-@[simp] theorem Poly.denote_mul (ctx : Context) (p : Poly) (k : Int) : (p.mul k).denote ctx = k * p.denote ctx := by
-  induction p <;> simp [mul, *]
-  rw [Int.mul_assoc]
-
 /-- Divibility constraint of the form `k ∣ p`. -/
 structure DvdCnstr where
   k : Int
@@ -623,6 +665,12 @@ structure DvdCnstr where
 def DvdCnstr.denote (ctx : Context) (c : DvdCnstr) : Prop :=
   c.k ∣ c.p.denote ctx
 
+def DvdCnstr.denote' (ctx : Context) (c : DvdCnstr) : Prop :=
+  c.k ∣ c.p.denote' ctx
+
+theorem DvdCnstr.denote'_eq_denote (ctx : Context) (c : DvdCnstr) : c.denote' ctx = c.denote ctx := by
+  simp [denote', denote, Poly.denote'_eq_denote]
+
 def DvdCnstr.isUnsat (c : DvdCnstr) : Bool :=
   c.p.getConst % c.p.gcdCoeffs c.k != 0
 
@@ -679,14 +727,14 @@ def RawDvdCnstr.norm (c : RawDvdCnstr) : DvdCnstr :=
 @[simp] theorem RawDvdCnstr.denote_norm_eq (ctx : Context) (c : RawDvdCnstr) : c.denote ctx = c.norm.denote ctx := by
   simp [norm, denote, DvdCnstr.denote]
 
-def RawDvdCnstr.isEqv (c₁ c₂ : RawDvdCnstr) (k : Int) : Bool :=
-  c₁.norm.isEqv c₂.norm k
+def RawDvdCnstr.isEqv (c : RawDvdCnstr) (c' : DvdCnstr) (k : Int) : Bool :=
+  c.norm.isEqv c' k
 
 def RawDvdCnstr.isUnsat (c : RawDvdCnstr) : Bool :=
   c.norm.isUnsat
 
-theorem RawDvdCnstr.eq_of_isEqv (ctx : Context) (c₁ c₂ : RawDvdCnstr) (k : Int) (h : isEqv c₁ c₂ k) : c₁.denote ctx = c₂.denote ctx := by
-  simp [DvdCnstr.eq_of_isEqv ctx c₁.norm c₂.norm k h]
+theorem RawDvdCnstr.eq_of_isEqv (ctx : Context) (c : RawDvdCnstr) (c' : DvdCnstr) (k : Int) (h : isEqv c c' k) : c.denote ctx = c'.denote' ctx := by
+  simp [DvdCnstr.eq_of_isEqv ctx c.norm c' k h, DvdCnstr.denote'_eq_denote]
 
 theorem RawDvdCnstr.eq_false_of_isUnsat (ctx : Context) (c : RawDvdCnstr) (h : c.isUnsat) : c.denote ctx = False := by
   simp [DvdCnstr.eq_false_of_isUnsat ctx c.norm h]

src/Lean/Meta/Tactic/LinearArith/Int/Basic.lean

@@ -68,10 +68,36 @@ end Int.Linear
 
 namespace Lean.Meta.Linear.Int
 
+def ofPoly (p : Int.Linear.Poly) : Expr :=
+  open Int.Linear.Poly in
+  match p with
+  | .num v => mkApp (mkConst ``num) (toExpr v)
+  | .add k v p => mkApp3 (mkConst ``add) (toExpr k) (toExpr v) (ofPoly p)
+
+instance : ToExpr Int.Linear.Poly where
+  toExpr a := ofPoly a
+  toTypeExpr := mkConst ``Int.Linear.Poly
+
+def ofRelCnstr (c : Int.Linear.RelCnstr) : Expr :=
+  match c with
+  | .eq p => mkApp (mkConst ``Int.Linear.RelCnstr.eq) (toExpr p)
+  | .le p => mkApp (mkConst ``Int.Linear.RelCnstr.le) (toExpr p)
+
+instance : ToExpr Int.Linear.RelCnstr where
+  toExpr a   := ofRelCnstr a
+  toTypeExpr := mkConst ``Int.Linear.RelCnstr
+
+def ofDvdCnstr (c : Int.Linear.DvdCnstr) : Expr :=
+   mkApp2 (mkConst ``Int.Linear.DvdCnstr.mk) (toExpr c.k) (toExpr c.p)
+
+instance : ToExpr Int.Linear.DvdCnstr where
+  toExpr a   := ofDvdCnstr a
+  toTypeExpr := mkConst ``Int.Linear.DvdCnstr
+
 def ofLinearExpr (e : Int.Linear.Expr) : Expr :=
   open Int.Linear.Expr in
   match e with
-  | .num v    => mkApp (mkConst ``num) (Lean.toExpr v)
+  | .num v    => mkApp (mkConst ``num) (toExpr v)
   | .var i    => mkApp (mkConst ``var) (mkNatLit i)
   | .neg a    => mkApp (mkConst ``neg) (ofLinearExpr a)
   | .add a b  => mkApp2 (mkConst ``add) (ofLinearExpr a) (ofLinearExpr b)
@@ -117,6 +143,27 @@ def _root_.Int.Linear.RawRelCnstr.denoteExpr (ctx : Array Expr) (c : Int.Linear.
 def _root_.Int.Linear.RawDvdCnstr.denoteExpr (ctx : Array Expr) (c : Int.Linear.RawDvdCnstr) : MetaM Expr := do
   return mkIntDvd (mkIntLit c.k) (← c.e.denoteExpr ctx)
 
+def _root_.Int.Linear.Poly.denoteExpr (ctx : Array Expr) (p : Int.Linear.Poly) : MetaM Expr := do
+  match p with
+  | .num k => return toExpr k
+  | .add 1 x p => go ctx[x]! p
+  | .add k x p => go (mkIntMul (toExpr k) ctx[x]!) p
+where
+  go (r : Expr)  (p : Int.Linear.Poly) : MetaM Expr :=
+    match p with
+    | .num 0 => return r
+    | .num k => return mkIntAdd r (toExpr k)
+    | .add 1 x p => go (mkIntAdd r ctx[x]!) p
+    | .add k x p => go (mkIntAdd r (mkIntMul (toExpr k) ctx[x]!)) p
+
+def _root_.Int.Linear.RelCnstr.denoteExpr (ctx : Array Expr) (c : Int.Linear.RelCnstr) : MetaM Expr := do
+  match c with
+  | .eq p => return mkIntEq (← p.denoteExpr ctx) (mkIntLit 0)
+  | .le p => return mkIntLE (← p.denoteExpr ctx) (mkIntLit 0)
+
+def _root_.Int.Linear.DvdCnstr.denoteExpr (ctx : Array Expr) (c : Int.Linear.DvdCnstr) : MetaM Expr := do
+  return mkIntDvd (mkIntLit c.k) (← c.p.denoteExpr ctx)
+
 namespace ToLinear
 
 structure State where

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

@@ -47,19 +47,18 @@ def simpRelCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   let some (c, atoms) ← toRawRelCnstr? e | return none
   withAbstractAtoms atoms ``Int fun atoms => do
     let lhs ← c.denoteExpr atoms
-    let p := c.norm
-    if p.isUnsat then
+    let c' := c.norm
+    if c'.isUnsat then
       let r := mkConst ``False
       let h := mkApp3 (mkConst ``Int.Linear.RawRelCnstr.eq_false_of_isUnsat) (toContextExpr atoms) (toExpr c) reflBoolTrue
       return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
-    else if p.isValid then
+    else if c'.isValid then
       let r := mkConst ``True
       let h := mkApp3 (mkConst ``Int.Linear.RawRelCnstr.eq_true_of_isValid) (toContextExpr atoms) (toExpr c) reflBoolTrue
       return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
     else
-      let c' := p.toRaw
-      if c != c' then
-        match p with
+      if c != c'.toRaw then
+        match c' with
         | .eq (.add 1 x (.add (-1) y (.num 0))) =>
           let r := mkIntEq atoms[x]! atoms[y]!
           let h := mkApp5 (mkConst ``Int.Linear.RawRelCnstr.eq_of_norm_eq_var) (toContextExpr atoms) (toExpr x) (toExpr y) (toExpr c) reflBoolTrue
@@ -69,23 +68,23 @@ def simpRelCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
           let h := mkApp5 (mkConst ``Int.Linear.RawRelCnstr.eq_of_norm_eq_const) (toContextExpr atoms) (toExpr x) (toExpr (-k)) (toExpr c) reflBoolTrue
           return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
         | _ =>
-          let k := p.gcdCoeffs
+          let k := c'.gcdCoeffs
           if k == 1 then
             let r ← c'.denoteExpr atoms
             let h := mkApp4 (mkConst ``Int.Linear.RawRelCnstr.eq_of_norm_eq) (toContextExpr atoms) (toExpr c) (toExpr c') reflBoolTrue
             return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
-          else if p.getConst % k == 0 then
-            let c' := (p.div k).toRaw
+          else if c'.getConst % k == 0 then
+            let c' := c'.div k
             let r ← c'.denoteExpr atoms
             let h := mkApp5 (mkConst ``Int.Linear.RawRelCnstr.eq_of_divBy) (toContextExpr atoms) (toExpr c) (toExpr c') (toExpr (Int.ofNat k)) reflBoolTrue
             return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
-          else if p.isEq then
+          else if c'.isEq then
             let r := mkConst ``False
             let h := mkApp4 (mkConst ``Int.Linear.RawRelCnstr.eq_false_of_isUnsat_coeff) (toContextExpr atoms) (toExpr c) (toExpr (Int.ofNat k)) reflBoolTrue
             return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
           else
             -- `p.isLe`: tighten the bound
-            let c' := (p.div k).toRaw
+            let c' := c'.div k
             let r ← c'.denoteExpr atoms
             let h := mkApp5 (mkConst ``Int.Linear.RawRelCnstr.eq_of_divByLe) (toContextExpr atoms) (toExpr c) (toExpr c') (toExpr (Int.ofNat k)) reflBoolTrue
             return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
@@ -135,8 +134,7 @@ def simpDvdCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     let k  := c'.p.gcdCoeffs c'.k
     if c'.p.getConst % k == 0 then
       let c' := c'.div k
-      let c' := c'.toRaw
-      if c == c' then
+      if c == c'.toRaw then
         return none
       let r ← c'.denoteExpr atoms
       let h := mkApp5 (mkConst ``Int.Linear.RawDvdCnstr.eq_of_isEqv) (toContextExpr atoms) (toExpr c) (toExpr c') (toExpr k) reflBoolTrue

tests/lean/run/liaByRefl.lean

@@ -74,14 +74,12 @@ example (x₁ x₂ x₃ : Int) : ((x₁ + x₂) + (x₂ + x₃) = x₃ + x₂) =
   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 (Expr.add (Expr.var 0) (Expr.var 1))
-         (Expr.num 0))
+    (.eq (.add 1 0 (.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 (Expr.add (Expr.var 0) (Expr.var 1))
-         (Expr.num 0))
+    (.le (Poly.add 1 0 (.add 1 1 (.num 0))))
     rfl

tests/lean/run/simp_int_arith.lean

@@ -292,3 +292,49 @@ example (a : Int) : 2+1 ∣ a + a + 1 - a + 1 + a ↔ 3 ∣ 2*a + 2 := by
 
 example (a b : Int) : 6 ∣ a + 21 - a + 3*a + 6*b + 12 ↔ 2 ∣ a + 2*b + 11 := by
   simp +arith
+
+theorem ex3 (a b : Int) : 6 ∣ a + (21 - a) + 3*(a + 2*b) + 12 ↔ 2 ∣ a + 2*b + 11 := by
+  simp +arith
+
+/--
+info: theorem ex3 : ∀ (a b : Int), 6 ∣ a + (21 - a) + 3 * (a + 2 * b) + 12 ↔ 2 ∣ a + 2 * b + 11 :=
+fun a b =>
+  of_eq_true
+    (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))
+            { 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.num 12) }
+            { k := 2, p := Poly.add 1 0 (Poly.add 2 1 (Poly.num 11)) } 3 (Eq.refl true))))
+      (iff_self (2 ∣ a + 2 * b + 11)))
+-/
+#guard_msgs (info) in
+open Lean in open Int.Linear in
+#print ex3
+
+theorem ex4 (a b : Int) : 6 ∣ a + (11 - a) + 3*(a + 2*b) - 11 ↔ 2 ∣ a + 2*b := by
+  simp +arith
+
+/--
+info: theorem ex4 : ∀ (a b : Int), 6 ∣ a + (11 - a) + 3 * (a + 2 * b) - 11 ↔ 2 ∣ a + 2 * b :=
+fun a b =>
+  of_eq_true
+    (Eq.trans
+      (congrArg (fun x => x ↔ 2 ∣ a + 2 * b)
+        (id
+          (RawDvdCnstr.eq_of_isEqv (RArray.branch 1 (RArray.leaf a) (RArray.leaf b))
+            { 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.num 11) }
+            { k := 2, p := Poly.add 1 0 (Poly.add 2 1 (Poly.num 0)) } 3 (Eq.refl true))))
+      (iff_self (2 ∣ a + 2 * b)))
+-/
+#guard_msgs (info) in
+open Lean in open Int.Linear in
+#print ex4