From 747ea91c3af40a95df169bbed44ed6a12e96127b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 15 Feb 2025 14:10:23 -0800 Subject: [PATCH] refactor: add `denote'` functions to `Int/Linear.lean` (#7094) This PR adds the functions `Poly.denote'`, `RelCnstr.denote'`, and `DvdCnstr.denote'`. These functions are useful for representing the denotation of normalized results in `simp +arith` and the `grind` preprocessor. This PR also adjusts all auxiliary normalization theorems to use them to represent the normalized constraints. Previously, we were converting `RelCnstr` and `DvdCnstr` back into raw constraints. While this overhead was reasonable for `simp +arith`, it is not for the cutsat procedure, which has no need for raw constraints. All constraints have already been normalized by the time they reach cutsat. --- src/Init/Data/Int/Linear.lean | 158 ++++++++++++------ .../Meta/Tactic/LinearArith/Int/Basic.lean | 49 +++++- .../Meta/Tactic/LinearArith/Int/Simp.lean | 24 ++- tests/lean/run/liaByRefl.lean | 6 +- tests/lean/run/simp_int_arith.lean | 46 +++++ 5 files changed, 210 insertions(+), 73 deletions(-) diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean index 2b0428916d..7d3d93073e 100644 --- a/src/Init/Data/Int/Linear.lean +++ b/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] diff --git a/src/Lean/Meta/Tactic/LinearArith/Int/Basic.lean b/src/Lean/Meta/Tactic/LinearArith/Int/Basic.lean index f2ffe827ba..7b70b3ef20 100644 --- a/src/Lean/Meta/Tactic/LinearArith/Int/Basic.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/LinearArith/Int/Simp.lean b/src/Lean/Meta/Tactic/LinearArith/Int/Simp.lean index 43e4b3647e..01acee0aaa 100644 --- a/src/Lean/Meta/Tactic/LinearArith/Int/Simp.lean +++ b/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 diff --git a/tests/lean/run/liaByRefl.lean b/tests/lean/run/liaByRefl.lean index 2902c2d02c..6b37c74ffb 100644 --- a/tests/lean/run/liaByRefl.lean +++ b/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 diff --git a/tests/lean/run/simp_int_arith.lean b/tests/lean/run/simp_int_arith.lean index f1860ec54f..15f252c18c 100644 --- a/tests/lean/run/simp_int_arith.lean +++ b/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