feat: propagate Eq

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/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

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