feat: propagate equality in grind (#6443)

This PR adds support for propagating the truth value of equalities in
the (WIP) `grind` tactic.

src/Init/Grind/Lemmas.lean

@@ -41,4 +41,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
 
+/-! 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/Lean/Meta/Tactic/Grind/Propagate.lean

@@ -116,10 +116,37 @@ private def propagateNotDown (e : Expr) : GoalM Unit := do
     let a := e.appArg!
     pushEqFalse a <| mkApp2 (mkConst ``Lean.Grind.eq_false_of_not_eq_true) a (← mkEqTrueProof e)
 
+/-- Propagates `Eq` upwards -/
+def propagateEqUp (e : Expr) : GoalM Unit := do
+  let a := e.appFn!.appArg!
+  let b := e.appArg!
+  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 ``of_eq_true) e (← mkEqProof a b)
+
+/-- Propagates `Eq` downwards -/
+def propagateEqDown (e : Expr) : GoalM Unit := do
+  if (← isEqTrue e) then
+    let a := e.appFn!.appArg!
+    let b := e.appArg!
+    pushEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
+
+/-- Propagates `HEq` downwards -/
+def propagateHEqDown (e : Expr) : GoalM Unit := do
+  if (← isEqTrue e) then
+    let a := e.appFn!.appFn!.appArg!
+    let b := e.appArg!
+    pushHEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
+
 /-- Propagates equalities upwards for logical connectives. -/
 def propagateConectivesUp (e : Expr) : GoalM Unit := do
   let .const declName _ := e.getAppFn | return ()
-  if declName == ``And && e.getAppNumArgs == 2 then
+  if declName == ``Eq && e.getAppNumArgs == 3 then
+    propagateEqUp e
+  else if declName == ``And && e.getAppNumArgs == 2 then
     propagateAndUp e
   else if declName == ``Or && e.getAppNumArgs == 2 then
     propagateOrUp e
@@ -130,7 +157,11 @@ def propagateConectivesUp (e : Expr) : GoalM Unit := do
 /-- Propagates equalities downwards for logical connectives. -/
 def propagateConnectivesDown (e : Expr) : GoalM Unit := do
   let .const declName _ := e.getAppFn | return ()
-  if declName == ``And && e.getAppNumArgs == 2 then
+  if declName == ``Eq && e.getAppNumArgs == 3 then
+    propagateEqDown e
+  else if declName == ``HEq && e.getAppNumArgs == 4 then
+    propagateHEqDown e
+  else if declName == ``And && e.getAppNumArgs == 2 then
     propagateAndDown e
   else if declName == ``Or && e.getAppNumArgs == 2 then
     propagateOrDown e

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

@@ -293,6 +293,12 @@ 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
+  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?
@@ -429,4 +435,10 @@ 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
+
 end Lean.Meta.Grind

tests/lean/run/grind_propagate_connectives.lean

@@ -9,6 +9,10 @@ elab "grind_test" : tactic => withMainContext do
     let falseExprs := (← filterENodes fun e => return e.self.isFVar && (← isEqFalse e.self)).toList.map (·.self)
     logInfo m!"true:  {trueExprs}"
     logInfo m!"false: {falseExprs}"
+    forEachEqc fun n => do
+      unless (← isProp n.self) || (← isType n.self) || n.size == 1 do
+        let eqc ← getEqc n.self
+        logInfo eqc
 
 set_option grind.debug true
 
@@ -60,6 +64,65 @@ example : ((p₁ ∧ p₂) ∨ q ∨ r) → ((p₂ ∧ p₁) ∨ ¬q) → p₂ =
   grind_test
   sorry
 
-example (p q r : Prop) : p ∨ (q ↔ r) → p = False → False := by
+/--
+info: true:  [q, r]
+---
+info: false: [p]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (p q r : Prop) : p ∨ (q ↔ r) → p = False → q → False := by
+  grind_test
+  sorry
+
+/--
+info: true:  [r]
+---
+info: false: [p, s]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (p q r : Prop) : p ∨ ¬(s ∨ (p ↔ r)) → p = False → False := by
+  grind_test
+  sorry
+
+/--
+info: true:  [p]
+---
+info: false: []
+---
+info: [a, b]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (p : Prop) (a : Vector Nat 5) (b : Vector Nat 6) : (p → HEq a b) → p → False := by
+  grind_test
+  sorry
+
+
+/--
+info: true:  [p, q]
+---
+info: false: [r]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (p q r : Prop) : p ∨ (q ↔ r) → q → ¬r → False := by
+  grind_test
+  sorry
+
+/--
+info: true:  [p, q]
+---
+info: false: [r]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (p q r : Prop) : p ∨ (q ↔ r) → ¬r → q → False := by
   grind_test
   sorry