test:

src/Lean/Expr.lean

@@ -2191,9 +2191,9 @@ def mkAndN : List Expr → Expr
   | [] => mkConst ``True
   | [p] => p
   | p :: ps => mkAnd p (mkAndN ps)
-/-- Return `Classical.em p` -/
+/-- Returns `Classical.em p` -/
 def mkEM (p : Expr) : Expr := mkApp (mkConst ``Classical.em) p
-/-- Return `p ↔ q` -/
+/-- Returns `p ↔ q` -/
 def mkIff (p q : Expr) : Expr := mkApp2 (mkConst ``Iff) p q
 
 /-! Constants for Nat typeclasses. -/
@@ -2271,9 +2271,10 @@ private def natEqPred : Expr :=
 def mkNatEq (a b : Expr) : Expr :=
   mkApp2 natEqPred a b
 
-/-- Given `a b : Prop`, return `a = b` -/
+private def propEq := mkApp (mkConst ``Eq [1]) (mkSort 0)
+/-- Given `a b : Prop`, returns `a = b` -/
 def mkPropEq (a b : Expr) : Expr :=
-  mkApp3 (mkConst ``Eq [levelOne]) (mkSort levelZero) a b
+  mkApp2 propEq a b
 
 /-! Constants for Int typeclasses. -/
 namespace Int

src/Lean/Meta/Check.lean

@@ -346,6 +346,16 @@ def isTypeCorrect (e : Expr) : MetaM Bool := do
   catch _ =>
     pure false
 
+/--
+Throw an exception if `e` cannot be type checked using the kernel.
+This function is used for debugging purposes only.
+-/
+def checkWithKernel (e : Expr) : MetaM Unit := do
+  let e ← instantiateExprMVars e
+  match Kernel.check (← getEnv) (← getLCtx) e with
+  | .ok .. => return ()
+  | .error ex => throwError "kernel type checker failed at{indentExpr e}\nwith error message\n{ex.toMessageData (← getOptions)}"
+
 builtin_initialize
   registerTraceClass `Meta.check
 

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

@@ -61,20 +61,28 @@ where
     | .num k => return mkApp2 (← getAddFn) acc (← denoteNum k)
     | .add k m p => go p (mkApp2 (← getAddFn) acc (← denoteTerm k m))
 
-def _root_.Lean.Grind.CommRing.Expr.denoteExpr (e : RingExpr) : M Expr := do
+@[specialize]
+private def denoteExprCore (getVar : Nat → Expr) (e : RingExpr) : M Expr := do
   go e
 where
   go : RingExpr → M Expr
   | .num k => denoteNum k
   | .natCast k => return mkApp (← getNatCastFn) (mkNatLit k)
   | .intCast k => return mkApp (← getIntCastFn) (mkIntLit k)
-  | .var x => return (← getRing).vars[x]!
+  | .var x => return getVar x
   | .add a b => return mkApp2 (← getAddFn) (← go a) (← go b)
   | .sub a b => return mkApp2 (← getSubFn) (← go a) (← go b)
   | .mul a b => return mkApp2 (← getMulFn) (← go a) (← go b)
   | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
   | .neg a => return mkApp (← getNegFn) (← go a)
 
+def _root_.Lean.Grind.CommRing.Expr.denoteExpr (e : RingExpr) : M Expr := do
+  let ring ← getRing
+  denoteExprCore (fun x => ring.vars[x]!) e
+
+def _root_.Lean.Grind.CommRing.Expr.denoteExpr' (vars : Array Expr) (e : RingExpr) : M Expr := do
+  denoteExprCore (fun x => vars[x]!) e
+
 private def mkEq (a b : Expr) : M Expr := do
   let r ← getRing
   return mkApp3 (mkConst ``Eq [r.u.succ]) r.type a b

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

@@ -11,6 +11,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
 import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
+import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
 import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
@@ -395,23 +396,41 @@ private def norm (vars : PArray Expr) (lhs rhs lhs' rhs' : RingExpr) : NormResul
 def mkLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
   let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
-  let ctx ← toContextExpr vars
-  let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst isPreorderInst orderedRingInst
-  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+  withAbstractAtoms vars ring.type fun vars => do
+    let ctx ← toContextExpr vars
+    let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst isPreorderInst orderedRingInst
+    let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+    let leFn := mkApp2 (mkConst ``LE.le [ring.u]) ring.type leInst
+    let le   := mkApp2 leFn (← lhs.denoteExpr' vars) (← rhs.denoteExpr' vars)
+    let le'  := mkApp2 leFn (← lhs'.denoteExpr' vars) (← rhs'.denoteExpr' vars)
+    let expected := mkPropEq le le'
+    return mkExpectedPropHint h expected
 
 def mkLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
   let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
-  let ctx ← toContextExpr vars
-  let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
-  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+  withAbstractAtoms vars ring.type fun vars => do
+    let ctx ← toContextExpr vars
+    let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
+    let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+    let ltFn := mkApp2 (mkConst ``LT.lt [ring.u]) ring.type ltInst
+    let lt   := mkApp2 ltFn (← lhs.denoteExpr' vars) (← rhs.denoteExpr' vars)
+    let lt'  := mkApp2 ltFn (← lhs'.denoteExpr' vars) (← rhs'.denoteExpr' vars)
+    let expected := mkPropEq lt lt'
+    return mkExpectedPropHint h expected
 
 def mkEqIffProof (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
   let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
-  let ctx ← toContextExpr vars
-  let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr [ring.u]) ring.type ring.commRingInst
-  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+  withAbstractAtoms vars ring.type fun vars => do
+    let ctx ← toContextExpr vars
+    let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr [ring.u]) ring.type ring.commRingInst
+    let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+    let eqFn := mkApp (mkConst ``Eq [Level.succ ring.u]) ring.type
+    let eq   := mkApp2 eqFn (← lhs.denoteExpr' vars) (← rhs.denoteExpr' vars)
+    let eq'  := mkApp2 eqFn (← lhs'.denoteExpr' vars) (← rhs'.denoteExpr' vars)
+    let expected := mkPropEq eq eq'
+    return mkExpectedPropHint h expected
 
 /--
 Given `e` and `e'` s.t. `e.toPoly == e'.toPoly`, returns a proof that `e.denote ctx = e'.denote ctx`
@@ -419,30 +438,52 @@ Given `e` and `e'` s.t. `e.toPoly == e'.toPoly`, returns a proof that `e.denote
 def mkTermEqProof (e e' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
   let { lhs, lhs', vars, .. } := norm ring.vars e (.num 0) e' (.num 0)
-  let ctx ← toContextExpr vars
-  let h := mkApp2 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_eq [ring.u]) ring.type ring.commRingInst
-  return mkApp4 h ctx (toExpr lhs) (toExpr lhs') eagerReflBoolTrue
+  withAbstractAtoms vars ring.type fun vars => do
+    let ctx ← toContextExpr vars
+    let h := mkApp2 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_eq [ring.u]) ring.type ring.commRingInst
+    let h := mkApp4 h ctx (toExpr lhs) (toExpr lhs') eagerReflBoolTrue
+    let eqFn := mkApp (mkConst ``Eq [Level.succ ring.u]) ring.type
+    let expected := mkApp2 eqFn (← lhs.denoteExpr' vars) (← lhs'.denoteExpr' vars)
+    return mkExpectedPropHint h expected
 
 def mkNonCommLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
   let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
-  let ctx ← toContextExpr vars
-  let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst isPreorderInst orderedRingInst
-  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+  withAbstractAtoms vars ring.type fun vars => do
+    let ctx ← toContextExpr vars
+    let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst isPreorderInst orderedRingInst
+    let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+    let leFn := mkApp2 (mkConst ``LE.le [ring.u]) ring.type leInst
+    let le   := mkApp2 leFn (← lhs.denoteExpr' vars) (← rhs.denoteExpr' vars)
+    let le'  := mkApp2 leFn (← lhs'.denoteExpr' vars) (← rhs'.denoteExpr' vars)
+    let expected := mkPropEq le le'
+    return mkExpectedPropHint h expected
 
 def mkNonCommLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
   let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
-  let ctx ← toContextExpr vars
-  let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
-  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+  withAbstractAtoms vars ring.type fun vars => do
+    let ctx ← toContextExpr vars
+    let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
+    let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+    let ltFn := mkApp2 (mkConst ``LT.lt [ring.u]) ring.type ltInst
+    let lt   := mkApp2 ltFn (← lhs.denoteExpr' vars) (← rhs.denoteExpr' vars)
+    let lt'  := mkApp2 ltFn (← lhs'.denoteExpr' vars) (← rhs'.denoteExpr' vars)
+    let expected := mkPropEq lt lt'
+    return mkExpectedPropHint h expected
 
 def mkNonCommEqIffProof (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
   let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
-  let ctx ← toContextExpr vars
-  let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr_nc [ring.u]) ring.type ring.ringInst
-  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+  withAbstractAtoms vars ring.type fun vars => do
+    let ctx ← toContextExpr vars
+    let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr_nc [ring.u]) ring.type ring.ringInst
+    let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+    let eqFn := mkApp (mkConst ``Eq [Level.succ ring.u]) ring.type
+    let eq   := mkApp2 eqFn (← lhs.denoteExpr' vars) (← rhs.denoteExpr' vars)
+    let eq'  := mkApp2 eqFn (← lhs'.denoteExpr' vars) (← rhs'.denoteExpr' vars)
+    let expected := mkPropEq eq eq'
+    return mkExpectedPropHint h expected
 
 /--
 Given `e` and `e'` s.t. `e.toPoly_nc == e'.toPoly_nc`, returns a proof that `e.denote ctx = e'.denote ctx`
@@ -450,8 +491,12 @@ Given `e` and `e'` s.t. `e.toPoly_nc == e'.toPoly_nc`, returns a proof that `e.d
 def mkNonCommTermEqProof (e e' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
   let { lhs, lhs', vars, .. } := norm ring.vars e (.num 0) e' (.num 0)
-  let ctx ← toContextExpr vars
-  let h := mkApp2 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_nc_eq [ring.u]) ring.type ring.ringInst
-  return mkApp4 h ctx (toExpr lhs) (toExpr lhs') eagerReflBoolTrue
+  withAbstractAtoms vars ring.type fun vars => do
+    let ctx ← toContextExpr vars
+    let h := mkApp2 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_nc_eq [ring.u]) ring.type ring.ringInst
+    let h := mkApp4 h ctx (toExpr lhs) (toExpr lhs') eagerReflBoolTrue
+    let eqFn := mkApp (mkConst ``Eq [Level.succ ring.u]) ring.type
+    let expected := mkApp2 eqFn (← lhs.denoteExpr' vars) (← lhs'.denoteExpr' vars)
+    return mkExpectedPropHint h expected
 
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -10,6 +10,28 @@ public import Lean.Meta.SynthInstance
 public import Init.Data.Rat.Basic
 public section
 namespace Lean.Meta.Grind.Arith
+/--
+To prevent the kernel from accidentally reducing the atoms in the equation while typechecking,
+we abstract over them.
+-/
+def withAbstractAtoms [Monad m] [MonadControlT MetaM m] [MonadLiftT CoreM m] [MonadLiftT MetaM m]
+    (atoms : Array Expr) (type : Expr) (k : Array Expr → m Expr) : m Expr := do
+  let rec go (i : Nat) (atoms' : Array Expr) (xs : Array Expr) (args : Array Expr) : m Expr := do
+    if h : i < atoms.size then
+      let atom := atoms[i]
+      if atom.isFVar then
+        go (i+1) (atoms'.push atom) xs args
+      else
+        withLocalDeclD (← mkFreshUserName `x) type fun x =>
+          go (i+1) (atoms'.push x) (xs.push x) (args.push atom)
+    else
+      let p ← k atoms'
+      if xs.isEmpty then
+        return p
+      else
+        return mkAppN (← mkLambdaFVars xs p) args
+  go 0 #[] #[] #[]
+
 /-- Returns `true` if `e` is a numeral and has type `Nat`. -/
 def isNatNum (e : Expr) : Bool := Id.run do
   let_expr OfNat.ofNat _ _ inst := e | false

src/Lean/Meta/Tactic/Grind/Order/Internalize.lean

@@ -77,20 +77,11 @@ def split (p : Poly) : Poly × Poly × Int :=
     else
       (.add k m lhs, rhs, c)
 
-def propEq := mkApp (mkConst ``Eq [1]) (mkSort 0)
-
-/--
-Given a proof `h` that `e = rel lhs rhs`, returns `(e', h')` where
-`e'` is `rel lhs rhs`, and `h'` is `h` with the expected proposition hint around it.
--/
-def mkExpectedHint (s : Struct) (e : Expr) (kind : CnstrKind) (lhs rhs : Expr) (h : Expr) : Expr × Expr :=
+def mkRel (s : Struct) (kind : CnstrKind) (lhs rhs : Expr) : Expr :=
   let rel := match kind with
     | .le => s.leFn
     | .lt => s.ltFn?.get!
-  let e' := mkApp2 rel lhs rhs
-  let prop :=  mkApp2 propEq e e'
-  let h' := mkExpectedPropHint h prop
-  (e', h')
+  mkApp2 rel lhs rhs
 
 def mkLeNorm0 (s : Struct) (ringInst : Expr) (lhs rhs : Expr) : Expr :=
   mkApp5 (mkConst ``Grind.CommRing.le_norm0 [s.u]) s.type ringInst s.leInst lhs rhs
@@ -111,13 +102,10 @@ Returns `rel lhs (rhs + 0)`
 -/
 def mkDenote0 [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m]
     (s : Struct) (kind : CnstrKind) (lhs rhs : Expr) : m Expr := do
-  let rel := match kind with
-    | .le => s.leFn
-    | .lt => s.ltFn?.get!
   let rhs' := mkApp2 (← getAddFn) rhs (mkApp (← getIntCastFn) (mkIntLit 0))
-  return mkApp2 rel lhs rhs'
+  return mkRel s kind lhs rhs'
 
-def mkCommRingCnstr? (e : Expr) (s : Struct) (kind : CnstrKind) (lhs rhs : Expr) : RingM (Option (Cnstr Expr)) := do
+def mkCommRingCnstr? (s : Struct) (kind : CnstrKind) (lhs rhs : Expr) : RingM (Option (Cnstr Expr)) := do
   if !isArithTerm lhs && !isArithTerm rhs then
     let e ← mkDenote0 s kind lhs rhs
     return some { u := lhs, v := rhs, k := 0, e, kind, h? := some (mkCnstrNorm0 s (← getRing).ringInst kind lhs rhs)  }
@@ -133,12 +121,12 @@ def mkCommRingCnstr? (e : Expr) (s : Struct) (kind : CnstrKind) (lhs rhs : Expr)
   let h ← match kind with
     | .le => mkLeIffProof s.leInst s.ltInst?.get! s.isPreorderInst s.orderedRingInst?.get! lhs rhs lhs' rhs'
     | .lt => mkLtIffProof s.leInst s.ltInst?.get! s.lawfulOrderLTInst?.get! s.isPreorderInst s.orderedRingInst?.get! lhs rhs lhs' rhs'
-  let (e', h') := mkExpectedHint s e kind u (← rhs'.denoteExpr) h
+  let e' := mkRel s kind u (← rhs'.denoteExpr)
   return some {
-    kind, u, v, k, e := e', h? := some h'
+    kind, u, v, k, e := e', h? := some h
   }
 
-def mkNonCommRingCnstr? (e : Expr) (s : Struct) (kind : CnstrKind) (lhs rhs : Expr) : NonCommRingM (Option (Cnstr Expr)) := do
+def mkNonCommRingCnstr? (s : Struct) (kind : CnstrKind) (lhs rhs : Expr) : NonCommRingM (Option (Cnstr Expr)) := do
   if !isArithTerm lhs && !isArithTerm rhs then
     let e ← mkDenote0 s kind lhs rhs
     return some { u := lhs, v := rhs, k := 0, e, kind, h? := some (mkCnstrNorm0 s (← getRing).ringInst kind lhs rhs)  }
@@ -155,18 +143,18 @@ def mkNonCommRingCnstr? (e : Expr) (s : Struct) (kind : CnstrKind) (lhs rhs : Ex
   let h ← match kind with
     | .le => mkNonCommLeIffProof s.leInst s.ltInst?.get! s.isPreorderInst s.orderedRingInst?.get! lhs rhs lhs' rhs'
     | .lt => mkNonCommLtIffProof s.leInst s.ltInst?.get! s.lawfulOrderLTInst?.get! s.isPreorderInst s.orderedRingInst?.get! lhs rhs lhs' rhs'
-  let (e', h') := mkExpectedHint s e kind u (← rhs'.denoteExpr) h
+  let e' := mkRel s kind u (← rhs'.denoteExpr)
   return some {
-    kind, u, v, k, e := e', h? := some h'
+    kind, u, v, k, e := e', h? := some h
   }
 
 def mkCnstr? (e : Expr) (kind : CnstrKind) (lhs rhs : Expr) : OrderM (Option (Cnstr Expr)) := do
   let s ← getStruct
   if let some ringId := s.ringId? then
     if s.isCommRing then
-      RingM.run ringId <| mkCommRingCnstr? e s kind lhs rhs
+      RingM.run ringId <| mkCommRingCnstr? s kind lhs rhs
     else
-      NonCommRingM.run ringId <| mkNonCommRingCnstr? e s kind lhs rhs
+      NonCommRingM.run ringId <| mkNonCommRingCnstr? s kind lhs rhs
   else
     return some { kind, u := lhs, v := rhs, e }
 

tests/lean/run/grind_proof_perf_issue.lean

@@ -0,0 +1,6 @@
+example {n : Nat} (hn : 500000 ≤ n) (hn' : n ≤ 2000000) : n - 500000 ≥ 1500001 → False := by
+  grind
+
+example {n : Nat} (hn : 57343 < n) (hn' : n < 1114112) :
+    n - (57343 + 1) < 1114111 - 57343 := by
+  grind