feat: One.one support in linarith (#8694)

This PR implements special support for `One.one` in linarith when the
structure is a ordered ring. It also fixes bugs during initialization.

src/Init/Grind/Ordered/Linarith.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 import Init.Grind.Ordered.Module
+import Init.Grind.Ordered.Ring
 import all Init.Data.Ord
 import all Init.Data.AC
 import Init.Data.RArray
@@ -450,6 +451,14 @@ theorem lt_unsat {α} [IntModule α] [Preorder α] (ctx : Context α) : (Poly.ni
   have := Preorder.lt_iff_le_not_le.mp h
   simp at this
 
+def zero_lt_one_cert (p : Poly) : Bool :=
+  p == .add (-1) 0 .nil
+
+theorem zero_lt_one {α} [Ring α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (p : Poly)
+    : zero_lt_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx < 0 := by
+  simp [zero_lt_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one, neg_hmul]
+  rw [neg_lt_iff, neg_zero]; apply Ring.IsOrdered.zero_lt_one
+
 /-!
 Coefficient normalization
 -/

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

@@ -102,7 +102,7 @@ def propagateIneq (e : Expr) (eqTrue : Bool) : GoalM Unit := do
       return ()
     let lhs := e.getArg! 2 numArgs
     let rhs := e.getArg! 3 numArgs
-    if (← isCommRing) then
+    if (← isOrderedCommRing) then
       propagateCommRingIneq e lhs rhs strict eqTrue
     -- TODO: non-commutative ring normalizer
     else

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

@@ -196,6 +196,10 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d
       | false, false => (``Grind.Linarith.le_le_combine, c₁, c₂)
     return mkApp6 (← mkIntModPreOrdThmPrefix declName) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p) reflBoolTrue
       (← c₁.toExprProof) (← c₂.toExprProof)
+  | .oneGtZero =>
+    let s ← getStruct
+    let h := mkApp5 (mkConst ``Grind.Linarith.zero_lt_one [s.u]) s.type (← getRingInst) s.preorderInst (← getRingIsOrdInst) (← getContext)
+    return mkApp3 h (← mkPolyDecl c'.p) reflBoolTrue (← mkEqRefl (← getOne))
   | _ => throwError "NIY"
 
 partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do

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

@@ -96,6 +96,6 @@ partial def reify? (e : Expr) (skipVar : Bool) : LinearM (Option LinExpr) := do
     if skipVar then
       return none
     else
-      return some (← asVar e)
+      return some (← toVar e)
 
 end  Lean.Meta.Grind.Arith.Linear

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

@@ -139,7 +139,10 @@ where
     let getRingIsOrdInst? : GoalM (Option Expr) := do
       let some ringInst := ringInst? | return none
       let isOrdType := mkApp3 (mkConst ``Grind.Ring.IsOrdered [u]) type ringInst preorderInst
-      return LOption.toOption (← trySynthInstance isOrdType)
+      let .some inst ← trySynthInstance isOrdType
+        | reportIssue! "type is an ordered `IntModule` and a `Ring`, but is not an ordered ring, failed to synthesize{indentExpr isOrdType}"
+          return none
+      return some inst
     let ringIsOrdInst? ← getRingIsOrdInst?
     let getNoNatZeroDivInst? : GoalM (Option Expr) := do
       let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type

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

@@ -86,6 +86,9 @@ def withRingM (x : RingM α) : LinearM α := do
 def isCommRing : LinearM Bool :=
   return (← getStruct).ringId?.isSome
 
+def isOrderedCommRing : LinearM Bool := do
+  return (← isCommRing) && (← getStruct).ringIsOrdInst?.isSome
+
 def isLinearOrder : LinearM Bool :=
   return (← getStruct).linearInst?.isSome
 
@@ -109,6 +112,11 @@ def getLinearOrderInst : LinearM Expr := do
     | throwError "`grind linarith` internal error, structure is not a linear order"
   return inst
 
+def getRingInst : LinearM Expr := do
+  let some inst := (← getStruct).ringInst?
+    | throwError "`grind linarith` internal error, structure is not a ring"
+  return inst
+
 def getCommRingInst : LinearM Expr := do
   let some inst := (← getStruct).commRingInst?
     | throwError "`grind linarith` internal error, structure is not a commutative ring"

tests/lean/run/grind_linarith_1.lean

@@ -61,5 +61,29 @@ example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
   grind
 
 example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b c : α)
-    : a < b → b < c → c < a → False := by
+    : a < b → 2*b < c → c < 2*a → False := by
   grind
+
+-- Test misconfigured instances
+/--
+trace: [grind.issues] type is an ordered `IntModule` and a `Ring`, but is not an ordered ring, failed to synthesize
+      Ring.IsOrdered α
+-/
+#guard_msgs (drop error, trace) in
+set_option trace.grind.issues true in
+example [CommRing α] [Preorder α] [IntModule.IsOrdered α] (a b c : α)
+    : a < b → b + b < c → c < a → False := by
+  grind
+
+example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+    : a < 2 → b < a → b > 5 → False := by
+  grind
+
+example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+    : a < One.one + 4 → b < a → b ≥ 5 → False := by
+  grind
+
+example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+    : a < One.one + 5 → b < a → b ≥ 5 → False := by
+  fail_if_success grind
+  sorry