feat: proof terms generation for CommRing and linarith interface (#8689)

This PR implements proof term generation for the `CommRing` and
`linarith` interface. It also fixes the `CommRing` helper theorems.

src/Init/Grind/CommRing/Poly.lean

@@ -1178,31 +1178,31 @@ theorem lt_norm {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Cont
   assumption
 
 theorem not_le_norm {α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (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]
+    : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx < 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
   replace h₁ := LinearOrder.lt_of_not_le h₁
   replace h₁ := add_lt_left h₁ (-lhs.denote ctx)
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
 theorem not_lt_norm {α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (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]
+    : core_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
   replace h₁ := LinearOrder.le_of_not_lt h₁
   replace h₁ := add_le_left h₁ (-lhs.denote ctx)
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
 theorem not_le_norm' {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (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]; intro h
+    : core_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denoteAsIntModule ctx ≤ 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
   replace h := add_le_right (rhs.denote ctx) h
   rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h
   contradiction
 
 theorem not_lt_norm' {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (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]; intro h
+    : core_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denoteAsIntModule ctx < 0 := by
+  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
   replace h := add_lt_right (rhs.denote ctx) h
   rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h
   contradiction

src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.Linear.Util
 import Lean.Meta.Tactic.Grind.Arith.Linear.Var
 
@@ -86,18 +87,6 @@ where
 def _root_.Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Grind.CommRing.Poly) : LinearM Expr := do
   match p with
   | .num k => denoteNum k
-  | .add k m p => go p (← denoteTerm k m)
-where
-  denoteTerm (k : Int) (m : Grind.CommRing.Mon) : LinearM Expr := do
-    if k == 1 then
-      m.denoteAsIntModuleExpr
-    else
-      return mkApp2 (← getStruct).hmulFn (mkIntLit k) (← m.denoteAsIntModuleExpr)
-
-  go (p : Grind.CommRing.Poly) (acc : Expr) : LinearM Expr := do
-    match p with
-    | .num 0 => return acc
-    | .num k => return mkApp2 (← getStruct).addFn acc (← denoteNum k)
-    | .add k m p => go p (mkApp2 (← getStruct).addFn acc (← denoteTerm k m))
+  | .add k m p => return mkApp2 (← getStruct).addFn (mkApp2 (← getRing).mulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p)
 
 end Lean.Meta.Grind.Arith.Linear

src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean

@@ -50,7 +50,7 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue :
     let lhs' ← p'.denoteAsIntModuleExpr
     let some lhs' ← reify? lhs' (skipVar := false) | return ()
     let p := lhs'.norm
-    let c : IneqCnstr := { p, strict, h := .coreCommRing e lhs rhs lhs' }
+    let c : IneqCnstr := { p, strict, h := .coreCommRing e lhs rhs p' lhs' }
     c.assert
   else if (← isLinearOrder) then
     let p' := (rhs.sub lhs).toPoly
@@ -58,7 +58,7 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue :
     let lhs' ← p'.denoteAsIntModuleExpr
     let some lhs' ← reify? lhs' (skipVar := false) | return ()
     let p := lhs'.norm
-    let c : IneqCnstr := { p, strict, h := .notCoreCommRing e lhs rhs lhs' }
+    let c : IneqCnstr := { p, strict, h := .notCoreCommRing e lhs rhs p' lhs' }
     c.assert
   else
     let p' := (lhs.sub rhs).toPoly

src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean

@@ -43,6 +43,7 @@ structure ProofM.State where
   cache       : Std.HashMap UInt64 Expr := {}
   polyMap     : Std.HashMap Poly Expr := {}
   exprMap     : Std.HashMap LinExpr Expr := {}
+  ringPolyMap : Std.HashMap CommRing.Poly Expr := {}
   ringExprMap : Std.HashMap RingExpr Expr := {}
 
 structure ProofM.Context where
@@ -86,6 +87,13 @@ def mkExprDecl (e : LinExpr) : ProofM Expr := do
   modify fun s => { s with exprMap := s.exprMap.insert e x }
   return x
 
+def mkRingPolyDecl (p : CommRing.Poly) : ProofM Expr := do
+  if let some x := (← get).ringPolyMap[p]? then
+    return x
+  let x := mkFVar (← mkFreshFVarId)
+  modify fun s => { s with ringPolyMap := s.ringPolyMap.insert p x }
+  return x
+
 def mkRingExprDecl (e : RingExpr) : ProofM Expr := do
   if let some x := (← get).ringExprMap[e]? then
     return x
@@ -103,7 +111,8 @@ where
     let h ← x
     let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.Linarith.Poly) toExpr
     let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.Linarith.Expr) toExpr
-    let h ← mkLetOfMap (← get).ringExprMap h `r (mkConst ``Grind.CommRing.Expr) toExpr
+    let h ← mkLetOfMap (← get).ringPolyMap h `rp (mkConst ``Grind.CommRing.Poly) toExpr
+    let h ← mkLetOfMap (← get).ringExprMap h `re (mkConst ``Grind.CommRing.Expr) toExpr
     mkLetFVars #[(← getContext), (← getRingContext)] h
 
 /--
@@ -131,6 +140,31 @@ private def mkIntModPreOrdThmPrefix (declName : Name) : ProofM Expr := do
   let s ← getStruct
   return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst s.preorderInst s.isOrdInst (← getContext)
 
+/--
+Returns the prefix of a theorem with name `declName` where the first five arguments are
+`{α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α)`
+This is the most common theorem prefix at `Linarith.lean`
+-/
+private def mkIntModLinOrdThmPrefix (declName : Name) : ProofM Expr := do
+  let s ← getStruct
+  return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst (← getLinearOrderInst) s.isOrdInst (← getContext)
+
+/--
+Returns the prefix of a theorem with name `declName` where the first five arguments are
+`{α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (rctx : Context α)`
+-/
+private def mkCommRingPreOrdThmPrefix (declName : Name) : ProofM Expr := do
+  let s ← getStruct
+  return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) s.preorderInst (← getRingIsOrdInst) (← getRingContext)
+
+/--
+Returns the prefix of a theorem with name `declName` where the first five arguments are
+`{α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (rctx : Context α)`
+-/
+private def mkCommRingLinOrdThmPrefix (declName : Name) : ProofM Expr := do
+  let s ← getStruct
+  return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLinearOrderInst) (← getRingIsOrdInst) (← getRingContext)
+
 mutual
 partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
   throwError "NIY"
@@ -140,6 +174,19 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d
   | .core e lhs rhs =>
     let h ← mkIntModPreOrdThmPrefix (if c'.strict then ``Grind.Linarith.lt_norm else ``Grind.Linarith.le_norm)
     return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) reflBoolTrue (mkOfEqTrueCore e (← mkEqTrueProof e))
+  | .notCore e lhs rhs =>
+    let h ← mkIntModLinOrdThmPrefix (if c'.strict then ``Grind.Linarith.not_le_norm else ``Grind.Linarith.not_lt_norm)
+    return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) reflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e))
+  | .coreCommRing e lhs rhs p' lhs' =>
+    let h' ← mkCommRingPreOrdThmPrefix (if c'.strict then ``Grind.CommRing.lt_norm else ``Grind.CommRing.le_norm)
+    let h' := mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl p') reflBoolTrue (mkOfEqTrueCore e (← mkEqTrueProof e))
+    let h ← mkIntModPreOrdThmPrefix (if c'.strict then ``Grind.Linarith.lt_norm else ``Grind.Linarith.le_norm)
+    return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) reflBoolTrue h'
+  | .notCoreCommRing e lhs rhs p' lhs' =>
+    let h' ← mkCommRingLinOrdThmPrefix (if c'.strict then ``Grind.CommRing.not_le_norm else ``Grind.CommRing.not_lt_norm)
+    let h' := mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl p') reflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e))
+    let h ← mkIntModPreOrdThmPrefix (if c'.strict then ``Grind.Linarith.lt_norm else ``Grind.Linarith.le_norm)
+    return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) reflBoolTrue h'
   | _ => throwError "NIY"
 
 partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do

src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean

@@ -40,8 +40,8 @@ structure IneqCnstr where
 inductive IneqCnstrProof where
   | core (e : Expr) (lhs rhs : LinExpr)
   | notCore (e : Expr) (lhs rhs : LinExpr)
-  | coreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (lhs' : LinExpr)
-  | notCoreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (lhs' : LinExpr)
+  | coreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr)
+  | notCoreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr)
   | combine (c₁ : IneqCnstr) (c₂ : IneqCnstr)
   | combineEq (c₁ : IneqCnstr) (c₂ : EqCnstr)
   | norm (c₁ : IneqCnstr) (k : Nat)

src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean

@@ -104,6 +104,21 @@ def setTermStructId (e : Expr) : LinearM Unit := do
     return ()
   modify' fun s => { s with exprToStructId := s.exprToStructId.insert { expr := e } structId }
 
+def getLinearOrderInst : LinearM Expr := do
+  let some inst := (← getStruct).linearInst?
+    | throwError "`grind linarith` internal error, structure is not a linear order"
+  return inst
+
+def getCommRingInst : LinearM Expr := do
+  let some inst := (← getStruct).commRingInst?
+    | throwError "`grind linarith` internal error, structure is not a commutative ring"
+  return inst
+
+def getRingIsOrdInst : LinearM Expr := do
+  let some inst := (← getStruct).ringIsOrdInst?
+    | throwError "`grind linarith` internal error, structure is not an ordered ring"
+  return inst
+
 /--
 Tries to evaluate the polynomial `p` using the partial model/assignment built so far.
 The result is `none` if the polynomial contains variables that have not been assigned.

tests/lean/run/grind_linarith_1.lean

@@ -14,3 +14,24 @@ example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)
     : (2:Int)*a + b < b + a + a → False := by
   fail_if_success grind -linarith
   grind
+
+example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b : α)
+    : (2:Int)*a + b ≥ b + a + a := by
+  grind
+
+#guard_msgs (drop error) in
+example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)
+    : (2:Int)*a + b ≥ b + a + a := by
+  fail_if_success grind
+
+example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+    : 2*a + b < b + a + a → False := by
+  grind
+
+example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+    : 2 + 2*a + b + 1 < b + a + a + 3 → False := by
+  grind
+
+example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α)
+    : 2 + 2*a + b + 1 <= b + a + a + 3 := by
+  grind