feat: add appMap field to Goal

Update modification time.

src/Init/Grind.lean

@@ -9,3 +9,4 @@ 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,6 +7,7 @@ prelude
 import Init.Core
 import Init.SimpLemmas
 import Init.Classical
+import Init.ByCases
 
 namespace Lean.Grind
 
@@ -41,6 +42,9 @@ 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

@@ -19,7 +19,15 @@ structure Config where
   eager : Bool := false
   deriving Inhabited, BEq
 
+end Lean.Grind
+
+namespace Lean.Parser.Tactic
+
 /-!
 `grind` tactic and related tactics.
 -/
-end Lean.Grind
+
+-- TODO: configuration option, parameters
+syntax (name := grind) "grind" : tactic
+
+end Lean.Parser.Tactic

src/Init/Grind/Util.lean

@@ -11,4 +11,9 @@ 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/Tactic.lean

@@ -44,3 +44,4 @@ 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
-    | .imp => mkConst ``Gate.imp
+    | .or => mkConst ``Gate.or
   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
-    | .imp => ``Std.Tactic.BVDecide.Reflect.Bool.imp_congr
+    | .or => ``Std.Tactic.BVDecide.Reflect.Bool.or_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.ite_congr)
+      (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.cond_congr)
       discrExpr lhsExpr rhsExpr
       discrEvalExpr lhsEvalExpr rhsEvalExpr
       discrProof lhsProof rhsProof

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

@@ -22,67 +22,70 @@ 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
-`if discrExpr = true then lhsExpr else rhsExpr`.
+`bif discrExpr then lhsExpr else rhsExpr`.
 -/
-def addIfLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+def addCondLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
     (discrExpr atomExpr lhsExpr rhsExpr : Expr) : LemmaM Unit := do
-  let some trueLemma ← mkIfTrueLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  let some trueLemma ← mkCondTrueLemma discr atom lhs discrExpr atomExpr lhsExpr rhsExpr | return ()
   LemmaM.addLemma trueLemma
-  let some falseLemma ← mkIfFalseLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  let some falseLemma ← mkCondFalseLemma discr atom rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
   LemmaM.addLemma falseLemma
 where
-  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)
+  mkCondTrueLemma (discr : ReifiedBVLogical) (atom lhs : ReifiedBVExpr)
       (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
-    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 resExpr := lhsExpr
+    let resValExpr := lhs
+    let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_true
 
-    let eqDiscrExpr ← mkAppM ``BEq.beq #[discrExpr, discrValExpr]
-    let eqDiscr ← ReifiedBVLogical.mkGate discr discrVal discrExpr discrValExpr .beq
+
+    let notDiscrExpr := mkApp (mkConst ``Bool.not) discrExpr
+    let notDiscr ← ReifiedBVLogical.mkNot discr discrExpr
 
     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 eqDiscr eqBV eqDiscrExpr eqBVExpr .imp
+    let imp ← ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr 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 lhs.width) discrExpr lhsExpr rhsExpr
 
-      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
+      -- !discr || (atom == rhs)
+      let impExpr := mkApp2 (mkConst ``Bool.or) notDiscrExpr eqBVExpr
 
       return mkApp4
         (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
-        decideImpExpr
+        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
         evalExpr
         congrProof
         lemmaProof

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

@@ -220,15 +220,12 @@ where
         .rotateRight
         ``BVUnOp.rotateRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
-    | ite _ discrExpr _ lhsExpr rhsExpr =>
-      let_expr Eq α discrExpr val := discrExpr | return none
-      let_expr Bool := α | return none
-      let_expr Bool.true := val | return none
+    | cond _ discrExpr lhsExpr rhsExpr =>
       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
-      addIfLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
+      addCondLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
       return some atom
     | _ => return none
 
@@ -392,10 +389,7 @@ where
       | Bool => gateReflection lhsExpr rhsExpr .beq
       | BitVec _ => goPred t
       | _ => return none
-    | ite _ discrExpr _ lhsExpr rhsExpr =>
-      let_expr Eq α discrExpr val := discrExpr | return none
-      let_expr Bool := α | return none
-      let_expr Bool.true := val | return none
+    | cond _ discrExpr lhsExpr rhsExpr =>
       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,6 +28,18 @@ 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
@@ -127,8 +139,6 @@ 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

@@ -0,0 +1,27 @@
+/-
+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.Tactic.Basic
+
+namespace Lean.Elab.Tactic
+open Meta
+
+def grind (mvarId : MVarId) (mainDeclName : Name) : MetaM Unit := do
+  let mvarIds ← Grind.main mvarId 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) =>
+    logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
+    let declName := (← Term.getDeclName?).getD `_grind
+    withMainContext do liftMetaFinishingTactic (grind · declName)
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic

src/Lean/Expr.lean

@@ -1648,6 +1648,23 @@ 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,6 +176,14 @@ 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/Tactic/Grind.lean

@@ -19,6 +19,7 @@ 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
 
 namespace Lean
 
@@ -28,7 +29,10 @@ builtin_initialize registerTraceClass `grind.issues
 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.simp
 builtin_initialize registerTraceClass `grind.congr
+builtin_initialize registerTraceClass `grind.proof
+builtin_initialize registerTraceClass `grind.proof.detail
 
 end Lean

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

@@ -9,58 +9,11 @@ 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
@@ -81,9 +34,6 @@ 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.
@@ -102,6 +52,35 @@ 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
@@ -113,9 +92,11 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
   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)
@@ -124,7 +105,14 @@ 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
-  -- TODO: propagate value inconsistency
+  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
   trace[grind.debug] "after addEqStep, {← ppState}"
   checkInvariants
 where
@@ -145,7 +133,6 @@ 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
@@ -162,10 +149,11 @@ 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

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

@@ -0,0 +1,49 @@
+/-
+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/Internalize.lean

@@ -0,0 +1,78 @@
+/-
+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
+
+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.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]
+  }
+
+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
+      updateAppMap e
+      propagateUp e
+
+end Lean.Meta.Grind

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Proof
 
 namespace Lean.Meta.Grind
 
@@ -19,6 +20,16 @@ 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
@@ -38,13 +49,16 @@ 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 let some argRoot ← getRoot? arg then
-          if isSameExpr argRoot e then
-            found := true
-            break
-      assert! found
+        if (← checkChild arg) then
+          found := true
+          break
+      unless found do
+        assert! (← checkChild parent.getAppFn)
   else
     -- All the parents are stored in the root of the equivalence class.
     assert! (← getParents e).isEmpty
@@ -54,12 +68,23 @@ 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[i]
+      let n₂ := nodes[j]
       -- 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.
 -/
@@ -71,5 +96,7 @@ 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,27 +14,6 @@ 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/Preprocessor.lean

@@ -17,6 +17,7 @@ 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
 
 namespace Lean.Meta.Grind
 namespace Preprocessor
@@ -98,6 +99,8 @@ 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
@@ -160,7 +163,10 @@ def preprocess (mvarId : MVarId) (mainDeclName : Name) : MetaM Preprocessor.Stat
   Preprocessor.preprocess mvarId |>.run |>.run mainDeclName
 
 def main (mvarId : MVarId) (mainDeclName : Name) : MetaM (List MVarId) := do
-  let s ← preprocess mvarId mainDeclName
-  return s.goals.toList.map (·.mvarId)
+  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
 
 end Lean.Meta.Grind

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

@@ -0,0 +1,35 @@
+/-
+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 ()
+  let arg := parent.appArg!
+  let ctor ← getRoot arg
+  unless ctor.isAppOf info.ctorName do return ()
+  if isSameExpr arg ctor then
+    let idx := info.numParams + info.i
+    unless idx < ctor.getAppNumArgs do return ()
+    let v := ctor.getArg! idx
+    pushEq parent v (← mkEqRefl v)
+  else
+    let newProj := mkApp parent.appFn! ctor
+    let newProj ← shareCommon newProj
+    internalize newProj (← getGeneration parent)
+
+end Lean.Meta.Grind

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

@@ -9,29 +9,231 @@ 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.
 -/
-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)
+@[export lean_grind_mk_eq_proof]
+def mkEqProofImpl (a b : Expr) : GoalM Expr := do
+  let p ← go
+  trace[grind.proof.detail] "{p}"
+  return p
+where
+  go : GoalM Expr := do
+    let n ← getRootENode a
+    if !n.heqProofs then
+      trace[grind.proof] "{a} = {b}"
+      mkEqProofCore a b (heq := false)
+    else
+      if (← hasSameType a b) then
+        trace[grind.proof] "{a} = {b}"
+        mkEqOfHEq (← mkEqProofCore a b (heq := true))
+      else
+        trace[grind.proof] "{a} ≡ {b}"
+        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)
+def mkHEqProof (a b : Expr) : GoalM Expr :=
+  mkEqProofCore a b (heq := true)
 
 end Lean.Meta.Grind

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind
 import Lean.Meta.Tactic.Grind.Proof
+import Lean.Meta.Tactic.Grind.PropagatorAttr
 
 namespace Lean.Meta.Grind
 
@@ -105,12 +106,13 @@ 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
@@ -120,7 +122,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 ``of_eq_true) e (← mkEqProof a b)
+    pushEqTrue e <| mkApp2 (mkConst ``eq_true) e (← mkEqProof a b)
 
 /-- Propagates `Eq` downwards -/
 builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
@@ -134,4 +136,10 @@ 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

@@ -0,0 +1,61 @@
+/-
+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

@@ -0,0 +1,53 @@
+/-
+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) : 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/Grind/Types.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Util.ShareCommon
+import Lean.HeadIndex
 import Lean.Meta.Basic
 import Lean.Meta.CongrTheorems
 import Lean.Meta.AbstractNestedProofs
@@ -20,6 +21,9 @@ 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.
@@ -34,6 +38,12 @@ 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
@@ -249,6 +259,12 @@ structure Goal where
   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. -/
@@ -266,10 +282,6 @@ abbrev GoalM := StateRefT Goal GrindM
 
 abbrev Propagator := Expr → GoalM Unit
 
-/-- 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 :=
   return isSameExpr e (← getTrueExpr)
@@ -291,6 +303,10 @@ def getENode (e : Expr) : GoalM ENode := do
     | 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
@@ -303,9 +319,12 @@ 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
-  let na ← getENode a
-  let nb ← getENode b
-  return isSameExpr na.root nb.root
+  if isSameExpr a b then
+    return true
+  else
+    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
@@ -321,6 +340,10 @@ 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
@@ -340,8 +363,12 @@ 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 (← isDefEq (← inferType lhs) (← inferType rhs)) then
+  if (← hasSameType lhs rhs) then
     pushEqCore lhs rhs proof (isHEq := false)
   else
     pushEqCore lhs rhs proof (isHEq := true)
@@ -428,6 +455,50 @@ def mkENode (e : Expr) (generation : Nat) : GoalM Unit := do
   let interpreted ← isInterpreted e
   mkENodeCore e interpreted ctor generation
 
+/-- 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`
@@ -452,12 +523,12 @@ def forEachEqc (f : ENode → GoalM Unit) : GoalM Unit := do
     if isSameExpr n.self n.root then
       f n
 
-private structure Methods where
+structure Methods where
   propagateUp   : Propagator := fun _ => return ()
   propagateDown : Propagator := fun _ => return ()
   deriving Inhabited
 
-private def Methods.toMethodsRef (m : Methods) : MethodsRef :=
+def Methods.toMethodsRef (m : Methods) : MethodsRef :=
   unsafe unsafeCast m
 
 private def MethodsRef.toMethods (m : MethodsRef) : Methods :=
@@ -472,91 +543,25 @@ def propagateUp (e : Expr) : GoalM Unit := do
 def propagateDown (e : Expr) : GoalM Unit := do
   (← getMethods).propagateDown e
 
-/-- 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
+/-- 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
-      ``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' {}
+      go first next acc
 
-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)
+/-- 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
 
 end Lean.Meta.Grind

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

@@ -49,17 +49,13 @@ If they do, they must disable the following `simprocs`.
 -/
 
 builtin_dsimproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
-  unless e.isAppOfArity ``Neg.neg 3 do return .continue
-  let arg := e.appArg!
+  let_expr Neg.neg _ _ arg ← e | return .continue
   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
-    if v < 0 then
-      return .done <| toExpr (- v)
-    else
-      return .done <| toExpr v
+    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/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -293,8 +293,15 @@ The semantics for `BVExpr`.
 -/
 def eval (assign : Assignment) : BVExpr w → BitVec w
   | .var idx =>
-    let ⟨bv⟩ := assign.get idx
-    bv.truncate w
+    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
   | .const val => val
   | .zeroExtend v expr => BitVec.zeroExtend v (eval assign expr)
   | .extract start len expr => BitVec.extractLsb' start len (eval assign expr)
@@ -308,8 +315,13 @@ 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 _ := by
-  rfl
+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
 
 @[simp]
 theorem eval_const : eval assign (.const val) = val := by rfl
@@ -454,7 +466,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) = if (eval assign d) then (eval assign l) else (eval assign r) := rfl
+  eval assign (.ite d l r) = bif (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
-  | imp
+  | or
 
 namespace Gate
 
@@ -26,13 +26,13 @@ def toString : Gate → String
   | and => "&&"
   | xor => "^^"
   | beq => "=="
-  | imp => "->"
+  | or => "||"
 
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
   | xor => (· ^^ ·)
   | beq => (· == ·)
-  | imp => (· → ·)
+  | or => (· || ·)
 
 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 => if d.eval a then l.eval a else r.eval a
+  | .ite d l r => bif 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) = if d.eval a then l.eval a else r.eval a := rfl
+@[simp] theorem eval_ite : eval a (.ite d l r) = bif 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⟩
-      | .imp =>
-        let ret := aig.mkImpCached input
-        have := LawfulOperator.le_size (f := mkImpCached) aig input
+      | .or =>
+        let ret := aig.mkOrCached input
+        have := LawfulOperator.le_size (f := mkOrCached) 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]
-    | imp =>
+    | or =>
       simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkImpCached), rih, lih]
+      rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), 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,7 +118,6 @@ 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,7 +41,14 @@ 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] ite_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]
 
 @[bv_normalize]
 theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide

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

@@ -13,8 +13,6 @@ 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 if_true (discr : Bool) (lhs rhs : BitVec w) :
-    decide ((discr == true) = true → ((if discr = true then lhs else rhs) == lhs) = true) = true := by
+theorem cond_true (discr : Bool) (lhs rhs : BitVec w) :
+    (!discr || ((bif discr then lhs else rhs) == lhs)) = true := by
   cases discr <;> simp
 
-theorem if_false (discr : Bool) (lhs rhs : BitVec w) :
-    decide ((discr == false) = true → ((if discr = true then lhs else rhs) == rhs) = true) = true := by
+theorem cond_false (discr : Bool) (lhs rhs : BitVec w) :
+    (discr || ((bif discr then lhs else rhs) == rhs)) = 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 imp_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (decide (lhs' → rhs')) = (decide (lhs → rhs)) := by
+theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
+    (lhs' || rhs') = (lhs || rhs) := by
   simp[*]
 
-theorem ite_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
+theorem cond_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
     (h3 : rhs' = rhs) :
-    (if discr' = true then lhs' else rhs') = (if discr = true then lhs else rhs) := by
+    (bif discr' = true then lhs' else rhs') = (bif 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

@@ -0,0 +1,6 @@
+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

@@ -0,0 +1,16 @@
+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,6 +85,7 @@ 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,17 +23,8 @@ 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 (a : Bool) (b c : BitVec 32) (h1 : b < c ↔ a) (h2 : a = true) : b < c := by
+theorem substructure_unit_5 (x : BitVec 32) : (if x.getLsbD 0 then !x.getLsbD 0 else x.getLsbD 0) = false := by
   bv_decide
 
-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
+theorem substructure_unit_6 (x y : BitVec 32) (h : x.getLsbD 0 = false) : (if x.getLsbD 0 then x else y) = y := by
   bv_decide

tests/lean/run/grind_congr.lean

@@ -13,6 +13,7 @@ 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

@@ -0,0 +1,100 @@
+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.proof true in
+set_option trace.grind.proof.detail 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.proof true in
+set_option trace.grind.proof.detail 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.proof true in
+set_option trace.grind.proof.detail 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_nested_proofs.lean

@@ -13,6 +13,7 @@ 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_pre.lean

@@ -1,19 +1,11 @@
-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
 
 /--
-warning: declaration uses 'sorry'
----
-info: a b c : Bool
+error: `grind` failed
+a b c : Bool
 p q : Prop
 left✝ : a = true
 right✝ : b = true ∨ c = true
@@ -22,34 +14,13 @@ right : q
 x✝ : b = false ∨ a = false
 ⊢ False
 -/
-#guard_msgs in
+#guard_msgs (error) in
 theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
-  grind_pre
-  trace_state
-  all_goals sorry
+  grind
 
 open Lean.Grind.Eager in
 /--
-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
-
+error: `grind` failed
 a b c : Bool
 p q : Prop
 left✝ : a = true
@@ -58,39 +29,32 @@ 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 in
+#guard_msgs (error) in
 theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
-  grind_pre
-  trace_state
-  all_goals sorry
-
+  grind
 
 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_pre
-  next hn =>
-  guard_hyp hn : ¬g (i + 1) j _ = i + j + 1
-  simp_arith [g] at hn
+  grind
 
 structure Point where
   x : Nat
   y : Int
 
 /--
-warning: declaration uses 'sorry'
----
-info: a₁ : Point
+error: `grind` failed
+a₁ : Point
 a₂ : Nat
 a₃ : Int
 as : List Point
@@ -104,15 +68,53 @@ y_eq : a₃ = b₃
 tail_eq : as = bs
 ⊢ False
 -/
-#guard_msgs in
+#guard_msgs (error) in
 theorem ex3 (h : a₁ :: { x := a₂, y := a₃ : Point } :: as = b₁ :: { x := b₂, y := b₃} :: bs) : False := by
-  grind_pre
-  trace_state
-  sorry
+  grind
 
 def h (a : α) := a
 
+set_option trace.grind.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.proof.detail true
+set_option trace.grind.proof true
 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
+/--
+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.proof.detail false in
+set_option trace.grind.proof false in
+set_option trace.grind.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
   sorry

tests/lean/run/grind_propagate_connectives.lean

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

tests/lean/run/grind_t1.lean

@@ -0,0 +1,77 @@
+example (a b : List Nat) : a = [] → b = [2] → a = b → False := by
+  grind
+
+example (a b : List Nat) : a = b → a = [] → b = [2] → False := by
+  grind
+
+example (a b : Bool) : a = true → b = false → a = b → False := by
+  grind
+
+example (a b : Sum Nat Bool) : a = .inl c → b = .inr true → a = b → False := by
+  grind
+
+example (a b : Sum Nat Bool) : a = b → a = .inl c → b = .inr true → a = b → False := by
+  grind
+
+inductive Foo (α : Type) : Nat → Type where
+  | a (v : α) : Foo α 0
+  | b (n : α) (m : Nat) (v : Vector Nat m) : Foo α (2*m)
+
+example (h₁ : Foo.b x 2 v = f₁) (h₂ : Foo.b y 2 w = f₂) : f₁ = f₂ → x = y := by
+  grind
+
+example (h₁ : Foo.a x = f₁) (h₂ : Foo.a y = f₂) : f₁ = f₂ → x = y := by
+  grind
+
+example (h₁ : a :: b = x) (h₂ : c :: d = y) : x = y → a = c := by
+  grind
+
+example (h : x = y) (h₁ : a :: b = x) (h₂ : c :: d = y) : a = c := by
+  grind
+
+example (h : x = y) (h₁ : a :: b = x) (h₂ : c :: d = y) : b = d := by
+  grind
+
+example (a b : Sum Nat Bool) : a = .inl x → b = .inl y → x ≠ y → a = b → False := by
+  grind
+
+example (a b : Nat) : a = 1 → b = 2 → a = b → False := by
+  grind
+
+example (a b c : Int) : a = 1 → c = -2 → a = b → c = b → False := by
+  grind
+
+example (a b : Char) : a = 'h' → b = 'w' → a = b → False := by
+  grind
+
+example (a b : String) : a = "hello" → b = "world" → a = b → False := by
+  grind
+
+example (a b c : String) : a = c → a = "hello" → c = "world" → c = b → False := by
+  grind
+
+example (a b c : BitVec 32) : a = c → a = 1#32 → c = 2#32 → c = b → False := by
+  grind
+
+example (a b c : UInt32) : a = c → a = 1 → c = 200 → c = b → False := by
+  grind
+
+structure Boo (α : Type) where
+  a : α
+  b : α
+  c : α
+
+example (a b d : Nat) (f : Nat → Boo Nat) : (f d).1 ≠ a → f d = ⟨b, v₁, v₂⟩ → b = a → False := by
+  grind
+
+def ex (a b c d : Nat) (f : Nat → Boo Nat) : (f d).2 ≠ a → f d = ⟨b, c, v₂⟩ → c = a → False := by
+  grind
+
+example (a b c : Nat) (f : Nat → Nat) : { a := f b, c, b := 4 : Boo Nat }.1 ≠ f a → f b = f c → a = c → False := by
+  grind
+
+example (a b c : Nat) (f : Nat → Nat) : p = { a := f b, c, b := 4 : Boo Nat } → p.1 ≠ f a → f b = f c → a = c → False := by
+  grind
+
+example (a b c : Nat) (f : Nat → Nat) : p.1 ≠ f a → p = { a := f b, c, b := 4 : Boo Nat } → f b = f c → a = c → False := by
+  grind