diff --git a/src/Init/Grind/Ordered/Ring.lean b/src/Init/Grind/Ordered/Ring.lean index 490bd0c5c6..cd01ac6ca6 100644 --- a/src/Init/Grind/Ordered/Ring.lean +++ b/src/Init/Grind/Ordered/Ring.lean @@ -236,20 +236,21 @@ instance [Ring R] [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] end Preorder +theorem mul_pos [LE R] [LT R] [IsPreorder R] [OrderedRing R] {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by + simpa [Semiring.zero_mul] using mul_lt_mul_of_pos_right h₁ h₂ + +theorem zero_le_one [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] : (0 : R) ≤ 1 := + Preorder.le_of_lt zero_lt_one + +theorem not_one_lt_zero [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] : ¬ ((1 : R) < 0) := + fun h => Preorder.lt_irrefl (0 : R) (Preorder.lt_trans zero_lt_one h) + section PartialOrder variable [LE R] [LT R] [IsPartialOrder R] [OrderedRing R] -theorem mul_pos {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by - simpa [Semiring.zero_mul] using mul_lt_mul_of_pos_right h₁ h₂ - variable [LawfulOrderLT R] -theorem zero_le_one : (0 : R) ≤ 1 := Preorder.le_of_lt zero_lt_one - -theorem not_one_lt_zero : ¬ ((1 : R) < 0) := - fun h => Preorder.lt_irrefl (0 : R) (Preorder.lt_trans zero_lt_one h) - theorem mul_le_mul_of_nonneg_left {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : c * a ≤ c * b := by rw [PartialOrder.le_iff_lt_or_eq] at h' cases h' with diff --git a/src/Init/Grind/Ring/Basic.lean b/src/Init/Grind/Ring/Basic.lean index ad71182c30..45f16878ba 100644 --- a/src/Init/Grind/Ring/Basic.lean +++ b/src/Init/Grind/Ring/Basic.lean @@ -204,6 +204,11 @@ theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂ theorem pow_add_congr (a r : α) (k k₁ k₂ : Nat) : k = k₁ + k₂ → a^k₁ * a^k₂ = r → a ^ k = r := by intros; subst k r; rw [pow_add] +theorem one_pow (n : Nat) : (1 : α) ^ n = 1 := by + induction n + next => simp [pow_zero] + next => simp [pow_succ, *, mul_one] + theorem natCast_pow (x : Nat) (k : Nat) : ((x ^ k : Nat) : α) = (x : α) ^ k := by induction k next => simp [pow_zero, Nat.pow_zero, natCast_one] @@ -376,6 +381,11 @@ variable {α : Type u} [CommSemiring α] theorem mul_left_comm (a b c : α) : a * (b * c) = b * (a * c) := by rw [← mul_assoc, ← mul_assoc, mul_comm a] +theorem mul_pow (a b : α) (n : Nat) : (a*b)^n = a^n * b^n := by + induction n + next => simp [pow_zero, mul_one] + next n ih => simp [pow_succ, ih, mul_comm, mul_assoc, mul_left_comm] + end CommSemiring open Semiring hiding add_comm add_assoc add_zero diff --git a/src/Init/Grind/Ring/CommSolver.lean b/src/Init/Grind/Ring/CommSolver.lean index 48ca432248..175e83ddd1 100644 --- a/src/Init/Grind/Ring/CommSolver.lean +++ b/src/Init/Grind/Ring/CommSolver.lean @@ -656,6 +656,29 @@ noncomputable def Expr.toPoly_k (e : Expr) : Poly := (k.beq 0)) e +def Mon.degreeOf (m : Mon) (x : Var) : Nat := + match m with + | .unit => 0 + | .mult pw m => bif pw.x == x then pw.k else degreeOf m x + +def Mon.cancelVar (m : Mon) (x : Var) : Mon := + match m with + | .unit => .unit + | .mult pw m => bif pw.x == x then m else .mult pw (cancelVar m x) + +def Poly.cancelVar' (c : Int) (x : Var) (p : Poly) (acc : Poly) : Poly := + match p with + | .num k => acc.addConst k + | .add k m p => + let n := m.degreeOf x + bif n > 0 && c^n ∣ k then + cancelVar' c x p (acc.insert (k / (c^n)) (m.cancelVar x)) + else + cancelVar' c x p (acc.insert k m) + +def Poly.cancelVar (c : Int) (x : Var) (p : Poly) : Poly := + cancelVar' c x p (.num 0) + @[simp] theorem Expr.toPoly_k_eq_toPoly (e : Expr) : e.toPoly_k = e.toPoly := by induction e <;> simp only [toPoly, toPoly_k] next a ih => rw [Poly.mulConst_k_eq_mulConst]; congr @@ -1175,6 +1198,72 @@ theorem Expr.eq_of_toPoly_nc_eq {α} [Ring α] (ctx : Context α) (a b : Expr) ( simp [denote_toPoly_nc] at h assumption +section +attribute [local simp] Semiring.pow_zero Semiring.mul_one Semiring.one_mul cond_eq_ite + +theorem Mon.denote_cancelVar [CommSemiring α] (ctx : Context α) (m : Mon) (x : Var) + : m.denote ctx = x.denote ctx ^ (m.degreeOf x) * (m.cancelVar x).denote ctx := by + fun_induction cancelVar <;> simp [degreeOf] + next h => + simp at h; simp [*, denote, Power.denote_eq] + next h ih => + simp at h; simp [*, denote, Semiring.mul_assoc, CommSemiring.mul_comm, CommSemiring.mul_left_comm] + +theorem Poly.denote_cancelVar' {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Int) (x : Var) (acc : Poly) + : c ≠ 0 → c * x.denote ctx = 1 → (p.cancelVar' c x acc).denote ctx = p.denote ctx + acc.denote ctx := by + intro h₁ h₂ + fun_induction cancelVar' + next acc k => simp [denote_addConst, denote, Semiring.add_comm] + next h ih => + simp [ih, denote_insert, denote] + conv => rhs; rw [Mon.denote_cancelVar (x := x)] + simp [← Semiring.add_assoc] + congr 1 + rw [Semiring.add_comm, Ring.zsmul_eq_intCast_mul,] + congr 1 + simp +zetaDelta [Int.dvd_def] at h + have ⟨d, h⟩ := h.2 + simp +zetaDelta [h] + rw [Int.mul_ediv_cancel_left _ (Int.pow_ne_zero h₁)] + rw [Ring.intCast_mul] + conv => rhs; lhs; rw [CommSemiring.mul_comm] + rw [Semiring.mul_assoc, Ring.intCast_pow] + congr 1 + rw [← Semiring.mul_assoc, ← CommSemiring.mul_pow, h₂, Semiring.one_pow, Semiring.one_mul] + next ih => + simp [ih, denote_insert, denote, Ring.zsmul_eq_intCast_mul, Semiring.add_assoc, + Semiring.add_comm, add_left_comm] + +theorem Poly.denote_cancelVar {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Int) (x : Var) + : c ≠ 0 → c * x.denote ctx = 1 → (p.cancelVar c x).denote ctx = p.denote ctx := by + intro h₁ h₂ + have := denote_cancelVar' ctx p c x (.num 0) h₁ h₂ + rw [cancelVar, this, denote, Ring.intCast_zero, Semiring.add_zero] + +noncomputable def cancel_var_cert (c : Int) (x : Var) (p₁ p₂ : Poly) : Bool := + c != 0 && p₂.beq' (p₁.cancelVar c x) + +theorem eq_cancel_var {α} [CommRing α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly) + : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx = 0 → p₂.denote ctx = 0 := by + simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂ + simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption + +theorem diseq_cancel_var {α} [CommRing α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly) + : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx ≠ 0 → p₂.denote ctx ≠ 0 := by + simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂ + simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption + +theorem le_cancel_var {α} [CommRing α] [LE α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly) + : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx ≤ 0 → p₂.denote ctx ≤ 0 := by + simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂ + simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption + +theorem lt_cancel_var {α} [CommRing α] [LT α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly) + : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx < 0 → p₂.denote ctx < 0 := by + simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂ + simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption + +end /-! Theorems for justifying the procedure for commutative rings with a characteristic in `grind`. -/ @@ -1398,6 +1487,21 @@ theorem mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : P simp [mul_cert]; intro _ h; subst p simp [Poly.denote_mulConst, *, mul_zero] +theorem eq_mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) + : mul_cert p₁ k p → p₁.denote ctx = 0 → p.denote ctx = 0 := by + apply mul + +noncomputable def mul_ne_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool := + k != 0 && (p₁.mulConst_k k |>.beq' p) + +theorem diseq_mul {α} [CommRing α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) + : mul_ne_cert p₁ k p → p₁.denote ctx ≠ 0 → p.denote ctx ≠ 0 := by + simp [mul_ne_cert]; intro h₁ _ h₂; subst p + simp [Poly.denote_mulConst]; intro h₃ + rw [← zsmul_eq_intCast_mul] at h₃ + have := no_int_zero_divisors h₁ h₃ + contradiction + theorem inv {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (p : Poly) : mul_cert p₁ (-1) p → p₁.denote ctx = 0 → p.denote ctx = 0 := mul ctx p₁ (-1) p @@ -1608,6 +1712,16 @@ theorem le_int_module {α} [CommRing α] [LE α] (ctx : Context α) (p : Poly) : p.denote ctx ≤ 0 → p.denoteAsIntModule ctx ≤ 0 := by simp [Poly.denoteAsIntModule_eq_denote] +noncomputable def mul_ineq_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool := + k > 0 && (p₁.mulConst_k k |>.beq' p) + +theorem le_mul {α} [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) + : mul_ineq_cert p₁ k p → p₁.denote ctx ≤ 0 → p.denote ctx ≤ 0 := by + simp [mul_ineq_cert]; intro h₁ _ h₂; subst p; simp [Poly.denote_mulConst] + replace h₂ := zsmul_nonpos (Int.le_of_lt h₁) h₂ + simp [Ring.zsmul_eq_intCast_mul] at h₂ + assumption + theorem lt_norm {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : core_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denote ctx < 0 := by simp [core_cert]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote] @@ -1619,6 +1733,13 @@ theorem lt_int_module {α} [CommRing α] [LT α] (ctx : Context α) (p : Poly) : p.denote ctx < 0 → p.denoteAsIntModule ctx < 0 := by simp [Poly.denoteAsIntModule_eq_denote] +theorem lt_mul {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) + : mul_ineq_cert p₁ k p → p₁.denote ctx < 0 → p.denote ctx < 0 := by + simp [mul_ineq_cert]; intro h₁ _ h₂; subst p; simp [Poly.denote_mulConst] + replace h₂ := zsmul_neg_iff k h₂ |>.mpr h₁ + simp [Ring.zsmul_eq_intCast_mul] at h₂ + assumption + theorem not_le_norm {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote ctx < 0 := by simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote] @@ -1642,6 +1763,13 @@ theorem inv_int_eq [Field α] [IsCharP α 0] (b : Int) : b != 0 → (denoteInt b have := IsCharP.intCast_eq_zero_iff (α := α) 0 b; simp [*] at this rw [Field.mul_inv_cancel this] +theorem intCast_eq_denoteInt [Field α] (b : Int) : (IntCast.intCast b : α) = denoteInt b := by + simp [denoteInt_eq] + +theorem inv_int_eq' [Field α] [IsCharP α 0] (b : Int) : b != 0 → (IntCast.intCast b : α) * (denoteInt b)⁻¹ = 1 := by + rw [intCast_eq_denoteInt] + apply inv_int_eq + theorem inv_int_eqC {α c} [Field α] [IsCharP α c] (b : Int) : b % c != 0 → (denoteInt b : α) * (denoteInt b)⁻¹ = 1 := by simp; intro h have : (denoteInt b : α) ≠ 0 := by diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean index 5e0a454131..69726f7b7a 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean @@ -274,4 +274,12 @@ where | .num k => .add acc (.num k) | .add k m p => go p (.add acc (goTerm k m)) +def Poly.maxDegreeOf (p : Poly) (x : Var) : Nat := + go p 0 +where + go (p : Poly) (max : Nat) : Nat := + match p with + | .num _ => max + | .add _ m p => go p (Nat.max max (m.degreeOf x)) + end Lean.Grind.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean index 6cb6eec636..00f8f6cb0b 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean @@ -115,4 +115,23 @@ def _root_.Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) : RingM Grind.CommR return { spol, m₁, m₂, k₁ := c₁, k₂ := c₂ } | _, _ => return {} +/-- Returns `some (val, x)` if `m` contains a variable `x` whose the denotation is `val⁻¹`. -/ +def _root_.Lean.Grind.CommRing.Mon.findInvNumeralVar? (m : Mon) : RingM (Option (Nat × Var)) := do + match m with + | .unit => return none + | .mult pw m => + let e := (← getRing).vars[pw.x]! + let_expr Inv.inv _ _ a := e | m.findInvNumeralVar? + let_expr OfNat.ofNat _ n _ := a | m.findInvNumeralVar? + let some n ← getNatValue? n | m.findInvNumeralVar? + return some (n, pw.x) + +/-- Returns `some (val, x)` if `p` contains a variable `x` whose the denotation is `val⁻¹`. -/ +def _root_.Lean.Grind.CommRing.Poly.findInvNumeralVar? (p : Poly) : RingM (Option (Nat × Var)) := do + match p with + | .num _ => return none + | .add _ m p => + let some r ← m.findInvNumeralVar? | p.findInvNumeralVar? + return some r + end Lean.Meta.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Den.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Den.lean new file mode 100644 index 0000000000..1254c56f0e --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Den.lean @@ -0,0 +1,43 @@ +/- +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 +-/ +module +prelude +public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM +import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify +import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr +import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly +namespace Lean.Meta.Grind.Arith.Linear + +partial def cleanupDenominators' (c : α) + (getPoly : α → CommRing.Poly) + (updateCnstr : α → CommRing.Poly → Int → Var → Nat → α) + : LinearM α := do + let s ← getStruct + if s.fieldInst?.isNone then return c + let some (_, char) := s.charInst? | return c + unless char == 0 do return c + withRingM <| go c +where + go (c : α) : CommRing.RingM α := do + let p := getPoly c + let some (val, x) ← p.findInvNumeralVar? | return c + let n := p.maxDegreeOf x + let p := p.mulConst (val ^ n) + let p := p.cancelVar val x + go (updateCnstr c p val x n) + +public def RingIneqCnstr.cleanupDenominators (c : RingIneqCnstr) : LinearM RingIneqCnstr := + cleanupDenominators' c (·.p) fun c p val x n => { c with p, h := .cancelDen c val x n } + +public def RingEqCnstr.cleanupDenominators (c : RingEqCnstr) : LinearM RingEqCnstr := + cleanupDenominators' c (·.p) fun c p val x n => { c with p, h := .cancelDen c val x n } + +public def RingDiseqCnstr.cleanupDenominators (c : RingDiseqCnstr) : LinearM RingDiseqCnstr := do + let s ← getStruct + if s.noNatDivInst?.isNone then return c + cleanupDenominators' c (·.p) fun c p val x n => { c with p, h := .cancelDen c val x n } + +end Lean.Meta.Grind.Arith.Linear diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean index 73a819e0c0..2c62c8543b 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean @@ -8,6 +8,7 @@ prelude public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr +import Lean.Meta.Tactic.Grind.Arith.Linear.Den import Lean.Meta.Tactic.Grind.Arith.Linear.Var import Lean.Meta.Tactic.Grind.Arith.Linear.StructId import Lean.Meta.Tactic.Grind.Arith.Linear.Reify @@ -48,6 +49,8 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue : if eqTrue then let p := (lhs.sub rhs).toPoly let c : RingIneqCnstr := { p, strict, h := .core e lhs rhs } + let c ← c.cleanupDenominators + let p := c.p let lhs ← p.toIntModuleExpr generation let some lhs ← reify? lhs (skipVar := false) generation | return () let p := lhs.norm @@ -57,6 +60,8 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue : let p := (rhs.sub lhs).toPoly let strict := !strict let c : RingIneqCnstr := { p, strict, h := .notCore e lhs rhs } + let c ← c.cleanupDenominators + let p := c.p let lhs ← p.toIntModuleExpr generation let some lhs ← reify? lhs (skipVar := false) generation | return () let p := lhs.norm diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean index 9fea50d7d1..e122dc75e1 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean @@ -204,6 +204,14 @@ private def mkCommRingThmPrefix (declName : Name) : ProofM Expr := do let s ← getStruct return mkApp3 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getRingContext) +/-- +Returns the prefix of a theorem with name `declName` where the first four arguments are +`{α} [CommRing α] [NoNatZeroDivisors α] (rctx : Context α)` +-/ +private def mkCommRingNoNatDivThmPrefix (declName : Name) : ProofM Expr := do + let s ← getStruct + return mkApp4 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getNoNatDivInst) (← getRingContext) + /-- Returns the prefix of a theorem with name `declName` where the first four arguments are `{α} [CommRing α] [LE α] (rctx : Context α)` @@ -244,6 +252,14 @@ private def mkCommRingLinOrdThmPrefix (declName : Name) : ProofM Expr := do let s ← getStruct return mkApp8 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLEInst) (← getLTInst) (← getLawfulOrderLTInst) (← getIsLinearOrderInst) (← getOrderedRingInst) (← getRingContext) +/-- +Returns the prefix of a theorem with name `declName` where the first three arguments are +`{α} [Field α] [IsCharP α 0]` +-/ +private def mkFieldChar0ThmPrefix (declName : Name) : ProofM Expr := do + let s ← getStruct + return mkApp3 (mkConst declName [s.u]) s.type s.fieldInst?.get! s.charInst?.get!.1 + partial def RingIneqCnstr.toExprProof (c' : RingIneqCnstr) : ProofM Expr := do match c'.h with | .core e lhs rhs => @@ -252,6 +268,20 @@ partial def RingIneqCnstr.toExprProof (c' : RingIneqCnstr) : ProofM Expr := do | .notCore e lhs rhs => let h' ← mkCommRingLinOrdThmPrefix (if c'.strict then ``Grind.CommRing.not_le_norm else ``Grind.CommRing.not_lt_norm) return mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl c'.p) eagerReflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e)) + | .cancelDen c val x n => + let h ← if c.strict then + mkCommRingLawfulPreOrdThmPrefix ``Grind.CommRing.lt_mul + else + mkCommRingPreOrdThmPrefix ``Grind.CommRing.le_mul + let p₁ := c.p.mulConst (val^n) + let p₁ ← mkRingPolyDecl p₁ + let h := mkApp5 h (← mkRingPolyDecl c.p) (toExpr (val^n)) p₁ eagerReflBoolTrue (← c.toExprProof) + let h_eq_one := mkApp2 (← mkFieldChar0ThmPrefix ``Grind.CommRing.inv_int_eq') (toExpr val) eagerReflBoolTrue + let h' ← if c.strict then + mkCommRingLTThmPrefix ``Grind.CommRing.lt_cancel_var + else + mkCommRingLEThmPrefix ``Grind.CommRing.le_cancel_var + return mkApp7 h' (toExpr val) (toExpr x) p₁ (← mkRingPolyDecl c'.p) eagerReflBoolTrue h_eq_one h partial def RingEqCnstr.toExprProof (c' : RingEqCnstr) : ProofM Expr := do match c'.h with @@ -262,12 +292,28 @@ partial def RingEqCnstr.toExprProof (c' : RingEqCnstr) : ProofM Expr := do let h ← c.toExprProof let h' ← mkCommRingThmPrefix ``Grind.CommRing.Stepwise.inv return mkApp4 h' (← mkRingPolyDecl c.p) (← mkRingPolyDecl c'.p) eagerReflBoolTrue h + | .cancelDen c val x n => + let h ← mkCommRingThmPrefix ``Grind.CommRing.Stepwise.eq_mul + let p₁ := c.p.mulConst (val^n) + let p₁ ← mkRingPolyDecl p₁ + let h := mkApp5 h (← mkRingPolyDecl c.p) (toExpr (val^n)) p₁ eagerReflBoolTrue (← c.toExprProof) + let h_eq_one := mkApp2 (← mkFieldChar0ThmPrefix ``Grind.CommRing.inv_int_eq') (toExpr val) eagerReflBoolTrue + let h' ← mkCommRingThmPrefix ``Grind.CommRing.eq_cancel_var + return mkApp7 h' (toExpr val) (toExpr x) p₁ (← mkRingPolyDecl c'.p) eagerReflBoolTrue h_eq_one h partial def RingDiseqCnstr.toExprProof (c' : RingDiseqCnstr) : ProofM Expr := do match c'.h with | .core a b lhs rhs => let h' ← mkCommRingThmPrefix ``Grind.CommRing.diseq_norm return mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl c'.p) eagerReflBoolTrue (← mkDiseqProof a b) + | .cancelDen c val x n => + let h ← mkCommRingNoNatDivThmPrefix ``Grind.CommRing.Stepwise.diseq_mul + let p₁ := c.p.mulConst (val^n) + let p₁ ← mkRingPolyDecl p₁ + let h := mkApp5 h (← mkRingPolyDecl c.p) (toExpr (val^n)) p₁ eagerReflBoolTrue (← c.toExprProof) + let h_eq_one := mkApp2 (← mkFieldChar0ThmPrefix ``Grind.CommRing.inv_int_eq') (toExpr val) eagerReflBoolTrue + let h' ← mkCommRingThmPrefix ``Grind.CommRing.diseq_cancel_var + return mkApp7 h' (toExpr val) (toExpr x) p₁ (← mkRingPolyDecl c'.p) eagerReflBoolTrue h_eq_one h mutual partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean index 0a2aab9d35..9c6ce7c139 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean @@ -8,6 +8,7 @@ prelude public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr +import Lean.Meta.Tactic.Grind.Arith.Linear.Den import Lean.Meta.Tactic.Grind.Arith.Linear.Var import Lean.Meta.Tactic.Grind.Arith.Linear.StructId import Lean.Meta.Tactic.Grind.Arith.Linear.Reify @@ -56,6 +57,8 @@ private def processNewCommRingEq' (a b : Expr) : LinearM Unit := do let generation := max (← getGeneration a) (← getGeneration b) let p := (lhs.sub rhs).toPoly let c : RingEqCnstr := { p, h := .core a b lhs rhs } + let c ← c.cleanupDenominators + let p := c.p let lhs ← p.toIntModuleExpr generation let some lhs ← reify? lhs (skipVar := false) generation | return () let p := lhs.norm @@ -274,6 +277,8 @@ private def processNewCommRingDiseq (a b : Expr) : LinearM Unit := do let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return () let p := (lhs.sub rhs).toPoly let c : RingDiseqCnstr := { p, h := .core a b lhs rhs } + let c ← c.cleanupDenominators + let p := c.p let generation := max (← getGeneration a) (← getGeneration b) let lhs ← p.toIntModuleExpr generation let some lhs ← reify? lhs (skipVar := false) generation | return () diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean index 9aac961fc8..a1bf0a01c0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean @@ -28,7 +28,7 @@ structure RingIneqCnstr where inductive RingIneqCnstrProof where | core (e : Expr) (lhs rhs : Grind.CommRing.Expr) | notCore (e : Expr) (lhs rhs : Grind.CommRing.Expr) - -- **TODO**: cleanup denominator proof step + | cancelDen (c : RingIneqCnstr) (val : Int) (x : Var) (n : Var) end mutual @@ -40,7 +40,7 @@ structure RingEqCnstr where inductive RingEqCnstrProof where | core (a b : Expr) (ra rb : Grind.CommRing.Expr) | symm (c : RingEqCnstr) - -- **TODO**: cleanup denominator proof step + | cancelDen (c : RingEqCnstr) (val : Int) (x : Var) (n : Var) end mutual @@ -51,7 +51,7 @@ structure RingDiseqCnstr where inductive RingDiseqCnstrProof where | core (a b : Expr) (ra rb : Grind.CommRing.Expr) - -- **TODO**: cleanup denominator proof step + | cancelDen (c : RingDiseqCnstr) (val : Int) (x : Var) (n : Var) end mutual diff --git a/tests/lean/grind/algebra/linarith_field.lean b/tests/lean/grind/algebra/linarith_field.lean deleted file mode 100644 index 29b23b1a5c..0000000000 --- a/tests/lean/grind/algebra/linarith_field.lean +++ /dev/null @@ -1,14 +0,0 @@ -open Std Lean.Grind - -variable {α : Type} [Field α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] - -example (a b : α) (h : a < b / 2) : 2 * a < b := by grind -example (a b : α) (h : a < b / 2) : a + a < b := by grind -example (a b : α) (h : a < b / 2) : 2 * a ≤ b := by grind -example (a b : α) (h : a < b / 2) : a + a ≤ b := by grind -example (a b : α) (h : a ≤ b / 2) : 2 * a ≤ b := by grind -example (a b : α) (h : a ≤ b / 2) : a + a ≤ b := by grind - -example (a b : α) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind - -example (a b : α) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind diff --git a/tests/lean/run/grind_clean_den.lean b/tests/lean/run/grind_clean_den.lean new file mode 100644 index 0000000000..a8de0236de --- /dev/null +++ b/tests/lean/run/grind_clean_den.lean @@ -0,0 +1,41 @@ +open Std Lean.Grind + +section +variable {α : Type} [Field α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] + +example (a b : α) (h : a < b * (3⁻¹)^2) : 9 * a < b := by grind +example (a b : α) (h : a ≤ b * (3⁻¹)^2) : 9 * a ≤ b := by grind +example (a b : α) (h : a < b / 2) : 2 * a < b := by grind +example (a b : α) (h : a < b / 2) : a + a < b := by grind +example (a b : α) (h : a < b / 2) : 2 * a ≤ b := by grind +example (a b : α) (h : a < b / 2) : a + a ≤ b := by grind +example (a b : α) (h : a ≤ b / 2) : 2 * a ≤ b := by grind +example (a b : α) (h : a ≤ b / 2) : a + a ≤ b := by grind +example (a b : α) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind +example (a b : α) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind + +example (a b : α) (h : a = b * (3⁻¹)^2) : 9 * a ≤ b := by grind +example (a b : α) (h : a = b / 2) : a + a ≤ b := by grind +example (a b : α) (h : a ≠ b) : a < b ∨ a > b := by grind +variable [NoNatZeroDivisors α] +example (a b : α) (h : a ≠ b * (3⁻¹)^2) : 9 * a < b ∨ 9 * a > b := by grind +example (a b : α) (h : a / 2 ≠ b / 9) : 9 * a < 2 * b ∨ 9 * a > 2 * b := by grind + +example (a b : α) (h : a < b / (2^2 - 3/2 + -1 + 1/2)) : 2 * a < b := by grind + +end + +example (a b : Rat) (h : a < b * (3⁻¹)^2) : 9 * a < b := by grind +example (a b : Rat) (h : a ≤ b * (3⁻¹)^2) : 9 * a ≤ b := by grind +example (a b : Rat) (h : a < b / 2) : 2 * a < b := by grind +example (a b : Rat) (h : a < b / 2) : a + a < b := by grind +example (a b : Rat) (h : a < b / 2) : 2 * a ≤ b := by grind +example (a b : Rat) (h : a < b / 2) : a + a ≤ b := by grind +example (a b : Rat) (h : a ≤ b / 2) : 2 * a ≤ b := by grind +example (a b : Rat) (h : a ≤ b / 2) : a + a ≤ b := by grind +example (a b : Rat) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind +example (a b : Rat) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind +example (a b : Rat) (h : a = b * (3⁻¹)^2) : 9 * a ≤ b := by grind +example (a b : Rat) (h : a = b / 2) : a + a ≤ b := by grind +example (a b : Rat) (h : a ≠ b * (3⁻¹)^2) : 9 * a < b ∨ 9 * a > b := by grind +example (a b : Rat) (h : a / 2 ≠ b / 9) : 9 * a < 2 * b ∨ 9 * a > 2 * b := by grind