feat: literal values in grind (#6464)

This PR completes support for literal values in the (WIP) `grind`
tactic. `grind` now closes the goal whenever it merges two equivalence
classes with distinct literal values.

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

@@ -106,6 +106,15 @@ private def closeGoalWithTrueEqFalse : GoalM Unit := do
     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
@@ -119,8 +128,8 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
   let mut valueInconsistency := false
   let mut trueEqFalse := false
   if lhsRoot.interpreted && rhsRoot.interpreted then
-    markAsInconsistent
     if lhsNode.root.isTrue || rhsNode.root.isTrue then
+      markAsInconsistent
       trueEqFalse := true
     else
       valueInconsistency := true
@@ -135,7 +144,9 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
   unless (← isInconsistent) do
     if lhsRoot.ctor && rhsRoot.ctor then
       propagateCtor lhsRoot.self rhsRoot.self
-  -- TODO: propagate value inconsistency
+  unless (← isInconsistent) do
+    if valueInconsistency then
+      closeGoalWithValuesEq lhsRoot.self rhsRoot.self
   trace[grind.debug] "after addEqStep, {← ppState}"
   checkInvariants
 where

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

@@ -44,7 +44,6 @@ def propagateCtor (a b : Expr) : GoalM Unit := do
     let .const declName _ := aType.getAppFn | return ()
     let noConfusionDeclName := Name.mkStr declName "noConfusion"
     unless (← getEnv).contains noConfusionDeclName do return ()
-    let target ← (← get).mvarId.getType
-    closeGoal (← mkNoConfusion target (← mkEqProof a b))
+    closeGoal (← mkNoConfusion (← getFalseExpr) (← mkEqProof a b))
 
 end Lean.Meta.Grind

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

@@ -478,7 +478,11 @@ def closeGoal (falseProof : Expr) : GoalM Unit := do
   markAsInconsistent
   let mvarId := (← get).mvarId
   unless (← mvarId.isAssigned) do
-    mvarId.assign falseProof
+    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

tests/lean/run/grind_t1.lean

@@ -34,3 +34,24 @@ example (h : x = y) (h₁ : a :: b = x) (h₂ : c :: d = y) : b = d := by
 
 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