feat: propagate connectives at addEqStep

src/Init/Grind/Lemmas.lean

@@ -5,10 +5,40 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Core
+import Init.SimpLemmas
+import Init.Classical
 
 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
+
 end Lean.Grind

src/Lean/Meta/Tactic/Grind.lean

@@ -15,6 +15,9 @@ 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
 
 namespace Lean
 

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

@@ -5,86 +5,13 @@ 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.Propagate
+import Lean.Meta.Tactic.Grind.PP
 
 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.
@@ -96,15 +23,6 @@ def mkENode (e : Expr) (generation : Nat) : GoalM Unit := do
   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]")
 
@@ -112,7 +30,7 @@ private def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
 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
+    pushEqHEq e e' congrPlaceholderProof
     -- TODO: we must check whether the types of the functions are the same
     -- TODO: update cgRoot for `e`
   else
@@ -242,7 +160,8 @@ where
     }
     let parents ← removeParents lhsRoot.self
     -- TODO: set propagateBool
-    updateRoots lhs rhsNode.root true -- TODO
+    let isTrueOrFalse ← isTrueExpr rhsNode.root <||> isFalseExpr rhsNode.root
+    updateRoots lhs rhsNode.root (isTrueOrFalse && !(← isInconsistent))
     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 +174,18 @@ where
       heqProofs  := isHEq || rhsRoot.heqProofs || lhsRoot.heqProofs
     }
     copyParentsTo parents rhsNode.root
+    unless (← isInconsistent) do
+      if isTrueOrFalse then
+        for parent in parents do
+          propagateConectivesUp parent
 
-  updateRoots (lhs : Expr) (rootNew : Expr) (_propagateBool : Bool) : GoalM Unit := do
+  updateRoots (lhs : Expr) (rootNew : Expr) (propagateTruth : Bool) : GoalM Unit := do
     let rec loop (e : Expr) : GoalM Unit := do
       -- TODO: propagateBool
       let n ← getENode e
       setENode e { n with root := rootNew }
+      if propagateTruth then
+        propagateConnectivesDown e
       if isSameExpr lhs n.next then return ()
       loop n.next
     loop lhs

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

@@ -12,12 +12,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

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

@@ -0,0 +1,80 @@
+/-
+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}"
+
+/-- 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
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,37 @@
+/-
+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
+
+/--
+Returns a proof that `a = b` (or `HEq a b`).
+It assumes `a` and `b` are in the same equivalence class.
+-/
+def mkEqProof (a b : Expr) : GoalM Expr := do
+  -- TODO
+  if (← isDefEq (← inferType a) (← inferType b)) then
+    mkSorry (← mkEq a b) (synthetic := false)
+  else
+    mkSorry (← mkHEq a b) (synthetic := false)
+
+/--
+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)
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,141 @@
+/-
+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.Proof
+
+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`.
+-/
+private def propagateAndUp (e : Expr) : GoalM Unit := do
+  let a := e.appFn!.appArg!
+  let b := e.appArg!
+  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`.
+-/
+private def propagateAndDown (e : Expr) : GoalM Unit := do
+  if (← isEqTrue e) then
+    let a := e.appFn!.appArg!
+    let b := e.appArg!
+    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`.
+-/
+private def propagateOrUp (e : Expr) : GoalM Unit := do
+  let a := e.appFn!.appArg!
+  let b := e.appArg!
+  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`.
+-/
+private def propagateOrDown (e : Expr) : GoalM Unit := do
+  if (← isEqFalse e) then
+    let a := e.appFn!.appArg!
+    let b := e.appArg!
+    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`.
+-/
+private def propagateNotUp (e : Expr) : GoalM Unit := do
+  let a := e.appArg!
+  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`.
+-/
+private def propagateNotDown (e : Expr) : GoalM Unit := do
+  if (← isEqFalse e) then
+    let a := e.appArg!
+    pushEqTrue a <| mkApp2 (mkConst ``Lean.Grind.eq_true_of_not_eq_false) a (← mkEqFalseProof e)
+  else if (← isEqTrue e) then
+    let a := e.appArg!
+    pushEqFalse a <| mkApp2 (mkConst ``Lean.Grind.eq_false_of_not_eq_true) a (← 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
+    propagateAndUp e
+  else if declName == ``Or && e.getAppNumArgs == 2 then
+    propagateOrUp e
+  else if declName == ``Not && e.getAppNumArgs == 1 then
+    propagateNotUp e
+  -- TODO support for equality between Props
+
+/-- 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
+    propagateAndDown e
+  else if declName == ``Or && e.getAppNumArgs == 2 then
+    propagateOrDown e
+  else if declName == ``Not && e.getAppNumArgs == 1 then
+    propagateNotDown e
+  -- TODO support for `if-then-else`, equality between Props
+
+end Lean.Meta.Grind

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

@@ -18,6 +18,20 @@ namespace Lean.Meta.Grind
   -- inserted into the E-graph
   unsafe ptrEq a b
 
+/--
+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"
+}
+
 structure Context where
   mainDeclName : Name
 
@@ -248,6 +262,14 @@ abbrev GoalM := StateRefT Goal GrindM
 @[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
 Otherwise, returns `none`s.
@@ -261,7 +283,17 @@ 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 `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 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
@@ -287,6 +319,35 @@ 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 } }
+
+@[inline] def pushEqHEq (lhs rhs proof : Expr) : GoalM Unit := do
+  if (← isDefEq (← inferType lhs) (← inferType 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`.

tests/lean/run/grind_propagate_connectives.lean

@@ -0,0 +1,61 @@
+import Lean
+
+-- Prints the equivalence class containing a `f` application
+open Lean Meta Elab Tactic Grind in
+elab "grind_test" : tactic => withMainContext do
+  let declName := (← Term.getDeclName?).getD `_main
+  Meta.Grind.preprocessAndProbe (← getMainGoal) declName do
+    let trueExprs := (← filterENodes fun e => return e.self.isFVar && (← isEqTrue e.self)).toList.map (·.self)
+    let falseExprs := (← filterENodes fun e => return e.self.isFVar && (← isEqFalse e.self)).toList.map (·.self)
+    logInfo m!"true:  {trueExprs}"
+    logInfo m!"false: {falseExprs}"
+
+set_option grind.debug true
+
+/--
+info: true:  [q, w]
+---
+info: false: [p, r]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : (p ∨ (q ∧ ¬r ∧ w)) → ¬p → False := by
+  grind_test
+  sorry
+
+/--
+info: true:  [r]
+---
+info: false: [p, q]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : (p ∨ q ∨ r) → (p ∨ ¬q) → ¬p → False := by
+  grind_test
+  sorry
+
+/--
+info: true:  [r]
+---
+info: false: [p₁, q]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : ((p₁ ∧ p₂) ∨ q ∨ r) → (p₁ ∨ ¬q) → p₁ = False → False := by
+  grind_test
+  sorry
+
+/--
+info: true:  [r]
+---
+info: false: [p₂, q]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : ((p₁ ∧ p₂) ∨ q ∨ r) → ((p₂ ∧ p₁) ∨ ¬q) → p₂ = False → False := by
+  grind_test
+  sorry