feat: add support for let-declarations to grind (#6529)

This PR adds support for `let`-declarations to the (WIP) `grind` tactic.

src/Init/Grind/Norm.lean

@@ -59,6 +59,12 @@ attribute [grind_norm] ite_true ite_false
 @[grind_norm↓] theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
   by_cases p <;> simp [*]
 
+@[grind_norm] theorem ite_true_false {_ : Decidable p} : (ite p True False) = p := by
+  by_cases p <;> simp
+
+@[grind_norm] theorem ite_false_true {_ : Decidable p} : (ite p False True) = ¬p := by
+  by_cases p <;> simp
+
 -- Forall
 @[grind_norm↓] theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x := by simp
 attribute [grind_norm] forall_and

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

@@ -190,15 +190,22 @@ where
     addEqStep lhs rhs proof isHEq
     processTodo
 
+/-- Adds a new equality `lhs = rhs`. It assumes `lhs` and `rhs` have already been internalized. -/
 def addEq (lhs rhs proof : Expr) : GoalM Unit := do
   addEqCore lhs rhs proof false
 
+
+/-- Adds a new heterogeneous equality `HEq lhs rhs`. It assumes `lhs` and `rhs` have already been internalized. -/
 def addHEq (lhs rhs proof : Expr) : GoalM Unit := do
   addEqCore lhs rhs proof true
 
-/--
-Adds a new `fact` justified by the given proof and using the given generation.
--/
+/-- Internalizes `lhs` and `rhs`, and then adds equality `lhs = rhs`. -/
+def addNewEq (lhs rhs proof : Expr) (generation : Nat) : GoalM Unit := do
+  internalize lhs generation
+  internalize rhs generation
+  addEq lhs rhs proof
+
+/-- Adds a new `fact` justified by the given proof and using the given generation. -/
 def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
   trace[grind.assert] "{fact}"
   if (← isInconsistent) then return ()

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

@@ -21,7 +21,7 @@ private inductive IntroResult where
   | newLocal (fvarId : FVarId) (goal : Goal)
   deriving Inhabited
 
-private def introNext (goal : Goal) : GrindM IntroResult := do
+private def introNext (goal : Goal) (generation : Nat) : GrindM IntroResult := do
   let target ← goal.mvarId.getType
   if target.isArrow then
     goal.mvarId.withContext do
@@ -58,7 +58,15 @@ private def introNext (goal : Goal) : GrindM IntroResult := do
         let mvarId ← mvarId.assert (← mkFreshUserName localDecl.userName) localDecl.type (mkFVar fvarId)
         return .newDepHyp { goal with mvarId }
       else
-        return .newLocal fvarId { goal with mvarId }
+        let goal := { goal with mvarId }
+        if target.isLet then
+          let v := target.letValue!
+          let r ← simp v
+          let x ← shareCommon (mkFVar fvarId)
+          let goal ← GoalM.run' goal <| addNewEq x r.expr (← r.getProof) generation
+          return .newLocal fvarId goal
+        else
+          return .newLocal fvarId goal
   else
     return .done
 
@@ -84,7 +92,7 @@ partial def intros (goal : Goal) (generation : Nat) : GrindM (List Goal) := do
   let rec go (goal : Goal) : StateRefT (Array Goal) GrindM Unit := do
     if goal.inconsistent then
       return ()
-    match (← introNext goal) with
+    match (← introNext goal generation) with
     | .done =>
       if let some mvarId ← goal.mvarId.byContra? then
         go { goal with mvarId }

tests/lean/run/grind_t1.lean

@@ -111,3 +111,6 @@ example (foo : Nat → Nat)
   grind
 
 end dite_propagator_test
+
+example (a : Nat) : let x := a + a; y = x → y = a + a := by
+  grind