chore: force update stage0

src/Init/Grind/Tactics.lean

@@ -102,11 +102,6 @@ structure Config where
   ring := true
   ringSteps := 10000
   /--
-  When `true` (default: `false`), the commutative ring procedure in `grind` constructs stepwise
-  proof terms, instead of a single-step Nullstellensatz certificate
-  -/
-  ringNull := false
-  /--
   When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
   `CommRing`.
   -/

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -341,7 +341,6 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
     let p ← (ra.sub rb).toPolyM
     addNewEq (← mkEqCnstr p (.core a b ra rb))
   else if let some semiringId ← inSameSemiring? a b then SemiringM.run semiringId do
-    if (← getConfig).ringNull then return () -- TODO: remove after we add Nullstellensatz certificates for semiring adapter
     trace_goal[grind.ring.assert] "{← mkEq a b}"
     let some sa ← toSemiringExpr? a | return ()
     let some sb ← toSemiringExpr? b | return ()
@@ -405,7 +404,6 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
     }
   else if let some semiringId ← inSameSemiring? a b then SemiringM.run semiringId do
     if (← getAddRightCancelInst?).isSome then
-      if (← getConfig).ringNull then return () -- TODO: remove after we add Nullstellensatz certificates for semiring adapter
       trace_goal[grind.ring.assert] "{mkNot (← mkEq a b)}"
       let some sa ← toSemiringExpr? a | return ()
       let some sb ← toSemiringExpr? b | return ()

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

@@ -19,181 +19,27 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
 public section
 
 namespace Lean.Meta.Grind.Arith.CommRing
-
-def toContextExprCore (vars : Array Expr) : RingM Expr := do
+/--
+Returns a context of type `RArray α` containing the variables `vars` where
+`α` is the type of the ring.
+-/
+private def toContextExpr (vars : Array Expr) : RingM Expr := do
   let ring ← getRing
   if h : 0 < vars.size then
     RArray.toExpr ring.type id (RArray.ofFn (vars[·]) h)
   else
     RArray.toExpr ring.type id (RArray.leaf (mkApp (← getNatCastFn) (toExpr 0)))
 
-/--
-Returns a context of type `RArray α` containing the variables of the given ring.
-`α` is the type of the ring.
--/
-def toContextExpr : RingM Expr := do
-  toContextExprCore (← getRing).vars.toArray
-
-private def toSContextExprCore' (vars : Array Expr) : SemiringM Expr := do
+private def toSContextExpr' (vars : Array Expr) : SemiringM Expr := do
   let semiring ← getSemiring
   if h : 0 < vars.size then
     RArray.toExpr semiring.type id (RArray.ofFn (vars[·]) h)
   else
     RArray.toExpr semiring.type id (RArray.leaf (mkApp (← getNatCastFn') (toExpr 0)))
 
-private def toSContextExpr' : SemiringM Expr := do
-  toSContextExprCore' (← getSemiring).vars.toArray
-
 /-- Similar to `toContextExpr`, but for semirings. -/
 private def toSContextExpr (semiringId : Nat) (vars : Array Expr) : RingM Expr := do
-  SemiringM.run semiringId do toSContextExprCore' vars
-
-def throwNoNatZeroDivisors : RingM α := do
-  throwError "`grind` internal error, `NoNatZeroDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}"
-
-def getPolyConst (p : Poly) : RingM Int := do
-  let .num k := p
-    | throwError "`grind` internal error, constant polynomial expected {indentExpr (← p.denoteExpr)}"
-  return k
-
-namespace Null
-/-!
-Proof term for a Nullstellensatz certificate.
--/
-
-/--
-A "pre" Nullstellensatz certificate.
-Recall that, given the hypotheses `h₁ : lhs₁ = rhs₁` ... `hₙ : lhsₙ = rhsₙ`,
-a Nullstellensatz certificate is of the form
-```
-q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
-```
-Each hypothesis is an `EqCnstr` justified by a `.core ..` `EqnCnstrProof`.
-We dynamically associate them with unique indices based on the order we find them
-during traversal.
-For the other `EqCnstr`s we compute a "pre" certificate as a dense array
-containing `q₁` ... `qₙ` needed to create the `EqCnstr`.
-
-We are assuming the number of hypotheses used to derive a conclusion is small
-and a dense array is a reasonable representation.
--/
-structure PreNullCert where
-  qs : Array Poly
-  /--
-  We don't use rational coefficients in the polynomials.
-  Thus, we need to track a denominator to justify the proof step `div`.
-  -/
-  d  : Int := 1
-  deriving Inhabited
-
-def PreNullCert.zero : PreNullCert :=
-  { qs := #[] }
-
-def PreNullCert.unit (i : Nat) (n : Nat) : PreNullCert :=
-  let qs := Array.replicate n (.num 0)
-  let qs := qs.set! i (.num 1)
-  { qs }
-
-def PreNullCert.div (c : PreNullCert) (k : Int) : RingM PreNullCert := do
-  return { c with d := c.d * k }
-
-def PreNullCert.mul (c : PreNullCert) (k : Int) : RingM PreNullCert := do
-  if k == 1 then
-    return c
-  else
-    let g := Int.gcd k c.d
-    let k := k / g
-    let d := c.d / g
-    if k == 1 then
-      return { c with d }
-    else
-      let qs ← c.qs.mapM fun q => q.mulConstM k
-      return { qs, d }
-
-def PreNullCert.combine (k₁ : Int) (m₁ : Mon) (c₁ : PreNullCert) (k₂ : Int) (m₂ : Mon) (c₂ : PreNullCert) : RingM PreNullCert := do
-  let d₁    := c₁.d
-  let d₂    := c₂.d
-  let k₁_d₂ := k₁*d₂
-  let k₂_d₁ := k₂*d₁
-  let d₁_d₂ := d₁*d₂
-  let g     := Int.gcd (Int.gcd k₁_d₂ k₂_d₁) d₁_d₂
-  let k₁    := k₁_d₂ / g
-  let k₂    := k₂_d₁ / g
-  let d     := d₁_d₂ / g
-  let qs₁   := c₁.qs
-  let qs₂   := c₂.qs
-  let n := Nat.max qs₁.size qs₂.size
-  let mut qs : Vector Poly n := Vector.replicate n (.num 0)
-  for h : i in *...n do
-    if h₁ : i < qs₁.size then
-      let q₁ ← qs₁[i].mulMonM k₁ m₁
-      if h₂ : i < qs₂.size then
-        let q₂ ← qs₂[i].mulMonM k₂ m₂
-        qs := qs.set i (← q₁.combineM q₂)
-      else
-        qs := qs.set i q₁
-    else
-      have : i < n := Std.PRange.lt_upper_of_mem h
-      have : qs₁.size = n ∨ qs₂.size = n := by simp +zetaDelta only [Nat.max_def, right_eq_ite_iff]; split <;> simp [*]
-      have : i < qs₂.size := by omega
-      let q₂ ← qs₂[i].mulMonM k₂ m₂
-      qs := qs.set i q₂
-  return { qs := qs.toArray, d }
-
-structure NullCertHypothesis where
-  h   : Expr
-  lhs : RingExpr
-  rhs : RingExpr
-
-structure ProofM.State where
-  /-- Mapping from `EqCnstr` to `PreNullCert` -/
-  cache       : Std.HashMap UInt64 PreNullCert := {}
-  hyps        : Array NullCertHypothesis := #[]
-
-abbrev ProofM := StateRefT ProofM.State RingM
-
-private abbrev caching (c : α) (k : ProofM PreNullCert) : ProofM PreNullCert := do
-  let addr := unsafe (ptrAddrUnsafe c).toUInt64 >>> 2
-  if let some h := (← get).cache[addr]? then
-    return h
-  else
-    let h ← k
-    modify fun s => { s with cache := s.cache.insert addr h }
-    return h
-
-structure NullCertExt where
-  d   : Int
-  qhs : Array (Poly × NullCertHypothesis)
-
-end Null
-
-section
-open Null
-partial def EqCnstr.toPreNullCert (c : EqCnstr) : ProofM PreNullCert := caching c do
-  match c.h with
-  | .core a b lhs rhs =>
-    let i := (← get).hyps.size
-    let h ← mkEqProof a b
-    modify fun s => { s with hyps := s.hyps.push { h, lhs, rhs } }
-    return PreNullCert.unit i (i+1)
-  | .coreS _a _b _sa _sb _ra _rb =>
-    throwError "`grind +ringNull` is not supported yet for this goal"
-  | .superpose k₁ m₁ c₁ k₂ m₂ c₂ => (← c₁.toPreNullCert).combine k₁ m₁ k₂ m₂ (← c₂.toPreNullCert)
-  | .simp k₁ c₁ k₂ m₂ c₂ => (← c₁.toPreNullCert).combine k₁ .unit k₂ m₂ (← c₂.toPreNullCert)
-  | .mul k c => (← c.toPreNullCert).mul k
-  | .div k c => (← c.toPreNullCert).div k
-  | .gcd .. | .numEq0 .. =>
-    throwError "`grind +ringNull` is not supported yet for this goal"
-
-def PolyDerivation.toPreNullCert (d : PolyDerivation) : ProofM PreNullCert := do
-  match d with
-  | .input _ => return .zero
-  | .step _p k₁ d k₂ m₂ c₂ =>
-    -- Recall that _p = k₁*d.getPoly + k₂*m₂*c.p
-    trace[grind.debug.ring.proof] ">> k₁: {k₁}, {(← d.toPreNullCert).d}, {(← c₂.toPreNullCert).d}"
-    (← d.toPreNullCert).combine k₁ .unit (-k₂) m₂ (← c₂.toPreNullCert)
-  | .normEq0 .. =>
-    throwError "`grind +ringNull` is not supported yet for this goal"
+  SemiringM.run semiringId do toSContextExpr' vars
 
 /-- Returns the multiplier `k` for the input polynomial. See comment at `PolyDerivation.step`. -/
 def PolyDerivation.getMultiplier (d : PolyDerivation) : Int :=
@@ -205,126 +51,13 @@ where
     | .step _ k₁ d .. => go d (k₁ * acc)
     | .normEq0 _ d .. => go d acc
 
-def EqCnstr.mkNullCertExt (c : EqCnstr) : RingM NullCertExt := do
-  let (nc, s) ← c.toPreNullCert.run {}
-  return { d := nc.d, qhs := nc.qs.zip s.hyps }
+private def throwNoNatZeroDivisors : RingM α := do
+  throwError "`grind` internal error, `NoNatZeroDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}"
 
-def PolyDerivation.mkNullCertExt (d : PolyDerivation) : RingM NullCertExt := do
-  let (nc, s) ← d.toPreNullCert.run {}
-  return { d := nc.d, qhs := nc.qs.zip s.hyps }
-
-def DiseqCnstr.mkNullCertExt (c : DiseqCnstr) : RingM NullCertExt :=
-  c.d.mkNullCertExt
-end
-
-namespace Null
-def NullCertExt.toPoly (nc : NullCertExt) : RingM Poly := do
-  let mut p : Poly := .num 0
-  for (q, h) in nc.qhs do
-    p ← p.combineM (← q.mulM (← (h.lhs.sub h.rhs).toPolyM))
-  return p
-
-def NullCertExt.check (c : EqCnstr) (nc : NullCertExt) : RingM Bool := do
-  let p₁ := c.p.mulConst' nc.d (← nonzeroChar?)
-  let p₂ ← nc.toPoly
-  return p₁ == p₂
-
-def NullCertExt.toNullCert (nc : NullCertExt) : Grind.CommRing.NullCert :=
-  go nc.qhs.size .empty (by omega)
-where
-  go (i : Nat) (acc : Grind.CommRing.NullCert) (h : i ≤ nc.qhs.size) : Grind.CommRing.NullCert :=
-    if h : i > 0 then
-      let i := i - 1
-      let (p, h) := nc.qhs[i]
-      go i (.add p h.lhs h.rhs acc) (by omega)
-    else
-      acc
-
-/--
-Given a `pr`, returns `pr h₁ ... hₙ`, where `n` is size `nc.qhs.size`, and `hᵢ`s
-are the equalities in the certificate.
--/
-def NullCertExt.applyEqs (pr : Expr) (nc : NullCertExt) : Expr :=
-  go 0 pr
-where
-  go (i : Nat) (pr : Expr) : Expr :=
-    if _ : i < nc.qhs.size then
-      let (_, h) := nc.qhs[i]
-      go (i + 1) (mkApp pr h.h)
-    else
-      pr
-
-private def getNoZeroDivInstIfNeeded? (k : Int) : RingM (Option Expr) := do
-  if k == 1 then
-    return none
-  else
-    let some inst ← noZeroDivisorsInst? | throwNoNatZeroDivisors
-    return some inst
-
-def setEqUnsat (c : EqCnstr) : RingM Unit := do
-  trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
-  let k ← getPolyConst c.p
-  let ncx ← c.mkNullCertExt
-  trace_goal[grind.ring.assert.unsat] "{ncx.d}*({← c.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}"
-  let ring ← getRing
-  let some (charInst, char) := ring.charInst?
-    | throwError "`grind` internal error, `IsCharP` instance is needed, but it is not available for{indentExpr (← getRing).type}\nconsider not using `+ringNull`"
-  let h := if char == 0 then
-    mkApp (mkConst ``Grind.CommRing.NullCert.eq_unsat [ring.u]) ring.type
-  else
-    mkApp2 (mkConst ``Grind.CommRing.NullCert.eq_unsatC [ring.u]) ring.type (toExpr char)
-  let ctx ← toContextExpr
-  let nc := toExpr (ncx.toNullCert)
-  let h := mkApp6 h ring.commRingInst charInst ctx nc (toExpr k) eagerReflBoolTrue
-  closeGoal <| ncx.applyEqs h
-
-def setDiseqUnsat (c : DiseqCnstr) : RingM Unit := do
-  trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
-  let ncx ← c.mkNullCertExt
-  trace_goal[grind.ring.assert.unsat] "multiplier: {c.d.getMultiplier}, {ncx.d}*({← c.d.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}"
-  let nc := toExpr (ncx.toNullCert)
-  let ring ← getRing
-  let ctx ← toContextExpr
-  let k := c.d.getMultiplier * ncx.d
-  let h := match (← nonzeroCharInst?), (← getNoZeroDivInstIfNeeded? k) with
-    | some (charInst, char), some nzDivInst =>
-      mkApp8 (mkConst ``Grind.CommRing.NullCert.ne_nzdiv_unsatC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst nzDivInst ctx nc (toExpr k)
-    | some (charInst, char), none =>
-      mkApp6 (mkConst ``Grind.CommRing.NullCert.ne_unsatC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst ctx nc
-    | none, some nzDivInst =>
-      mkApp6 (mkConst ``Grind.CommRing.NullCert.ne_nzdiv_unsat [ring.u]) ring.type ring.commRingInst nzDivInst ctx nc (toExpr k)
-    | none, none =>
-      mkApp4 (mkConst ``Grind.CommRing.NullCert.ne_unsat [ring.u]) ring.type ring.commRingInst ctx nc
-  let h := mkApp4 h (toExpr c.rlhs) (toExpr c.rrhs) eagerReflBoolTrue (← mkDiseqProof c.lhs c.rhs)
-  closeGoal <| ncx.applyEqs h
-
-def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit := do
-  let ncx ← d.mkNullCertExt
-  let nc := toExpr (ncx.toNullCert)
-  let ring ← getRing
-  let ctx ← toContextExpr
-  let k := d.getMultiplier * ncx.d
-  let h := match (← nonzeroCharInst?), (← getNoZeroDivInstIfNeeded? k) with
-    | some (charInst, char), some nzDivInst =>
-      mkApp8 (mkConst ``Grind.CommRing.NullCert.eq_nzdivC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst nzDivInst ctx nc (toExpr k)
-    | some (charInst, char), none =>
-      mkApp6 (mkConst ``Grind.CommRing.NullCert.eqC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst ctx nc
-    | none, some nzDivInst =>
-      mkApp6 (mkConst ``Grind.CommRing.NullCert.eq_nzdiv [ring.u]) ring.type ring.commRingInst nzDivInst ctx nc (toExpr k)
-    | none, none =>
-      mkApp4 (mkConst ``Grind.CommRing.NullCert.eq [ring.u]) ring.type ring.commRingInst ctx nc
-  let h := mkApp3 h (toExpr ra) (toExpr rb) eagerReflBoolTrue
-  trace_goal[grind.debug.ring.impEq] "{a}, {b}"
-  let eq := mkApp3 (mkConst ``Eq [.succ ring.u]) ring.type a b
-  pushEq a b <| mkExpectedPropHint (ncx.applyEqs h) eq
-
-end Null
-
-namespace Stepwise
-/-!
-Alternative proof term construction where we generate a sub-term for each step in
-the derivation.
--/
+private def getPolyConst (p : Poly) : RingM Int := do
+  let .num k := p
+    | throwError "`grind` internal error, constant polynomial expected {indentExpr (← p.denoteExpr)}"
+  return k
 
 structure ProofM.State where
   cache       : Std.HashMap UInt64 Expr := {}
@@ -369,16 +102,16 @@ local macro "declare! " decls:ident a:ident : term =>
        modify fun s => { s with $decls:ident := (s.$decls).insert $a x };
        return x)
 
-def mkPolyDecl (p : Poly) : ProofM Expr := do
+private def mkPolyDecl (p : Poly) : ProofM Expr := do
   declare! polyDecls p
 
-def mkExprDecl (e : RingExpr) : ProofM Expr := do
+private def mkExprDecl (e : RingExpr) : ProofM Expr := do
   declare! exprDecls e
 
-def mkSExprDecl (e : SemiringExpr) : ProofM Expr := do
+private def mkSExprDecl (e : SemiringExpr) : ProofM Expr := do
   declare! sexprDecls e
 
-def mkMonDecl (m : Mon) : ProofM Expr := do
+private def mkMonDecl (m : Mon) : ProofM Expr := do
   declare! monDecls m
 
 private def mkStepBasicPrefix (declName : Name) : ProofM Expr := do
@@ -516,7 +249,7 @@ private def mkContext (h : Expr) : ProofM Expr := do
   if h.hasLooseBVars then
     let ring ← getRing
     let ctxType := mkApp (mkConst ``RArray [ring.u]) ring.type
-    let ctxVal ← toContextExprCore vars
+    let ctxVal ← toContextExpr vars
     return .letE `ctx ctxType ctxVal h (nondep := false)
   else
     return h
@@ -549,7 +282,7 @@ where
     mkSemiringContext h
 
 open Lean.Grind.CommRing in
-def setEqUnsat (c : EqCnstr) : RingM Unit := do
+def EqCnstr.setUnsat  (c : EqCnstr) : RingM Unit := do
   let h ← withProofContext do
     let ring ← getRing
     if let some (charInst, char) := ring.charInst? then
@@ -565,7 +298,7 @@ def setEqUnsat (c : EqCnstr) : RingM Unit := do
       throwError "`grind ring` internal error, unexpected unsat eq proof {← c.denoteExpr}"
   closeGoal h
 
-def setDiseqUnsat (c : DiseqCnstr) : RingM Unit := do
+def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do
   let h ← withProofContext do
     let heq ← mkImpEqExprProof c.rlhs c.rrhs c.d
     let hne ← if let some (sa, sb) := c.ofSemiring? then
@@ -583,34 +316,21 @@ def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Uni
   let eq := mkApp3 (mkConst ``Eq [.succ ring.u]) ring.type a b
   pushEq a b <| mkExpectedPropHint heq eq
 
-end Stepwise
-
-def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do
-  if (← getConfig).ringNull then
-    Null.setEqUnsat c
-  else
-    Stepwise.setEqUnsat c
-
-def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do
-  if (← getConfig).ringNull then
-    Null.setDiseqUnsat c
-  else
-    Stepwise.setDiseqUnsat c
-
-def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit := do
-  if (← getConfig).ringNull then
-    Null.propagateEq a b ra rb d
-  else
-    Stepwise.propagateEq a b ra rb d
-
 /--
 Given `a` and `b`, such that `a ≠ b` in the core and `sa` and `sb` their reified semiring
 terms s.t. `sa.toPoly == sb.toPoly`, close the goal.
 -/
 def setSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : SemiringM Unit := do
-  let ctx ← toSContextExpr'
   let semiring ← getSemiring
   let hne ← mkDiseqProof a b
+  let usedVars     := sa.collectVars >> sb.collectVars <| {}
+  let vars'        := usedVars.toArray
+  let varRename    := mkVarRename vars'
+  let vars         := (← getSemiring).vars
+  let vars         := vars'.map fun x => vars[x]!
+  let sa           := sa.renameVars varRename
+  let sb           := sb.renameVars varRename
+  let ctx          ← toSContextExpr' vars
   let h := mkApp3 (mkConst ``Grind.Ring.OfSemiring.eq_normS [semiring.u]) semiring.type semiring.commSemiringInst ctx
   let h := mkApp3 h (toExpr sa) (toExpr sb) eagerReflBoolTrue
   closeGoal (mkApp hne h)

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {

tests/lean/run/grind_ring_2.lean

@@ -40,15 +40,9 @@ example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 600000*x = 1 → 300*y
 example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
   grind
 
-example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
-  grind +ringNull
-
 example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
   grind
 
-example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
-  grind +ringNull
-
 example [CommRing α] (x y : α) : x*y*x = 1 → x*y*y = y → y = 1 := by
   grind
 

tests/lean/run/grind_semiring_norm.lean

@@ -11,4 +11,18 @@ example (a b : R) : (a + 2 * b)^2 = 4 * b^2 + b * 4 * a + a^2 := by grind
 
 example (a b : R) : (a + b)^2 ≠ a^2 + 2 * a * b + b^2 → False := by grind
 
+/--
+trace: [grind.debug.proof] fun h h_1 =>
+      h_1
+        (Ring.OfSemiring.eq_normS (RArray.branch 1 (RArray.leaf a) (RArray.leaf b))
+          (((Ring.OfSemiring.Expr.var 0).add (Ring.OfSemiring.Expr.var 1)).pow 2)
+          ((((Ring.OfSemiring.Expr.var 0).pow 2).add
+                (((Ring.OfSemiring.Expr.num 2).mul (Ring.OfSemiring.Expr.var 0)).mul (Ring.OfSemiring.Expr.var 1))).add
+            ((Ring.OfSemiring.Expr.var 1).pow 2))
+          (eagerReduce (Eq.refl true)))
+-/
+#guard_msgs in -- context should contain only `a` and `b`
+set_option trace.grind.debug.proof true in
+example (a b c d : R) : c + d = d → (a + b)^2 ≠ a^2 + 2 * a * b + b^2 → False := by grind
+
 end CommSemiring