feat: check cgRoot at Inv.lean

This PR adds support for projection functions to the (WIP) `grind`
tactic.

src/Init/Grind.lean

@@ -8,3 +8,5 @@ import Init.Grind.Norm
 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

@@ -5,10 +5,49 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Core
+import Init.SimpLemmas
+import Init.Classical
+import Init.ByCases
 
 namespace Lean.Grind
 
 theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' → q) : p → q :=
   fun hp => h (he.mp hp)
 
+/-! And -/
+
+theorem and_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∧ b) = b := by simp [h]
+theorem and_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ∧ b) = a := by simp [h]
+theorem and_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∧ b) = False := by simp [h]
+theorem and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∧ b) = False := by simp [h]
+
+theorem eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = True) : a = True := by simp_all
+theorem eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = True) : b = True := by simp_all
+
+/-! Or -/
+
+theorem or_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∨ b) = True := by simp [h]
+theorem or_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ∨ b) = True := by simp [h]
+theorem or_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∨ b) = b := by simp [h]
+theorem or_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∨ b) = a := by simp [h]
+
+theorem eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = False) : a = False := by simp_all
+theorem eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = False) : b = False := by simp_all
+
+/-! Not -/
+
+theorem not_eq_of_eq_true {a : Prop} (h : a = True) : (Not a) = False := by simp [h]
+theorem not_eq_of_eq_false {a : Prop} (h : a = False) : (Not a) = True := by simp [h]
+
+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]
+theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by simp [h]
+
 end Lean.Grind

src/Init/Grind/Norm.lean

@@ -41,7 +41,7 @@ attribute [grind_norm] not_true
 attribute [grind_norm] not_false_eq_true
 
 -- Implication as a clause
-@[grind_norm] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+@[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
 -- And

src/Init/Grind/Propagator.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.NotationExtra
+
+namespace Lean.Parser
+
+/-- A user-defined propagator for the `grind` tactic. -/
+-- TODO: not implemented yet
+syntax (docComment)? "grind_propagator " (Tactic.simpPre <|> Tactic.simpPost) ident " (" ident ")" " := " term : command
+
+/-- A builtin propagator for the `grind` tactic. -/
+syntax (docComment)? "builtin_grind_propagator " ident (Tactic.simpPre <|> Tactic.simpPost) ident " := " term : command
+
+/-- Auxiliary attribute for builtin `grind` propagators. -/
+syntax (name := grindPropagatorBuiltinAttr) "builtin_grind_propagator" (Tactic.simpPre <|> Tactic.simpPost) ident : attr
+
+macro_rules
+  | `($[$doc?:docComment]? builtin_grind_propagator $propagatorName:ident $direction $op:ident := $body) => do
+    let propagatorType := `Lean.Meta.Grind.Propagator
+    `($[$doc?:docComment]? def $propagatorName:ident : $(mkIdent propagatorType) := $body
+      attribute [builtin_grind_propagator $direction $op] $propagatorName)
+
+end Lean.Parser

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

@@ -15,6 +15,11 @@ import Lean.Meta.Tactic.Grind.Core
 import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.MarkNestedProofs
 import Lean.Meta.Tactic.Grind.Inv
+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
 
@@ -24,6 +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

@@ -5,154 +5,14 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.Util
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Inv
-import Lean.Meta.LitValues
+import Lean.Meta.Tactic.Grind.PP
+import Lean.Meta.Tactic.Grind.Ctor
+import Lean.Meta.Tactic.Grind.Internalize
 
 namespace Lean.Meta.Grind
-/-- Helper function for pretty printing the state for debugging purposes. -/
-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
-    e.withApp fun f args => do
-      let r ← if f.isConst then
-        ppExpr f
-      else
-        ppENodeRef f
-      let mut r := r
-      for arg in args do
-        r := r ++ " " ++ (← ppENodeRef arg)
-      return r
-  else
-    ppExpr e
-
-/-- Helper function for pretty printing the state for debugging purposes. -/
-def ppENodeDecl (e : Expr) : GoalM Format := do
-  let mut r := f!"{← ppENodeRef e} := {← ppENodeDeclValue e}"
-  let n ← getENode e
-  unless isSameExpr e n.root do
-    r := r ++ f!" ↦ {← ppENodeRef n.root}"
-  if n.interpreted then
-    r := r ++ ", [val]"
-  if n.ctor then
-    r := r ++ ", [ctor]"
-  if grind.debug.get (← getOptions) then
-    if let some target ← getTarget? e then
-      r := r ++ f!" ↝ {← ppENodeRef target}"
-  return r
-
-/-- Pretty print goal state for debugging purposes. -/
-def ppState : GoalM Format := do
-  let mut r := f!"Goal:"
-  let nodes ← getENodes
-  for node in nodes do
-    r := r ++ "\n" ++ (← ppENodeDecl node.self)
-  let eqcs ← getEqcs
-  for eqc in eqcs do
-    if eqc.length > 1 then
-      r := r ++ "\n" ++ "{" ++ (Format.joinSep (← eqc.mapM ppENodeRef) ", ") ++  "}"
-  return r
-
-/--
-Returns `true` if `e` is `True`, `False`, or a literal value.
-See `LitValues` for supported literals.
--/
-def isInterpreted (e : Expr) : MetaM Bool := do
-  if e.isTrue || e.isFalse then return true
-  isLitValue e
-
-/--
-Creates an `ENode` for `e` if one does not already exist.
-This method assumes `e` has been hashconsed.
--/
-def mkENode (e : Expr) (generation : Nat) : GoalM Unit := do
-  if (← alreadyInternalized e) then return ()
-  let ctor := (← isConstructorAppCore? e).isSome
-  let interpreted ← isInterpreted e
-  mkENodeCore e interpreted ctor generation
-
-private def pushNewEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit :=
-  modify fun s => { s with newEqs := s.newEqs.push { lhs, rhs, proof, isHEq } }
-
-@[inline] private def pushNewEq (lhs rhs proof : Expr) : GoalM Unit := do
-  if (← isDefEq (← inferType lhs) (← inferType rhs)) then
-    pushNewEqCore lhs rhs proof (isHEq := false)
-  else
-    pushNewEqCore lhs rhs proof (isHEq := true)
-
-/-- We use this auxiliary constant to mark delayed congruence proofs. -/
-private def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
-
-/-- Adds `e` to congruence table. -/
-def addCongrTable (e : Expr) : GoalM Unit := do
-  if let some { e := e' } := (← get).congrTable.find? { e } then
-    trace[grind.congr] "{e} = {e'}"
-    pushNewEq 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
@@ -174,12 +34,6 @@ where
       proof?  := proofNew?
     }
 
-private def markAsInconsistent : GoalM Unit :=
-  modify fun s => { s with inconsistent := true }
-
-def isInconsistent : GoalM Bool :=
-  return (← get).inconsistent
-
 /--
 Remove `root` parents from the congruence table.
 This is an auxiliary function performed while merging equivalence classes.
@@ -198,6 +52,23 @@ 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
+
 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
@@ -209,9 +80,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)
@@ -220,7 +93,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
@@ -241,8 +121,7 @@ where
       flipped
     }
     let parents ← removeParents lhsRoot.self
-    -- TODO: set propagateBool
-    updateRoots lhs rhsNode.root true -- TODO
+    updateRoots lhs rhsNode.root
     trace[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
     reinsertParents parents
     setENode lhsNode.root { (← getENode lhsRoot.self) with -- We must retrieve `lhsRoot` since it was updated.
@@ -255,12 +134,16 @@ where
       heqProofs  := isHEq || rhsRoot.heqProofs || lhsRoot.heqProofs
     }
     copyParentsTo parents rhsNode.root
+    unless (← isInconsistent) do
+      for parent in parents do
+        propagateUp parent
 
-  updateRoots (lhs : Expr) (rootNew : Expr) (_propagateBool : Bool) : GoalM Unit := do
+  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
+        propagateDown e
       if isSameExpr lhs n.next then return ()
       loop n.next
     loop lhs

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,68 @@
+/-
+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 } }
+
+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
+      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
 
@@ -12,12 +13,6 @@ namespace Lean.Meta.Grind
 Debugging support code for checking basic invariants.
 -/
 
-register_builtin_option grind.debug : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "check invariants after updates"
-}
-
 private def checkEqc (root : ENode) : GoalM Unit := do
   let mut size := 0
   let mut curr := root.self
@@ -25,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
@@ -44,24 +49,54 @@ 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 isSameExpr (← getRoot arg) e then
+        if (← checkChild arg) then
           found := true
           break
-      assert! found
+      unless found do
+        assert! (← checkChild parent.getAppFn)
   else
     -- All the parents are stored in the root of the equivalence class.
     assert! (← getParents e).isEmpty
 
+private def checkPtrEqImpliesStructEq : GoalM Unit := do
+  let nodes ← getENodes
+  for h₁ : i in [: nodes.size] do
+    let n₁ := nodes[i]
+    for h₂ : j in [i+1 : nodes.size] do
+      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}"
+
 /--
-Check basic invariants if `grind.debug` is enabled.
+Checks basic invariants if `grind.debug` is enabled.
 -/
-def checkInvariants : GoalM Unit := do
+def checkInvariants (expensive := false) : GoalM Unit := do
   if grind.debug.get (← getOptions) then
     for (_, node) in (← get).enodes do
       checkParents node.self
       if isSameExpr node.self node.root then
         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

@@ -0,0 +1,59 @@
+/-
+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.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind
+
+/-- Helper function for pretty printing the state for debugging purposes. -/
+def ppENodeRef (e : Expr) : GoalM Format := do
+  let some n ← getENode? e | return "_"
+  return f!"#{n.idx}"
+
+/-- Helper function for pretty printing the state for debugging purposes. -/
+def ppENodeDeclValue (e : Expr) : GoalM Format := do
+  if e.isApp && !(← isLitValue e) then
+    e.withApp fun f args => do
+      let r ← if f.isConst then
+        ppExpr f
+      else
+        ppENodeRef f
+      let mut r := r
+      for arg in args do
+        r := r ++ " " ++ (← ppENodeRef arg)
+      return r
+  else
+    ppExpr e
+
+/-- Helper function for pretty printing the state for debugging purposes. -/
+def ppENodeDecl (e : Expr) : GoalM Format := do
+  let mut r := f!"{← ppENodeRef e} := {← ppENodeDeclValue e}"
+  let n ← getENode e
+  unless isSameExpr e n.root do
+    r := r ++ f!" ↦ {← ppENodeRef n.root}"
+  if n.interpreted then
+    r := r ++ ", [val]"
+  if n.ctor then
+    r := r ++ ", [ctor]"
+  if grind.debug.get (← getOptions) then
+    if let some target ← getTarget? e then
+      r := r ++ f!" ↝ {← ppENodeRef target}"
+  return r
+
+/-- Pretty print goal state for debugging purposes. -/
+def ppState : GoalM Format := do
+  let mut r := f!"Goal:"
+  let nodes ← getENodes
+  for node in nodes do
+    r := r ++ "\n" ++ (← ppENodeDecl node.self)
+  let eqcs ← getEqcs
+  for eqc in eqcs do
+    if eqc.length > 1 then
+      r := r ++ "\n" ++ "{" ++ (Format.joinSep (← eqc.mapM ppENodeRef) ", ") ++  "}"
+  return r
+
+end Lean.Meta.Grind

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

@@ -16,41 +16,20 @@ import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
-import Lean.Meta.Tactic.Grind.MarkNestedProofs
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Run
 
 namespace Lean.Meta.Grind
 namespace Preprocessor
 
--- TODO: use congruence closure and decision procedures during pre-processing
--- TODO: implement `simp` discharger using preprocessor state
-
-structure Context where
-  simp     : Simp.Context
-  simprocs : Array Simp.Simprocs
-  deriving Inhabited
-
 structure State where
-  simpStats : Simp.Stats := {}
   goals     : PArray Goal := {}
   deriving Inhabited
 
-abbrev PreM := ReaderT Context $ StateRefT State GrindM
+abbrev PreM := StateRefT State GrindM
 
 def PreM.run (x : PreM α) : GrindM α := do
-  let thms ← grindNormExt.getTheorems
-  let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
-  let simp ← Simp.mkContext
-    (config := { arith := true })
-    (simpTheorems := #[thms])
-    (congrTheorems := (← getSimpCongrTheorems))
-  x { simp, simprocs } |>.run' {}
-
-def simp (_goal : Goal) (e : Expr) : PreM Simp.Result := do
-  -- TODO: use `goal` state in the simplifier
-  let simpStats := (← get).simpStats
-  let (r, simpStats) ← Meta.simp e (← read).simp (← read).simprocs (stats := simpStats)
-  modify fun s => { s with simpStats }
-  return r
+ x.run' {}
 
 inductive IntroResult where
   | done
@@ -70,24 +49,16 @@ def introNext (goal : Goal) : PreM IntroResult := do
         let tag ← goal.mvarId.getTag
         let q := target.bindingBody!
         -- TODO: keep applying simp/eraseIrrelevantMData/canon/shareCommon until no progress
-        let r ← simp goal p
-        let p' := r.expr
-        let p' ← markNestedProofs p'
-        let p' ← unfoldReducible p'
-        let p' ← eraseIrrelevantMData p'
-        let p' ← foldProjs p'
-        let p' ← normalizeLevels p'
-        let p' ← canon p'
-        let p' ← shareCommon p'
+        let r ← pre p
         let fvarId ← mkFreshFVarId
-        let lctx := (← getLCtx).mkLocalDecl fvarId target.bindingName! p' target.bindingInfo!
+        let lctx := (← getLCtx).mkLocalDecl fvarId target.bindingName! r.expr target.bindingInfo!
         let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) q .syntheticOpaque tag
         let mvarIdNew := mvarNew.mvarId!
         mvarIdNew.withContext do
           let h ← mkLambdaFVars #[mkFVar fvarId] mvarNew
           match r.proof? with
           | some he =>
-            let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq) #[p, p', q, he, h]
+            let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq) #[p, r.expr, q, he, h]
             goal.mvarId.assign hNew
             return .newHyp fvarId { goal with mvarId := mvarIdNew }
           | none =>
@@ -128,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
@@ -169,6 +142,8 @@ def preprocess (mvarId : MVarId) : PreM State := do
   loop (← mkGoal mvarId)
   if (← isTracingEnabledFor `grind.pre) then
     trace[grind.pre] (← ppGoals)
+  for goal in (← get).goals do
+    discard <| GoalM.run' goal <| checkInvariants (expensive := true)
   get
 
 def preprocessAndProbe (mvarId : MVarId) (p : GoalM Unit) : PreM Unit := do
@@ -188,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

@@ -0,0 +1,239 @@
+/-
+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.Sorry -- TODO: remove
+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.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)
+
+def mkHEqProof (a b : Expr) : GoalM Expr :=
+  mkEqProofCore a b (heq := true)
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,145 @@
+/-
+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
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+
+namespace Lean.Meta.Grind
+
+/--
+Propagates equalities for a conjunction `a ∧ b` based on the truth values
+of its components `a` and `b`. This function checks the truth value of `a` and `b`,
+and propagates the following equalities:
+
+- If `a = True`, propagates `(a ∧ b) = b`.
+- If `b = True`, propagates `(a ∧ b) = a`.
+- If `a = False`, propagates `(a ∧ b) = False`.
+- If `b = False`, propagates `(a ∧ b) = False`.
+-/
+builtin_grind_propagator propagateAndUp ↑And := fun e => do
+  let_expr And a b := e | return ()
+  if (← isEqTrue a) then
+    -- a = True → (a ∧ b) = b
+    pushEq e b <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+  else if (← isEqTrue b) then
+    -- b = True → (a ∧ b) = a
+    pushEq e a <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+  else if (← isEqFalse a) then
+    -- a = False → (a ∧ b) = False
+    pushEqFalse e <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_false_left) a b (← mkEqFalseProof a)
+  else if (← isEqFalse b) then
+    -- b = False → (a ∧ b) = False
+    pushEqFalse e <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_false_right) a b (← mkEqFalseProof b)
+
+/--
+Propagates truth values downwards for a conjunction `a ∧ b` when the
+expression itself is known to be `True`.
+-/
+builtin_grind_propagator propagateAndDown ↓And := fun e => do
+  if (← isEqTrue e) then
+    let_expr And a b := e | return ()
+    let h ← mkEqTrueProof e
+    pushEqTrue a <| mkApp3 (mkConst ``Lean.Grind.eq_true_of_and_eq_true_left) a b h
+    pushEqTrue b <| mkApp3 (mkConst ``Lean.Grind.eq_true_of_and_eq_true_right) a b h
+
+/--
+Propagates equalities for a disjunction `a ∨ b` based on the truth values
+of its components `a` and `b`. This function checks the truth value of `a` and `b`,
+and propagates the following equalities:
+
+- If `a = False`, propagates `(a ∨ b) = b`.
+- If `b = False`, propagates `(a ∨ b) = a`.
+- If `a = True`, propagates `(a ∨ b) = True`.
+- If `b = True`, propagates `(a ∨ b) = True`.
+-/
+builtin_grind_propagator propagateOrUp ↑Or := fun e => do
+  let_expr Or a b := e | return ()
+  if (← isEqFalse a) then
+    -- a = False → (a ∨ b) = b
+    pushEq e b <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_false_left) a b (← mkEqFalseProof a)
+  else if (← isEqFalse b) then
+    -- b = False → (a ∨ b) = a
+    pushEq e a <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_false_right) a b (← mkEqFalseProof b)
+  else if (← isEqTrue a) then
+    -- a = True → (a ∨ b) = True
+    pushEqTrue e <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+  else if (← isEqTrue b) then
+    -- b = True → (a ∧ b) = True
+    pushEqTrue e <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+
+/--
+Propagates truth values downwards for a disjuction `a ∨ b` when the
+expression itself is known to be `False`.
+-/
+builtin_grind_propagator propagateOrDown ↓Or := fun e => do
+  if (← isEqFalse e) then
+    let_expr Or a b := e | return ()
+    let h ← mkEqFalseProof e
+    pushEqFalse a <| mkApp3 (mkConst ``Lean.Grind.eq_false_of_or_eq_false_left) a b h
+    pushEqFalse b <| mkApp3 (mkConst ``Lean.Grind.eq_false_of_or_eq_false_right) a b h
+
+/--
+Propagates equalities for a negation `Not a` based on the truth value of `a`.
+This function checks the truth value of `a` and propagates the following equalities:
+
+- If `a = False`, propagates `(Not a) = True`.
+- If `a = True`, propagates `(Not a) = False`.
+-/
+builtin_grind_propagator propagateNotUp ↑Not := fun e => do
+  let_expr Not a := e | return ()
+  if (← isEqFalse a) then
+    -- a = False → (Not a) = True
+    pushEqTrue e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_false) a (← mkEqFalseProof a)
+  else if (← isEqTrue a) then
+    -- a = True → (Not a) = False
+    pushEqFalse e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_true) a (← mkEqTrueProof a)
+
+/--
+Propagates truth values downwards for a negation expression `Not a` based on the truth value of `Not a`.
+This function performs the following:
+
+- If `(Not a) = False`, propagates `a = True`.
+- 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
+    pushEqTrue a <| mkApp2 (mkConst ``Lean.Grind.eq_true_of_not_eq_false) a (← mkEqFalseProof e)
+  else if (← isEqTrue e) then
+    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
+  let_expr Eq _ a b := e | return ()
+  if (← isEqTrue a) then
+    pushEq e b <| mkApp3 (mkConst ``Lean.Grind.eq_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+  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)
+
+/-- Propagates `Eq` downwards -/
+builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
+  if (← isEqTrue e) then
+    let_expr Eq _ a b := e | return ()
+    pushEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
+
+/-- Propagates `HEq` downwards -/
+builtin_grind_propagator propagateHEqDown ↓HEq := fun e => do
+  if (← isEqTrue e) then
+    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/Simp.lean

@@ -0,0 +1,41 @@
+/-
+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.Simp.Main
+import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.MarkNestedProofs
+
+namespace Lean.Meta.Grind
+
+-- TODO: use congruence closure and decision procedures during pre-processing
+-- TODO: implement `simp` discharger using preprocessor state
+
+/-- Simplifies the given expression using the `grind` simprocs and normalization theorems. -/
+def simp (e : Expr) : GrindM Simp.Result := do
+  let simpStats := (← get).simpStats
+  let (r, simpStats) ← Meta.simp e (← readThe Context).simp (← readThe Context).simprocs (stats := simpStats)
+  modify fun s => { s with simpStats }
+  return r
+
+/--
+Simplifies `e` using `grind` normalization theorems and simprocs,
+and then applies several other preprocessing steps.
+-/
+def pre (e : Expr) : GrindM Simp.Result := do
+  let r ← simp e
+  let e' := r.expr
+  let e' ← markNestedProofs e'
+  let e' ← unfoldReducible e'
+  let e' ← eraseIrrelevantMData e'
+  let e' ← foldProjs e'
+  let e' ← normalizeLevels e'
+  let e' ← canon e'
+  let e' ← shareCommon e'
+  trace[grind.simp] "{e}\n===>\n{e'}"
+  return { r with expr := e' }
+
+end Lean.Meta.Grind

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

@@ -8,8 +8,10 @@ import Lean.Util.ShareCommon
 import Lean.Meta.Basic
 import Lean.Meta.CongrTheorems
 import Lean.Meta.AbstractNestedProofs
-import Lean.Meta.Tactic.Grind.Canon
+import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Grind.Canon
+import Lean.Meta.Tactic.Grind.Attr
 
 namespace Lean.Meta.Grind
 
@@ -18,12 +20,36 @@ namespace Lean.Meta.Grind
   -- inserted into the E-graph
   unsafe ptrEq a b
 
-structure Context where
-  mainDeclName : Name
+/-- We use this auxiliary constant to mark delayed congruence proofs. -/
+def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
 
 /--
-Key for the congruence theorem cache.
+Returns `true` if `e` is `True`, `False`, or a literal value.
+See `LitValues` for supported literals.
 -/
+def isInterpreted (e : Expr) : MetaM Bool := do
+  if e.isTrue || e.isFalse then return true
+  isLitValue e
+
+register_builtin_option grind.debug : Bool := {
+  defValue := false
+  group    := "debug"
+  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
+  mainDeclName : Name
+
+/-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
   f       : Expr
   numArgs : Nat
@@ -36,6 +62,7 @@ instance : BEq CongrTheoremCacheKey where
 instance : Hashable CongrTheoremCacheKey where
   hash a := mixHash (unsafe ptrAddrUnsafe a.f).toUInt64 (hash a.numArgs)
 
+/-- State for the `GrindM` monad. -/
 structure State where
   canon      : Canon.State := {}
   /-- `ShareCommon` (aka `Hashconsing`) state. -/
@@ -48,25 +75,29 @@ structure State where
   Remark: we currently do not reuse congruence theorems
   -/
   congrThms  : PHashMap CongrTheoremCacheKey CongrTheorem := {}
+  simpStats  : Simp.Stats := {}
   trueExpr   : Expr
   falseExpr  : Expr
 
-abbrev GrindM := ReaderT Context $ StateRefT State MetaM
+private opaque MethodsRefPointed : NonemptyType.{0}
+private def MethodsRef : Type := MethodsRefPointed.type
+instance : Nonempty MethodsRef := MethodsRefPointed.property
 
-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)
-  x { mainDeclName } |>.run' { scState, trueExpr, falseExpr }
+abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 
+/-- Returns the internalized `True` constant.  -/
 def getTrueExpr : GrindM Expr := do
   return (← get).trueExpr
 
+/-- Returns the internalized `False` constant.  -/
 def getFalseExpr : GrindM Expr := do
   return (← get).falseExpr
 
 def getMainDeclName : GrindM Name :=
-  return (← read).mainDeclName
+  return (← readThe Context).mainDeclName
+
+@[inline] def getMethodsRef : GrindM MethodsRef :=
+  read
 
 /--
 Abtracts nested proofs in `e`. This is a preprocessing step performed before internalization.
@@ -82,9 +113,9 @@ Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have
 been hash-consing. We perform this step before we internalize expressions.
 -/
 def shareCommon (e : Expr) : GrindM Expr := do
-  modifyGet fun { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr } =>
+  modifyGet fun { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats } =>
     let (e, scState) := ShareCommon.State.shareCommon scState e
-    (e, { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr })
+    (e, { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats })
 
 /--
 Canonicalizes nested types, type formers, and instances in `e`.
@@ -242,11 +273,15 @@ def Goal.admit (goal : Goal) : MetaM Unit :=
 
 abbrev GoalM := StateRefT Goal GrindM
 
-@[inline] def GoalM.run (goal : Goal) (x : GoalM α) : GrindM (α × Goal) :=
-  goal.mvarId.withContext do StateRefT'.run x goal
+abbrev Propagator := Expr → GoalM Unit
 
-@[inline] def GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal :=
-  goal.mvarId.withContext do StateRefT'.run' (x *> get) goal
+/-- Returns `true` if `e` is the internalized `True` expression.  -/
+def isTrueExpr (e : Expr) : GrindM Bool :=
+  return isSameExpr e (← getTrueExpr)
+
+/-- Returns `true` if `e` is the internalized `False` expression.  -/
+def isFalseExpr (e : Expr) : GrindM Bool :=
+  return isSameExpr e (← getFalseExpr)
 
 /--
 Returns `some n` if `e` has already been "internalized" into the
@@ -261,7 +296,30 @@ def getENode (e : Expr) : GoalM ENode := do
     | throwError "internal `grind` error, term has not been internalized{indentExpr e}"
   return n
 
-/-- Returns `true` is the root of its equivalence class. -/
+/-- 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
+  return isSameExpr n.root (← getTrueExpr)
+
+/-- Returns `true` if `e` is in the equivalence class of `False`. -/
+def isEqFalse (e : Expr) : GoalM Bool := do
+  let n ← getENode e
+  return isSameExpr n.root (← getFalseExpr)
+
+/-- 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
+
+/-- Returns `true` if the root of its equivalence class. -/
 def isRoot (e : Expr) : GoalM Bool := do
   let some n ← getENode? e | return false -- `e` has not been internalized. Panic instead?
   return isSameExpr n.root e
@@ -275,6 +333,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
@@ -287,6 +349,39 @@ def getTarget? (e : Expr) : GoalM (Option Expr) := do
   let some n ← getENode? e | return none
   return n.target?
 
+/--
+If `isHEq` is `false`, it pushes `lhs = rhs` with `proof` to `newEqs`.
+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
+    pushEqCore lhs rhs proof (isHEq := false)
+  else
+    pushEqCore lhs rhs proof (isHEq := true)
+
+/-- Pushes `lhs = rhs` with `proof` to `newEqs`. -/
+@[inline] def pushEq (lhs rhs proof : Expr) : GoalM Unit :=
+  pushEqCore lhs rhs proof (isHEq := false)
+
+/-- Pushes `HEq lhs rhs` with `proof` to `newEqs`. -/
+@[inline] def pushHEq (lhs rhs proof : Expr) : GoalM Unit :=
+  pushEqCore lhs rhs proof (isHEq := true)
+
+/-- Pushes `a = True` with `proof` to `newEqs`. -/
+def pushEqTrue (a proof : Expr) : GoalM Unit := do
+  pushEq a (← getTrueExpr) proof
+
+/-- Pushes `a = False` with `proof` to `newEqs`. -/
+def pushEqFalse (a proof : Expr) : GoalM Unit := do
+  pushEq a (← getFalseExpr) proof
+
 /--
 Records that `parent` is a parent of `child`. This function actually stores the
 information in the root (aka canonical representative) of `child`.
@@ -343,12 +438,59 @@ def mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) : GoalM
   }
   modify fun s => { s with nextIdx := s.nextIdx + 1 }
 
-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)
+/--
+Creates an `ENode` for `e` if one does not already exist.
+This method assumes `e` has been hashconsed.
+-/
+def mkENode (e : Expr) (generation : Nat) : GoalM Unit := do
+  if (← alreadyInternalized e) then return ()
+  let ctor := (← isConstructorAppCore? e).isSome
+  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
@@ -368,4 +510,51 @@ def filterENodes (p : ENode → GoalM Bool) : GoalM (Array ENode) := do
       ref.modify (·.push n)
   ref.get
 
+def forEachEqc (f : ENode → GoalM Unit) : GoalM Unit := do
+  let nodes ← getENodes
+  for n in nodes do
+    if isSameExpr n.self n.root then
+      f n
+
+structure Methods where
+  propagateUp   : Propagator := fun _ => return ()
+  propagateDown : Propagator := fun _ => return ()
+  deriving Inhabited
+
+def Methods.toMethodsRef (m : Methods) : MethodsRef :=
+  unsafe unsafeCast m
+
+private def MethodsRef.toMethods (m : MethodsRef) : Methods :=
+  unsafe unsafeCast m
+
+@[inline] def getMethods : GrindM Methods :=
+  return (← getMethodsRef).toMethods
+
+def propagateUp (e : Expr) : GoalM Unit := do
+  (← getMethods).propagateUp e
+
+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
+
+/-- 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/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