fix: ensure comm ring works with grind.debug

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -158,7 +158,7 @@ where op (f : Int → Int → Int) (x y : Expr) : Option Int :=
 
 /-- Construct the term with type hint `(Eq.refl a : a = b)`-/
 def mkEqReflWithExpectedType (a b : Expr) : MetaM Expr := do
-  mkExpectedTypeHint (← mkEqRefl a) (← mkEq a b)
+  return mkExpectedPropHint (← mkEqRefl a) (← mkEq a b)
 
 /--
 Analyzes a newly recorded atom,

src/Lean/Expr.lean

@@ -2210,6 +2210,10 @@ private def natEqPred : Expr :=
 def mkNatEq (a b : Expr) : Expr :=
   mkApp2 natEqPred a b
 
+/-- Given `a b : Prop`, return `a = b` -/
+def mkPropEq (a b : Expr) : Expr :=
+  mkApp3 (mkConst ``Eq [levelOne]) (mkSort levelZero) a b
+
 /-! Constants for Int typeclasses. -/
 namespace Int
 

src/Lean/Meta/AppBuilder.lean

@@ -17,12 +17,21 @@ def mkId (e : Expr) : MetaM Expr := do
   let u    ← getLevel type
   return mkApp2 (mkConst ``id [u]) type e
 
+def mkExpectedTypeHintCore (e : Expr) (expectedType : Expr) (expectedTypeUniv : Level) : Expr :=
+  mkApp2 (mkConst ``id [expectedTypeUniv]) expectedType e
+
 /--
-  Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, returns
-  term `@id expectedType e`. -/
+Given `proof` s.t. `inferType proof` is definitionally equal to `expectedProp`, returns
+term `@id expectedProp proof`. -/
+def mkExpectedPropHint (proof : Expr) (expectedProp : Expr) : Expr :=
+  mkExpectedTypeHintCore proof expectedProp levelZero
+
+/--
+Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, returns
+term `@id expectedType e`. -/
 def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
   let u ← getLevel expectedType
-  return mkApp2 (mkConst ``id [u]) expectedType e
+  return mkExpectedTypeHintCore e expectedType u
 
 /--
 `mkLetFun x v e` creates the encoding for the `let_fun x := v; e` expression.
@@ -536,7 +545,7 @@ def mkDecideProof (p : Expr) : MetaM Expr := do
   let decP      ← mkDecide p
   let decEqTrue ← mkEq decP (mkConst ``Bool.true)
   let h         ← mkEqRefl (mkConst ``Bool.true)
-  let h         ← mkExpectedTypeHint h decEqTrue
+  let h         := mkExpectedPropHint h decEqTrue
   mkAppM ``of_decide_eq_true #[h]
 
 /-- Returns `a < b` -/

src/Lean/Meta/Tactic/AC/Main.lean

@@ -124,7 +124,7 @@ def buildNormProof (preContext : PreContext) (l r : Expr) : MetaM (Lean.Expr ×
     let rhs := convert acExprNormed
     let proof := mkAppN (mkConst ``Context.eq_of_norm [u]) #[α, context, lhs, rhs, ←mkEqRefl (mkConst ``Bool.true)]
     let proofType ← mkEq (convertTarget vars acExpr) (convertTarget vars acExprNormed)
-    let proof ← mkExpectedTypeHint proof proofType
+    let proof := mkExpectedPropHint proof proofType
     return proof
   let some (_, _, tgt) := (← inferType proof).eq? | panic! "unexpected proof type"
   return (proof, tgt)

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

@@ -265,6 +265,7 @@ def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Uni
       mkApp4 (mkConst ``Grind.CommRing.NullCert.eq [ring.u]) ring.type ring.commRingInst ctx nc
   let h := mkApp3 h (toExpr ra) (toExpr rb) reflBoolTrue
   trace_goal[grind.debug.ring.impEq] "{a}, {b}"
-  pushEq a b <| ncx.applyEqs h
+  let eq := mkApp3 (mkConst ``Eq [.succ ring.u]) ring.type a b
+  pushEq a b <| mkExpectedPropHint (ncx.applyEqs h) eq
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -265,12 +265,12 @@ private def addNewInstance (thm : EMatchTheorem) (proof : Expr) (generation : Na
     prop ← annotateMatchEqnType prop (← read).initApp
     -- We must add a hint here because `annotateMatchEqnType` introduces `simpMatchDiscrsOnly` and
     -- `Grind.PreMatchCond` which are not reducible.
-    proof ← mkExpectedTypeHint proof prop
+    proof := mkExpectedPropHint proof prop
   else if (← isEqnThm thm.origin.key) then
     prop ← annotateEqnTypeConds prop
     -- We must add a hint because `annotateEqnTypeConds` introduces `Grind.PreMatchCond`
     -- which is not reducible.
-    proof ← mkExpectedTypeHint proof prop
+    proof := mkExpectedPropHint proof prop
   trace_goal[grind.ematch.instance] "{← thm.origin.pp}: {prop}"
   addTheoremInstance thm proof prop (generation+1)
 

src/Lean/Meta/Tactic/Grind/MatchDiscrOnly.lean

@@ -49,6 +49,6 @@ def eraseSimpMatchDiscrsOnly (e : Expr) : MetaM Simp.Result := do
     reducible. Thus, `e` and `e'` are not definitionally equal in this setting, and we must
     add a hint.
     -/
-    return { expr := e', proof? := (← mkExpectedTypeHint (← mkEqRefl e') (← mkEq e e')) }
+    return { expr := e', proof? := mkExpectedPropHint (← mkEqRefl e') (← mkEq e e') }
 
 end Lean.Meta.Grind

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

@@ -207,6 +207,6 @@ def replacePreMatchCond (e : Expr) : MetaM Simp.Result := do
       let_expr Grind.PreMatchCond p := e | return .continue e
       return .continue (markAsMatchCond p)
     let e' ← Core.transform e (pre := pre)
-    return { expr := e', proof? := (← mkExpectedTypeHint (← mkEqRefl e') (← mkEq e e')) }
+    return { expr := e', proof? := mkExpectedPropHint (← mkEqRefl e') (← mkEq e e') }
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Replace.lean

@@ -27,7 +27,7 @@ def _root_.Lean.MVarId.replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqP
     let target   ← mvarId.getType
     let u        ← getLevel target
     let eq       ← mkEq target targetNew
-    let newProof ← mkExpectedTypeHint eqProof eq
+    let newProof := mkExpectedPropHint eqProof eq
     let val  := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, newProof, mvarNew]
     mvarId.assign val
     return mvarNew.mvarId!

src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean

@@ -37,37 +37,37 @@ def simpEq? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     if p.isUnsatEq then
       let r := mkConst ``False
       let h := mkApp4 (mkConst ``Int.Linear.eq_eq_false) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
-      return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+      return some (r, mkExpectedPropHint h (mkPropEq e r))
     else if p.isValidEq then
       let r := mkConst ``True
       let h := mkApp4 (mkConst ``Int.Linear.eq_eq_true) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
-      return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+      return some (r, mkExpectedPropHint h (mkPropEq e r))
     else if p.toExpr == a && b == .num 0 then
       return none
     else match p with
       | .add 1 x (.add (-1) y (.num 0)) =>
         let r := mkIntEq atoms[x]! atoms[y]!
         let h := mkApp6 (mkConst ``Int.Linear.norm_eq_var) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr x) (toExpr y) reflBoolTrue
-        return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+        return some (r, mkExpectedPropHint h (mkPropEq e r))
       | .add 1 x (.num k) =>
         let r := mkIntEq atoms[x]! (toExpr (-k))
         let h := mkApp6 (mkConst ``Int.Linear.norm_eq_var_const) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr x) (toExpr (-k)) reflBoolTrue
-        return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+        return some (r, mkExpectedPropHint h (mkPropEq e r))
       | _ =>
         let k := p.gcdCoeffs'
         if k == 1 then
           let r := mkIntEq (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
           let h := mkApp5 (mkConst ``Int.Linear.norm_eq) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) reflBoolTrue
-          return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+          return some (r, mkExpectedPropHint h (mkPropEq e r))
         else if p.getConst % k == 0 then
           let p := p.div k
           let r := mkIntEq (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
           let h := mkApp6 (mkConst ``Int.Linear.norm_eq_coeff) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
-          return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+          return some (r, mkExpectedPropHint h (mkPropEq e r))
         else
           let r := mkConst ``False
           let h := mkApp5 (mkConst ``Int.Linear.eq_eq_false_of_divCoeff) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr (Int.ofNat k)) reflBoolTrue
-          return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+          return some (r, mkExpectedPropHint h (mkPropEq e r))
 
 
 def simpLe? (e : Expr) (checkIfModified : Bool) : MetaM (Option (Expr × Expr)) := do
@@ -80,11 +80,11 @@ def simpLe? (e : Expr) (checkIfModified : Bool) : MetaM (Option (Expr × Expr))
     if p.isUnsatLe then
       let r := mkConst ``False
       let h := mkApp4 (mkConst ``Int.Linear.le_eq_false) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
-      return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+      return some (r, mkExpectedPropHint h (mkPropEq e r))
     else if p.isValidLe then
       let r := mkConst ``True
       let h := mkApp4 (mkConst ``Int.Linear.le_eq_true) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
-      return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+      return some (r, mkExpectedPropHint h (mkPropEq e r))
     else if checkIfModified && p.toExpr == a && b == .num 0 then
       return none
     else
@@ -92,7 +92,7 @@ def simpLe? (e : Expr) (checkIfModified : Bool) : MetaM (Option (Expr × Expr))
       if k == 1 then
         let r := mkIntLE (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
         let h := mkApp5 (mkConst ``Int.Linear.norm_le) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) reflBoolTrue
-        return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+        return some (r, mkExpectedPropHint h (mkPropEq e r))
       else
         let tight := p.getConst % k != 0
         let p := p.div k
@@ -101,7 +101,7 @@ def simpLe? (e : Expr) (checkIfModified : Bool) : MetaM (Option (Expr × Expr))
           pure <| mkApp6 (mkConst ``Int.Linear.norm_le_coeff_tight) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
         else
           pure <| mkApp6 (mkConst ``Int.Linear.norm_le_coeff) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
-        return some (r, ← mkExpectedTypeHint h (← mkEq e r))
+        return some (r, mkExpectedPropHint h (mkPropEq e r))
 
 def simpRel? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   if let some arg := e.not? then
@@ -155,11 +155,11 @@ def simpDvd? (e : Expr) : MetaM (Option (Expr × Expr)) := do
         pure <| mkApp5 (mkConst ``Int.Linear.norm_dvd) (← toContextExpr atoms) (toExpr d) (toExpr e) (toExpr p) reflBoolTrue
       else
         pure <| mkApp7 (mkConst ``Int.Linear.norm_dvd_gcd) (← toContextExpr atoms) (toExpr d) (toExpr e) (toExpr d') (toExpr p) (toExpr g) reflBoolTrue
-      return some (rhs, ← mkExpectedTypeHint h (← mkEq lhs rhs))
+      return some (rhs, mkExpectedPropHint h (mkPropEq lhs rhs))
     else
       let rhs := mkConst ``False
       let h := mkApp4 (mkConst ``Int.Linear.dvd_eq_false) (← toContextExpr atoms) (toExpr d) (toExpr e) reflBoolTrue
-      return some (rhs, ← mkExpectedTypeHint h (← mkEq lhs rhs))
+      return some (rhs, mkExpectedPropHint h (mkPropEq lhs rhs))
 
 def simpExpr? (lhs : Expr) : MetaM (Option (Expr × Expr)) := do
   let (e, atoms) ← toLinearExpr lhs
@@ -169,7 +169,7 @@ def simpExpr? (lhs : Expr) : MetaM (Option (Expr × Expr)) := do
     -- We only return some if monomials were fused
     let h := mkApp4 (mkConst ``Int.Linear.Expr.eq_of_norm_eq) (← toContextExpr atoms) (toExpr e) (toExpr p) reflBoolTrue
     let rhs ← p.denoteExpr (atoms[·]!)
-    return some (rhs, ← mkExpectedTypeHint h (← mkEq lhs rhs))
+    return some (rhs, mkExpectedPropHint h (mkIntEq lhs rhs))
   else
     return none
 

src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean

@@ -19,17 +19,17 @@ def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     if c₂.isUnsat then
       let r := mkConst ``False
       let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr atoms) (toExpr c) reflBoolTrue
-      return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
+      return some (r, mkExpectedPropHint p (mkPropEq lhs r))
     else if c₂.isValid then
       let r := mkConst ``True
       let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr atoms) (toExpr c) reflBoolTrue
-      return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
+      return some (r, mkExpectedPropHint p (mkPropEq lhs r))
     else
       let c₂ : LinearCnstr := c₂.toExpr
       let r ← c₂.toArith atoms
       if r != lhs then
         let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr atoms) (toExpr c) (toExpr c₂) reflBoolTrue
-        return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
+        return some (r, mkExpectedPropHint p (mkPropEq lhs r))
       else
         return none
 
@@ -40,19 +40,19 @@ def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     match_expr arg with
     | LE.le α _ _ _ =>
       if α.isConstOf ``Nat then
-        eNew?   := some (← mkLE (← mkAdd (arg.getArg! 3) (mkNatLit 1)) (arg.getArg! 2))
+        eNew?   := some (mkNatLE (mkNatAdd (arg.getArg! 3) (mkNatLit 1)) (arg.getArg! 2))
         thmName := ``Nat.not_le_eq
     | GE.ge α _ _ _ =>
       if α.isConstOf ``Nat then
-        eNew?   := some (← mkLE (← mkAdd (arg.getArg! 2) (mkNatLit 1)) (arg.getArg! 3))
+        eNew?   := some (mkNatLE (mkNatAdd (arg.getArg! 2) (mkNatLit 1)) (arg.getArg! 3))
         thmName := ``Nat.not_ge_eq
     | LT.lt α _ _ _ =>
       if α.isConstOf ``Nat then
-        eNew?   := some (← mkLE (arg.getArg! 3) (arg.getArg! 2))
+        eNew?   := some (mkNatLE (arg.getArg! 3) (arg.getArg! 2))
         thmName := ``Nat.not_lt_eq
     | GT.gt α _ _ _ =>
       if α.isConstOf ``Nat then
-        eNew?   := some (← mkLE (arg.getArg! 2) (arg.getArg! 3))
+        eNew?   := some (mkNatLE (arg.getArg! 2) (arg.getArg! 3))
         thmName := ``Nat.not_gt_eq
     | _ => pure ()
     if let some eNew := eNew? then
@@ -76,6 +76,6 @@ def simpExpr? (input : Expr) : MetaM (Option (Expr × Expr)) := do
     return none
   let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr e) (toExpr e') reflBoolTrue
   let r ← e'.toArith ctx
-  return some (r, ← mkExpectedTypeHint p (← mkEq input r))
+  return some (r, mkExpectedPropHint p (mkNatEq input r))
 
 end Lean.Meta.Simp.Arith.Nat

tests/lean/run/grind_ring_1.lean

@@ -1,4 +1,6 @@
 set_option grind.warning false
+set_option grind.debug true
+
 open Lean.Grind
 
 example [CommRing α] (x : α) : (x + 1)*(x - 1) = x^2 - 1 := by

tests/lean/run/grind_ring_2.lean

@@ -1,4 +1,5 @@
 set_option grind.warning false
+set_option grind.debug true
 open Lean.Grind
 
 example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by