chore: check whether pointer equality implies structural equality in grind

This PR checks whether in the internal state of the `grind` tactic
pointer equality implies structural equality.

src/Init/Grind.lean

@@ -9,4 +9,3 @@ import Init.Grind.Tactics
 import Init.Grind.Lemmas
 import Init.Grind.Cases
 import Init.Grind.Propagator
-import Init.Grind.Util

src/Init/Grind/Lemmas.lean

@@ -7,7 +7,6 @@ prelude
 import Init.Core
 import Init.SimpLemmas
 import Init.Classical
-import Init.ByCases
 
 namespace Lean.Grind
 
@@ -42,9 +41,6 @@ theorem not_eq_of_eq_false {a : Prop} (h : a = False) : (Not a) = True := by sim
 theorem eq_false_of_not_eq_true {a : Prop} (h : (Not a) = True) : a = False := by simp_all
 theorem eq_true_of_not_eq_false {a : Prop} (h : (Not a) = False) : a = True := by simp_all
 
-theorem false_of_not_eq_self {a : Prop} (h : (Not a) = a) : False := by
-  by_cases a <;> simp_all
-
 /-! Eq -/
 
 theorem eq_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a = b) = b := by simp [h]

src/Init/Grind/Tactics.lean

@@ -12,33 +12,14 @@ The configuration for `grind`.
 Passed to `grind` using, for example, the `grind (config := { eager := true })` syntax.
 -/
 structure Config where
-  /-- When `eager` is true (default: `false`), `grind` eagerly splits `if-then-else` and `match` expressions during internalization. -/
-  eager : Bool := false
-  /-- Maximum number of branches (i.e., case-splits) in the proof search tree. -/
-  splits : Nat := 100
   /--
-  Maximum number of E-matching (aka heuristic theorem instantiation)
-  in a proof search tree branch.
+  When `eager` is true (default: `false`), `grind` eagerly splits `if-then-else` and `match`
+  expressions.
   -/
-  ematch : Nat := 5
-  /--
-  Maximum term generation.
-  The input goal terms have generation 0. When we instantiate a theorem using a term from generation `n`,
-  the new terms have generation `n+1`. Thus, this parameter limits the length of an instantiation chain. -/
-  gen : Nat := 5
-  /-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
-  instances : Nat := 1000
+  eager : Bool := false
   deriving Inhabited, BEq
 
-end Lean.Grind
-
-namespace Lean.Parser.Tactic
-
 /-!
 `grind` tactic and related tactics.
 -/
-
--- TODO: parameters
-syntax (name := grind) "grind" optConfig : tactic
-
-end Lean.Parser.Tactic
+end Lean.Grind

src/Init/Grind/Util.lean

@@ -11,9 +11,4 @@ namespace Lean.Grind
 /-- A helper gadget for annotating nested proofs in goals. -/
 def nestedProof (p : Prop) (h : p) : p := h
 
-set_option pp.proofs true
-
-theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (nestedProof p hp) (nestedProof q hq) := by
-  subst h; apply HEq.refl
-
 end Lean.Grind

src/Lean/Elab/Calc.lean

@@ -131,18 +131,14 @@ def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) :
     if ← isDefEqGuarded r er then
       let mut failed := false
       unless ← isDefEqGuarded lhs elhs do
-        let (lhs, elhs) ← addPPExplicitToExposeDiff lhs elhs
-        let (lhsTy, elhsTy) ← addPPExplicitToExposeDiff (← inferType lhs) (← inferType elhs)
         logErrorAt steps[0]!.term m!"\
-          invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {lhsTy}"}\n\
-          but is expected to be{indentD m!"{elhs} : {elhsTy}"}"
+          invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {← inferType lhs}"}\n\
+          but is expected to be{indentD m!"{elhs} : {← inferType elhs}"}"
         failed := true
       unless ← isDefEqGuarded rhs erhs do
-        let (rhs, erhs) ← addPPExplicitToExposeDiff rhs erhs
-        let (rhsTy, erhsTy) ← addPPExplicitToExposeDiff (← inferType rhs) (← inferType erhs)
         logErrorAt steps.back!.term m!"\
-          invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {rhsTy}"}\n\
-          but is expected to be{indentD m!"{erhs} : {erhsTy}"}"
+          invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {← inferType rhs}"}\n\
+          but is expected to be{indentD m!"{erhs} : {← inferType erhs}"}"
         failed := true
       if failed then
         throwAbortTerm

src/Lean/Elab/CheckTactic.lean

@@ -38,7 +38,6 @@ def elabCheckTactic : CommandElab := fun stx => do
       | [next] => do
         let (val, _, _) ← matchCheckGoalType stx (←next.getType)
         if !(← Meta.withReducible <| isDefEq val expTerm) then
-          let (val, expTerm) ← addPPExplicitToExposeDiff val expTerm
           throwErrorAt stx
             m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
       | _ => do

src/Lean/Elab/Deriving.lean

@@ -16,4 +16,3 @@ import Lean.Elab.Deriving.FromToJson
 import Lean.Elab.Deriving.SizeOf
 import Lean.Elab.Deriving.Hashable
 import Lean.Elab.Deriving.Ord
-import Lean.Elab.Deriving.ToExpr

src/Lean/Elab/Deriving/ToExpr.lean

@@ -1,237 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kyle Miller
--/
-prelude
-import Lean.Meta.Transform
-import Lean.Elab.Deriving.Basic
-import Lean.Elab.Deriving.Util
-import Lean.ToLevel
-import Lean.ToExpr
-
-/-!
-# `ToExpr` deriving handler
-
-This module defines a `ToExpr` deriving handler for inductive types.
-It supports mutually inductive types as well.
-
-The `ToExpr` deriving handlers support universe level polymorphism, via the `Lean.ToLevel` class.
-To use `ToExpr` in places where there is universe polymorphism, make sure a `[ToLevel.{u}]` instance is available,
-though be aware that the `ToLevel` mechanism does not support `max` or `imax` expressions.
-
-Implementation note: this deriving handler was initially modeled after the `Repr` deriving handler, but
-1. we need to account for universe levels,
-2. the `ToExpr` class has two fields rather than one, and
-3. we don't handle structures specially.
--/
-
-namespace Lean.Elab.Deriving.ToExpr
-
-open Lean Elab Parser.Term
-open Meta Command Deriving
-
-/--
-Given `args := #[e₁, e₂, …, eₙ]`, constructs the syntax `Expr.app (… (Expr.app (Expr.app f e₁) e₂) …) eₙ`.
--/
-def mkAppNTerm (f : Term) (args : Array Term) : MetaM Term :=
-  args.foldlM (fun a b => ``(Expr.app $a $b)) f
-
-/-- Fixes the output of `mkInductiveApp` to explicitly reference universe levels. -/
-def updateIndType (indVal : InductiveVal) (t : Term) : TermElabM Term :=
-  let levels := indVal.levelParams.toArray.map mkIdent
-  match t with
-  | `(@$f $args*) => `(@$f.{$levels,*} $args*)
-  | _ => throwError "(internal error) expecting output of `mkInductiveApp`"
-
-/--
-Creates a term that evaluates to an expression representing the inductive type.
-Uses `toExpr` and `toTypeExpr` for the arguments to the type constructor.
--/
-def mkToTypeExpr (indVal : InductiveVal) (argNames : Array Name) : TermElabM Term := do
-  let levels ← indVal.levelParams.toArray.mapM (fun u => `(Lean.toLevel.{$(mkIdent u)}))
-  forallTelescopeReducing indVal.type fun xs _ => do
-    let mut args : Array Term := #[]
-    for argName in argNames, x in xs do
-      let a := mkIdent argName
-      if ← Meta.isType x then
-        args := args.push <| ← ``(toTypeExpr $a)
-      else
-        args := args.push <| ← ``(toExpr $a)
-    mkAppNTerm (← ``(Expr.const $(quote indVal.name) [$levels,*])) args
-
-/--
-Creates the body of the `toExpr` function for the `ToExpr` instance, which is a `match` expression
-that calls `toExpr` and `toTypeExpr` to assemble an expression for a given term.
-For recursive inductive types, `auxFunName` refers to the `ToExpr` instance for the current type.
-For mutually recursive types, we rely on the local instances set up by `mkLocalInstanceLetDecls`.
--/
-def mkToExprBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) (levelInsts : Array Term) :
-    TermElabM Term := do
-  let discrs ← mkDiscrs header indVal
-  let alts ← mkAlts
-  `(match $[$discrs],* with $alts:matchAlt*)
-where
-  /-- Create the `match` cases, one per constructor. -/
-  mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do
-    let levels ← levelInsts.mapM fun inst => `($(inst).toLevel)
-    let mut alts := #[]
-    for ctorName in indVal.ctors do
-      let ctorInfo ← getConstInfoCtor ctorName
-      let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do
-        let mut patterns := #[]
-        -- add `_` pattern for indices, before the constructor's pattern
-        for _ in [:indVal.numIndices] do
-          patterns := patterns.push (← `(_))
-        let mut ctorArgs := #[]
-        let mut rhsArgs : Array Term := #[]
-        let mkArg (x : Expr) (a : Term) : TermElabM Term := do
-          if (← inferType x).isAppOf indVal.name then
-            `($(mkIdent auxFunName) $levelInsts* $a)
-          else if ← Meta.isType x then
-            ``(toTypeExpr $a)
-          else
-            ``(toExpr $a)
-        -- add `_` pattern for inductive parameters, which are inaccessible
-        for i in [:ctorInfo.numParams] do
-          let a := mkIdent header.argNames[i]!
-          ctorArgs := ctorArgs.push (← `(_))
-          rhsArgs := rhsArgs.push <| ← mkArg xs[i]! a
-        for i in [:ctorInfo.numFields] do
-          let a := mkIdent (← mkFreshUserName `a)
-          ctorArgs := ctorArgs.push a
-          rhsArgs := rhsArgs.push <| ← mkArg xs[ctorInfo.numParams + i]! a
-        patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*))
-        let rhs : Term ← mkAppNTerm (← ``(Expr.const $(quote ctorInfo.name) [$levels,*])) rhsArgs
-        `(matchAltExpr| | $[$patterns:term],* => $rhs)
-      alts := alts.push alt
-    return alts
-
-/--
-For nested and mutually recursive inductive types, we define `partial` instances,
-and the strategy is to have local `ToExpr` instances in scope for the body of each instance.
-This way, each instance can freely use `toExpr` and `toTypeExpr` for each of the types in `ctx`.
-
-This is a modified copy of `Lean.Elab.Deriving.mkLocalInstanceLetDecls`,
-since we need to include the `toTypeExpr` field in the `letDecl`
-Note that, for simplicity, each instance gets its own definition of each others' `toTypeExpr` fields.
-These are very simple fields, so avoiding the duplication is not worth it.
--/
-def mkLocalInstanceLetDecls (ctx : Deriving.Context) (argNames : Array Name) (levelInsts : Array Term) :
-    TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do
-  let mut letDecls := #[]
-  for indVal in ctx.typeInfos, auxFunName in ctx.auxFunNames do
-    let currArgNames ← mkInductArgNames indVal
-    let numParams    := indVal.numParams
-    let currIndices  := currArgNames[numParams:]
-    let binders      ← mkImplicitBinders currIndices
-    let argNamesNew  := argNames[:numParams] ++ currIndices
-    let indType      ← mkInductiveApp indVal argNamesNew
-    let instName     ← mkFreshUserName `localinst
-    let toTypeExpr   ← mkToTypeExpr indVal argNames
-    -- Recall that mutually inductive types all use the same universe levels, hence we pass the same ToLevel instances to each aux function.
-    let letDecl      ← `(Parser.Term.letDecl| $(mkIdent instName):ident $binders:implicitBinder* : ToExpr $indType :=
-                          { toExpr     := $(mkIdent auxFunName) $levelInsts*,
-                            toTypeExpr := $toTypeExpr })
-    letDecls := letDecls.push letDecl
-  return letDecls
-
-open TSyntax.Compat in
-/--
-Makes a `toExpr` function for the given inductive type.
-The implementation of each `toExpr` function for a (mutual) inductive type is given as top-level private definitions.
-These are assembled into `ToExpr` instances in `mkInstanceCmds`.
-For mutual/nested inductive types, then each of the types' `ToExpr` instances are provided as local instances,
-to wire together the recursion (necessitating these auxiliary definitions being `partial`).
--/
-def mkAuxFunction (ctx : Deriving.Context) (i : Nat) : TermElabM Command := do
-  let auxFunName := ctx.auxFunNames[i]!
-  let indVal     := ctx.typeInfos[i]!
-  let header     ← mkHeader ``ToExpr 1 indVal
-  /- We make the `ToLevel` instances be explicit here so that we can pass the instances from the instances to the
-     aux functions. This lets us ensure universe level variables are being lined up,
-     without needing to use `ident.{u₁,…,uₙ}` syntax, which could conditionally be incorrect
-     depending on the ambient CommandElabM scope state.
-     TODO(kmill): deriving handlers should run in a scope with no `universes` or `variables`. -/
-  let (toLevelInsts, levelBinders) := Array.unzip <| ← indVal.levelParams.toArray.mapM fun u => do
-    let inst := mkIdent (← mkFreshUserName `inst)
-    return (inst, ← `(explicitBinderF| ($inst : ToLevel.{$(mkIdent u)})))
-  let mut body ← mkToExprBody header indVal auxFunName toLevelInsts
-  if ctx.usePartial then
-    let letDecls ← mkLocalInstanceLetDecls ctx header.argNames toLevelInsts
-    body ← mkLet letDecls body
-  /- We need to alter the last binder (the one for the "target") to have explicit universe levels
-     so that the `ToLevel` instance arguments can use them. -/
-  let addLevels binder :=
-    match binder with
-    | `(bracketedBinderF| ($a : $ty)) => do `(bracketedBinderF| ($a : $(← updateIndType indVal ty)))
-    | _ => throwError "(internal error) expecting inst binder"
-  let binders := header.binders.pop ++ levelBinders ++ #[← addLevels header.binders.back!]
-  if ctx.usePartial then
-    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Expr := $body:term)
-  else
-    `(private         def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Expr := $body:term)
-
-/--
-Creates all the auxiliary functions (using `mkAuxFunction`) for the (mutual) inductive type(s).
-Wraps the resulting definition commands in `mutual ... end`.
--/
-def mkAuxFunctions (ctx : Deriving.Context) : TermElabM Syntax := do
-  let mut auxDefs := #[]
-  for i in [:ctx.typeInfos.size] do
-    auxDefs := auxDefs.push (← mkAuxFunction ctx i)
-  `(mutual $auxDefs:command* end)
-
-open TSyntax.Compat in
-/--
-Assuming all of the auxiliary definitions exist,
-creates all the `instance` commands for the `ToExpr` instances for the (mutual) inductive type(s).
-This is a modified copy of `Lean.Elab.Deriving.mkInstanceCmds` to account for `ToLevel` instances.
--/
-def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) :
-    TermElabM (Array Command) := do
-  let mut instances := #[]
-  for indVal in ctx.typeInfos, auxFunName in ctx.auxFunNames do
-    if typeNames.contains indVal.name then
-      let argNames     ← mkInductArgNames indVal
-      let binders      ← mkImplicitBinders argNames
-      let binders      := binders ++ (← mkInstImplicitBinders ``ToExpr indVal argNames)
-      let (toLevelInsts, levelBinders) := Array.unzip <| ← indVal.levelParams.toArray.mapM fun u => do
-        let inst := mkIdent (← mkFreshUserName `inst)
-        return (inst, ← `(instBinderF| [$inst : ToLevel.{$(mkIdent u)}]))
-      let binders      := binders ++ levelBinders
-      let indType      ← updateIndType indVal (← mkInductiveApp indVal argNames)
-      let toTypeExpr   ← mkToTypeExpr indVal argNames
-      let instCmd ← `(instance $binders:implicitBinder* : ToExpr $indType where
-                        toExpr := $(mkIdent auxFunName) $toLevelInsts*
-                        toTypeExpr := $toTypeExpr)
-      instances := instances.push instCmd
-  return instances
-
-/--
-Returns all the commands necessary to construct the `ToExpr` instances.
--/
-def mkToExprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "toExpr" declNames[0]!
-  let cmds := #[← mkAuxFunctions ctx] ++ (← mkInstanceCmds ctx declNames)
-  trace[Elab.Deriving.toExpr] "\n{cmds}"
-  return cmds
-
-/--
-The main entry point to the `ToExpr` deriving handler.
--/
-def mkToExprInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
-  if (← declNames.allM isInductive) && declNames.size > 0 then
-    let cmds ← withFreshMacroScope <| liftTermElabM <| mkToExprInstanceCmds declNames
-    -- Enable autoimplicits, used for universe levels.
-    withScope (fun scope => { scope with opts := autoImplicit.set scope.opts true }) do
-      elabCommand (mkNullNode cmds)
-    return true
-  else
-    return false
-
-builtin_initialize
-  registerDerivingHandler ``Lean.ToExpr mkToExprInstanceHandler
-  registerTraceClass `Elab.Deriving.toExpr
-
-end Lean.Elab.Deriving.ToExpr

src/Lean/Elab/Tactic.lean

@@ -44,4 +44,3 @@ import Lean.Elab.Tactic.DiscrTreeKey
 import Lean.Elab.Tactic.BVDecide
 import Lean.Elab.Tactic.BoolToPropSimps
 import Lean.Elab.Tactic.Classical
-import Lean.Elab.Tactic.Grind

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -82,7 +82,7 @@ instance : ToExpr Gate where
     | .and => mkConst ``Gate.and
     | .xor => mkConst ``Gate.xor
     | .beq => mkConst ``Gate.beq
-    | .or => mkConst ``Gate.or
+    | .imp => mkConst ``Gate.imp
   toTypeExpr := mkConst ``Gate
 
 instance : ToExpr BVPred where

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean

@@ -91,7 +91,7 @@ where
     | .and => ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
     | .xor => ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
     | .beq => ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
-    | .or => ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
+    | .imp => ``Std.Tactic.BVDecide.Reflect.Bool.imp_congr
 
 /--
 Construct the reified version of `Bool.not subExpr`.
@@ -136,7 +136,7 @@ def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr)
         lhsEvalExpr lhsProof?
         rhsEvalExpr rhsProof? | return none
     return mkApp9
-      (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.cond_congr)
+      (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.ite_congr)
       discrExpr lhsExpr rhsExpr
       discrEvalExpr lhsEvalExpr rhsEvalExpr
       discrProof lhsProof rhsProof

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean

@@ -22,70 +22,67 @@ This function adds the two lemmas:
 - `discrExpr = false → atomExpr = rhsExpr`
 It assumes that `discrExpr`, `lhsExpr` and `rhsExpr` are the expressions corresponding to `discr`,
 `lhs` and `rhs`. Furthermore it assumes that `atomExpr` is of the form
-`bif discrExpr then lhsExpr else rhsExpr`.
+`if discrExpr = true then lhsExpr else rhsExpr`.
 -/
-def addCondLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+def addIfLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
     (discrExpr atomExpr lhsExpr rhsExpr : Expr) : LemmaM Unit := do
-  let some trueLemma ← mkCondTrueLemma discr atom lhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  let some trueLemma ← mkIfTrueLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
   LemmaM.addLemma trueLemma
-  let some falseLemma ← mkCondFalseLemma discr atom rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  let some falseLemma ← mkIfFalseLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
   LemmaM.addLemma falseLemma
 where
-  mkCondTrueLemma (discr : ReifiedBVLogical) (atom lhs : ReifiedBVExpr)
+  mkIfTrueLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
+    mkIfLemma true discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
+
+  mkIfFalseLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
+    mkIfLemma false discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
+
+  mkIfLemma (discrVal : Bool) (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
       (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
-    let resExpr := lhsExpr
-    let resValExpr := lhs
-    let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_true
+    let resExpr := if discrVal then lhsExpr else rhsExpr
+    let resValExpr := if discrVal then lhs else rhs
+    let lemmaName :=
+      if discrVal then
+        ``Std.Tactic.BVDecide.Reflect.BitVec.if_true
+      else
+        ``Std.Tactic.BVDecide.Reflect.BitVec.if_false
+    let discrValExpr := toExpr discrVal
+    let discrVal ← ReifiedBVLogical.mkBoolConst discrVal
 
-
-    let notDiscrExpr := mkApp (mkConst ``Bool.not) discrExpr
-    let notDiscr ← ReifiedBVLogical.mkNot discr discrExpr
+    let eqDiscrExpr ← mkAppM ``BEq.beq #[discrExpr, discrValExpr]
+    let eqDiscr ← ReifiedBVLogical.mkGate discr discrVal discrExpr discrValExpr .beq
 
     let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
     let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
     let eqBV ← ReifiedBVLogical.ofPred eqBVPred
 
-    let imp ← ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr eqBVExpr .or
+    let imp ← ReifiedBVLogical.mkGate eqDiscr eqBV eqDiscrExpr eqBVExpr .imp
 
     let proof := do
       let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
       let congrProof := (← imp.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalExpr)
       let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr lhs.width) discrExpr lhsExpr rhsExpr
 
-      -- !discr || (atom == rhs)
-      let impExpr := mkApp2 (mkConst ``Bool.or) notDiscrExpr eqBVExpr
+      let trueExpr := mkConst ``Bool.true
+      let eqDiscrTrueExpr ← mkEq eqDiscrExpr trueExpr
+      let eqBVExprTrueExpr ← mkEq eqBVExpr trueExpr
+      let impExpr ← mkArrow eqDiscrTrueExpr eqBVExprTrueExpr
+      -- construct a `Decidable` instance for the implication using forall_prop_decidable
+      let decEqDiscrTrue := mkApp2 (mkConst ``instDecidableEqBool) eqDiscrExpr trueExpr
+      let decEqBVExprTrue := mkApp2 (mkConst ``instDecidableEqBool) eqBVExpr trueExpr
+      let impDecidable := mkApp4 (mkConst ``forall_prop_decidable)
+        eqDiscrTrueExpr
+        (.lam .anonymous eqDiscrTrueExpr eqBVExprTrueExpr .default)
+        decEqDiscrTrue
+        (.lam .anonymous eqDiscrTrueExpr decEqBVExprTrue .default)
+
+      let decideImpExpr := mkApp2 (mkConst ``Decidable.decide) impExpr impDecidable
 
       return mkApp4
         (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
-        impExpr
-        evalExpr
-        congrProof
-        lemmaProof
-    return some ⟨imp.bvExpr, proof, imp.expr⟩
-
-  mkCondFalseLemma (discr : ReifiedBVLogical) (atom rhs : ReifiedBVExpr)
-      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
-    let resExpr := rhsExpr
-    let resValExpr := rhs
-    let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_false
-
-    let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
-    let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
-    let eqBV ← ReifiedBVLogical.ofPred eqBVPred
-
-    let imp ← ReifiedBVLogical.mkGate discr eqBV discrExpr eqBVExpr .or
-
-    let proof := do
-      let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
-      let congrProof := (← imp.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalExpr)
-      let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr rhs.width) discrExpr lhsExpr rhsExpr
-
-      -- discr || (atom == rhs)
-      let impExpr := mkApp2 (mkConst ``Bool.or) discrExpr eqBVExpr
-
-      return mkApp4
-        (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
-        impExpr
+        decideImpExpr
         evalExpr
         congrProof
         lemmaProof

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -220,12 +220,15 @@ where
         .rotateRight
         ``BVUnOp.rotateRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
-    | cond _ discrExpr lhsExpr rhsExpr =>
+    | ite _ discrExpr _ lhsExpr rhsExpr =>
+      let_expr Eq α discrExpr val := discrExpr | return none
+      let_expr Bool := α | return none
+      let_expr Bool.true := val | return none
       let some atom ← ReifiedBVExpr.bitVecAtom x true | return none
       let some discr ← ReifiedBVLogical.of discrExpr | return none
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none
-      addCondLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
+      addIfLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
       return some atom
     | _ => return none
 
@@ -389,7 +392,10 @@ where
       | Bool => gateReflection lhsExpr rhsExpr .beq
       | BitVec _ => goPred t
       | _ => return none
-    | cond _ discrExpr lhsExpr rhsExpr =>
+    | ite _ discrExpr _ lhsExpr rhsExpr =>
+      let_expr Eq α discrExpr val := discrExpr | return none
+      let_expr Bool := α | return none
+      let_expr Bool.true := val | return none
       let some discr ← goOrAtom discrExpr | return none
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -28,18 +28,6 @@ namespace Frontend.Normalize
 open Lean.Meta
 open Std.Tactic.BVDecide.Normalize
 
-builtin_simproc ↓ [bv_normalize] reduceCond (cond _ _ _) := fun e => do
-  let_expr f@cond α c tb eb := e | return .continue
-  let r ← Simp.simp c
-  if r.expr.cleanupAnnotations.isConstOf ``Bool.true then
-    let pr := mkApp (mkApp4 (mkConst ``Bool.cond_pos f.constLevels!) α c tb eb) (← r.getProof)
-    return .visit { expr := tb, proof? := pr }
-  else if r.expr.cleanupAnnotations.isConstOf ``Bool.false then
-    let pr := mkApp (mkApp4 (mkConst ``Bool.cond_neg f.constLevels!) α c tb eb) (← r.getProof)
-    return .visit { expr := eb, proof? := pr }
-  else
-    return .continue
-
 builtin_simproc [bv_normalize] eqToBEq (((_ : Bool) = (_ : Bool))) := fun e => do
   let_expr Eq _ lhs rhs := e | return .continue
   match_expr rhs with
@@ -139,6 +127,8 @@ builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _))
       else
         return .continue
 
+attribute [builtin_bv_normalize_proc↓] reduceIte
+
 /-- Return a number `k` such that `2^k = n`. -/
 private def Nat.log2Exact (n : Nat) : Option Nat := do
   guard <| n ≠ 0

src/Lean/Elab/Tactic/Grind.lean

@@ -1,49 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Grind.Tactics
-import Lean.Meta.Tactic.Grind
-import Lean.Elab.Command
-import Lean.Elab.Tactic.Basic
-import Lean.Elab.Tactic.Config
-
-namespace Lean.Elab.Tactic
-open Meta
-
-declare_config_elab elabGrindConfig Grind.Config
-
-open Command Term in
-@[builtin_command_elab Lean.Parser.Command.grindPattern]
-def elabGrindPattern : CommandElab := fun stx => do
-  match stx with
-  | `(grind_pattern $thmName:ident => $terms,*) => do
-    liftTermElabM do
-      let declName ← resolveGlobalConstNoOverload thmName
-      discard <| addTermInfo thmName (← mkConstWithLevelParams declName)
-      let info ← getConstInfo declName
-      forallTelescope info.type fun xs _ => do
-        let patterns ← terms.getElems.mapM fun term => do
-          let pattern ← instantiateMVars (← elabTerm term none)
-          let pattern ← Grind.unfoldReducible pattern
-          return pattern.abstract xs
-        Grind.addEMatchTheorem declName xs.size patterns.toList
-  | _ => throwUnsupportedSyntax
-
-def grind (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) : MetaM Unit := do
-  let mvarIds ← Grind.main mvarId config mainDeclName
-  unless mvarIds.isEmpty do
-    throwError "`grind` failed\n{goalsToMessageData mvarIds}"
-
-@[builtin_tactic Lean.Parser.Tactic.grind] def evalApplyRfl : Tactic := fun stx => do
-  match stx with
-  | `(tactic| grind $config:optConfig) =>
-    logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
-    let declName := (← Term.getDeclName?).getD `_grind
-    let config ← elabGrindConfig config
-    withMainContext do liftMetaFinishingTactic (grind · config declName)
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic

src/Lean/Expr.lean

@@ -1648,23 +1648,6 @@ def isFalse (e : Expr) : Bool :=
 def isTrue (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``True
 
-/--
-`getForallArity type` returns the arity of a `forall`-type. This function consumes nested annotations,
-and performs pending beta reductions. It does **not** use whnf.
-Examples:
-- If `a` is `Nat`, `getForallArity a` returns `0`
-- If `a` is `Nat → Bool`, `getForallArity a` returns `1`
--/
-partial def getForallArity : Expr → Nat
-  | .mdata _ b       => getForallArity b
-  | .forallE _ _ b _ => getForallArity b + 1
-  | e                =>
-    if e.isHeadBetaTarget then
-      getForallArity e.headBeta
-    else
-      let e' := e.cleanupAnnotations
-      if e != e' then getForallArity e' else 0
-
 /--
 Checks if an expression is a "natural number numeral in normal form",
 i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`

src/Lean/Meta/AppBuilder.lean

@@ -176,14 +176,6 @@ def mkEqOfHEq (h : Expr) : MetaM Expr := do
   | _ =>
     throwAppBuilderException ``eq_of_heq m!"heterogeneous equality proof expected{indentExpr h}"
 
-/-- Given `h : Eq a b`, returns a proof of `HEq a b`. -/
-def mkHEqOfEq (h : Expr) : MetaM Expr := do
-  let hType ← infer h
-  let some (α, a, b) := hType.eq?
-    | throwAppBuilderException ``heq_of_eq m!"equality proof expected{indentExpr h}"
-  let u ← getLevel α
-  return mkApp4 (mkConst ``heq_of_eq [u]) α a b h
-
 /--
 If `e` is `@Eq.refl α a`, return `a`.
 -/

src/Lean/Meta/Check.lean

@@ -17,6 +17,14 @@ namespace Lean.Meta
 private def ensureType (e : Expr) : MetaM Unit := do
   discard <| getLevel e
 
+def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
+  let lctx ← getLCtx
+  match lctx.find? fvarId with
+  | some (LocalDecl.ldecl _ _ _ t v _ _) => do
+    let vType ← inferType v
+    throwError "invalid let declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}"
+  | _ => unreachable!
+
 private def checkConstant (constName : Name) (us : List Level) : MetaM Unit := do
   let cinfo ← getConstInfo constName
   unless us.length == cinfo.levelParams.length do
@@ -169,15 +177,6 @@ where
     catch _ =>
       return (a, b)
 
-def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
-  let lctx ← getLCtx
-  match lctx.find? fvarId with
-  | some (LocalDecl.ldecl _ _ _ t v _ _) => do
-    let vType ← inferType v
-    let (vType, t) ← addPPExplicitToExposeDiff vType t
-    throwError "invalid let declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}"
-  | _ => unreachable!
-
 /--
   Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
 -/

src/Lean/Meta/Tactic/Grind.lean

@@ -19,30 +19,16 @@ import Lean.Meta.Tactic.Grind.Proof
 import Lean.Meta.Tactic.Grind.Propagate
 import Lean.Meta.Tactic.Grind.PP
 import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.Ctor
-import Lean.Meta.Tactic.Grind.Parser
-import Lean.Meta.Tactic.Grind.EMatchTheorem
 
 namespace Lean
 
-/-! Trace options for `grind` users -/
 builtin_initialize registerTraceClass `grind
-builtin_initialize registerTraceClass `grind.assert
-builtin_initialize registerTraceClass `grind.eqc
-builtin_initialize registerTraceClass `grind.internalize
-builtin_initialize registerTraceClass `grind.ematch
-builtin_initialize registerTraceClass `grind.ematch.pattern
-builtin_initialize registerTraceClass `grind.ematch.instance
-builtin_initialize registerTraceClass `grind.ematch.instance.assignment
+builtin_initialize registerTraceClass `grind.eq
 builtin_initialize registerTraceClass `grind.issues
-builtin_initialize registerTraceClass `grind.simp
-
-/-! Trace options for `grind` developers -/
+builtin_initialize registerTraceClass `grind.add
+builtin_initialize registerTraceClass `grind.pre
 builtin_initialize registerTraceClass `grind.debug
-builtin_initialize registerTraceClass `grind.debug.proofs
-builtin_initialize registerTraceClass `grind.debug.congr
-builtin_initialize registerTraceClass `grind.debug.pre
-builtin_initialize registerTraceClass `grind.debug.proof
-builtin_initialize registerTraceClass `grind.debug.proj
+builtin_initialize registerTraceClass `grind.simp
+builtin_initialize registerTraceClass `grind.congr
 
 end Lean

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

@@ -9,11 +9,58 @@ import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.PP
-import Lean.Meta.Tactic.Grind.Ctor
-import Lean.Meta.Tactic.Grind.Internalize
 
 namespace Lean.Meta.Grind
 
+/-- We use this auxiliary constant to mark delayed congruence proofs. -/
+private def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
+
+/-- Adds `e` to congruence table. -/
+private def addCongrTable (e : Expr) : GoalM Unit := do
+  if let some { e := e' } := (← get).congrTable.find? { e } then
+    trace[grind.congr] "{e} = {e'}"
+    pushEqHEq e e' congrPlaceholderProof
+    -- TODO: we must check whether the types of the functions are the same
+    -- TODO: update cgRoot for `e`
+  else
+    modify fun s => { s with congrTable := s.congrTable.insert { e } }
+
+partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
+  if (← alreadyInternalized e) then return ()
+  match e with
+  | .bvar .. => unreachable!
+  | .sort .. => return ()
+  | .fvar .. | .letE .. | .lam .. | .forallE .. =>
+    mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
+  | .lit .. | .const .. =>
+    mkENode e generation
+  | .mvar ..
+  | .mdata ..
+  | .proj .. =>
+    trace[grind.issues] "unexpected term during internalization{indentExpr e}"
+    mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
+  | .app .. =>
+    if (← isLitValue e) then
+      -- We do not want to internalize the components of a literal value.
+      mkENode e generation
+    else e.withApp fun f args => do
+      if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
+        -- We only internalize the proposition. We can skip the proof because of
+        -- proof irrelevance
+        let c := args[0]!
+        internalize c generation
+        registerParent e c
+      else
+        unless f.isConst do
+          internalize f generation
+          registerParent e f
+        for h : i in [: args.size] do
+          let arg := args[i]
+          internalize arg generation
+          registerParent e arg
+      mkENode e generation
+      addCongrTable e
+
 /--
 The fields `target?` and `proof?` in `e`'s `ENode` are encoding a transitivity proof
 from `e` to the root of the equivalence class
@@ -34,6 +81,9 @@ where
       proof?  := proofNew?
     }
 
+private def markAsInconsistent : GoalM Unit :=
+  modify fun s => { s with inconsistent := true }
+
 /--
 Remove `root` parents from the congruence table.
 This is an auxiliary function performed while merging equivalence classes.
@@ -52,51 +102,20 @@ private def reinsertParents (parents : ParentSet) : GoalM Unit := do
   for parent in parents do
     addCongrTable parent
 
-/-- Closes the goal when `True` and `False` are in the same equivalence class. -/
-private def closeGoalWithTrueEqFalse : GoalM Unit := do
-  let mvarId := (← get).mvarId
-  unless (← mvarId.isAssigned) do
-    let trueEqFalse ← mkEqFalseProof (← getTrueExpr)
-    let falseProof ← mkEqMP trueEqFalse (mkConst ``True.intro)
-    closeGoal falseProof
-
-/-- Closes the goal when `lhs` and `rhs` are both literal values and belong to the same equivalence class. -/
-private def closeGoalWithValuesEq (lhs rhs : Expr) : GoalM Unit := do
-  let p ← mkEq lhs rhs
-  let hp ← mkEqProof lhs rhs
-  let d ← mkDecide p
-  let pEqFalse := mkApp3 (mkConst ``eq_false_of_decide) p d.appArg! (mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Bool) (mkConst ``false))
-  let falseProof ← mkEqMP pEqFalse hp
-  closeGoal falseProof
-
-/--
-Updates the modification time to `gmt` for the parents of `root`.
-The modification time is used to decide which terms are considered during e-matching.
--/
-private partial def updateMT (root : Expr) : GoalM Unit := do
-  let gmt := (← get).gmt
-  for parent in (← getParents root) do
-    let node ← getENode parent
-    if node.mt < gmt then
-      setENode parent { node with mt := gmt }
-      updateMT parent
-
 private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
+  trace[grind.eq] "{lhs} {if isHEq then "≡" else "="} {rhs}"
   let lhsNode ← getENode lhs
   let rhsNode ← getENode rhs
   if isSameExpr lhsNode.root rhsNode.root then
     -- `lhs` and `rhs` are already in the same equivalence class.
     trace[grind.debug] "{← ppENodeRef lhs} and {← ppENodeRef rhs} are already in the same equivalence class"
     return ()
-  trace[grind.eqc] "{lhs} {if isHEq then "≡" else "="} {rhs}"
   let lhsRoot ← getENode lhsNode.root
   let rhsRoot ← getENode rhsNode.root
   let mut valueInconsistency := false
-  let mut trueEqFalse := false
   if lhsRoot.interpreted && rhsRoot.interpreted then
     if lhsNode.root.isTrue || rhsNode.root.isTrue then
       markAsInconsistent
-      trueEqFalse := true
     else
       valueInconsistency := true
   if    (lhsRoot.interpreted && !rhsRoot.interpreted)
@@ -105,14 +124,7 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
     go rhs lhs rhsNode lhsNode rhsRoot lhsRoot true
   else
     go lhs rhs lhsNode rhsNode lhsRoot rhsRoot false
-  if trueEqFalse then
-    closeGoalWithTrueEqFalse
-  unless (← isInconsistent) do
-    if lhsRoot.ctor && rhsRoot.ctor then
-      propagateCtor lhsRoot.self rhsRoot.self
-  unless (← isInconsistent) do
-    if valueInconsistency then
-      closeGoalWithValuesEq lhsRoot.self rhsRoot.self
+  -- TODO: propagate value inconsistency
   trace[grind.debug] "after addEqStep, {← ppState}"
   checkInvariants
 where
@@ -133,6 +145,7 @@ where
       flipped
     }
     let parents ← removeParents lhsRoot.self
+    -- TODO: set propagateBool
     updateRoots lhs rhsNode.root
     trace[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
     reinsertParents parents
@@ -149,11 +162,10 @@ where
     unless (← isInconsistent) do
       for parent in parents do
         propagateUp parent
-    unless (← isInconsistent) do
-      updateMT rhsRoot.self
 
   updateRoots (lhs : Expr) (rootNew : Expr) : GoalM Unit := do
     let rec loop (e : Expr) : GoalM Unit := do
+      -- TODO: propagateBool
       let n ← getENode e
       setENode e { n with root := rootNew }
       unless (← isInconsistent) do
@@ -181,7 +193,6 @@ where
     if (← isInconsistent) then
       resetNewEqs
       return ()
-    checkSystem "grind"
     let some { lhs, rhs, proof, isHEq } := (← popNextEq?) | return ()
     addEqStep lhs rhs proof isHEq
     processTodo
@@ -196,7 +207,7 @@ def addHEq (lhs rhs proof : Expr) : GoalM Unit := do
 Adds a new `fact` justified by the given proof and using the given generation.
 -/
 def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
-  trace[grind.assert] "{fact}"
+  trace[grind.add] "{proof} : {fact}"
   if (← isInconsistent) then return ()
   resetNewEqs
   let_expr Not p := fact
@@ -204,6 +215,7 @@ def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
   go p true
 where
   go (p : Expr) (isNeg : Bool) : GoalM Unit := do
+    trace[grind.add] "isNeg: {isNeg}, {p}"
     match_expr p with
     | Eq _ lhs rhs => goEq p lhs rhs isNeg false
     | HEq _ lhs _ rhs => goEq p lhs rhs isNeg true

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

@@ -1,49 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Grind.Types
-
-namespace Lean.Meta.Grind
-
-private partial def propagateInjEqs (eqs : Expr) (proof : Expr) : GoalM Unit := do
-  match_expr eqs with
-  | And left right =>
-    propagateInjEqs left (.proj ``And 0 proof)
-    propagateInjEqs right (.proj ``And 1 proof)
-  | Eq _ lhs rhs    => pushEq lhs rhs proof
-  | HEq _ lhs _ rhs => pushHEq lhs rhs proof
-  | _ =>
-   trace[grind.issues] "unexpected injectivity theorem result type{indentExpr eqs}"
-   return ()
-
-/--
-Given constructors `a` and `b`, propagate equalities if they are the same,
-and close goal if they are different.
--/
-def propagateCtor (a b : Expr) : GoalM Unit := do
-  let aType ← whnfD (← inferType a)
-  let bType ← whnfD (← inferType b)
-  unless (← withDefault <| isDefEq aType bType) do
-    return ()
-  let ctor₁ := a.getAppFn
-  let ctor₂ := b.getAppFn
-  if ctor₁ == ctor₂ then
-    let .const ctorName _ := a.getAppFn | return ()
-    let injDeclName := Name.mkStr ctorName "inj"
-    unless (← getEnv).contains injDeclName do return ()
-    let info ← getConstInfo injDeclName
-    let n := info.type.getForallArity
-    let mask : Array (Option Expr) := mkArray n none
-    let mask := mask.set! (n-1) (some (← mkEqProof a b))
-    let injLemma ← mkAppOptM injDeclName mask
-    propagateInjEqs (← inferType injLemma) injLemma
-  else
-    let .const declName _ := aType.getAppFn | return ()
-    let noConfusionDeclName := Name.mkStr declName "noConfusion"
-    unless (← getEnv).contains noConfusionDeclName do return ()
-    closeGoal (← mkNoConfusion (← getFalseExpr) (← mkEqProof a b))
-
-end Lean.Meta.Grind

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

@@ -1,309 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Internalize
-
-namespace Lean.Meta.Grind
-/--
-Theorem instance found using E-matching.
-Recall that we only internalize new instances after we complete a full round of E-matching. -/
-structure EMatchTheoremInstance where
-  proof      : Expr
-  prop       : Expr
-  generation : Nat
-  deriving Inhabited
-
-namespace EMatch
-/-! This module implements a simple E-matching procedure as a backtracking search. -/
-
-/-- We represent an `E-matching` problem as a list of constraints. -/
-inductive Cnstr where
-  | /-- Matches pattern `pat` with term `e` -/
-    «match» (pat : Expr) (e : Expr)
-  | /-- This constraint is used to encode multi-patterns. -/
-    «continue» (pat : Expr)
-  deriving Inhabited
-
-/--
-Internal "marker" for representing unassigned elemens in the `assignment` field.
-This is a small hack to avoid one extra level of indirection by using `Option Expr` at `assignment`.
--/
-private def unassigned : Expr := mkConst (Name.mkSimple "[grind_unassigned]")
-
-private def assignmentToMessageData (assignment : Array Expr) : Array MessageData :=
-  assignment.reverse.map fun e =>
-    if isSameExpr e unassigned then m!"_" else m!"{e}"
-
-/--
-Choice point for the backtracking search.
-The state of the procedure contains a stack of choices.
--/
-structure Choice where
-  /-- Contraints to be processed. -/
-  cnstrs     : List Cnstr
-  /-- Maximum term generation found so far. -/
-  gen        : Nat
-  /-- Partial assignment so far. Recall that pattern variables are encoded as de-Bruijn variables. -/
-  assignment : Array Expr
-  deriving Inhabited
-
-/-- Context for the E-matching monad. -/
-structure Context where
-  /-- `useMT` is `true` if we are using the mod-time optimization. It is always set to false for new `EMatchTheorem`s. -/
-  useMT : Bool := true
-  /-- `EMatchTheorem` being processed. -/
-  thm   : EMatchTheorem := default
-  deriving Inhabited
-
-/-- State for the E-matching monad -/
-structure State where
-  /-- Choices that still have to be processed. -/
-  choiceStack  : List Choice := []
-  newInstances : Array EMatchTheoremInstance := #[]
-  deriving Inhabited
-
-abbrev M := ReaderT Context $ StateRefT State GoalM
-
-def M.run' (x : M α) : GoalM α :=
-  x {} |>.run' {}
-
-/--
-Assigns `bidx := e` in `c`. If `bidx` is already assigned in `c`, we check whether
-`e` and `c.assignment[bidx]` are in the same equivalence class.
-This function assumes `bidx < c.assignment.size`.
-Recall that we initialize the assignment array with the number of theorem parameters.
--/
-private def assign? (c : Choice) (bidx : Nat) (e : Expr) : OptionT GoalM Choice := do
-  if h : bidx < c.assignment.size then
-    let v := c.assignment[bidx]
-    if isSameExpr v unassigned then
-      return { c with assignment := c.assignment.set bidx e }
-    else
-      guard (← isEqv v e)
-      return c
-  else
-    -- `Choice` was not properly initialized
-    unreachable!
-
-/--
-Returns `true` if the function `pFn` of a pattern is equivalent to the function `eFn`.
-Recall that we ignore universe levels in patterns.
--/
-private def eqvFunctions (pFn eFn : Expr) : Bool :=
-  (pFn.isFVar && pFn == eFn)
-  || (pFn.isConst && eFn.isConstOf pFn.constName!)
-
-/--
-Matches arguments of pattern `p` with term `e`. Returns `some` if successful,
-and `none` otherwise. It may update `c`s assignment and list of contraints to be
-processed.
--/
-private partial def matchArgs? (c : Choice) (p : Expr) (e : Expr) : OptionT GoalM Choice := do
-  if !p.isApp then return c -- Done
-  let pArg := p.appArg!
-  let eArg := e.appArg!
-  let goFn c := matchArgs? c p.appFn! e.appFn!
-  if isPatternDontCare pArg then
-    goFn c
-  else if pArg.isBVar then
-    goFn (← assign? c pArg.bvarIdx! eArg)
-  else if let some pArg := groundPattern? pArg then
-    guard (← isEqv pArg eArg)
-    goFn c
-  else
-    goFn { c with cnstrs := .match pArg eArg :: c.cnstrs }
-
-/--
-Matches pattern `p` with term `e` with respect to choice `c`.
-We traverse the equivalence class of `e` looking for applications compatible with `p`.
-For each candidate application, we match the arguments and may update `c`s assignments and contraints.
-We add the updated choices to the choice stack.
--/
-private partial def processMatch (c : Choice) (p : Expr) (e : Expr) : M Unit := do
-  let maxGeneration ← getMaxGeneration
-  let pFn := p.getAppFn
-  let numArgs := p.getAppNumArgs
-  let mut curr := e
-  repeat
-    let n ← getENode curr
-    if n.generation <= maxGeneration
-       -- uses heterogeneous equality or is the root of its congruence class
-       && (n.heqProofs || isSameExpr curr n.cgRoot)
-       && eqvFunctions pFn curr.getAppFn
-       && curr.getAppNumArgs == numArgs then
-      if let some c ← matchArgs? c p curr |>.run then
-        let gen := n.generation
-        let c := { c with gen := Nat.max gen c.gen }
-        modify fun s => { s with choiceStack := c :: s.choiceStack }
-    curr ← getNext curr
-    if isSameExpr curr e then break
-
-/-- Processes `continue` contraint used to implement multi-patterns. -/
-private def processContinue (c : Choice) (p : Expr) : M Unit := do
-  let some apps := (← getThe Goal).appMap.find? p.toHeadIndex
-    | return ()
-  let maxGeneration ← getMaxGeneration
-  for app in apps do
-    let n ← getENode app
-    if n.generation <= maxGeneration
-       && (n.heqProofs || isSameExpr n.cgRoot app) then
-      if let some c ← matchArgs? c p app |>.run then
-        let gen := n.generation
-        let c := { c with gen := Nat.max gen c.gen }
-        modify fun s => { s with choiceStack := c :: s.choiceStack }
-
-/--
-Stores new theorem instance in the state.
-Recall that new instances are internalized later, after a full round of ematching.
--/
-private def addNewInstance (origin : Origin) (proof : Expr) (generation : Nat) : M Unit := do
-  let proof ← instantiateMVars proof
-  if grind.debug.proofs.get (← getOptions) then
-    check proof
-  let prop ← inferType proof
-  trace[grind.ematch.instance] "{← origin.pp}: {prop}"
-  modify fun s => { s with newInstances := s.newInstances.push { proof, prop, generation } }
-  modifyThe Goal fun s => { s with numInstances := s.numInstances + 1 }
-
-/--
-After processing a (multi-)pattern, use the choice assignment to instantiate the proof.
-Missing parameters are synthesized using type inference and type class synthesis."
--/
-private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do
-  let thm := (← read).thm
-  unless (← markTheorenInstance thm.proof c.assignment) do
-    return ()
-  trace[grind.ematch.instance.assignment] "{← thm.origin.pp}: {assignmentToMessageData c.assignment}"
-  let proof ← thm.getProofWithFreshMVarLevels
-  let numParams := thm.numParams
-  assert! c.assignment.size == numParams
-  let (mvars, bis, _) ← forallMetaBoundedTelescope (← inferType proof) numParams
-  if mvars.size != thm.numParams then
-    trace[grind.issues] "unexpected number of parameters at {← thm.origin.pp}"
-    return ()
-  -- Apply assignment
-  for h : i in [:mvars.size] do
-    let v := c.assignment[numParams - i - 1]!
-    unless isSameExpr v unassigned do
-      let mvarId := mvars[i].mvarId!
-      unless (← mvarId.checkedAssign v) do
-        trace[grind.issues] "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}"
-        return ()
-  -- Synthesize instances
-  for mvar in mvars, bi in bis do
-    if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
-      let type ← inferType mvar
-      unless (← synthesizeInstance mvar type) do
-        trace[grind.issues] "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
-        return ()
-  if (← mvars.allM (·.mvarId!.isAssigned)) then
-    addNewInstance thm.origin (mkAppN proof mvars) c.gen
-  else
-    -- instance has hypothesis
-    mkImp mvars 0 proof #[]
-where
-  synthesizeInstance (x type : Expr) : MetaM Bool := do
-    let .some val ← trySynthInstance type | return false
-    isDefEq x val
-
-  mkImp (mvars : Array Expr) (i : Nat) (proof : Expr) (xs : Array Expr) : M Unit := do
-    if h : i < mvars.size then
-      let mvar := mvars[i]
-      if (← mvar.mvarId!.isAssigned) then
-        mkImp mvars (i+1) (mkApp proof mvar) xs
-      else
-        let mvarType ← instantiateMVars (← inferType mvar)
-        if mvarType.hasMVar then
-          let thm := (← read).thm
-          trace[grind.issues] "failed to create hypothesis for instance of {← thm.origin.pp} hypothesis type has metavars{indentExpr mvarType}"
-          return ()
-        withLocalDeclD (← mkFreshUserName `h) mvarType fun x => do
-          mkImp mvars (i+1) (mkApp proof x) (xs.push x)
-    else
-      let proof ← instantiateMVars proof
-      let proof ← mkLambdaFVars xs proof
-      let thm := (← read).thm
-      addNewInstance thm.origin proof c.gen
-
-/-- Process choice stack until we don't have more choices to be processed. -/
-private partial def processChoices : M Unit := do
-  unless (← get).choiceStack.isEmpty do
-    checkSystem "ematch"
-    if (← checkMaxInstancesExceeded) then return ()
-    let c ← modifyGet fun s : State => (s.choiceStack.head!, { s with choiceStack := s.choiceStack.tail! })
-    match c.cnstrs with
-    | [] => instantiateTheorem c
-    | .match p e :: cnstrs => processMatch { c with cnstrs } p e
-    | .continue p :: cnstrs => processContinue { c with cnstrs } p
-    processChoices
-
-private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
-  let some apps := (← getThe Goal).appMap.find? p.toHeadIndex
-    | return ()
-  let numParams  := (← read).thm.numParams
-  let assignment := mkArray numParams unassigned
-  let useMT      := (← read).useMT
-  let gmt        := (← getThe Goal).gmt
-  for app in apps do
-    if (← checkMaxInstancesExceeded) then return ()
-    let n ← getENode app
-    if (n.heqProofs || isSameExpr n.cgRoot app) &&
-       (!useMT || n.mt == gmt) then
-      if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then
-        modify fun s => { s with choiceStack := [c] }
-        processChoices
-
-def ematchTheorem (thm : EMatchTheorem) : M Unit := do
-  if (← checkMaxInstancesExceeded) then return ()
-  withReader (fun ctx => { ctx with thm }) do
-    let ps := thm.patterns
-    match ps, (← read).useMT with
-    | [p],   _     => main p []
-    | p::ps, false => main p (ps.map (.continue ·))
-    | _::_,  true  => tryAll ps []
-    | _,     _     => unreachable!
-where
-  /--
-  When using the mod-time optimization with multi-patterns,
-  we must start ematching at each different pattern. That is,
-  if we have `[p₁, p₂, p₃]`, we must execute
-  - `main p₁ [.continue p₂, .continue p₃]`
-  - `main p₂ [.continue p₁, .continue p₃]`
-  - `main p₃ [.continue p₁, .continue p₂]`
-  -/
-  tryAll (ps : List Expr) (cs : List Cnstr) : M Unit := do
-    match ps with
-    | []    => return ()
-    | p::ps =>
-      main p (cs.reverse ++ (ps.map (.continue ·)))
-      tryAll ps (.continue p :: cs)
-
-def ematchTheorems (thms : PArray EMatchTheorem) : M Unit := do
-  thms.forM ematchTheorem
-
-end EMatch
-
-open EMatch
-
-/-- Performs one round of E-matching, and returns new instances. -/
-def ematch : GoalM (Array EMatchTheoremInstance) := do
-  let go (thms newThms : PArray EMatchTheorem) : EMatch.M (Array EMatchTheoremInstance) := do
-    withReader (fun ctx => { ctx with useMT := true }) <| ematchTheorems thms
-    withReader (fun ctx => { ctx with useMT := false }) <| ematchTheorems newThms
-    return (← get).newInstances
-  if (← checkMaxInstancesExceeded) then
-    return #[]
-  else
-    let insts ← go (← get).thms (← get).newThms |>.run'
-    modify fun s => { s with
-      thms         := s.thms ++ s.newThms
-      newThms      := {}
-      gmt          := s.gmt + 1
-    }
-    return insts
-
-end Lean.Meta.Grind

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

@@ -1,354 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.HeadIndex
-import Lean.PrettyPrinter
-import Lean.Util.FoldConsts
-import Lean.Util.CollectFVars
-import Lean.Meta.Basic
-import Lean.Meta.InferType
-
-namespace Lean.Meta.Grind
-
-inductive Origin where
-  /-- A global declaration in the environment. -/
-  | decl (declName : Name)
-  /-- A local hypothesis. -/
-  | fvar (fvarId : FVarId)
-  /--
-  A proof term provided directly to a call to `grind` where `ref`
-  is the provided grind argument. The `id` is a unique identifier for the call.
-  -/
-  | stx (id : Name) (ref : Syntax)
-  | other
-  deriving Inhabited, Repr
-
-/-- A unique identifier corresponding to the origin. -/
-def Origin.key : Origin → Name
-  | .decl declName => declName
-  | .fvar fvarId   => fvarId.name
-  | .stx id _      => id
-  | .other         => `other
-
-def Origin.pp [Monad m] [MonadEnv m] [MonadError m] (o : Origin) : m MessageData := do
-  match o with
-  | .decl declName => return MessageData.ofConst (← mkConstWithLevelParams declName)
-  | .fvar fvarId   => return mkFVar fvarId
-  | .stx _ ref     => return ref
-  | .other         => return "[unknown]"
-
-/-- A theorem for heuristic instantiation based on E-matching. -/
-structure EMatchTheorem where
-  /--
-  It stores universe parameter names for universe polymorphic proofs.
-  Recall that it is non-empty only when we elaborate an expression provided by the user.
-  When `proof` is just a constant, we can use the universe parameter names stored in the declaration.
-  -/
-  levelParams : Array Name
-  proof       : Expr
-  numParams   : Nat
-  patterns    : List Expr
-  /-- Contains all symbols used in `pattterns`. -/
-  symbols     : List HeadIndex
-  origin      : Origin
-  deriving Inhabited
-
-/-- The key is a symbol from `EMatchTheorem.symbols`. -/
-abbrev EMatchTheorems := PHashMap Name (List EMatchTheorem)
-
-def EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchTheorems := Id.run do
-  let .const declName :: syms := thm.symbols
-    | unreachable!
-  let thm := { thm with symbols := syms }
-  if let some thms := s.find? declName then
-    return PersistentHashMap.insert s declName (thm::thms)
-  else
-    return PersistentHashMap.insert s declName [thm]
-
-def EMatchTheorem.getProofWithFreshMVarLevels (thm : EMatchTheorem) : MetaM Expr := do
-  if thm.proof.isConst && thm.levelParams.isEmpty then
-    let declName := thm.proof.constName!
-    let info ← getConstInfo declName
-    if info.levelParams.isEmpty then
-      return thm.proof
-    else
-      mkConstWithFreshMVarLevels declName
-  else if thm.levelParams.isEmpty then
-    return thm.proof
-  else
-    let us ← thm.levelParams.mapM fun _ => mkFreshLevelMVar
-    return thm.proof.instantiateLevelParamsArray thm.levelParams us
-
-private builtin_initialize ematchTheoremsExt : SimpleScopedEnvExtension EMatchTheorem EMatchTheorems ←
-  registerSimpleScopedEnvExtension {
-    addEntry := EMatchTheorems.insert
-    initial  := .empty
-  }
-
--- TODO: create attribute?
-private def forbiddenDeclNames := #[``Eq, ``HEq, ``Iff, ``And, ``Or, ``Not]
-
-private def isForbidden (declName : Name) := forbiddenDeclNames.contains declName
-
-private def dontCare := mkConst (Name.mkSimple "[grind_dontcare]")
-
-def mkGroundPattern (e : Expr) : Expr :=
-  mkAnnotation `grind.ground_pat e
-
-def groundPattern? (e : Expr) : Option Expr :=
-  annotation? `grind.ground_pat e
-
-private def isGroundPattern (e : Expr) : Bool :=
-  groundPattern? e |>.isSome
-
-def isPatternDontCare (e : Expr) : Bool :=
-  e == dontCare
-
-private def isAtomicPattern (e : Expr) : Bool :=
-  e.isBVar || isPatternDontCare e || isGroundPattern e
-
-partial def ppPattern (pattern : Expr) : MessageData := Id.run do
-  if let some e := groundPattern? pattern then
-    return m!"`[{e}]"
-  else if isPatternDontCare pattern then
-    return m!"?"
-  else match pattern with
-    | .bvar idx => return m!"#{idx}"
-    | _ =>
-      let mut r := m!"{pattern.getAppFn}"
-      for arg in pattern.getAppArgs do
-        let mut argFmt ← ppPattern arg
-        if !isAtomicPattern arg then
-          argFmt := MessageData.paren argFmt
-        r := r ++ " " ++ argFmt
-      return r
-
-namespace NormalizePattern
-
-structure State where
-  symbols    : Array HeadIndex := #[]
-  symbolSet  : Std.HashSet HeadIndex := {}
-  bvarsFound : Std.HashSet Nat := {}
-
-abbrev M := StateRefT State MetaM
-
-private def saveSymbol (h : HeadIndex) : M Unit := do
-  unless (← get).symbolSet.contains h do
-    modify fun s => { s with symbols := s.symbols.push h, symbolSet := s.symbolSet.insert h }
-
-private def foundBVar (idx : Nat) : M Bool :=
-  return (← get).bvarsFound.contains idx
-
-private def saveBVar (idx : Nat) : M Unit := do
-  modify fun s => { s with bvarsFound := s.bvarsFound.insert idx }
-
-private def getPatternFn? (pattern : Expr) : Option Expr :=
-  if !pattern.isApp then
-    none
-  else match pattern.getAppFn with
-    | f@(.const declName _) => if isForbidden declName then none else some f
-    | f@(.fvar _) => some f
-    | _ => none
-
-/--
-Returns a bit-mask `mask` s.t. `mask[i]` is true if the the corresponding argument is
-- a type or type former, or
-- a proof, or
-- an instance implicit argument
-
-When `mask[i]`, we say the corresponding argument is a "support" argument.
--/
-private def getPatternFunMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do
-  forallBoundedTelescope (← inferType f) numArgs fun xs _ => do
-    xs.mapM fun x => do
-      if (← isTypeFormer x <||> isProof x) then
-        return true
-      else
-        return (← x.fvarId!.getDecl).binderInfo matches .instImplicit
-
-private partial def go (pattern : Expr) (root := false) : M Expr := do
-  if root && !pattern.hasLooseBVars then
-    throwError "invalid pattern, it does not have pattern variables"
-  let some f := getPatternFn? pattern
-    | throwError "invalid pattern, (non-forbidden) application expected"
-  assert! f.isConst || f.isFVar
-  saveSymbol f.toHeadIndex
-  let mut args := pattern.getAppArgs
-  let supportMask ← getPatternFunMask f args.size
-  for i in [:args.size] do
-    let arg := args[i]!
-    let isSupport := supportMask[i]?.getD false
-    let arg ← if !arg.hasLooseBVars then
-      if arg.hasMVar then
-        pure dontCare
-      else
-        pure <| mkGroundPattern arg
-    else match arg with
-      | .bvar idx =>
-        if isSupport && (← foundBVar idx) then
-          pure dontCare
-        else
-          saveBVar idx
-          pure arg
-      | _ =>
-        if isSupport then
-          pure dontCare
-        else if let some _ := getPatternFn? arg then
-          go arg
-        else
-          pure dontCare
-    args := args.set! i arg
-  return mkAppN f args
-
-def main (patterns : List Expr) : MetaM (List Expr × List HeadIndex × Std.HashSet Nat) := do
-  let (patterns, s) ← patterns.mapM go |>.run {}
-  return (patterns, s.symbols.toList, s.bvarsFound)
-
-end NormalizePattern
-
-/--
-Returns `true` if free variables in `type` are not in `thmVars` or are in `fvarsFound`.
-We use this function to check whether `type` is fully instantiated.
--/
-private def checkTypeFVars (thmVars : FVarIdSet) (fvarsFound : FVarIdSet) (type : Expr) : Bool :=
-  let typeFVars := (collectFVars {} type).fvarIds
-  typeFVars.all fun fvarId => !thmVars.contains fvarId || fvarsFound.contains fvarId
-
-/--
-Given an type class instance type `instType`, returns true if free variables in input parameters
-1- are not in `thmVars`, or
-2- are in `fvarsFound`.
-Remark: `fvarsFound` is a subset of `thmVars`
--/
-private def canBeSynthesized (thmVars : FVarIdSet) (fvarsFound : FVarIdSet) (instType : Expr) : MetaM Bool := do
-  forallTelescopeReducing instType fun xs type => type.withApp fun classFn classArgs => do
-    for x in xs do
-      unless checkTypeFVars thmVars fvarsFound (← inferType x) do return false
-    forallBoundedTelescope (← inferType classFn) type.getAppNumArgs fun params _ => do
-      for param in params, classArg in classArgs do
-        let paramType ← inferType param
-        if !paramType.isAppOf ``semiOutParam && !paramType.isAppOf ``outParam then
-          unless checkTypeFVars thmVars fvarsFound classArg do
-            return false
-      return true
-
-/--
-Auxiliary type for the `checkCoverage` function.
--/
-inductive CheckCoverageResult where
-  | /-- `checkCoverage` succeeded -/
-    ok
-  | /--
-    `checkCoverage` failed because some of the theorem parameters are missing,
-    `pos` contains their positions
-    -/
-    missing (pos : List Nat)
-
-/--
-After we process a set of patterns, we obtain the set of de Bruijn indices in these patterns.
-We say they are pattern variables. This function checks whether the set of pattern variables is sufficient for
-instantiating the theorem with proof `thmProof`. The theorem has `numParams` parameters.
-The missing parameters:
-1- we may be able to infer them using type inference or type class synthesis, or
-2- they are propositions, and may become hypotheses of the instantiated theorem.
-
-For type class instance parameters, we must check whether the free variables in class input parameters are available.
--/
-private def checkCoverage (thmProof : Expr) (numParams : Nat) (bvarsFound : Std.HashSet Nat) : MetaM CheckCoverageResult := do
-  if bvarsFound.size == numParams then return .ok
-  forallBoundedTelescope (← inferType thmProof) numParams fun xs _ => do
-    assert! numParams == xs.size
-    let patternVars := bvarsFound.toList.map fun bidx => xs[numParams - bidx - 1]!.fvarId!
-    -- `xs` as a `FVarIdSet`.
-    let thmVars : FVarIdSet := RBTree.ofList <| xs.toList.map (·.fvarId!)
-    -- Collect free variables occurring in `e`, and insert the ones that are in `thmVars` into `fvarsFound`
-    let update (fvarsFound : FVarIdSet) (e : Expr) : FVarIdSet :=
-      (collectFVars {} e).fvarIds.foldl (init := fvarsFound) fun s fvarId =>
-        if thmVars.contains fvarId then s.insert fvarId else s
-    -- Theorem variables found so far. We initialize with the variables occurring in patterns
-    -- Remark: fvarsFound is a subset of thmVars
-    let mut fvarsFound : FVarIdSet := RBTree.ofList patternVars
-    for patternVar in patternVars do
-      let type ← patternVar.getType
-      fvarsFound := update fvarsFound type
-    if fvarsFound.size == numParams then return .ok
-    -- Now, we keep traversing remaining variables and collecting
-    -- `processed` contains the variables we have already processed.
-    let mut processed : FVarIdSet := RBTree.ofList patternVars
-    let mut modified := false
-    repeat
-      modified := false
-      for x in xs do
-        let fvarId := x.fvarId!
-        unless processed.contains fvarId do
-          let xType ← inferType x
-          if fvarsFound.contains fvarId then
-            -- Collect free vars in `x`s type and mark as processed
-            fvarsFound := update fvarsFound xType
-            processed := processed.insert fvarId
-            modified := true
-          else if (← isProp xType) then
-            -- If `x` is a proposition, and all theorem variables in `x`s type have already been found
-            -- add it to `fvarsFound` and mark it as processed.
-            if checkTypeFVars thmVars fvarsFound xType then
-              fvarsFound := fvarsFound.insert fvarId
-              processed := processed.insert fvarId
-              modified := true
-          else if (← fvarId.getDecl).binderInfo matches .instImplicit then
-            -- If `x` is instance implicit, check whether
-            -- we have found all free variables needed to synthesize instance
-            if (← canBeSynthesized thmVars fvarsFound xType) then
-              fvarsFound := fvarsFound.insert fvarId
-              fvarsFound := update fvarsFound xType
-              processed := processed.insert fvarId
-              modified := true
-      if fvarsFound.size == numParams then
-        return .ok
-      if !modified then
-        break
-    let mut pos := #[]
-    for h : i in [:xs.size] do
-      let fvarId := xs[i].fvarId!
-      unless fvarsFound.contains fvarId do
-        pos := pos.push i
-    return .missing pos.toList
-
-/--
-Given a theorem with proof `proof` and `numParams` parameters, returns a message
-containing the parameters at positions `paramPos`.
--/
-private def ppParamsAt (proof : Expr) (numParms : Nat) (paramPos : List Nat) : MetaM MessageData := do
-  forallBoundedTelescope (← inferType proof) numParms fun xs _ => do
-    let mut msg := m!""
-    let mut first := true
-    for h : i in [:xs.size] do
-      if paramPos.contains i then
-        let x := xs[i]
-        if first then first := false else msg := msg ++ "\n"
-        msg := msg ++ m!"{x} : {← inferType x}"
-    addMessageContextFull msg
-
-def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM Unit := do
-  let .thmInfo info ← getConstInfo declName
-    | throwError "`{declName}` is not a theorem, you cannot assign patterns to non-theorems for the `grind` tactic"
-  let us := info.levelParams.map mkLevelParam
-  let proof := mkConst declName us
-  let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
-  assert! symbols.all fun s => s matches .const _
-  trace[grind.ematch.pattern] "{declName}: {patterns.map ppPattern}"
-  if let .missing pos ← checkCoverage proof numParams bvarFound then
-     let pats : MessageData := m!"{patterns.map ppPattern}"
-     throwError "invalid pattern(s) for `{declName}`{indentD pats}\nthe following theorem parameters cannot be instantiated:{indentD (← ppParamsAt proof numParams pos)}"
-  ematchTheoremsExt.add {
-     proof, patterns, numParams, symbols
-     levelParams := #[]
-     origin      := .decl declName
-  }
-
-def getEMatchTheorems : CoreM EMatchTheorems :=
-  return ematchTheoremsExt.getState (← getEnv)
-
-end Lean.Meta.Grind

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

@@ -1,114 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Grind.Util
-import Lean.Meta.LitValues
-import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Util
-
-namespace Lean.Meta.Grind
-
-/-- Adds `e` to congruence table. -/
-def addCongrTable (e : Expr) : GoalM Unit := do
-  if let some { e := e' } := (← get).congrTable.find? { e } then
-    -- `f` and `g` must have the same type.
-    -- See paper: Congruence Closure in Intensional Type Theory
-    let f := e.getAppFn
-    let g := e'.getAppFn
-    unless isSameExpr f g do
-      unless (← hasSameType f g) do
-        trace[grind.issues] "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
-        return ()
-    trace[grind.debug.congr] "{e} = {e'}"
-    pushEqHEq e e' congrPlaceholderProof
-    let node ← getENode e
-    setENode e { node with cgRoot := e' }
-  else
-    modify fun s => { s with congrTable := s.congrTable.insert { e } }
-
-private def updateAppMap (e : Expr) : GoalM Unit := do
-  let key := e.toHeadIndex
-  modify fun s => { s with
-    appMap := if let some es := s.appMap.find? key then
-      s.appMap.insert key (e :: es)
-    else
-      s.appMap.insert key [e]
-  }
-
-mutual
-/-- Internalizes the nested ground terms in the given pattern. -/
-private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do
-  if pattern.isBVar || isPatternDontCare pattern then
-    return pattern
-  else if let some e := groundPattern? pattern then
-    let e ← shareCommon (← canon (← normalizeLevels (← unfoldReducible e)))
-    internalize e generation
-    return mkGroundPattern e
-  else pattern.withApp fun f args => do
-    return mkAppN f (← args.mapM (internalizePattern · generation))
-
-private partial def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
-  if let some thms := (← get).thmMap.find? fName then
-    modify fun s => { s with thmMap := s.thmMap.erase fName }
-    let appMap := (← get).appMap
-    for thm in thms do
-      let symbols := thm.symbols.filter fun sym => !appMap.contains sym
-      let thm := { thm with symbols }
-      match symbols with
-      | [] =>
-        -- Recall that we use the proof as part of the key for a set of instances found so far.
-        -- We don't want to use structural equality when comparing keys.
-        let proof ← shareCommon thm.proof
-        let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation)) }
-        trace[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}"
-        modify fun s => { s with newThms := s.newThms.push thm }
-      | _ =>
-        trace[grind.ematch] "reinsert `{thm.origin.key}`"
-        modify fun s => { s with thmMap := s.thmMap.insert thm }
-
-partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
-  if (← alreadyInternalized e) then return ()
-  trace[grind.internalize] "{e}"
-  match e with
-  | .bvar .. => unreachable!
-  | .sort .. => return ()
-  | .fvar .. | .letE .. | .lam .. | .forallE .. =>
-    mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
-  | .lit .. | .const .. =>
-    mkENode e generation
-  | .mvar ..
-  | .mdata ..
-  | .proj .. =>
-    trace[grind.issues] "unexpected term during internalization{indentExpr e}"
-    mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
-  | .app .. =>
-    if (← isLitValue e) then
-      -- We do not want to internalize the components of a literal value.
-      mkENode e generation
-    else e.withApp fun f args => do
-      if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
-        -- We only internalize the proposition. We can skip the proof because of
-        -- proof irrelevance
-        let c := args[0]!
-        internalize c generation
-        registerParent e c
-      else
-        if let .const fName _ := f then
-          activateTheoremPatterns fName generation
-        else
-          internalize f generation
-          registerParent e f
-        for h : i in [: args.size] do
-          let arg := args[i]
-          internalize arg generation
-          registerParent e arg
-      mkENode e generation
-      addCongrTable e
-      updateAppMap e
-      propagateUp e
-end
-
-end Lean.Meta.Grind

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

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Proof
 
 namespace Lean.Meta.Grind
 
@@ -20,16 +19,6 @@ private def checkEqc (root : ENode) : GoalM Unit := do
     size := size + 1
     -- The root of `curr` must be `root`
     assert! isSameExpr (← getRoot curr) root.self
-    -- Check congruence root
-    if curr.isApp then
-      if let some { e } := (← get).congrTable.find? { e := curr } then
-        if (← hasSameType e.getAppFn curr.getAppFn) then
-          assert! isSameExpr e (← getENode curr).cgRoot
-      else
-        assert! isSameExpr curr (← getENode curr).cgRoot
-    -- If the equivalence class does not have HEq proofs, then the types must be definitionally equal.
-    unless root.heqProofs do
-      assert! (← hasSameType curr root.self)
     -- Starting at `curr`, following the `target?` field leads to `root`.
     let mut n := curr
     repeat
@@ -49,16 +38,13 @@ private def checkParents (e : Expr) : GoalM Unit := do
   if (← isRoot e) then
     for parent in (← getParents e) do
       let mut found := false
-      let checkChild (child : Expr) : GoalM Bool := do
-        let some childRoot ← getRoot? child | return false
-        return isSameExpr childRoot e
       -- There is an argument `arg` s.t. root of `arg` is `e`.
       for arg in parent.getAppArgs do
-        if (← checkChild arg) then
-          found := true
-          break
-      unless found do
-        assert! (← checkChild parent.getAppFn)
+        if let some argRoot ← getRoot? arg then
+          if isSameExpr argRoot e then
+            found := true
+            break
+      assert! found
   else
     -- All the parents are stored in the root of the equivalence class.
     assert! (← getParents e).isEmpty
@@ -68,23 +54,12 @@ private def checkPtrEqImpliesStructEq : GoalM Unit := do
   for h₁ : i in [: nodes.size] do
     let n₁ := nodes[i]
     for h₂ : j in [i+1 : nodes.size] do
-      let n₂ := nodes[j]
+      let n₂ := nodes[i]
       -- We don't have multiple nodes for the same expression
       assert! !isSameExpr n₁.self n₂.self
       -- and the two expressions must not be structurally equal
       assert! !Expr.equal n₁.self n₂.self
 
-private def checkProofs : GoalM Unit := do
-  let eqcs ← getEqcs
-  for eqc in eqcs do
-    for a in eqc do
-      for b in eqc do
-        unless isSameExpr a b do
-          let p ← mkEqProof a b
-          trace[grind.debug.proofs] "{a} = {b}"
-          check p
-          trace[grind.debug.proofs] "checked: {← inferType p}"
-
 /--
 Checks basic invariants if `grind.debug` is enabled.
 -/
@@ -96,7 +71,5 @@ def checkInvariants (expensive := false) : GoalM Unit := do
         checkEqc node
     if expensive then
       checkPtrEqImpliesStructEq
-  if expensive && grind.debug.proofs.get (← getOptions) then
-    checkProofs
 
 end Lean.Meta.Grind

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

@@ -14,6 +14,27 @@ def ppENodeRef (e : Expr) : GoalM Format := do
   let some n ← getENode? e | return "_"
   return f!"#{n.idx}"
 
+/-- Returns expressions in the given expression equivalence class. -/
+partial def getEqc (e : Expr) : GoalM (List Expr) :=
+  go e e []
+where
+  go (first : Expr) (e : Expr) (acc : List Expr) : GoalM (List Expr) := do
+    let next ← getNext e
+    let acc := e :: acc
+    if isSameExpr first next then
+      return acc
+    else
+      go first next acc
+
+/-- Returns all equivalence classes in the current goal. -/
+partial def getEqcs : GoalM (List (List Expr)) := do
+  let mut r := []
+  let nodes ← getENodes
+  for node in nodes do
+    if isSameExpr node.root node.self then
+      r := (← getEqc node.self) :: r
+  return r
+
 /-- Helper function for pretty printing the state for debugging purposes. -/
 def ppENodeDeclValue (e : Expr) : GoalM Format := do
   if e.isApp && !(← isLitValue e) then

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

@@ -1,15 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Parser.Command
-
-namespace Lean.Parser.Command
-/-!
-Builtin parsers for `grind` related commands
--/
-@[builtin_command_parser] def grindPattern := leading_parser
-  "grind_pattern " >>  ident >> darrow >> sepBy1 termParser ","
-end Lean.Parser.Command

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

@@ -17,8 +17,6 @@ import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
 import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.Run
-import Lean.Meta.Tactic.Grind.EMatch
 
 namespace Lean.Meta.Grind
 namespace Preprocessor
@@ -100,8 +98,6 @@ def applyInjection? (goal : Goal) (fvarId : FVarId) : MetaM (Option Goal) := do
     return none
 
 partial def loop (goal : Goal) : PreM Unit := do
-  if goal.inconsistent then
-    return ()
   match (← introNext goal) with
   | .done =>
     if let some mvarId ← goal.mvarId.byContra? then
@@ -123,14 +119,13 @@ partial def loop (goal : Goal) : PreM Unit := do
     else
       loop goal
 
-def ppGoals (goals : PArray Goal) : PreM Format := do
+def ppGoals : PreM Format := do
   let mut r := f!""
-  for goal in goals do
+  for goal in (← get).goals do
     let (f, _) ← GoalM.run goal ppState
     r := r ++ Format.line ++ f
   return r
 
--- TODO: refactor this code
 def preprocess (mvarId : MVarId) : PreM State := do
   mvarId.ensureProp
   -- TODO: abstract metavars
@@ -142,12 +137,9 @@ def preprocess (mvarId : MVarId) : PreM State := do
   let mvarId ← mvarId.unfoldReducible
   let mvarId ← mvarId.betaReduce
   loop (← mkGoal mvarId)
-  let goals := (← get).goals
-  -- Testing `ematch` module here. We will rewrite this part later.
-  let goals ← goals.mapM fun goal => GoalM.run' goal (discard <| ematch)
   if (← isTracingEnabledFor `grind.pre) then
-    trace[grind.debug.pre] (← ppGoals goals)
-  for goal in goals do
+    trace[grind.pre] (← ppGoals)
+  for goal in (← get).goals do
     discard <| GoalM.run' goal <| checkInvariants (expensive := true)
   get
 
@@ -162,16 +154,13 @@ open Preprocessor
 
 def preprocessAndProbe (mvarId : MVarId) (mainDeclName : Name) (p : GoalM Unit) : MetaM Unit :=
   withoutModifyingMCtx do
-    Preprocessor.preprocessAndProbe mvarId p |>.run |>.run mainDeclName {}
+    Preprocessor.preprocessAndProbe mvarId p |>.run |>.run mainDeclName
 
-def preprocess (mvarId : MVarId) (mainDeclName : Name) (config : Grind.Config) : MetaM Preprocessor.State :=
-  Preprocessor.preprocess mvarId |>.run |>.run mainDeclName config
+def preprocess (mvarId : MVarId) (mainDeclName : Name) : MetaM Preprocessor.State :=
+  Preprocessor.preprocess mvarId |>.run |>.run mainDeclName
 
-def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) : MetaM (List MVarId) := do
-  let go : GrindM (List MVarId) := do
-    let s ← Preprocessor.preprocess mvarId |>.run
-    let goals := s.goals.toList.filter fun goal => !goal.inconsistent
-    return goals.map (·.mvarId)
-  go.run mainDeclName config
+def main (mvarId : MVarId) (mainDeclName : Name) : MetaM (List MVarId) := do
+  let s ← preprocess mvarId mainDeclName
+  return s.goals.toList.map (·.mvarId)
 
 end Lean.Meta.Grind

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

@@ -1,39 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.ProjFns
-import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Internalize
-
-namespace Lean.Meta.Grind
-
-/--
-If `parent` is a projection-application `proj_i c`,
-check whether the root of the equivalence class containing `c` is a constructor-application `ctor ... a_i ...`.
-If so, internalize the term `proj_i (ctor ... a_i ...)` and add the equality `proj_i (ctor ... a_i ...) = a_i`.
--/
-def propagateProjEq (parent : Expr) : GoalM Unit := do
-  let .const declName _ := parent.getAppFn | return ()
-  let some info ← getProjectionFnInfo? declName | return ()
-  unless info.numParams + 1 == parent.getAppNumArgs do return ()
-  -- It is wasteful to add equation if `parent` is not the root of its congruence class
-  unless (← isCongrRoot parent) do return ()
-  let arg := parent.appArg!
-  let ctor ← getRoot arg
-  unless ctor.isAppOf info.ctorName do return ()
-  let parentNew ← if isSameExpr arg ctor then
-    pure parent
-  else
-    let parentNew ← shareCommon (mkApp parent.appFn! ctor)
-    internalize parentNew (← getGeneration parent)
-    pure parentNew
-  trace[grind.debug.proj] "{parentNew}"
-  let idx := info.numParams + info.i
-  unless idx < ctor.getAppNumArgs do return ()
-  let v := ctor.getArg! idx
-  pushEq parentNew v (← mkEqRefl v)
-
-end Lean.Meta.Grind

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

@@ -9,231 +9,29 @@ import Lean.Meta.Tactic.Grind.Types
 
 namespace Lean.Meta.Grind
 
-private def isEqProof (h : Expr) : MetaM Bool := do
-  return (← whnfD (← inferType h)).isAppOf ``Eq
-
-private def flipProof (h : Expr) (flipped : Bool) (heq : Bool) : MetaM Expr := do
-  let mut h' := h
-  if (← pure heq <&&> isEqProof h') then
-    h' ← mkHEqOfEq h'
-  if flipped then
-    if heq then mkHEqSymm h' else mkEqSymm h'
-  else
-    return h'
-
-private def mkRefl (a : Expr) (heq : Bool) : MetaM Expr :=
-  if heq then mkHEqRefl a else mkEqRefl a
-
-private def mkTrans (h₁ h₂ : Expr) (heq : Bool) : MetaM Expr :=
-  if heq then
-    mkHEqTrans h₁ h₂
-  else
-    mkEqTrans h₁ h₂
-
-private def mkTrans' (h₁ : Option Expr) (h₂ : Expr) (heq : Bool) : MetaM Expr := do
-  let some h₁ := h₁ | return h₂
-  mkTrans h₁ h₂ heq
-
-/--
-Given `h : HEq a b`, returns a proof `a = b` if `heq == false`.
-Otherwise, it returns `h`.
--/
-private def mkEqOfHEqIfNeeded (h : Expr) (heq : Bool) : MetaM Expr := do
-  if heq then return h else mkEqOfHEq h
-
-/--
-Given `lhs` and `rhs` that are in the same equivalence class,
-find the common expression that are in the paths from `lhs` and `rhs` to
-the root of their equivalence class.
-Recall that this expression must exist since it is the root itself in the
-worst case.
--/
-private def findCommon (lhs rhs : Expr) : GoalM Expr := do
-  let mut visited : RBMap Nat Expr compare := {}
-  let mut it := lhs
-  -- Mark elements found following the path from `lhs` to the root.
-  repeat
-    let n ← getENode it
-    visited := visited.insert n.idx n.self
-    let some target := n.target? | break
-    it := target
-  -- Find the marked element from the path from `rhs` to the root.
-  it := rhs
-  repeat
-    let n ← getENode it
-    if let some common := visited.find? n.idx then
-      return common
-    let some target := n.target? | unreachable! --
-    it := target
-  unreachable!
-
-/--
-Returns `true` if we can construct a congruence proof for `lhs = rhs` using `congrArg`, `congrFun`, and `congr`.
-`f` (`g`) is the function of the `lhs` (`rhs`) application. `numArgs` is the number of arguments.
--/
-private partial def isCongrDefaultProofTarget (lhs rhs : Expr) (f g : Expr) (numArgs : Nat) : GoalM Bool := do
-  unless isSameExpr f g do return false
-  let info := (← getFunInfo f).paramInfo
-  let rec loop (lhs rhs : Expr) (i : Nat) : GoalM Bool := do
-    if lhs.isApp then
-      let a₁ := lhs.appArg!
-      let a₂ := rhs.appArg!
-      let i  := i - 1
-      unless isSameExpr a₁ a₂ do
-        if h : i < info.size then
-          if info[i].hasFwdDeps then
-            -- Cannot use `congrArg` because there are forward dependencies
-            return false
-        else
-          return false -- Don't have information about argument
-      loop lhs.appFn! rhs.appFn! i
-    else
-      return true
-  loop lhs rhs numArgs
-
-mutual
-  /--
-  Given `lhs` and `rhs` proof terms of the form `nestedProof p hp` and `nestedProof q hq`,
-  constructs a congruence proof for `HEq (nestedProof p hp) (nestedProof q hq)`.
-  `p` and `q` are in the same equivalence class.
-  -/
-  private partial def mkNestedProofCongr (lhs rhs : Expr) (heq : Bool) : GoalM Expr := do
-    let p  := lhs.appFn!.appArg!
-    let hp := lhs.appArg!
-    let q  := rhs.appFn!.appArg!
-    let hq := rhs.appArg!
-    let h  := mkApp5 (mkConst ``Lean.Grind.nestedProof_congr) p q (← mkEqProofCore p q false) hp hq
-    mkEqOfHEqIfNeeded h heq
-
-  /--
-  Constructs a congruence proof for `lhs` and `rhs` using `congr`, `congrFun`, and `congrArg`.
-  This function assumes `isCongrDefaultProofTarget` returned `true`.
-  -/
-  private partial def mkCongrDefaultProof (lhs rhs : Expr) (heq : Bool) : GoalM Expr := do
-    let rec loop (lhs rhs : Expr) : GoalM (Option Expr) := do
-      if lhs.isApp then
-        let a₁ := lhs.appArg!
-        let a₂ := rhs.appArg!
-        if let some proof ← loop lhs.appFn! rhs.appFn! then
-          if isSameExpr a₁ a₂ then
-            mkCongrFun proof a₁
-          else
-            mkCongr proof (← mkEqProofCore a₁ a₂ false)
-        else if isSameExpr a₁ a₂ then
-          return none -- refl case
-        else
-          mkCongrArg lhs.appFn! (← mkEqProofCore a₁ a₂ false)
-      else
-        return none
-    let r := (← loop lhs rhs).get!
-    if heq then mkHEqOfEq r else return r
-
-  /-- Constructs a congruence proof for `lhs` and `rhs`. -/
-  private partial def mkCongrProof (lhs rhs : Expr) (heq : Bool) : GoalM Expr := do
-    let f := lhs.getAppFn
-    let g := rhs.getAppFn
-    let numArgs := lhs.getAppNumArgs
-    assert! rhs.getAppNumArgs == numArgs
-    if f.isConstOf ``Lean.Grind.nestedProof && g.isConstOf ``Lean.Grind.nestedProof && numArgs == 2 then
-      mkNestedProofCongr lhs rhs heq
-    else if (← isCongrDefaultProofTarget lhs rhs f g numArgs) then
-      mkCongrDefaultProof lhs rhs heq
-    else
-      let thm ← mkHCongrWithArity f numArgs
-      assert! thm.argKinds.size == numArgs
-      let rec loop (lhs rhs : Expr) (i : Nat) : GoalM Expr := do
-        let i := i - 1
-        if lhs.isApp then
-          let proof ← loop lhs.appFn! rhs.appFn! i
-          let a₁  := lhs.appArg!
-          let a₂  := rhs.appArg!
-          let k   := thm.argKinds[i]!
-          return mkApp3 proof a₁ a₂ (← mkEqProofCore a₁ a₂ (k matches .heq))
-        else
-          return thm.proof
-      let proof ← loop lhs rhs numArgs
-      if isSameExpr f g then
-        mkEqOfHEqIfNeeded proof heq
-      else
-        /-
-        `lhs` is of the form `f a_1 ... a_n`
-        `rhs` is of the form `g b_1 ... b_n`
-        `proof : HEq (f a_1 ... a_n) (f b_1 ... b_n)`
-        We construct a proof for `HEq (f a_1 ... a_n) (g b_1 ... b_n)` using `Eq.ndrec`
-        -/
-        let motive ← withLocalDeclD (← mkFreshUserName `x) (← inferType f) fun x => do
-          mkLambdaFVars #[x] (← mkHEq lhs (mkAppN x rhs.getAppArgs))
-        let fEq ← mkEqProofCore f g false
-        let proof ← mkEqNDRec motive proof fEq
-        mkEqOfHEqIfNeeded proof heq
-
-  private partial def realizeEqProof (lhs rhs : Expr) (h : Expr) (flipped : Bool) (heq : Bool) : GoalM Expr := do
-    let h ← if h == congrPlaceholderProof then
-      mkCongrProof lhs rhs heq
-    else
-      flipProof h flipped heq
-
-  /-- Given `acc : lhs₀ = lhs`, returns a proof of `lhs₀ = common`. -/
-  private partial def mkProofTo (lhs : Expr) (common : Expr) (acc : Option Expr) (heq : Bool) : GoalM (Option Expr) := do
-    if isSameExpr lhs common then
-      return acc
-    let n ← getENode lhs
-    let some target := n.target? | unreachable!
-    let some h := n.proof? | unreachable!
-    let h ← realizeEqProof lhs target h n.flipped heq
-    -- h : lhs = target
-    let acc ← mkTrans' acc h heq
-    mkProofTo target common (some acc) heq
-
-  /-- Given `lhsEqCommon : lhs = common`, returns a proof for `lhs = rhs`. -/
-  private partial def mkProofFrom (rhs : Expr) (common : Expr) (lhsEqCommon? : Option Expr) (heq : Bool) : GoalM (Option Expr) := do
-    if isSameExpr rhs common then
-      return lhsEqCommon?
-    let n ← getENode rhs
-    let some target := n.target? | unreachable!
-    let some h := n.proof? | unreachable!
-    let h ← realizeEqProof target rhs h (!n.flipped) heq
-    -- `h : target = rhs`
-    let h' ← mkProofFrom target common lhsEqCommon? heq
-    -- `h' : lhs = target`
-    mkTrans' h' h heq
-
-  private partial def mkEqProofCore (lhs rhs : Expr) (heq : Bool) : GoalM Expr := do
-    if isSameExpr lhs rhs then
-      return (← mkRefl lhs heq)
-    let n₁ ← getENode lhs
-    let n₂ ← getENode rhs
-    assert! isSameExpr n₁.root n₂.root
-    let common ← findCommon lhs rhs
-    let lhsEqCommon? ← mkProofTo lhs common none heq
-    let some lhsEqRhs ← mkProofFrom rhs common lhsEqCommon? heq | unreachable!
-    return lhsEqRhs
-end
-
 /--
 Returns a proof that `a = b` (or `HEq a b`).
 It assumes `a` and `b` are in the same equivalence class.
 -/
-@[export lean_grind_mk_eq_proof]
-def mkEqProofImpl (a b : Expr) : GoalM Expr := do
-  let p ← go
-  trace[grind.debug.proof] "{p}"
-  return p
-where
-  go : GoalM Expr := do
-    let n ← getRootENode a
-    if !n.heqProofs then
-      trace[grind.debug.proof] "{a} = {b}"
-      mkEqProofCore a b (heq := false)
-    else
-      if (← hasSameType a b) then
-        trace[grind.debug.proof] "{a} = {b}"
-        mkEqOfHEq (← mkEqProofCore a b (heq := true))
-      else
-        trace[grind.debug.proof] "{a} ≡ {b}"
-        mkEqProofCore a b (heq := true)
+def mkEqProof (a b : Expr) : GoalM Expr := do
+  -- TODO
+  if (← isDefEq (← inferType a) (← inferType b)) then
+    mkSorry (← mkEq a b) (synthetic := false)
+  else
+    mkSorry (← mkHEq a b) (synthetic := false)
 
-def mkHEqProof (a b : Expr) : GoalM Expr :=
-  mkEqProofCore a b (heq := true)
+/--
+Returns a proof that `a = True`.
+It assumes `a` and `True` are in the same equivalence class.
+-/
+def mkEqTrueProof (a : Expr) : GoalM Expr := do
+  mkEqProof a (← getTrueExpr)
+
+/--
+Returns a proof that `a = False`.
+It assumes `a` and `False` are in the same equivalence class.
+-/
+def mkEqFalseProof (a : Expr) : GoalM Expr := do
+  mkEqProof a (← getFalseExpr)
 
 end Lean.Meta.Grind

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

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind
 import Lean.Meta.Tactic.Grind.Proof
-import Lean.Meta.Tactic.Grind.PropagatorAttr
 
 namespace Lean.Meta.Grind
 
@@ -106,13 +105,12 @@ This function performs the following:
 - If `(Not a) = True`, propagates `a = False`.
 -/
 builtin_grind_propagator propagateNotDown ↓Not := fun e => do
-  let_expr Not a := e | return ()
   if (← isEqFalse e) then
+    let_expr Not a := e | return ()
     pushEqTrue a <| mkApp2 (mkConst ``Lean.Grind.eq_true_of_not_eq_false) a (← mkEqFalseProof e)
   else if (← isEqTrue e) then
+    let_expr Not a := e | return ()
     pushEqFalse a <| mkApp2 (mkConst ``Lean.Grind.eq_false_of_not_eq_true) a (← mkEqTrueProof e)
-  else if (← isEqv e a) then
-    closeGoal <| mkApp2 (mkConst ``Lean.Grind.false_of_not_eq_self) a (← mkEqProof e a)
 
 /-- Propagates `Eq` upwards -/
 builtin_grind_propagator propagateEqUp ↑Eq := fun e => do
@@ -122,7 +120,7 @@ builtin_grind_propagator propagateEqUp ↑Eq := fun e => do
   else if (← isEqTrue b) then
     pushEq e a <| mkApp3 (mkConst ``Lean.Grind.eq_eq_of_eq_true_right) a b (← mkEqTrueProof b)
   else if (← isEqv a b) then
-    pushEqTrue e <| mkApp2 (mkConst ``eq_true) e (← mkEqProof a b)
+    pushEqTrue e <| mkApp2 (mkConst ``of_eq_true) e (← mkEqProof a b)
 
 /-- Propagates `Eq` downwards -/
 builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
@@ -136,10 +134,4 @@ builtin_grind_propagator propagateHEqDown ↓HEq := fun e => do
     let_expr HEq _ a _ b := e | return ()
     pushHEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
 
-/-- Propagates `HEq` upwards -/
-builtin_grind_propagator propagateHEqUp ↑HEq := fun e => do
-  let_expr HEq _ a _ b := e | return ()
-  if (← isEqv a b) then
-    pushEqTrue e <| mkApp2 (mkConst ``eq_true) e (← mkHEqProof a b)
-
 end Lean.Meta.Grind

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

@@ -1,61 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Grind
-import Lean.Meta.Tactic.Grind.Proof
-
-namespace Lean.Meta.Grind
-
-/-- Builtin propagators. -/
-structure BuiltinPropagators where
-  up   : Std.HashMap Name Propagator := {}
-  down : Std.HashMap Name Propagator := {}
-  deriving Inhabited
-
-builtin_initialize builtinPropagatorsRef : IO.Ref BuiltinPropagators ← IO.mkRef {}
-
-private def registerBuiltinPropagatorCore (declName : Name) (up : Bool) (proc : Propagator) : IO Unit := do
-  unless (← initializing) do
-    throw (IO.userError s!"invalid builtin `grind` propagator declaration, it can only be registered during initialization")
-  if up then
-    if (← builtinPropagatorsRef.get).up.contains declName then
-      throw (IO.userError s!"invalid builtin `grind` upward propagator `{declName}`, it has already been declared")
-    builtinPropagatorsRef.modify fun { up, down } => { up := up.insert declName proc, down }
-  else
-    if (← builtinPropagatorsRef.get).down.contains declName then
-      throw (IO.userError s!"invalid builtin `grind` downward propagator `{declName}`, it has already been declared")
-    builtinPropagatorsRef.modify fun { up, down } => { up, down := down.insert declName proc }
-
-def registerBuiltinUpwardPropagator (declName : Name) (proc : Propagator) : IO Unit :=
-  registerBuiltinPropagatorCore declName true proc
-
-def registerBuiltinDownwardPropagator (declName : Name) (proc : Propagator) : IO Unit :=
-  registerBuiltinPropagatorCore declName false proc
-
-private def addBuiltin (propagatorName : Name) (stx : Syntax) : AttrM Unit := do
-  let go : MetaM Unit := do
-    let up := stx[1].getKind == ``Lean.Parser.Tactic.simpPost
-    let addDeclName := if up then
-      ``registerBuiltinUpwardPropagator
-    else
-      ``registerBuiltinDownwardPropagator
-    let declName ← resolveGlobalConstNoOverload stx[2]
-    let val := mkAppN (mkConst addDeclName) #[toExpr declName, mkConst propagatorName]
-    let initDeclName ← mkFreshUserName (propagatorName ++ `declare)
-    declareBuiltin initDeclName val
-  go.run' {}
-
-builtin_initialize
-  registerBuiltinAttribute {
-    ref             := by exact decl_name%
-    name            := `grindPropagatorBuiltinAttr
-    descr           := "Builtin `grind` propagator procedure"
-    applicationTime := AttributeApplicationTime.afterCompilation
-    erase           := fun _ => throwError "Not implemented yet, [-builtin_simproc]"
-    add             := fun declName stx _ => addBuiltin declName stx
-  }
-
-end Lean.Meta.Grind

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

@@ -1,54 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Grind.Lemmas
-import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.PropagatorAttr
-import Lean.Meta.Tactic.Grind.Proj
-
-namespace Lean.Meta.Grind
-
-def mkMethods : CoreM Methods := do
-  let builtinPropagators ← builtinPropagatorsRef.get
-  return {
-    propagateUp := fun e => do
-     let .const declName _ := e.getAppFn | return ()
-     propagateProjEq e
-     if let some prop := builtinPropagators.up[declName]? then
-       prop e
-    propagateDown := fun e => do
-     let .const declName _ := e.getAppFn | return ()
-     if let some prop := builtinPropagators.down[declName]? then
-       prop e
-  }
-
-def GrindM.run (x : GrindM α) (mainDeclName : Name) (config : Grind.Config) : MetaM α := do
-  let scState := ShareCommon.State.mk _
-  let (falseExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``False)
-  let (trueExpr, scState)  := ShareCommon.State.shareCommon scState (mkConst ``True)
-  let thms ← grindNormExt.getTheorems
-  let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
-  let simp ← Simp.mkContext
-    (config := { arith := true })
-    (simpTheorems := #[thms])
-    (congrTheorems := (← getSimpCongrTheorems))
-  x (← mkMethods).toMethodsRef { mainDeclName, config, simprocs, simp } |>.run' { scState, trueExpr, falseExpr }
-
-@[inline] def GoalM.run (goal : Goal) (x : GoalM α) : GrindM (α × Goal) :=
-  goal.mvarId.withContext do StateRefT'.run x goal
-
-@[inline] def GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal :=
-  goal.mvarId.withContext do StateRefT'.run' (x *> get) goal
-
-def mkGoal (mvarId : MVarId) : GrindM Goal := do
-  let trueExpr ← getTrueExpr
-  let falseExpr ← getFalseExpr
-  let thmMap ← getEMatchTheorems
-  GoalM.run' { mvarId, thmMap } do
-    mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0)
-    mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0)
-
-end Lean.Meta.Grind

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

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Grind.Tactics
 import Lean.Util.ShareCommon
-import Lean.HeadIndex
 import Lean.Meta.Basic
 import Lean.Meta.CongrTheorems
 import Lean.Meta.AbstractNestedProofs
@@ -14,7 +12,6 @@ import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.Attr
-import Lean.Meta.Tactic.Grind.EMatchTheorem
 
 namespace Lean.Meta.Grind
 
@@ -23,9 +20,6 @@ namespace Lean.Meta.Grind
   -- inserted into the E-graph
   unsafe ptrEq a b
 
-/-- We use this auxiliary constant to mark delayed congruence proofs. -/
-def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
-
 /--
 Returns `true` if `e` is `True`, `False`, or a literal value.
 See `LitValues` for supported literals.
@@ -40,18 +34,11 @@ register_builtin_option grind.debug : Bool := {
   descr    := "check invariants after updates"
 }
 
-register_builtin_option grind.debug.proofs : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "check proofs between the elements of all equivalence classes"
-}
-
 /-- Context for `GrindM` monad. -/
 structure Context where
-  simp         : Simp.Context
-  simprocs     : Array Simp.Simprocs
+  simp     : Simp.Context
+  simprocs : Array Simp.Simprocs
   mainDeclName : Name
-  config       : Grind.Config
 
 /-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
@@ -89,10 +76,6 @@ instance : Nonempty MethodsRef := MethodsRefPointed.property
 
 abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 
-/-- Returns the user-defined configuration options -/
-def getConfig : GrindM Grind.Config :=
-  return (← readThe Context).config
-
 /-- Returns the internalized `True` constant.  -/
 def getTrueExpr : GrindM Expr := do
   return (← get).trueExpr
@@ -107,10 +90,6 @@ def getMainDeclName : GrindM Name :=
 @[inline] def getMethodsRef : GrindM MethodsRef :=
   read
 
-/-- Returns maximum term generation that is considered during ematching. -/
-def getMaxGeneration : GrindM Nat := do
-  return (← getConfig).gen
-
 /--
 Abtracts nested proofs in `e`. This is a preprocessing step performed before internalization.
 -/
@@ -203,44 +182,31 @@ structure NewEq where
   proof : Expr
   isHEq : Bool
 
-/--
-Key for the `ENodeMap` and `ParentMap` map.
-We use pointer addresses and rely on the fact all internalized expressions
-have been hash-consed, i.e., we have applied `shareCommon`.
--/
-private structure ENodeKey where
-  expr : Expr
+abbrev ENodes := PHashMap USize ENode
 
-instance : Hashable ENodeKey where
-  hash k := unsafe (ptrAddrUnsafe k.expr).toUInt64
-
-instance : BEq ENodeKey where
-  beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
-
-abbrev ENodeMap := PHashMap ENodeKey ENode
-
-/--
-Key for the congruence table.
-We need access to the `enodes` to be able to retrieve the equivalence class roots.
--/
-structure CongrKey (enodes : ENodeMap) where
+structure CongrKey (enodes : ENodes) where
   e : Expr
 
-private def hashRoot (enodes : ENodeMap) (e : Expr) : UInt64 :=
-  if let some node := enodes.find? { expr := e } then
-    unsafe (ptrAddrUnsafe node.root).toUInt64
+private abbrev toENodeKey (e : Expr) : USize :=
+  unsafe ptrAddrUnsafe e
+
+private def hashRoot (enodes : ENodes) (e : Expr) : UInt64 :=
+  if let some node := enodes.find? (toENodeKey e) then
+    toENodeKey node.root |>.toUInt64
   else
     13
 
-private def hasSameRoot (enodes : ENodeMap) (a b : Expr) : Bool := Id.run do
-  if isSameExpr a b then
+private def hasSameRoot (enodes : ENodes) (a b : Expr) : Bool := Id.run do
+  let ka := toENodeKey a
+  let kb := toENodeKey b
+  if ka == kb then
     return true
   else
-    let some n1 := enodes.find? { expr := a } | return false
-    let some n2 := enodes.find? { expr := b } | return false
-    isSameExpr n1.root n2.root
+    let some n1 := enodes.find? ka | return false
+    let some n2 := enodes.find? kb | return false
+    toENodeKey n1.root == toENodeKey n2.root
 
-def congrHash (enodes : ENodeMap) (e : Expr) : UInt64 :=
+def congrHash (enodes : ENodes) (e : Expr) : UInt64 :=
   if e.isAppOfArity ``Lean.Grind.nestedProof 2 then
     -- We only hash the proposition
     hashRoot enodes (e.getArg! 0)
@@ -252,7 +218,7 @@ where
     | .app f a => go f (mixHash r (hashRoot enodes a))
     | _ => mixHash r (hashRoot enodes e)
 
-partial def isCongruent (enodes : ENodeMap) (a b : Expr) : Bool :=
+partial def isCongruent (enodes : ENodes) (a b : Expr) : Bool :=
   if a.isAppOfArity ``Lean.Grind.nestedProof 2 && b.isAppOfArity ``Lean.Grind.nestedProof 2 then
     hasSameRoot enodes (a.getArg! 0) (b.getArg! 0)
   else
@@ -272,51 +238,17 @@ instance : Hashable (CongrKey enodes) where
 instance : BEq (CongrKey enodes) where
   beq k1 k2 := isCongruent enodes k1.e k2.e
 
-abbrev CongrTable (enodes : ENodeMap) := PHashSet (CongrKey enodes)
+abbrev CongrTable (enodes : ENodes) := PHashSet (CongrKey enodes)
 
 -- Remark: we cannot use pointer addresses here because we have to traverse the tree.
 abbrev ParentSet := RBTree Expr Expr.quickComp
-abbrev ParentMap := PHashMap ENodeKey ParentSet
-
-/--
-The E-matching module instantiates theorems using the `EMatchTheorem proof` and a (partial) assignment.
-We want to avoid instantiating the same theorem with the same assignment more than once.
-Therefore, we store the (pre-)instance information in set.
-Recall that the proofs of activated theorems have been hash-consed.
-The assignment contains internalized expressions, which have also been hash-consed.
--/
-structure PreInstance where
-  proof      : Expr
-  assignment : Array Expr
-
-instance : Hashable PreInstance where
-  hash i := Id.run do
-    let mut r := unsafe (ptrAddrUnsafe i.proof >>> 3).toUInt64
-    for v in i.assignment do
-      r := mixHash r (unsafe (ptrAddrUnsafe v >>> 3).toUInt64)
-    return r
-
-instance : BEq PreInstance where
-  beq i₁ i₂ := Id.run do
-    unless isSameExpr i₁.proof i₂.proof do return false
-    unless i₁.assignment.size == i₂.assignment.size do return false
-    for v₁ in i₁.assignment, v₂ in i₂.assignment do
-      unless isSameExpr v₁ v₂ do return false
-    return true
-
-abbrev PreInstanceSet := PHashSet PreInstance
+abbrev ParentMap := PHashMap USize ParentSet
 
 structure Goal where
   mvarId       : MVarId
-  enodes       : ENodeMap := {}
+  enodes       : ENodes := {}
   parents      : ParentMap := {}
   congrTable   : CongrTable enodes := {}
-  /--
-  A mapping from each function application index (`HeadIndex`) to a list of applications with that index.
-  Recall that the `HeadIndex` for a constant is its constant name, and for a free variable,
-  it is its unique id.
-  -/
-  appMap       : PHashMap HeadIndex (List Expr) := {}
   /-- Equations to be processed. -/
   newEqs       : Array NewEq := #[]
   /-- `inconsistent := true` if `ENode`s for `True` and `False` are in the same equivalence class. -/
@@ -325,19 +257,6 @@ structure Goal where
   gmt          : Nat := 0
   /-- Next unique index for creating ENodes -/
   nextIdx      : Nat := 0
-  /-- Active theorems that we have performed ematching at least once. -/
-  thms         : PArray EMatchTheorem := {}
-  /-- Active theorems that we have not performed any round of ematching yet. -/
-  newThms      : PArray EMatchTheorem := {}
-  /--
-  Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols.
-  Local theorem provided by users are added directly into `newThms`.
-  -/
-  thmMap       : EMatchTheorems
-  /-- Number of theorem instances generated so far -/
-  numInstances : Nat := 0
-  /-- (pre-)instances found so far -/
-  instances    : PreInstanceSet := {}
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -347,20 +266,9 @@ abbrev GoalM := StateRefT Goal GrindM
 
 abbrev Propagator := Expr → GoalM Unit
 
-/--
-A helper function used to mark a theorem instance found by the E-matching module.
-It returns `true` if it is a new instance and `false` otherwise.
--/
-def markTheorenInstance (proof : Expr) (assignment : Array Expr) : GoalM Bool := do
-  let k := { proof, assignment }
-  if (← get).instances.contains k then
-    return false
-  modify fun s => { s with instances := s.instances.insert k }
-  return true
-
-/-- Returns `true` if the maximum number of instances has been reached. -/
-def checkMaxInstancesExceeded : GoalM Bool := do
-  return (← get).numInstances >= (← getConfig).instances
+/-- Return `true` if the goal is inconsistent. -/
+def isInconsistent : GoalM Bool :=
+  return (← get).inconsistent
 
 /-- Returns `true` if `e` is the internalized `True` expression.  -/
 def isTrueExpr (e : Expr) : GrindM Bool :=
@@ -375,18 +283,14 @@ Returns `some n` if `e` has already been "internalized" into the
 Otherwise, returns `none`s.
 -/
 def getENode? (e : Expr) : GoalM (Option ENode) :=
-  return (← get).enodes.find? { expr := e }
+  return (← get).enodes.find? (unsafe ptrAddrUnsafe e)
 
 /-- Returns node associated with `e`. It assumes `e` has already been internalized. -/
 def getENode (e : Expr) : GoalM ENode := do
-  let some n := (← get).enodes.find? { expr := e }
+  let some n := (← get).enodes.find? (unsafe ptrAddrUnsafe e)
     | throwError "internal `grind` error, term has not been internalized{indentExpr e}"
   return n
 
-/-- Returns the generation of the given term. Is assumes it has been internalized -/
-def getGeneration (e : Expr) : GoalM Nat :=
-  return (← getENode e).generation
-
 /-- Returns `true` if `e` is in the equivalence class of `True`. -/
 def isEqTrue (e : Expr) : GoalM Bool := do
   let n ← getENode e
@@ -399,12 +303,9 @@ def isEqFalse (e : Expr) : GoalM Bool := do
 
 /-- Returns `true` if `a` and `b` are in the same equivalence class. -/
 def isEqv (a b : Expr) : GoalM Bool := do
-  if isSameExpr a b then
-    return true
-  else
-    let na ← getENode a
-    let nb ← getENode b
-    return isSameExpr na.root nb.root
+  let na ← getENode a
+  let nb ← getENode b
+  return isSameExpr na.root nb.root
 
 /-- Returns `true` if the root of its equivalence class. -/
 def isRoot (e : Expr) : GoalM Bool := do
@@ -420,17 +321,13 @@ def getRoot? (e : Expr) : GoalM (Option Expr) := do
 def getRoot (e : Expr) : GoalM Expr :=
   return (← getENode e).root
 
-/-- Returns the root enode in the equivalence class of `e`. -/
-def getRootENode (e : Expr) : GoalM ENode := do
-  getENode (← getRoot e)
-
 /-- Returns the next element in the equivalence class of `e`. -/
 def getNext (e : Expr) : GoalM Expr :=
   return (← getENode e).next
 
 /-- Returns `true` if `e` has already been internalized. -/
 def alreadyInternalized (e : Expr) : GoalM Bool :=
-  return (← get).enodes.contains { expr := e }
+  return (← get).enodes.contains (unsafe ptrAddrUnsafe e)
 
 def getTarget? (e : Expr) : GoalM (Option Expr) := do
   let some n ← getENode? e | return none
@@ -443,12 +340,8 @@ Otherwise, it pushes `HEq lhs rhs`.
 def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit :=
   modify fun s => { s with newEqs := s.newEqs.push { lhs, rhs, proof, isHEq } }
 
-/-- Return `true` if `a` and `b` have the same type. -/
-def hasSameType (a b : Expr) : MetaM Bool :=
-  withDefault do isDefEq (← inferType a) (← inferType b)
-
 @[inline] def pushEqHEq (lhs rhs proof : Expr) : GoalM Unit := do
-  if (← hasSameType lhs rhs) then
+  if (← isDefEq (← inferType lhs) (← inferType rhs)) then
     pushEqCore lhs rhs proof (isHEq := false)
   else
     pushEqCore lhs rhs proof (isHEq := true)
@@ -475,8 +368,9 @@ information in the root (aka canonical representative) of `child`.
 -/
 def registerParent (parent : Expr) (child : Expr) : GoalM Unit := do
   let some childRoot ← getRoot? child | return ()
-  let parents := if let some parents := (← get).parents.find? { expr := childRoot } then parents else {}
-  modify fun s => { s with parents := s.parents.insert { expr := childRoot } (parents.insert parent) }
+  let key := toENodeKey childRoot
+  let parents := if let some parents := (← get).parents.find? key then parents else {}
+  modify fun s => { s with parents := s.parents.insert key (parents.insert parent) }
 
 /--
 Returns the set of expressions `e` is a child of, or an expression in
@@ -484,7 +378,7 @@ Returns the set of expressions `e` is a child of, or an expression in
 The information is only up to date if `e` is the root (aka canonical representative) of the equivalence class.
 -/
 def getParents (e : Expr) : GoalM ParentSet := do
-  let some parents := (← get).parents.find? { expr := e } | return {}
+  let some parents := (← get).parents.find? (toENodeKey e) | return {}
   return parents
 
 /--
@@ -492,7 +386,7 @@ Similar to `getParents`, but also removes the entry `e ↦ parents` from the par
 -/
 def getParentsAndReset (e : Expr) : GoalM ParentSet := do
   let parents ← getParents e
-  modify fun s => { s with parents := s.parents.erase { expr := e } }
+  modify fun s => { s with parents := s.parents.erase (toENodeKey e) }
   return parents
 
 /--
@@ -500,14 +394,15 @@ Copy `parents` to the parents of `root`.
 `root` must be the root of its equivalence class.
 -/
 def copyParentsTo (parents : ParentSet) (root : Expr) : GoalM Unit := do
-  let mut curr := if let some parents := (← get).parents.find? { expr := root } then parents else {}
+  let key := toENodeKey root
+  let mut curr := if let some parents := (← get).parents.find? key then parents else {}
   for parent in parents do
     curr := curr.insert parent
-  modify fun s => { s with parents := s.parents.insert { expr := root } curr }
+  modify fun s => { s with parents := s.parents.insert key curr }
 
 def setENode (e : Expr) (n : ENode) : GoalM Unit :=
   modify fun s => { s with
-    enodes := s.enodes.insert { expr := e } n
+    enodes := s.enodes.insert (unsafe ptrAddrUnsafe e) n
     congrTable := unsafe unsafeCast s.congrTable
   }
 
@@ -533,54 +428,6 @@ def mkENode (e : Expr) (generation : Nat) : GoalM Unit := do
   let interpreted ← isInterpreted e
   mkENodeCore e interpreted ctor generation
 
-/-- Returns `true` is `e` is the root of its congruence class. -/
-def isCongrRoot (e : Expr) : GoalM Bool := do
-  return isSameExpr e (← getENode e).cgRoot
-
-/-- Return `true` if the goal is inconsistent. -/
-def isInconsistent : GoalM Bool :=
-  return (← get).inconsistent
-
-/--
-Returns a proof that `a = b` (or `HEq a b`).
-It assumes `a` and `b` are in the same equivalence class.
--/
--- Forward definition
-@[extern "lean_grind_mk_eq_proof"]
-opaque mkEqProof (a b : Expr) : GoalM Expr
-
-/--
-Returns a proof that `a = True`.
-It assumes `a` and `True` are in the same equivalence class.
--/
-def mkEqTrueProof (a : Expr) : GoalM Expr := do
-  mkEqProof a (← getTrueExpr)
-
-/--
-Returns a proof that `a = False`.
-It assumes `a` and `False` are in the same equivalence class.
--/
-def mkEqFalseProof (a : Expr) : GoalM Expr := do
-  mkEqProof a (← getFalseExpr)
-
-/-- Marks current goal as inconsistent without assigning `mvarId`. -/
-def markAsInconsistent : GoalM Unit := do
-  modify fun s => { s with inconsistent := true }
-
-/--
-Closes the current goal using the given proof of `False` and
-marks it as inconsistent if it is not already marked so.
--/
-def closeGoal (falseProof : Expr) : GoalM Unit := do
-  markAsInconsistent
-  let mvarId := (← get).mvarId
-  unless (← mvarId.isAssigned) do
-    let target ← mvarId.getType
-    if target.isFalse then
-      mvarId.assign falseProof
-    else
-      mvarId.assign (← mkFalseElim target falseProof)
-
 /-- Returns all enodes in the goal -/
 def getENodes : GoalM (Array ENode) := do
   -- We must sort because we are using pointer addresses as keys in `enodes`
@@ -605,12 +452,12 @@ def forEachEqc (f : ENode → GoalM Unit) : GoalM Unit := do
     if isSameExpr n.self n.root then
       f n
 
-structure Methods where
+private structure Methods where
   propagateUp   : Propagator := fun _ => return ()
   propagateDown : Propagator := fun _ => return ()
   deriving Inhabited
 
-def Methods.toMethodsRef (m : Methods) : MethodsRef :=
+private def Methods.toMethodsRef (m : Methods) : MethodsRef :=
   unsafe unsafeCast m
 
 private def MethodsRef.toMethods (m : MethodsRef) : Methods :=
@@ -625,25 +472,91 @@ def propagateUp (e : Expr) : GoalM Unit := do
 def propagateDown (e : Expr) : GoalM Unit := do
   (← getMethods).propagateDown e
 
-/-- Returns expressions in the given expression equivalence class. -/
-partial def getEqc (e : Expr) : GoalM (List Expr) :=
-  go e e []
-where
-  go (first : Expr) (e : Expr) (acc : List Expr) : GoalM (List Expr) := do
-    let next ← getNext e
-    let acc := e :: acc
-    if isSameExpr first next then
-      return acc
-    else
-      go first next acc
+/-- Builtin propagators. -/
+structure BuiltinPropagators where
+  up   : Std.HashMap Name Propagator := {}
+  down : Std.HashMap Name Propagator := {}
+  deriving Inhabited
 
-/-- Returns all equivalence classes in the current goal. -/
-partial def getEqcs : GoalM (List (List Expr)) := do
-  let mut r := []
-  let nodes ← getENodes
-  for node in nodes do
-    if isSameExpr node.root node.self then
-      r := (← getEqc node.self) :: r
-  return r
+builtin_initialize builtinPropagatorsRef : IO.Ref BuiltinPropagators ← IO.mkRef {}
+
+private def registerBuiltinPropagatorCore (declName : Name) (up : Bool) (proc : Propagator) : IO Unit := do
+  unless (← initializing) do
+    throw (IO.userError s!"invalid builtin `grind` propagator declaration, it can only be registered during initialization")
+  if up then
+    if (← builtinPropagatorsRef.get).up.contains declName then
+      throw (IO.userError s!"invalid builtin `grind` upward propagator `{declName}`, it has already been declared")
+    builtinPropagatorsRef.modify fun { up, down } => { up := up.insert declName proc, down }
+  else
+    if (← builtinPropagatorsRef.get).down.contains declName then
+      throw (IO.userError s!"invalid builtin `grind` downward propagator `{declName}`, it has already been declared")
+    builtinPropagatorsRef.modify fun { up, down } => { up, down := down.insert declName proc }
+
+def registerBuiltinUpwardPropagator (declName : Name) (proc : Propagator) : IO Unit :=
+  registerBuiltinPropagatorCore declName true proc
+
+def registerBuiltinDownwardPropagator (declName : Name) (proc : Propagator) : IO Unit :=
+  registerBuiltinPropagatorCore declName false proc
+
+private def addBuiltin (propagatorName : Name) (stx : Syntax) : AttrM Unit := do
+  let go : MetaM Unit := do
+    let up := stx[1].getKind == ``Lean.Parser.Tactic.simpPost
+    let addDeclName := if up then
+      ``registerBuiltinUpwardPropagator
+    else
+      ``registerBuiltinDownwardPropagator
+    let declName ← resolveGlobalConstNoOverload stx[2]
+    let val := mkAppN (mkConst addDeclName) #[toExpr declName, mkConst propagatorName]
+    let initDeclName ← mkFreshUserName (propagatorName ++ `declare)
+    declareBuiltin initDeclName val
+  go.run' {}
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `grindPropagatorBuiltinAttr
+    descr           := "Builtin `grind` propagator procedure"
+    applicationTime := AttributeApplicationTime.afterCompilation
+    erase           := fun _ => throwError "Not implemented yet, [-builtin_simproc]"
+    add             := fun declName stx _ => addBuiltin declName stx
+  }
+
+def mkMethods : CoreM Methods := do
+  let builtinPropagators ← builtinPropagatorsRef.get
+  return {
+    propagateUp := fun e => do
+     let .const declName _ := e.getAppFn | return ()
+     if let some prop := builtinPropagators.up[declName]? then
+       prop e
+    propagateDown := fun e => do
+     let .const declName _ := e.getAppFn | return ()
+     if let some prop := builtinPropagators.down[declName]? then
+       prop e
+  }
+
+def GrindM.run (x : GrindM α) (mainDeclName : Name) : MetaM α := do
+  let scState := ShareCommon.State.mk _
+  let (falseExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``False)
+  let (trueExpr, scState)  := ShareCommon.State.shareCommon scState (mkConst ``True)
+  let thms ← grindNormExt.getTheorems
+  let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
+  let simp ← Simp.mkContext
+    (config := { arith := true })
+    (simpTheorems := #[thms])
+    (congrTheorems := (← getSimpCongrTheorems))
+  x (← mkMethods).toMethodsRef { mainDeclName, simprocs, simp } |>.run' { scState, trueExpr, falseExpr }
+
+@[inline] def GoalM.run (goal : Goal) (x : GoalM α) : GrindM (α × Goal) :=
+  goal.mvarId.withContext do StateRefT'.run x goal
+
+@[inline] def GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal :=
+  goal.mvarId.withContext do StateRefT'.run' (x *> get) goal
+
+def mkGoal (mvarId : MVarId) : GrindM Goal := do
+  let trueExpr ← getTrueExpr
+  let falseExpr ← getFalseExpr
+  GoalM.run' { mvarId } do
+    mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0)
+    mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0)
 
 end Lean.Meta.Grind

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

@@ -49,13 +49,17 @@ If they do, they must disable the following `simprocs`.
 -/
 
 builtin_dsimproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
-  let_expr Neg.neg _ _ arg ← e | return .continue
+  unless e.isAppOfArity ``Neg.neg 3 do return .continue
+  let arg := e.appArg!
   if arg.isAppOfArity ``OfNat.ofNat 3 then
     -- We return .done to ensure `Neg.neg` is not unfolded even when `ground := true`.
     return .done e
   else
     let some v ← fromExpr? arg | return .continue
-    return .done <| toExpr (- v)
+    if v < 0 then
+      return .done <| toExpr (- v)
+    else
+      return .done <| toExpr v
 
 /-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator. -/
 builtin_dsimproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -123,15 +123,6 @@ unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) :=
   } `Lean.PrettyPrinter.Delaborator.delabAttribute
 @[builtin_init mkDelabAttribute] opaque delabAttribute : KeyedDeclsAttribute Delab
 
-/--
-`@[app_delab c]` registers a delaborator for applications with head constant `c`.
-Such delaborators also apply to the constant `c` itself (known as a "nullary application").
-
-This attribute should be applied to definitions of type `Lean.PrettyPrinter.Delaborator.Delab`.
-
-When defining delaborators for constant applications, one should prefer this attribute over `@[delab app.c]`,
-as `@[app_delab c]` first performs name resolution on `c` in the current scope.
--/
 macro "app_delab" id:ident : attr => do
   match ← Macro.resolveGlobalName id.getId with
   | [] => Macro.throwErrorAt id s!"unknown declaration '{id.getId}'"

src/Lean/ToExpr.lean

@@ -14,15 +14,10 @@ namespace Lean
 /--
 We use the `ToExpr` type class to convert values of type `α` into
 expressions that denote these values in Lean.
-
-Examples:
+Example:
 ```
 toExpr true = .const ``Bool.true []
-
-toTypeExpr Bool = .const ``Bool []
 ```
-
-See also `ToLevel` for representing universe levels as `Level` expressions.
 -/
 class ToExpr (α : Type u) where
   /-- Convert a value `a : α` into an expression that denotes `a` -/

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -293,15 +293,8 @@ The semantics for `BVExpr`.
 -/
 def eval (assign : Assignment) : BVExpr w → BitVec w
   | .var idx =>
-    let packedBv := assign.get idx
-    /-
-    This formulation improves performance, as in a well formed expression the condition always holds
-    so there is no need for the more involved `BitVec.truncate` logic.
-    -/
-    if h : packedBv.w = w then
-      h ▸ packedBv.bv
-    else
-      packedBv.bv.truncate w
+    let ⟨bv⟩ := assign.get idx
+    bv.truncate w
   | .const val => val
   | .zeroExtend v expr => BitVec.zeroExtend v (eval assign expr)
   | .extract start len expr => BitVec.extractLsb' start len (eval assign expr)
@@ -315,13 +308,8 @@ def eval (assign : Assignment) : BVExpr w → BitVec w
   | .arithShiftRight lhs rhs => BitVec.sshiftRight' (eval assign lhs) (eval assign rhs)
 
 @[simp]
-theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.truncate w := by
-  rw [eval]
-  split
-  · next h =>
-    subst h
-    simp
-  · rfl
+theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.truncate _ := by
+  rfl
 
 @[simp]
 theorem eval_const : eval assign (.const val) = val := by rfl
@@ -466,7 +454,7 @@ def eval (assign : BVExpr.Assignment) (expr : BVLogicalExpr) : Bool :=
 @[simp] theorem eval_not : eval assign (.not x) = !eval assign x := rfl
 @[simp] theorem eval_gate : eval assign (.gate g x y) = g.eval (eval assign x) (eval assign y) := rfl
 @[simp] theorem eval_ite :
-  eval assign (.ite d l r) = bif (eval assign d) then (eval assign l) else (eval assign r) := rfl
+  eval assign (.ite d l r) = if (eval assign d) then (eval assign l) else (eval assign r) := rfl
 
 def Sat (x : BVLogicalExpr) (assign : BVExpr.Assignment) : Prop := eval assign x = true
 

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean

@@ -18,7 +18,7 @@ inductive Gate
   | and
   | xor
   | beq
-  | or
+  | imp
 
 namespace Gate
 
@@ -26,13 +26,13 @@ def toString : Gate → String
   | and => "&&"
   | xor => "^^"
   | beq => "=="
-  | or => "||"
+  | imp => "->"
 
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
   | xor => (· ^^ ·)
   | beq => (· == ·)
-  | or => (· || ·)
+  | imp => (· → ·)
 
 end Gate
 
@@ -59,13 +59,13 @@ def eval (a : α → Bool) : BoolExpr α → Bool
   | .const b => b
   | .not x => !eval a x
   | .gate g x y => g.eval (eval a x) (eval a y)
-  | .ite d l r => bif d.eval a then l.eval a else r.eval a
+  | .ite d l r => if d.eval a then l.eval a else r.eval a
 
 @[simp] theorem eval_literal : eval a (.literal l) = a l := rfl
 @[simp] theorem eval_const : eval a (.const b) = b := rfl
 @[simp] theorem eval_not : eval a (.not x) = !eval a x := rfl
 @[simp] theorem eval_gate : eval a (.gate g x y) = g.eval (eval a x) (eval a y) := rfl
-@[simp] theorem eval_ite : eval a (.ite d l r) = bif d.eval a then l.eval a else r.eval a := rfl
+@[simp] theorem eval_ite : eval a (.ite d l r) = if d.eval a then l.eval a else r.eval a := rfl
 
 def Sat (a : α → Bool) (x : BoolExpr α) : Prop := eval a x = true
 def Unsat (x : BoolExpr α) : Prop := ∀ f, eval f x = false

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean

@@ -75,9 +75,9 @@ where
         let ret := aig.mkBEqCached input
         have := LawfulOperator.le_size (f := mkBEqCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
-      | .or =>
-        let ret := aig.mkOrCached input
-        have := LawfulOperator.le_size (f := mkOrCached) aig input
+      | .imp =>
+        let ret := aig.mkImpCached input
+        have := LawfulOperator.le_size (f := mkImpCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
 
 namespace ofBoolExprCached
@@ -127,9 +127,9 @@ theorem go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.size) (hbounds) :
     | beq =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
-    | or =>
+    | imp =>
       simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih]
+      rw [AIG.LawfulOperator.decl_eq (f := mkImpCached), rih, lih]
 
 theorem go_isPrefix_aig {aig : AIG β} :
     IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -118,6 +118,7 @@ theorem BitVec.srem_umod (x y : BitVec w) :
   rw [BitVec.srem_eq]
   cases x.msb <;> cases y.msb <;> simp
 
+attribute [bv_normalize] Bool.cond_eq_if
 attribute [bv_normalize] BitVec.abs_eq
 attribute [bv_normalize] BitVec.twoPow_eq
 

src/Std/Tactic/BVDecide/Normalize/Bool.lean

@@ -41,14 +41,7 @@ attribute [bv_normalize] Bool.not_not
 attribute [bv_normalize] Bool.and_self_left
 attribute [bv_normalize] Bool.and_self_right
 attribute [bv_normalize] eq_self
-attribute [bv_normalize] Bool.cond_self
-attribute [bv_normalize] cond_false
-attribute [bv_normalize] cond_true
-attribute [bv_normalize] Bool.cond_not
-
-@[bv_normalize]
-theorem if_eq_cond {b : Bool} {x y : α} : (if b = true then x else y) = (bif b then x else y) := by
-  rw [cond_eq_if]
+attribute [bv_normalize] ite_self
 
 @[bv_normalize]
 theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide

src/Std/Tactic/BVDecide/Normalize/Prop.lean

@@ -13,6 +13,8 @@ This module contains the `Prop` simplifying part of the `bv_normalize` simp set.
 namespace Std.Tactic.BVDecide
 namespace Frontend.Normalize
 
+attribute [bv_normalize] ite_true
+attribute [bv_normalize] ite_false
 attribute [bv_normalize] dite_true
 attribute [bv_normalize] dite_false
 attribute [bv_normalize] and_true

src/Std/Tactic/BVDecide/Reflect.lean

@@ -123,12 +123,12 @@ theorem umod_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' =
     (lhs' % rhs') = (lhs % rhs) := by
   simp[*]
 
-theorem cond_true (discr : Bool) (lhs rhs : BitVec w) :
-    (!discr || ((bif discr then lhs else rhs) == lhs)) = true := by
+theorem if_true (discr : Bool) (lhs rhs : BitVec w) :
+    decide ((discr == true) = true → ((if discr = true then lhs else rhs) == lhs) = true) = true := by
   cases discr <;> simp
 
-theorem cond_false (discr : Bool) (lhs rhs : BitVec w) :
-    (discr || ((bif discr then lhs else rhs) == rhs)) = true := by
+theorem if_false (discr : Bool) (lhs rhs : BitVec w) :
+    decide ((discr == false) = true → ((if discr = true then lhs else rhs) == rhs) = true) = true := by
   cases discr <;> simp
 
 end BitVec
@@ -150,13 +150,13 @@ theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
     (lhs' == rhs') = (lhs == rhs) := by
   simp[*]
 
-theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (lhs' || rhs') = (lhs || rhs) := by
+theorem imp_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
+    (decide (lhs' → rhs')) = (decide (lhs → rhs)) := by
   simp[*]
 
-theorem cond_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
+theorem ite_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
     (h3 : rhs' = rhs) :
-    (bif discr' = true then lhs' else rhs') = (bif discr = true then lhs else rhs) := by
+    (if discr' = true then lhs' else rhs') = (if discr = true then lhs else rhs) := by
   simp[*]
 
 theorem false_of_eq_true_of_eq_false (h₁ : x = true) (h₂ : x = false) : False := by

tests/lean/run/6043.lean

@@ -1,6 +0,0 @@
-import Std.Tactic.BVDecide
-
-theorem extracted_1 (x : BitVec 32) :
-  BitVec.ofBool (x != 51#32) &&& BitVec.ofBool (x != 50#32) =
-    BitVec.ofBool (4294967294#32 > x + 4294967244#32) := by
-  bv_decide

tests/lean/run/6467.lean

@@ -1,16 +0,0 @@
-theorem confuses_the_user : -(no_index (OfNat.ofNat <| nat_lit 2)) = -2 := by
-  simp
-
-theorem ex : -(no_index (OfNat.ofNat <| nat_lit 2)) = (2 : Int) := by
-  simp only [Int.reduceNeg]
-  guard_target =ₛ -2 = 2
-  sorry
-
-theorem its_true_really : -(no_index (OfNat.ofNat <| nat_lit 2)) = -2 := by
-  rfl
-
-example : -(-(no_index (OfNat.ofNat <| nat_lit 2))) = 2 := by
-  simp
-
-example : -(no_index (-(no_index (OfNat.ofNat <| nat_lit 2)))) = -(-(-(-3+1))) := by
-  simp

tests/lean/run/bv_decide_rewriter.lean

@@ -85,7 +85,6 @@ example : (BitVec.twoPow 16 2) = 4#16 := by bv_normalize
 example {x : BitVec 16} : x / (BitVec.twoPow 16 2) = x >>> 2 := by bv_normalize
 example {x : BitVec 16} : x / (BitVec.ofNat 16 8) = x >>> 3 := by bv_normalize
 example {x y : Bool} (h1 : x && y) : x || y := by bv_normalize
-example (a b c: Bool) : (if a then b else c) = (if !a then c else b) := by bv_normalize
 
 section
 

tests/lean/run/bv_substructure.lean

@@ -23,8 +23,17 @@ theorem substructure_unit_3' (x y : BitVec 8) : Bool.xor (x = y) (y ≠ x) := by
 theorem substructure_unit_4 (a b : Bool) : (a && b) = (b && a) := by
   bv_decide
 
-theorem substructure_unit_5 (x : BitVec 32) : (if x.getLsbD 0 then !x.getLsbD 0 else x.getLsbD 0) = false := by
+theorem substructure_unit_5 (a : Bool) (b c : BitVec 32) (h1 : b < c ↔ a) (h2 : a = true) : b < c := by
   bv_decide
 
-theorem substructure_unit_6 (x y : BitVec 32) (h : x.getLsbD 0 = false) : (if x.getLsbD 0 then x else y) = y := by
+theorem substructure_unit_6 (a b c: Bool) : (if a then b else c) = (if !a then c else b) := by
+  bv_decide
+
+theorem substructure_unit_7 (a b c: Bool) : (bif a then b else c) = (bif !a then c else b) := by
+  bv_decide
+
+theorem substructure_unit_8 (x : BitVec 32) : (if x.getLsbD 0 then !x.getLsbD 0 else x.getLsbD 0) = false := by
+  bv_decide
+
+theorem substructure_unit_9 (x y : BitVec 32) (h : x.getLsbD 0 = false) : (if x.getLsbD 0 then x else y) = y := by
   bv_decide

tests/lean/run/derivingToExpr.lean

@@ -1,204 +0,0 @@
-import Lean.Elab.Deriving.ToExpr
-
-/-!
-# Tests for the `ToExpr` deriving handler
--/
-
-open Lean
-
-/-!
-Test without universes
--/
-inductive MonoOption' (α : Type) : Type
-  | some (a : α)
-  | none
-  deriving ToExpr
-
-/--
-info: Lean.Expr.app
-  (Lean.Expr.app (Lean.Expr.const `MonoOption'.some []) (Lean.Expr.const `Bool []))
-  (Lean.Expr.const `Bool.true [])
--/
-#guard_msgs in
-#eval repr <| toExpr <| MonoOption'.some true
-
-/-!
-Test with a universe polymorphic type parameter
--/
-inductive Option' (α : Type u)
-  | some (a : α)
-  | none
-  deriving ToExpr
-
-/--
-info: Lean.Expr.app
-  (Lean.Expr.app (Lean.Expr.const `Option'.some [Lean.Level.zero]) (Lean.Expr.const `Bool []))
-  (Lean.Expr.const `Bool.true [])
--/
-#guard_msgs in
-#eval repr <| toExpr <| Option'.some true
-
-example : ToExpr (Option' Nat) := inferInstance
-
-/-!
-Test with higher universe levels
--/
-structure MyULift.{r, s} (α : Type s) : Type (max s r) where
-  up :: down : α
-  deriving ToExpr
-
-/--
-info: Lean.Expr.app
-  (Lean.Expr.app
-    (Lean.Expr.const `Option'.some [Lean.Level.succ (Lean.Level.succ (Lean.Level.zero))])
-    (Lean.Expr.app
-      (Lean.Expr.const `MyULift [Lean.Level.succ (Lean.Level.succ (Lean.Level.zero)), Lean.Level.zero])
-      (Lean.Expr.const `Bool [])))
-  (Lean.Expr.app
-    (Lean.Expr.app
-      (Lean.Expr.const `MyULift.up [Lean.Level.succ (Lean.Level.succ (Lean.Level.zero)), Lean.Level.zero])
-      (Lean.Expr.const `Bool []))
-    (Lean.Expr.const `Bool.true []))
--/
-#guard_msgs in
-#eval repr <| toExpr <| Option'.some (MyULift.up.{2} true)
-
-example : ToExpr (Option' <| MyULift.{20} Nat) := inferInstance
-example [ToLevel.{u}] : ToExpr (Option' <| MyULift.{u} Nat) := inferInstance
-
-/-!
-Test with empty type.
--/
-inductive Empty'
-  deriving ToExpr
-
-/-!
-Test with recursive type
--/
-inductive List' (α : Type u)
-  | cons (a : α) (as : List' α)
-  | nil
-  deriving ToExpr
-
-/-!
-Test with nested type
--/
-inductive Foo
-  | l (x : List Foo)
-  deriving ToExpr
-
-/-!
-Test with mutual inductive type
--/
-mutual
-inductive A
-  | nil
-  | cons (a : A) (b : B)
-  deriving ToExpr
-inductive B
-  | cons₁ (a : A)
-  | cons₂ (a : A) (b : B)
-  deriving ToExpr
-end
-
-/--
-info: Lean.Expr.app
-  (Lean.Expr.app (Lean.Expr.const `A.cons []) (Lean.Expr.const `A.nil []))
-  (Lean.Expr.app (Lean.Expr.const `B.cons₁ []) (Lean.Expr.const `A.nil []))
--/
-#guard_msgs in
-#eval repr <| toExpr <| A.cons A.nil (B.cons₁ A.nil)
-/--
-info: Lean.Expr.app
-  (Lean.Expr.app (Lean.Expr.const `B.cons₂ []) (Lean.Expr.const `A.nil []))
-  (Lean.Expr.app (Lean.Expr.const `B.cons₁ []) (Lean.Expr.const `A.nil []))
--/
-#guard_msgs in
-#eval repr <| toExpr <| B.cons₂ A.nil (B.cons₁ A.nil)
-
-/-!
-Test with explicit universe level
--/
-
-inductive WithUniverse.{u} (α : Type u)
-  | foo (a : α)
-  deriving ToExpr
-
-/-!
-Test with universe level coming from `universe` command
--/
-universe u in
-inductive WithAmbientUniverse (α : Type u)
-  | foo (a : α)
-  deriving ToExpr
-
-/-!
-Test with an ambient universe `u`, a directly specified universe `v`, and an implicit universe `w`.
--/
-universe u in
-structure WithAmbientUniverseTriple.{v} (α : Type u) (β : Type v) (γ : Type w) where
-  a : α
-  b : β
-  c : γ
-  deriving ToExpr
-
-/-!
-Test using the `variable` command, with an autoimplicit universe.
--/
-variable (α : Type u) in
-inductive VariableParameter : Type u
-  | foo (a : α)
-  deriving ToExpr
-
-/-!
-Mutual inductive with universe levels.
--/
-mutual
-inductive A' (α : Type u) where
-  | mk (x : α) (a : A' α) (b : B' α)
-  deriving ToExpr
-inductive B' (α : Type u) where
-  | mk (x : α) (a : A' α) (b : B' α)
-  deriving ToExpr
-end
-
-/-!
-Nested with universe level.
--/
-inductive Foo' (α : Type u)
-  | l (x : α) (x : List (Foo' α))
-  deriving ToExpr
-
-/-!
-### Tests with without universe autoimplicits.
--/
-section NoAutoImplicit
-set_option autoImplicit false
-
-/-!
-Test with universe specified directly on the type
--/
-inductive ExplicitList'.{u} (α : Type u)
-  | cons (a : α) (as : List' α)
-  | nil
-  deriving ToExpr
-
-/-!
-Test with ambient (explicit) universe
--/
-universe u in
-inductive AmbientList' (α : Type u)
-  | cons (a : α) (as : List' α)
-  | nil
-  deriving ToExpr
-
-/-!
-Test with both ambient and directly specified universes.
--/
-universe u in
-structure ExplicitAmbientPair.{v} (α : Type u) (β : Type v) where
-  a : α
-  b : β
-  deriving ToExpr
-
-end NoAutoImplicit

tests/lean/run/grind_congr.lean

@@ -13,7 +13,6 @@ elab "grind_test" : tactic => withMainContext do
     logInfo eqc
 
 set_option grind.debug true
-set_option grind.debug.proofs true
 
 /--
 info: [d, f b, c, f a]

tests/lean/run/grind_congr1.lean

@@ -1,97 +0,0 @@
-set_option warningAsError false
-set_option grind.debug true
-set_option grind.debug.proofs true
-
-example (a b : Nat) (f : Nat → Nat) : (h₁ : a = b) → f a = f b := by
-  grind
-
-example (a b : Nat) (f : Nat → Nat) : (h₁ : a = b) → (h₂ : f a ≠ f b) → False := by
-  grind
-
-example (a b : Nat) (f : Nat → Nat) : a = b → f (f a) ≠ f (f b) → False := by
-  grind
-
-example (a b c : Nat) (f : Nat → Nat) : a = b → c = b → f (f a) ≠ f (f c) → False := by
-  grind
-
-example (a b c : Nat) (f : Nat → Nat → Nat) : a = b → c = b → f (f a b) a ≠ f (f c c) c → False := by
-  grind
-
-example (a b c : Nat) (f : Nat → Nat → Nat) : a = b → c = b → f (f a b) a = f (f c c) c := by
-  grind
-
-example (a b c d : Nat) : a = b → b = c → c = d → a = d := by
-  grind
-
-infix:50 "===" => HEq
-
-example (a b c d : Nat) : a === b → b = c → c === d → a === d := by
-  grind
-
-example (a b c d : Nat) : a = b → b = c → c === d → a === d := by
-  grind
-
-opaque f {α : Type} : α → α → α := fun a _ => a
-opaque g : Nat → Nat
-
-example (a b c : Nat) : a = b → g a === g b := by
-  grind
-
-example (a b c : Nat) : a = b → c = b → f (f a b) (g c) = f (f c a) (g b) := by
-  grind
-
-example (a b c d e x y : Nat) : a = b → a = x → b = y → c = d → c = e → c = b → a = e := by
-  grind
-
-namespace Ex1
-opaque f (a b : Nat) : a > b → Nat
-opaque g : Nat → Nat
-
-example (a₁ a₂ b₁ b₂ c d : Nat)
-        (H₁ : a₁ > b₁)
-        (H₂ : a₂ > b₂) :
-        a₁ = c → a₂ = c →
-        b₁ = d → d  = b₂ →
-        g (g (f a₁ b₁ H₁)) = g (g (f a₂ b₂ H₂)) := by
-  grind
-end Ex1
-
-namespace Ex2
-def f (α : Type) (a : α) : α := a
-
-example (a : α) (b : β) : (h₁ : α = β) → (h₂ : HEq a b) → HEq (f α a) (f β b) := by
-  grind
-
-end Ex2
-
-example (f g : (α : Type) → α → α) (a : α) (b : β) : (h₁ : α = β) → (h₂ : HEq a b) → (h₃ : f = g) → HEq (f α a) (g β b) := by
-  grind
-
-set_option trace.grind.debug.proof true in
-example (f : {α : Type} → α → Nat → Bool → Nat) (a b : Nat) : f a 0 true = v₁ → f b 0 true = v₂ → a = b → v₁ = v₂ := by
-  grind
-
-set_option trace.grind.debug.proof true in
-example (f : {α : Type} → α → Nat → Bool → Nat) (a b : Nat) : f a b x = v₁ → f a b y = v₂ → x = y → v₁ = v₂ := by
-  grind
-
-set_option trace.grind.debug.proof true in
-theorem ex1 (f : {α : Type} → α → Nat → Bool → Nat) (a b c : Nat) : f a b x = v₁ → f c b y = v₂ → a = c → x = y → v₁ = v₂ := by
-  grind
-
-#print ex1
-
-
-example (n1 n2 n3 : Nat) (v1 w1 : Vector Nat n1) (w1' : Vector Nat n3) (v2 w2 : Vector Nat n2) :
-        n1 = n3 → v1 = w1 → HEq w1 w1' → v2 = w2 → HEq (v1 ++ v2) (w1' ++ w2) := by
-  grind
-
-example (n1 n2 n3 : Nat) (v1 w1 : Vector Nat n1) (w1' : Vector Nat n3) (v2 w2 : Vector Nat n2) :
-        HEq n1 n3 → v1 = w1 → HEq w1 w1' → HEq v2 w2 → HEq (v1 ++ v2) (w1' ++ w2) := by
-  grind
-
-theorem ex2 (n1 n2 n3 : Nat) (v1 w1 v : Vector Nat n1) (w1' : Vector Nat n3) (v2 w2 w : Vector Nat n2) :
-        HEq n1 n3 → v1 = w1 → HEq w1 w1' → HEq v2 w2 → HEq (w1' ++ w2) (v ++ w) → HEq (v1 ++ v2) (v ++ w) := by
-  grind
-
-#print ex2

tests/lean/run/grind_ematch1.lean

@@ -1,62 +0,0 @@
-set_option trace.grind.ematch.pattern true
-grind_pattern Array.get_set_eq  => a.set i v h
-grind_pattern Array.get_set_ne => (a.set i v hi)[j]
-
--- Trace instances of the theorems above found using ematching
-
-set_option trace.grind.ematch.instance true
-
-set_option grind.debug.proofs true
-
-/--
-info: [grind.ematch.instance] Array.get_set_eq: (bs.set j w ⋯)[j] = w
-[grind.ematch.instance] Array.get_set_eq: (as.set i v ⋯)[i] = v
--/
-#guard_msgs (info) in
-example (as : Array α)
-        (i : Nat)
-        (h₁ : i < as.size)
-        (h₂ : bs = as.set i v)
-        (_  : ds = bs)
-        (h₂ : j < bs.size)
-        (h₃ : cs = bs.set j w)
-        (h₄ : i ≠ j)
-        (h₅ : i < cs.size)
-        : p ↔ (cs[i] = as[i]) := by
-  fail_if_success grind
-  sorry
-
-opaque R : Nat → Nat → Prop
-theorem Rtrans (a b c : Nat) : R a b → R b c → R a c := sorry
-
-grind_pattern Rtrans => R a b, R b c
-
-/--
-info: [grind.ematch.instance] Rtrans: R b c → R c d → R b d
-[grind.ematch.instance] Rtrans: R a b → R b c → R a c
--/
-#guard_msgs (info) in
-example : R a b → R b c → R c d → False := by
-  fail_if_success grind
-  sorry
-
--- In the following test we are performing one round of ematching only
-/--
-info: [grind.ematch.instance] Rtrans: R c d → R d e → R c e
-[grind.ematch.instance] Rtrans: R c d → R d n → R c n
-[grind.ematch.instance] Rtrans: R b c → R c d → R b d
-[grind.ematch.instance] Rtrans: R a b → R b c → R a c
--/
-#guard_msgs (info) in
-example : R a b → R b c → R c d → R d e → R d n → False := by
-  fail_if_success grind
-  sorry
-
-/--
-info: [grind.ematch.instance] Rtrans: R c d → R d e → R c e
-[grind.ematch.instance] Rtrans: R c d → R d n → R c n
--/
-#guard_msgs (info) in
-example : R a b → R b c → R c d → R d e → R d n → False := by
-  fail_if_success grind (instances := 2)
-  sorry

tests/lean/run/grind_nested_proofs.lean

@@ -13,7 +13,6 @@ elab "grind_test" : tactic => withMainContext do
     logInfo (← getEqc n.self)
 
 set_option grind.debug true
-set_option grind.debug.proofs true
 
 /-
 Recall that array access terms, such as `a[i]`, have nested proofs.

tests/lean/run/grind_pattern1.lean

@@ -1,114 +0,0 @@
-set_option trace.grind.ematch.pattern true
-
-/--
-info: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem ? `[Nat] #4 ? ? (@Array.push ? #3 #2) #1 ?]
--/
-#guard_msgs in
-grind_pattern Array.getElem_push_lt => (a.push x)[i]
-
-
-/-- info: [grind.ematch.pattern] List.getElem_attach: [@getElem ? `[Nat] ? ? ? (@List.attach #3 #2) #1 ?] -/
-#guard_msgs in
-grind_pattern List.getElem_attach => xs.attach[i]
-
-/--
-info: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 ? ? (@HAppend.hAppend ? ? ? ? #1 (@List.cons ? #0 (@List.nil ?))) #0]
--/
-#guard_msgs in
-grind_pattern List.mem_concat_self => a ∈ xs ++ [a]
-
-def foo (x : Nat) := x + x
-
-/--
-error: `foo` is not a theorem, you cannot assign patterns to non-theorems for the `grind` tactic
--/
-#guard_msgs in
-grind_pattern foo => x + x
-
-/--
-error: invalid pattern(s) for `Array.getElem_push_lt`
-  [@Array.push #4 #3 #2]
-the following theorem parameters cannot be instantiated:
-  i : Nat
-  h : i < a.size
----
-info: [grind.ematch.pattern] Array.getElem_push_lt: [@Array.push #4 #3 #2]
--/
-#guard_msgs in
-grind_pattern Array.getElem_push_lt => (a.push x)
-
-class Foo (α : Type) (β : outParam Type) where
-  a : Unit
-
-class Boo (α : Type) (β : Type) where
-  b : β
-
-def f [Foo α β] [Boo α β] (a : α) : (α × β) :=
-  (a, Boo.b α)
-
-instance [Foo α β] : Foo (List α) (Array β) where
-  a := ()
-
-instance [Boo α β] : Boo (List α) (Array β) where
-  b := #[Boo.b α]
-
-theorem fEq [Foo α β] [Boo α β] (a : List α) : (f a).1 = a := rfl
-
-/-- info: [grind.ematch.pattern] fEq: [@f ? ? ? ? #0] -/
-#guard_msgs in
-grind_pattern fEq => f a
-
-theorem fEq2 [Foo α β] [Boo α β] (a : List α) (_h : a.length > 5) : (f a).1 = a := rfl
-
-/-- info: [grind.ematch.pattern] fEq2: [@f ? ? ? ? #1] -/
-#guard_msgs in
-grind_pattern fEq2 => f a
-
-def g [Boo α β] (a : α) : (α × β) :=
-  (a, Boo.b α)
-
-theorem gEq [Boo α β] (a : List α) : (g (β := Array β) a).1 = a := rfl
-
-/--
-error: invalid pattern(s) for `gEq`
-  [@g ? ? ? #0]
-the following theorem parameters cannot be instantiated:
-  β : Type
-  inst✝ : Boo α β
----
-info: [grind.ematch.pattern] gEq: [@g ? ? ? #0]
--/
-#guard_msgs in
-grind_pattern gEq => g a
-
-def plus (a : Nat) (b : Nat) := a + b
-
-theorem hThm1 (h : b > 10) : plus a b + plus a c > 10 := by
-  unfold plus; omega
-
-/--
-error: invalid pattern(s) for `hThm1`
-  [plus #2 #3]
-the following theorem parameters cannot be instantiated:
-  c : Nat
----
-info: [grind.ematch.pattern] hThm1: [plus #2 #3]
--/
-#guard_msgs in
-grind_pattern hThm1 => plus a b
-
-/--
-error: invalid pattern(s) for `hThm1`
-  [plus #2 #1]
-the following theorem parameters cannot be instantiated:
-  b : Nat
-  h : b > 10
----
-info: [grind.ematch.pattern] hThm1: [plus #2 #1]
--/
-#guard_msgs in
-grind_pattern hThm1 => plus a c
-
-/-- info: [grind.ematch.pattern] hThm1: [plus #2 #1, plus #2 #3] -/
-#guard_msgs in
-grind_pattern hThm1 => plus a c, plus a b

tests/lean/run/grind_pattern2.lean

@@ -1,81 +0,0 @@
-def Set (α : Type) := α → Bool
-
-def insertElem [DecidableEq α] (s : Set α) (a : α) : Set α :=
-  fun x => a = x || s x
-
-def contains (s : Set α) (a : α) : Bool :=
-  s a
-
-theorem contains_insert [DecidableEq α] (s : Set α) (a : α) : contains (insertElem s a) a := by
-  simp [contains, insertElem]
-
-grind_pattern contains_insert => contains (insertElem s a) a
-
--- TheoremPattern activation test
-
-set_option trace.grind.ematch true
-set_option trace.grind.ematch.pattern true
-
-/--
-warning: declaration uses 'sorry'
----
-info: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem ? #2 #1 #0) #0]
--/
-#guard_msgs in
-example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
-        s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by
-  fail_if_success grind
-  sorry
-
-/--
-warning: declaration uses 'sorry'
----
-info: [grind.ematch] reinsert `contains_insert`
-[grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem ? #2 #1 #0) #0]
--/
-#guard_msgs in
-example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
-        ¬ contains s₂ a₂ → s₂ = insertElem s₁ a₁ → a₁ = a₂ → False := by
-  fail_if_success grind
-  sorry
-
-def a := 10
-def b := 20
-def foo (x : List Nat) (y : List Nat) := x ++ y ++ x
-
-theorem fooThm : foo x [a, b] = x ++ [a, b] ++ x := rfl
-
-/-- info: [grind.ematch.pattern] fooThm: [foo #0 `[[a, b]]] -/
-#guard_msgs in
-grind_pattern fooThm => foo x [a, b]
-
-
-/--
-warning: declaration uses 'sorry'
----
-info: [grind.internalize] foo x y
-[grind.internalize] [a, b]
-[grind.internalize] Nat
-[grind.internalize] a
-[grind.internalize] [b]
-[grind.internalize] b
-[grind.internalize] []
-[grind.ematch] activated `fooThm`, [foo #0 `[[a, b]]]
-[grind.internalize] x
-[grind.internalize] y
-[grind.internalize] z
--/
-#guard_msgs in
-set_option trace.grind.internalize true in
-example : foo x y = z → False := by
-  fail_if_success grind
-  sorry
-
-theorem arrEx [Add α] (as : Array α) (h₁ : i < as.size) (h₂ : i = j) : as[i]+as[j] = as[i] + as[i] := by sorry
-
-
-/--
-info: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 ? ? ? (@getElem ? `[Nat] ? ? ? #2 #5 ?) (@getElem ? `[Nat] ? ? ? #2 #4 ?)]
--/
-#guard_msgs in
-grind_pattern arrEx => as[i]+as[j]'(h₂▸h₁)

tests/lean/run/grind_pre.lean

@@ -1,11 +1,19 @@
+import Lean
+
+open Lean Meta Elab Tactic Grind in
+elab "grind_pre" : tactic => do
+  let declName := (← Term.getDeclName?).getD `_main
+  liftMetaTactic fun mvarId => do
+    Meta.Grind.main mvarId declName
+
 abbrev f (a : α) := a
 
 set_option grind.debug true
-set_option grind.debug.proofs true
 
 /--
-error: `grind` failed
-a b c : Bool
+warning: declaration uses 'sorry'
+---
+info: a b c : Bool
 p q : Prop
 left✝ : a = true
 right✝ : b = true ∨ c = true
@@ -14,13 +22,34 @@ right : q
 x✝ : b = false ∨ a = false
 ⊢ False
 -/
-#guard_msgs (error) in
+#guard_msgs in
 theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
-  grind
+  grind_pre
+  trace_state
+  all_goals sorry
 
 open Lean.Grind.Eager in
 /--
-error: `grind` failed
+warning: declaration uses 'sorry'
+---
+info: a b c : Bool
+p q : Prop
+left✝ : a = true
+h✝ : b = true
+left : p
+right : q
+h : b = false
+⊢ False
+
+a b c : Bool
+p q : Prop
+left✝ : a = true
+h✝ : b = true
+left : p
+right : q
+h : a = false
+⊢ False
+
 a b c : Bool
 p q : Prop
 left✝ : a = true
@@ -29,32 +58,39 @@ left : p
 right : q
 h : b = false
 ⊢ False
+
+a b c : Bool
+p q : Prop
+left✝ : a = true
+h✝ : c = true
+left : p
+right : q
+h : a = false
+⊢ False
 -/
-#guard_msgs (error) in
+#guard_msgs in
 theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
-  grind
+  grind_pre
+  trace_state
+  all_goals sorry
+
 
 def g (i : Nat) (j : Nat) (_ : i > j := by omega) := i + j
 
-/--
-error: `grind` failed
-i j : Nat
-h : j + 1 < i + 1
-h✝ : j + 1 ≤ i
-x✝ : ¬g (i + 1) j ⋯ = i + j + 1
-⊢ False
--/
-#guard_msgs (error) in
 example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by
-  grind
+  grind_pre
+  next hn =>
+  guard_hyp hn : ¬g (i + 1) j _ = i + j + 1
+  simp_arith [g] at hn
 
 structure Point where
   x : Nat
   y : Int
 
 /--
-error: `grind` failed
-a₁ : Point
+warning: declaration uses 'sorry'
+---
+info: a₁ : Point
 a₂ : Nat
 a₃ : Int
 as : List Point
@@ -68,51 +104,15 @@ y_eq : a₃ = b₃
 tail_eq : as = bs
 ⊢ False
 -/
-#guard_msgs (error) in
+#guard_msgs in
 theorem ex3 (h : a₁ :: { x := a₂, y := a₃ : Point } :: as = b₁ :: { x := b₂, y := b₃} :: bs) : False := by
-  grind
+  grind_pre
+  trace_state
+  sorry
 
 def h (a : α) := a
 
-set_option trace.grind.debug.pre true in
-example (p : Prop) (a b c : Nat) : p → a = 0 → a = b → h a = h c → a = c ∧ c = a → a = b ∧ b = a → a = c := by
-  grind
-
-set_option trace.grind.debug.proof true
-set_option trace.grind.debug.pre true
-/--
-error: `grind` failed
-α : Type
-a : α
-p q r : Prop
-h₁ : HEq p a
-h₂ : HEq q a
-h₃ : p = r
-⊢ False
--/
-#guard_msgs (error) in
-example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by
-  grind
-
-example (a b : Nat) (f : Nat → Nat) : (h₁ : a = b) → (h₂ : f a ≠ f b) → False := by
-  grind
-
-example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → q = r := by
-  grind
-
-/--
-warning: declaration uses 'sorry'
----
-info: [grind.issues] found congruence between
-      g b
-    and
-      f a
-    but functions have different types
--/
-#guard_msgs in
-set_option trace.grind.issues true in
-set_option trace.grind.debug.proof false in
-set_option trace.grind.debug.pre false in
-example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by
-  fail_if_success grind
+set_option trace.grind.pre true
+example (p : Prop) (a b c : Nat) : p → a = 0 → a = b → h a = h c → a = c ∧ c = a → a = b ∧ b = a → a ≠ c := by
+  grind_pre
   sorry

tests/lean/run/grind_propagate_connectives.lean

@@ -15,7 +15,6 @@ elab "grind_test" : tactic => withMainContext do
         logInfo eqc
 
 set_option grind.debug true
-set_option grind.debug.proofs true
 
 /--
 info: true:  [q, w]