diff --git a/src/Init/Grind/CommRing.lean b/src/Init/Grind/CommRing.lean index f7bb9cb9b3..2c3c675b8a 100644 --- a/src/Init/Grind/CommRing.lean +++ b/src/Init/Grind/CommRing.lean @@ -9,3 +9,4 @@ import Init.Grind.CommRing.Int import Init.Grind.CommRing.UInt import Init.Grind.CommRing.SInt import Init.Grind.CommRing.BitVec +import Init.Grind.CommRing.Poly diff --git a/src/Init/Grind/CommRing/SOM.lean b/src/Init/Grind/CommRing/Poly.lean similarity index 82% rename from src/Init/Grind/CommRing/SOM.lean rename to src/Init/Grind/CommRing/Poly.lean index bd82b04fc3..f869b3b79c 100644 --- a/src/Init/Grind/CommRing/SOM.lean +++ b/src/Init/Grind/CommRing/Poly.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Init.Data.Nat.Lemmas +import Init.Data.Hashable import Init.Data.Ord import Init.Data.RArray import Init.Grind.CommRing.Basic @@ -41,7 +42,7 @@ def Expr.denote {α} [CommRing α] (ctx : Context α) : Expr → α structure Power where x : Var k : Nat - deriving BEq, Repr + deriving BEq, Repr, Hashable instance : LawfulBEq Power where eq_of_beq {a} := by cases a <;> intro b <;> cases b <;> simp_all! [BEq.beq] @@ -58,14 +59,13 @@ def Power.denote {α} [CommRing α] (ctx : Context α) : Power → α | k => x.denote ctx ^ k inductive Mon where - | leaf (p : Power) - | cons (p : Power) (m : Mon) + | unit + | mult (p : Power) (m : Mon) deriving BEq, Repr instance : LawfulBEq Mon where eq_of_beq {a} := by induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq] - next p₁ p₂ => cases p₁ <;> cases p₂ <;> simp <;> intros <;> simp [*] next p₁ m₁ p₂ m₂ ih => cases p₁ <;> cases p₂ <;> simp <;> intros <;> simp [*] next h => exact ih h @@ -75,45 +75,32 @@ instance : LawfulBEq Mon where assumption def Mon.denote {α} [CommRing α] (ctx : Context α) : Mon → α - | .leaf p => p.denote ctx - | .cons p m => p.denote ctx * denote ctx m - -def Mon.denote' {α} [CommRing α] (ctx : Context α) : Mon → α - | .leaf p => p.denote ctx - | .cons p m => go (p.denote ctx) m -where - go (acc : α) : Mon → α - | .leaf p => acc * p.denote ctx - | .cons p m => go (acc * p.denote ctx) m + | unit => 1 + | .mult p m => p.denote ctx * denote ctx m def Mon.ofVar (x : Var) : Mon := - .leaf { x, k := 1 } + .mult { x, k := 1 } .unit def Mon.concat (m₁ m₂ : Mon) : Mon := match m₁ with - | .leaf p => .cons p m₂ - | .cons p m₁ => .cons p (concat m₁ m₂) + | .unit => m₂ + | .mult pw m₁ => .mult pw (concat m₁ m₂) -def Mon.mulPow (p : Power) (m : Mon) : Mon := +def Mon.mulPow (pw : Power) (m : Mon) : Mon := match m with - | .leaf p' => - bif p.varLt p' then - .cons p m - else bif p'.varLt p then - .cons p' (.leaf p) + | .unit => + .mult pw .unit + | .mult pw' m => + bif pw.varLt pw' then + .mult pw (.mult pw' m) + else bif pw'.varLt pw then + .mult pw' (mulPow pw m) else - .leaf { x := p.x, k := p.k + p'.k } - | .cons p' m => - bif p.varLt p' then - .cons p (.cons p' m) - else bif p'.varLt p then - .cons p' (mulPow p m) - else - .cons { x := p.x, k := p.k + p'.k } m + .mult { x := pw.x, k := pw.k + pw'.k } m def Mon.length : Mon → Nat - | .leaf _ => 1 - | .cons _ m => 1 + length m + | .unit => 0 + | .mult _ m => 1 + length m def hugeFuel := 1000000 @@ -126,19 +113,19 @@ where | 0 => concat m₁ m₂ | fuel + 1 => match m₁, m₂ with - | m₁, .leaf p => m₁.mulPow p - | .leaf p, m₂ => m₂.mulPow p - | .cons p₁ m₁, .cons p₂ m₂ => - bif p₁.varLt p₂ then - .cons p₁ (go fuel m₁ (.cons p₂ m₂)) - else bif p₂.varLt p₁ then - .cons p₂ (go fuel (.cons p₁ m₁) m₂) + | m₁, .unit => m₁ + | .unit, m₂ => m₂ + | .mult pw₁ m₁, .mult pw₂ m₂ => + bif pw₁.varLt pw₂ then + .mult pw₁ (go fuel m₁ (.mult pw₂ m₂)) + else bif pw₂.varLt pw₁ then + .mult pw₂ (go fuel (.mult pw₁ m₁) m₂) else - .cons { x := p₁.x, k := p₁.k + p₂.k } (go fuel m₁ m₂) + .mult { x := pw₁.x, k := pw₁.k + pw₂.k } (go fuel m₁ m₂) def Mon.degree : Mon → Nat - | .leaf p => p.k - | .cons p m => p.k + degree m + | .unit => 0 + | .mult pw m => pw.k + degree m def Var.revlex (x y : Var) : Ordering := bif x.blt y then .gt @@ -155,24 +142,16 @@ def Power.revlex (p₁ p₂ : Power) : Ordering := def Mon.revlexWF (m₁ m₂ : Mon) : Ordering := match m₁, m₂ with - | .leaf p₁, .leaf p₂ => p₁.revlex p₂ - | .leaf p₁, .cons p₂ m₂ => - bif p₁.x.ble p₂.x then - .gt + | .unit, .unit => .eq + | .unit, .mult .. => .gt + | .mult .., .unit => .lt + | .mult pw₁ m₁, .mult pw₂ m₂ => + bif pw₁.x == pw₂.x then + revlexWF m₁ m₂ |>.then (powerRevlex pw₁.k pw₂.k) + else bif pw₁.x.blt pw₂.x then + revlexWF m₁ (.mult pw₂ m₂) |>.then .gt else - revlexWF (.leaf p₁) m₂ |>.then .gt - | .cons p₁ m₁, .leaf p₂ => - bif p₂.x.ble p₁.x then - .lt - else - revlexWF m₁ (.leaf p₂) |>.then .lt - | .cons p₁ m₁, .cons p₂ m₂ => - bif p₁.x == p₂.x then - revlexWF m₁ m₂ |>.then (powerRevlex p₁.k p₂.k) - else bif p₁.x.blt p₂.x then - revlexWF m₁ (.cons p₂ m₂) |>.then .gt - else - revlexWF (.cons p₁ m₁) m₂ |>.then .lt + revlexWF (.mult pw₁ m₁) m₂ |>.then .lt def Mon.revlexFuel (fuel : Nat) (m₁ m₂ : Mon) : Ordering := match fuel with @@ -182,24 +161,16 @@ def Mon.revlexFuel (fuel : Nat) (m₁ m₂ : Mon) : Ordering := revlexWF m₁ m₂ | fuel + 1 => match m₁, m₂ with - | .leaf p₁, .leaf p₂ => p₁.revlex p₂ - | .leaf p₁, .cons p₂ m₂ => - bif p₁.x.ble p₂.x then - .gt + | .unit, .unit => .eq + | .unit, .mult .. => .gt + | .mult .., .unit => .lt + | .mult pw₁ m₁, .mult pw₂ m₂ => + bif pw₁.x == pw₂.x then + revlexFuel fuel m₁ m₂ |>.then (powerRevlex pw₁.k pw₂.k) + else bif pw₁.x.blt pw₂.x then + revlexFuel fuel m₁ (.mult pw₂ m₂) |>.then .gt else - revlexFuel fuel (.leaf p₁) m₂ |>.then .gt - | .cons p₁ m₁, .leaf p₂ => - bif p₂.x.ble p₁.x then - .lt - else - revlexFuel fuel m₁ (.leaf p₂) |>.then .lt - | .cons p₁ m₁, .cons p₂ m₂ => - bif p₁.x == p₂.x then - revlexFuel fuel m₁ m₂ |>.then (powerRevlex p₁.k p₂.k) - else bif p₁.x.blt p₂.x then - revlexFuel fuel m₁ (.cons p₂ m₂) |>.then .gt - else - revlexFuel fuel (.cons p₁ m₁) m₂ |>.then .lt + revlexFuel fuel (.mult pw₁ m₁) m₂ |>.then .lt def Mon.revlex (m₁ m₂ : Mon) : Ordering := revlexFuel hugeFuel m₁ m₂ @@ -255,6 +226,8 @@ where def Poly.insert (k : Int) (m : Mon) (p : Poly) : Poly := bif k == 0 then p + else bif m == .unit then + p.addConst k else go p where @@ -291,6 +264,8 @@ where def Poly.mulMon (k : Int) (m : Mon) (p : Poly) : Poly := bif k == 0 then .num 0 + else bif m == .unit then + p.mulConst k else go p where @@ -347,15 +322,17 @@ def Expr.toPoly : Expr → Poly | .pow a k => match a with | .num n => .num (n^k) - | .var x => Poly.ofMon (.leaf {x, k}) + | .var x => Poly.ofMon (.mult {x, k} .unit) | _ => a.toPoly.pow k /-! **Definitions for the `IsCharP` case** -We considered using a single set of definitions parameterized by `Option c`, but decided against it to avoid -unnecessary kernel‑reduction overhead. Once we can specialize definitions before they reach the kernel, +We considered using a single set of definitions parameterized by `Option c` or simply set `c = 0` since +`n % 0 = n` in Lean, but decided against it to avoid unnecessary kernel‑reduction overhead. +Once we can specialize definitions before they reach the kernel, we can merge the two versions. Until then, the `IsCharP` definitions will carry the `C` suffix. +We use them whenever we can infer the characteristic using type class instance synthesis. -/ def Poly.addConstC (p : Poly) (k : Int) (c : Nat) : Poly := match p with @@ -469,7 +446,7 @@ where | .pow a k => match a with | .num n => .num ((n^k) % c) - | .var x => Poly.ofMon (.leaf {x, k}) + | .var x => Poly.ofMon (.mult {x, k} .unit) | _ => (go a).powC k c /-! @@ -480,25 +457,13 @@ theorem Power.denote_eq {α} [CommRing α] (ctx : Context α) (p : Power) : p.denote ctx = p.x.denote ctx ^ p.k := by cases p <;> simp [Power.denote] <;> split <;> simp [pow_zero, pow_succ, one_mul] -theorem Mon.denote'_go_eq_denote {α} [CommRing α] (ctx : Context α) (a : α) (m : Mon) - : denote'.go ctx a m = a * denote ctx m := by - induction m generalizing a <;> simp [Mon.denote, Mon.denote'.go] - next p' m ih => - simp [Mon.denote] at ih - rw [ih, mul_assoc] - -theorem Mon.denote'_eq_denote {α} [CommRing α] (ctx : Context α) (m : Mon) - : denote' ctx m = denote ctx m := by - cases m <;> simp [Mon.denote, Mon.denote'] - next p m => apply denote'_go_eq_denote - theorem Mon.denote_ofVar {α} [CommRing α] (ctx : Context α) (x : Var) : denote ctx (ofVar x) = x.denote ctx := by - simp [denote, ofVar, Power.denote_eq, pow_succ, pow_zero, one_mul] + simp [denote, ofVar, Power.denote_eq, pow_succ, pow_zero, one_mul, mul_one] theorem Mon.denote_concat {α} [CommRing α] (ctx : Context α) (m₁ m₂ : Mon) : denote ctx (concat m₁ m₂) = m₁.denote ctx * m₂.denote ctx := by - induction m₁ <;> simp [concat, denote, *] + induction m₁ <;> simp [concat, denote, one_mul, *] next p₁ m₁ ih => rw [mul_assoc] private theorem le_of_blt_false {a b : Nat} : a.blt b = false → b ≤ a := by @@ -513,14 +478,7 @@ private theorem eq_of_blt_false {a b : Nat} : a.blt b = false → b.blt a = fals theorem Mon.denote_mulPow {α} [CommRing α] (ctx : Context α) (p : Power) (m : Mon) : denote ctx (mulPow p m) = p.denote ctx * m.denote ctx := by - fun_induction mulPow <;> simp [mulPow, *] - next => simp [denote] - next => simp [denote]; rw [mul_comm] - next p' h₁ h₂ => - have := eq_of_blt_false h₁ h₂ - simp [denote, Power.denote_eq, this, pow_add] - next => simp [denote] - next => simp [denote, mul_assoc, mul_comm, mul_left_comm, *] + fun_induction mulPow <;> simp [mulPow, denote, mul_assoc, mul_comm, mul_left_comm, *] next h₁ h₂ => have := eq_of_blt_false h₁ h₂ simp [denote, Power.denote_eq, pow_add, this, mul_assoc] @@ -529,10 +487,9 @@ theorem Mon.denote_mul {α} [CommRing α] (ctx : Context α) (m₁ m₂ : Mon) : denote ctx (mul m₁ m₂) = m₁.denote ctx * m₂.denote ctx := by unfold mul generalize hugeFuel = fuel - fun_induction mul.go <;> simp [mul.go, denote, denote_concat, denote_mulPow, *] - next => rw [mul_comm] - next => simp [mul_assoc] - next => simp [mul_assoc, mul_left_comm, mul_comm] + fun_induction mul.go + <;> simp [mul.go, denote, denote_concat, denote_mulPow, one_mul, mul_one, + mul_assoc, mul_left_comm, mul_comm, *] next h₁ h₂ _ => have := eq_of_blt_false h₁ h₂ simp [Power.denote_eq, pow_add, mul_assoc, mul_left_comm, mul_comm, this] @@ -561,7 +518,6 @@ private theorem then_eq (o₁ o₂ : Ordering) : o₁.then o₂ = .eq ↔ o₁ = theorem Mon.eq_of_revlexWF {m₁ m₂ : Mon} : m₁.revlexWF m₂ = .eq → m₁ = m₂ := by fun_induction revlexWF <;> simp [revlexWF, *, then_gt, then_lt, then_eq] - next => apply Power.eq_of_revlex next p₁ m₁ p₂ m₂ h ih => cases p₁; cases p₂; intro h₁ h₂; simp [ih h₁, h] simp at h h₂ @@ -570,7 +526,6 @@ theorem Mon.eq_of_revlexWF {m₁ m₂ : Mon} : m₁.revlexWF m₂ = .eq → m₁ theorem Mon.eq_of_revlexFuel {fuel : Nat} {m₁ m₂ : Mon} : revlexFuel fuel m₁ m₂ = .eq → m₁ = m₂ := by fun_induction revlexFuel <;> simp [revlexFuel, *, then_gt, then_lt, then_eq] next => apply eq_of_revlexWF - next => apply Power.eq_of_revlex next p₁ m₁ p₂ m₂ h ih => cases p₁; cases p₂; intro h₁ h₂; simp [ih h₁, h] simp at h h₂ @@ -603,13 +558,17 @@ theorem Poly.denote_insert {α} [CommRing α] (ctx : Context α) (k : Int) (m : simp [insert, cond_eq_if] <;> split next => simp [*, intCast_zero, zero_mul, zero_add] next => - fun_induction insert.go <;> simp_all +zetaDelta [insert.go, denote, cond_eq_if] - next h₁ _ h₂ => - rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, h₂, intCast_zero, zero_mul, zero_add] - next h₁ _ _ => - rw [intCast_add, right_distrib, add_assoc, Mon.eq_of_grevlex h₁] + split + next h => + simp at h <;> simp [*, Mon.denote, denote_addConst, mul_one, add_comm] next => - rw [add_left_comm] + fun_induction insert.go <;> simp_all +zetaDelta [insert.go, denote, cond_eq_if] + next h₁ h₂ => + rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, h₂, intCast_zero, zero_mul, zero_add] + next h₁ _ => + rw [intCast_add, right_distrib, add_assoc, Mon.eq_of_grevlex h₁] + next => + rw [add_left_comm] theorem Poly.denote_concat {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly) : (concat p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by @@ -632,10 +591,14 @@ theorem Poly.denote_mulMon {α} [CommRing α] (ctx : Context α) (k : Int) (m : simp [mulMon, cond_eq_if] <;> split next => simp [denote, *, intCast_zero, zero_mul] next => - fun_induction mulMon.go <;> simp [mulMon.go, denote, *] - next h => simp +zetaDelta at h; simp [*, intCast_zero, mul_zero] - next => simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc] - next => simp [Mon.denote_mul, intCast_mul, left_distrib, mul_comm, mul_left_comm, mul_assoc] + split + next h => + simp at h; simp [*, Mon.denote, mul_one, denote_mulConst] + next => + fun_induction mulMon.go <;> simp [mulMon.go, denote, *] + next h => simp +zetaDelta at h; simp [*, intCast_zero, mul_zero] + next => simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc] + next => simp [Mon.denote_mul, intCast_mul, left_distrib, mul_comm, mul_left_comm, mul_assoc] theorem Poly.denote_combine {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly) : (combine p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by @@ -668,11 +631,9 @@ theorem Expr.denote_toPoly {α} [CommRing α] (ctx : Context α) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by fun_induction toPoly <;> simp [toPoly, denote, Poly.denote, Poly.denote_ofVar, Poly.denote_combine, - Poly.denote_mul, Poly.denote_mulConst, Poly.denote_pow, *] - next => rw [intCast_neg, neg_mul, intCast_one, one_mul] - next => rw [intCast_neg, neg_mul, intCast_one, one_mul, sub_eq_add_neg] - next => rw [intCast_pow] - next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq] + Poly.denote_mul, Poly.denote_mulConst, Poly.denote_pow, intCast_pow, intCast_neg, intCast_one, + neg_mul, one_mul, sub_eq_add_neg, *] + next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq, mul_one] theorem Expr.eq_of_toPoly_eq {α} [CommRing α] (ctx : Context α) (a b : Expr) (h : a.toPoly == b.toPoly) : a.denote ctx = b.denote ctx := by have h := congrArg (Poly.denote ctx) (eq_of_beq h) @@ -789,7 +750,7 @@ theorem Expr.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context next => rw [intCast_neg, neg_mul, intCast_one, one_mul] next => rw [intCast_neg, neg_mul, intCast_one, one_mul, sub_eq_add_neg] next => rw [IsCharP.intCast_emod, intCast_pow] - next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq] + next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq, mul_one] theorem Expr.eq_of_toPolyC_eq {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr) (h : a.toPolyC c == b.toPolyC c) : a.denote ctx = b.denote ctx := by diff --git a/src/Lean/Meta/Tactic/Grind/Arith.lean b/src/Lean/Meta/Tactic/Grind/Arith.lean index 1f4ef22d00..fd95e0a5a7 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith.lean @@ -9,3 +9,4 @@ import Lean.Meta.Tactic.Grind.Arith.Types import Lean.Meta.Tactic.Grind.Arith.Main import Lean.Meta.Tactic.Grind.Arith.Offset import Lean.Meta.Tactic.Grind.Arith.Cutsat +import Lean.Meta.Tactic.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean new file mode 100644 index 0000000000..97ccff2b2a --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean @@ -0,0 +1,7 @@ +/- +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.CommRing.Poly diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean new file mode 100644 index 0000000000..43a54f268c --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean @@ -0,0 +1,75 @@ +/- +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.Grind.CommRing.Poly +namespace Lean.Grind.CommRing + +/-- `lcm m₁ m₂` returns the least common multiple of the given monomials. -/ +def Mon.lcm : Mon → Mon → Mon + | .unit, m₂ => m₂ + | m₁, .unit => m₁ + | .mult pw₁ m₁, .mult pw₂ m₂ => + match compare pw₁.x pw₂.x with + | .eq => .mult { x := pw₁.x, k := max pw₁.k pw₂.k } (lcm m₁ m₂) + | .lt => .mult pw₁ (lcm m₁ (.mult pw₂ m₂)) + | .gt => .mult pw₂ (lcm (.mult pw₁ m₁) m₂) + +/-- +`divides m₁ m₂` returns `true` if monomial `m₁` divides `m₂` +Example: `x^2.z` divides `w.x^3.y^2.z` +-/ +def Mon.divides : Mon → Mon → Bool + | .unit, _ => true + | _, .unit => false + | .mult pw₁ m₁, .mult pw₂ m₂ => + match compare pw₁.x pw₂.x with + | .eq => pw₁.k ≤ pw₂.k && divides m₁ m₂ + | .lt => false + | .gt => divides (.mult pw₁ m₁) m₂ + +/-- +Given `m₁` and `m₂` such that `m₂.divides m₁`, then +`m₁.div m₂` returns the result. +Example `w.x^3.y^2.z` div `x^2.z` returns `w.x.y^2` +-/ +def Mon.div : Mon → Mon → Mon + | m₁, .unit => m₁ + | .unit, _ => .unit -- reachable only if pre-condition does not hold + | .mult pw₁ m₁, .mult pw₂ m₂ => + match compare pw₁.x pw₂.x with + | .eq => + let k := pw₁.k - pw₂.k + if k == 0 then + div m₁ m₂ + else + .mult { x := pw₁.x, k } (div m₁ m₂) + | .lt => .mult pw₁ (div m₁ (.mult pw₂ m₂)) + | .gt => .unit -- reachable only if pre-condition does not hold + +/-- +`coprime m₁ m₂` returns `true` if the given monomials +do not have any variable in common. +-/ +def Mon.coprime : Mon → Mon → Bool + | .unit, _ => true + | _, .unit => true + | .mult pw₁ m₁, .mult pw₂ m₂ => + match compare pw₁.x pw₂.x with + | .eq => false + | .lt => coprime m₁ (.mult pw₂ m₂) + | .gt => coprime (.mult pw₁ m₁) m₂ + +/-- Returns the S-polynomial for `p₁` and `p₂`. -/ +def Poly.superpose (p₁ p₂ : Poly) : Poly := + match p₁, p₂ with + | .add k₁ m₁ p₁, .add k₂ m₂ p₂ => + let m := m₁.lcm m₂ + let p₁ := p₁.mulMon k₂ (m.div m₁) + let p₂ := p₂.mulMon (-k₁) (m.div m₂) + p₁.combine p₂ + | _, _ => .num 0 + +end Lean.Grind.CommRing diff --git a/tests/lean/run/grind_mon_order.lean b/tests/lean/run/grind_mon_order.lean index 587bead987..57956f5644 100644 --- a/tests/lean/run/grind_mon_order.lean +++ b/tests/lean/run/grind_mon_order.lean @@ -1,4 +1,4 @@ -import Init.Grind.CommRing.SOM +import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly open Lean.Grind.CommRing def w : Var := 0 @@ -7,9 +7,9 @@ def y : Var := 2 def z : Var := 3 macro:100 (priority:=high) a:ident "^" k:num : term => `(Power.mk $a $k) -infixr:70 (priority:=high) "." => Mon.cons +infixr:70 (priority:=high) "." => Mon.mult instance : Coe Power Mon where - coe p := Mon.leaf p + coe p := Mon.mult p .unit instance : Coe Var Power where coe x := x^1 @@ -54,3 +54,48 @@ example : check_revlex (z) (w^8) := rfl example : check_revlex (z) (x^100) := rfl example : check_revlex (z^100) (z) := rfl example : check_revlex (x^2 . y^2 . z^5) (x^2 . y^3 . z^4) := rfl + +example : Mon.div (w^2 . y^2 . z) (w^2 . y) = y . z := rfl +example : Mon.div (w^2 . y^2 . z) y = w^2 . y . z := rfl +example : Mon.div (w^2 . y^2 . z) (y^2) = w^2 . z := rfl +example : Mon.div (w^2 . y^4) .unit = w^2 . y^4 := rfl +example : Mon.div (w^2 . y^4) (w^2 . y^4) = .unit := rfl +example : Mon.div (w^2 . y^4) (w^2 . y^5) = .unit := rfl +example : Mon.div (w^5) w = w^4 := rfl +example : Mon.div (w^5 . x^3 . y^2) (w^2 . x) = w^3 . x^2 . y^2 := rfl +example : Mon.div (y^2 . z^3) (y . z) = y . z^2 := rfl +example : Mon.div (x . y) (x . y) = .unit := rfl +example : Mon.div (w . x^2 . y) (w . x . y) = x := rfl + +example : Mon.divides (x^2) (w^5) = false := rfl + +def check_divides (m₁ m₂ : Mon) := + m₂.divides m₁ && (m₁ == m₂ || !m₁.divides m₂) + +example : check_divides (w^5) w := rfl +example : check_divides (w^2 . y^2 . z) (w^2 . y) := rfl +example : check_divides (w^2 . y^2 . z) y := rfl +example : check_divides (w^2 . y^2 . z) (y^2) := rfl +example : check_divides (w^2 . y^4) .unit := rfl +example : check_divides (w^2 . y^4) (w^2 . y^4) := rfl +example : check_divides (w^5) w := rfl +example : check_divides (w^5 . x^3 . y^2) (w^2 . x) := rfl +example : check_divides (x . y) (x . y) := rfl + +#eval Mon.lcm Mon.unit (w^3 . y^2) + +def check_lcm (m₁ m₂ r : Mon) := + m₁.lcm m₁ == m₁ && + m₂.lcm m₂ == m₂ && + m₁.lcm m₂ == r && + m₂.lcm m₁ == r + +example : check_lcm (.unit) (w^3 . y^2) (w^3 . y^2) := by native_decide +example : check_lcm (w^3 . y^2) Mon.unit (w^3 . y^2) := by native_decide +example : check_lcm (w^2) (w^5) (w^5) := by native_decide +example : check_lcm x y (x . y) := by native_decide +example : check_lcm y z (y . z) := by native_decide +example : check_lcm (w^2 . x^3) (w^5 . x . y^2) (w^5 . x^3 . y^2) := by native_decide +example : check_lcm (w . x . y) z (w . x . y . z) := by native_decide +example : check_lcm (x^2 . y^3) (x^2 . y^5) (x^2 . y^5) := by native_decide +example : check_lcm (w^100 . x^2) (x^50 . y) (w^100 . x^50 . y) := by native_decide diff --git a/tests/lean/run/grind_som1.lean b/tests/lean/run/grind_som1.lean index d28d532fa9..e1d4d3b2ea 100644 --- a/tests/lean/run/grind_som1.lean +++ b/tests/lean/run/grind_som1.lean @@ -1,5 +1,4 @@ import Lean -import Init.Grind.CommRing.SOM open Lean.Grind open Lean.Grind.CommRing diff --git a/tests/lean/run/grind_spoly.lean b/tests/lean/run/grind_spoly.lean new file mode 100644 index 0000000000..87859a9cc5 --- /dev/null +++ b/tests/lean/run/grind_spoly.lean @@ -0,0 +1,33 @@ +import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly +open Lean.Grind.CommRing + + +def w : Expr := .var 0 +def x : Expr := .var 1 +def y : Expr := .var 2 +def z : Expr := .var 3 + +instance : Add Expr where + add a b := .add a b +instance : Sub Expr where + sub a b := .sub a b +instance : Neg Expr where + neg a := .neg a +instance : Mul Expr where + mul a b := .mul a b +instance : HPow Expr Nat Expr where + hPow a k := .pow a k +instance : OfNat Expr n where + ofNat := .num n + +def check_spoly (e₁ e₂ r : Expr) : Bool := + e₁.toPoly.superpose e₂.toPoly == r.toPoly && + e₂.toPoly.superpose e₁.toPoly == (-r).toPoly + +example : check_spoly (y^2 - x + 1) (x*y - 1 + y) (-x^2 + y + x - y^2) := by native_decide +example : check_spoly (y - z + 1) (x*y - 1) (-x*z + 1 + x) := by native_decide +example : check_spoly (z^3 - x*y) (z*y - 1) (z^2 - x*y^2) := by native_decide +example : check_spoly (x + 1) (z + 1) (z - x) := by native_decide +example : check_spoly (w^2*x - y) (w*x^2 - z) (-y*x + z*w) := by native_decide +example : check_spoly (2*z^3 - x*y) (3*z*y - 1) (2*z^2 - 3*x*y^2) := by native_decide +example : check_spoly (2*x + 3) (3*z + 1) (9*z - 2*x) := by native_decide