From 63cf571553696e648a49beb7c2cfd81f974713bc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 20 Apr 2025 14:49:14 -0700 Subject: [PATCH] feat: add functions for converting ring reified terms back into `Expr` (#8033) This PR adds functions for converting `CommRing` reified terms back into Lean expressions. --- .../Meta/Tactic/Grind/Arith/CommRing.lean | 5 ++ .../Grind/Arith/CommRing/DenoteExpr.lean | 76 +++++++++++++++++++ .../Meta/Tactic/Grind/Arith/CommRing/Eq.lean | 33 ++++++-- .../Tactic/Grind/Arith/CommRing/Proof.lean | 2 - .../Tactic/Grind/Arith/CommRing/Util.lean | 2 +- 5 files changed, 107 insertions(+), 11 deletions(-) create mode 100644 src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean index 5a446357d8..781b2d5c74 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean @@ -14,11 +14,16 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.Var import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify import Lean.Meta.Tactic.Grind.Arith.CommRing.Eq import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof +import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr namespace Lean builtin_initialize registerTraceClass `grind.ring builtin_initialize registerTraceClass `grind.ring.internalize builtin_initialize registerTraceClass `grind.ring.assert +builtin_initialize registerTraceClass `grind.ring.assert.unsat (inherited := true) +builtin_initialize registerTraceClass `grind.ring.assert.trivial (inherited := true) +builtin_initialize registerTraceClass `grind.ring.assert.store (inherited := true) +builtin_initialize registerTraceClass `grind.ring.assert.discard (inherited := true) end Lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean new file mode 100644 index 0000000000..63e2adeaff --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean @@ -0,0 +1,76 @@ +/- +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.Util +import Lean.Meta.Tactic.Grind.Arith.CommRing.Var + +namespace Lean.Meta.Grind.Arith.CommRing +/-! +Helper functions for converting reified terms back into their denotations. +-/ + +private def denoteNum (ring : Ring) (k : Int) : MetaM Expr := do + return mkApp ring.intCastFn (toExpr k) + +def _root_.Lean.Grind.CommRing.Power.denoteExpr' (ring : Ring) (pw : Power) : MetaM Expr := do + let x := ring.vars[pw.x]! + if pw.k == 1 then + return x + else + return mkApp2 ring.powFn x (toExpr pw.k) + +def _root_.Lean.Grind.CommRing.Mon.denoteExpr' (ring : Ring) (m : Mon) : MetaM Expr := do + match m with + | .unit => denoteNum ring 1 + | .mult pw m => go m (← pw.denoteExpr' ring) +where + go (m : Mon) (acc : Expr) : MetaM Expr := do + match m with + | .unit => return acc + | .mult pw m => go m (mkApp2 ring.mulFn acc (← pw.denoteExpr' ring)) + +def _root_.Lean.Grind.CommRing.Poly.denoteExpr' (ring : Ring) (p : Poly) : MetaM Expr := do + match p with + | .num k => denoteNum ring k + | .add k m p => go p (← denoteTerm k m) +where + denoteTerm (k : Int) (m : Mon) : MetaM Expr := do + if k == 1 then + m.denoteExpr' ring + else + return mkApp2 ring.mulFn (← denoteNum ring k) (← m.denoteExpr' ring) + + go (p : Poly) (acc : Expr) : MetaM Expr := do + match p with + | .num 0 => return acc + | .num k => return mkApp2 ring.addFn acc (← denoteNum ring k) + | .add k m p => go p (mkApp2 ring.addFn acc (← denoteTerm k m)) + +def _root_.Lean.Grind.CommRing.Expr.denoteExpr' (ring : Ring) (e : RingExpr) : MetaM Expr := do + go e +where + go : RingExpr → MetaM Expr + | .num k => denoteNum ring k + | .var x => return ring.vars[x]! + | .add a b => return mkApp2 ring.addFn (← go a) (← go b) + | .sub a b => return mkApp2 ring.subFn (← go a) (← go b) + | .mul a b => return mkApp2 ring.mulFn (← go a) (← go b) + | .pow a k => return mkApp2 ring.powFn (← go a) (toExpr k) + | .neg a => return mkApp ring.negFn (← go a) + +def _root_.Lean.Grind.CommRing.Power.denoteExpr (ringId : Nat) (pw : Power) : GoalM Expr := do + pw.denoteExpr' (← getRing ringId) + +def _root_.Lean.Grind.CommRing.Mon.denoteExpr (ringId : Nat) (m : Mon) : GoalM Expr := do + m.denoteExpr' (← getRing ringId) + +def _root_.Lean.Grind.CommRing.Poly.denoteExpr (ringId : Nat) (p : Poly) : GoalM Expr := do + p.denoteExpr' (← getRing ringId) + +def _root_.Lean.Grind.CommRing.Expr.denoteExpr (ringId : Nat) (e : RingExpr) : GoalM Expr := do + e.denoteExpr' (← getRing ringId) + +end Lean.Meta.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Eq.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Eq.lean index 3cdff0b6ac..ab96411cf2 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Eq.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Eq.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura prelude import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof +import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr namespace Lean.Meta.Grind.Arith.CommRing @@ -30,26 +31,42 @@ private def inSameRing? (a b : Expr) : GoalM (Option Nat) := do def processNewEqImpl (a b : Expr) : GoalM Unit := do if isSameExpr a b then return () -- TODO: check why this is needed let some ringId ← inSameRing? a b | return () - trace[grind.ring] "{← mkEq a b}" + trace[grind.ring.assert] "{← mkEq a b}" let some ra ← toRingExpr? ringId a | return () let some rb ← toRingExpr? ringId b | return () - let p ← toPoly ringId (ra.sub rb) + let p ← (ra.sub rb).toPolyM ringId if let .num k := p then - if k != 0 && (← hasChar ringId) then + if k == 0 then + trace[grind.ring.assert.trivial] "{← p.denoteExpr ringId} = 0" + else if (← hasChar ringId) then + trace[grind.ring.assert.unsat] "{← p.denoteExpr ringId} = 0" setEqUnsat ringId k a b ra rb - return () + else + -- Remark: we currently don't do anything if the characteristic is not known. + trace[grind.ring.assert.discard] "{← p.denoteExpr ringId} = 0" + return () + + trace[grind.ring.assert.store] "{← p.denoteExpr ringId} = 0" -- TODO: save equality @[export lean_process_ring_diseq] def processNewDiseqImpl (a b : Expr) : GoalM Unit := do let some ringId ← inSameRing? a b | return () - trace[grind.ring] "{mkNot (← mkEq a b)}" + trace[grind.ring.assert] "{mkNot (← mkEq a b)}" let some ra ← toRingExpr? ringId a | return () let some rb ← toRingExpr? ringId b | return () - let p ← toPoly ringId (ra.sub rb) - if p == .num 0 then - setNeUnsat ringId a b ra rb + let p ← (ra.sub rb).toPolyM ringId + if let .num k := p then + if k == 0 then + trace[grind.ring.assert.unsat] "{← p.denoteExpr ringId} ≠ 0" + setNeUnsat ringId a b ra rb + else + -- Remark: if the characteristic is known, it is trivial. + -- Otherwise, we don't do anything. + trace[grind.ring.assert.trivial] "{← p.denoteExpr ringId} ≠ 0" return () + + trace[grind.ring.assert.store] "{← p.denoteExpr ringId} ≠ 0" -- TODO: save disequalitys end Lean.Meta.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean index 431eddb3a0..c560dda7e3 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean @@ -30,12 +30,10 @@ private def mkLemmaPrefix (ringId : Nat) (declName declNameC : Name) : GoalM Exp return mkApp3 (mkConst declName [ring.u]) ring.type ring.commRingInst ctx def setNeUnsat (ringId : Nat) (a b : Expr) (ra rb : RingExpr) : GoalM Unit := do - trace[grind.ring.assert] "unsat diseq {a}, {b}" let h ← mkLemmaPrefix ringId ``Grind.CommRing.ne_unsat ``Grind.CommRing.ne_unsatC closeGoal <| mkApp4 h (toExpr ra) (toExpr rb) reflBoolTrue (← mkDiseqProof a b) def setEqUnsat (ringId : Nat) (k : Int) (a b : Expr) (ra rb : RingExpr) : GoalM Unit := do - trace[grind.ring.assert] "unsat eq {a}, {b}" let mut h ← mkLemmaPrefix ringId ``Grind.CommRing.eq_unsat ``Grind.CommRing.eq_unsatC let (charInst, c) ← getCharInst ringId if c == 0 then diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean index 6ceaef6947..b8ed266da9 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean @@ -66,7 +66,7 @@ def getCharInst (ringId : Nat) : GoalM (Expr × Nat) := do Converts the given ring expression into a multivariate polynomial. If the ring has a nonzero characteristic, it is used during normalization. -/ -def toPoly (ringId : Nat) (e : RingExpr) : GoalM Poly := do +def _root_.Lean.Grind.CommRing.Expr.toPolyM (ringId : Nat) (e : RingExpr) : GoalM Poly := do if let some c ← nonzeroChar? ringId then return e.toPolyC c else