feat: propagate implication in the grind tactic (#6556)

This PR adds propagators for implication to the `grind` tactic. It also
disables the normalization rule: `(p → q) = (¬ p ∨ q)`

src/Init/Grind/Lemmas.lean

@@ -35,6 +35,15 @@ theorem or_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∨ b) = a :=
 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
 
+/-! Implies -/
+
+theorem imp_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a → b) = True := by simp [h]
+theorem imp_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a → b) = True := by simp [h]
+theorem imp_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a → b) = b := by simp [h]
+
+theorem eq_true_of_imp_eq_false {a b : Prop} (h : (a → b) = False) : a = True := by simp_all
+theorem eq_false_of_imp_eq_false {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]

src/Init/Grind/Norm.lean

@@ -41,9 +41,10 @@ attribute [grind_norm] not_true
 -- False
 attribute [grind_norm] not_false_eq_true
 
+-- Remark: we disabled the following normalization rule because we want this information when implementing splitting heuristics
 -- Implication as a clause
-@[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
-  by_cases p <;> by_cases q <;> simp [*]
+-- @[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+--  by_cases p <;> by_cases q <;> simp [*]
 
 -- And
 @[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by

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

@@ -15,20 +15,42 @@ If `parent` is a projection-application `proj_i c`,
 check whether the root of the equivalence class containing `c` is a constructor-application `ctor ... a_i ...`.
 If so, internalize the term `proj_i (ctor ... a_i ...)` and add the equality `proj_i (ctor ... a_i ...) = a_i`.
 -/
-def propagateForallProp (parent : Expr) : GoalM Unit := do
-  let .forallE n p q bi := parent | return ()
-  trace[grind.debug.forallPropagator] "{parent}"
-  unless (← isEqTrue p) do return ()
-  trace[grind.debug.forallPropagator] "isEqTrue, {parent}"
-  let h₁ ← mkEqTrueProof p
-  let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁)
-  let r ← simp qh₁
-  let q := mkLambda n bi p q
-  let q' := r.expr
-  internalize q' (← getGeneration parent)
-  trace[grind.debug.forallPropagator] "q': {q'} for{indentExpr parent}"
-  let h₂ ← r.getProof
-  let h := mkApp5 (mkConst ``Lean.Grind.forall_propagator) p q q' h₁ h₂
-  pushEq parent q' h
+def propagateForallPropUp (e : Expr) : GoalM Unit := do
+  let .forallE n p q bi := e | return ()
+  trace[grind.debug.forallPropagator] "{e}"
+  if !q.hasLooseBVars then
+    propagateImpliesUp p q
+  else
+    unless (← isEqTrue p) do return
+    trace[grind.debug.forallPropagator] "isEqTrue, {e}"
+    let h₁ ← mkEqTrueProof p
+    let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁)
+    let r ← simp qh₁
+    let q := mkLambda n bi p q
+    let q' := r.expr
+    internalize q' (← getGeneration e)
+    trace[grind.debug.forallPropagator] "q': {q'} for{indentExpr e}"
+    let h₂ ← r.getProof
+    let h := mkApp5 (mkConst ``Lean.Grind.forall_propagator) p q q' h₁ h₂
+    pushEq e q' h
+where
+  propagateImpliesUp (a b : Expr) : GoalM Unit := do
+    unless (← alreadyInternalized b) do return ()
+    if (← isEqFalse a) then
+      -- a = False → (a → b) = True
+      pushEqTrue e <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_false_left) a b (← mkEqFalseProof a)
+    else if (← isEqTrue a) then
+      -- a = True → (a → b) = b
+      pushEq e b <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+    else if (← isEqTrue b) then
+      -- b = True → (a → b) = True
+      pushEqTrue e <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+
+def propagateImpliesDown (e : Expr) : GoalM Unit := do
+  if (← isEqFalse e) then
+    let .forallE _ a b _ := e | return ()
+    let h ← mkEqFalseProof e
+    pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_imp_eq_false) a b h
+    pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_imp_eq_false) a b h
 
 end Lean.Meta.Grind

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

@@ -95,11 +95,14 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
   | .sort .. => return ()
   | .fvar .. | .letE .. | .lam .. =>
     mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
-  | .forallE _ d _ _ =>
+  | .forallE _ d b _ =>
     mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
     if (← isProp d <&&> isProp e) then
       internalize d generation
       registerParent e d
+      unless b.hasLooseBVars do
+        internalize b generation
+        registerParent e b
       propagateUp e
   | .lit .. | .const .. =>
     mkENode e generation

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

@@ -23,12 +23,13 @@ def mkMethods (fallback : Fallback) : CoreM Methods := do
   return {
     fallback
     propagateUp := fun e => do
-     propagateForallProp e
+     propagateForallPropUp e
      let .const declName _ := e.getAppFn | return ()
      propagateProjEq e
      if let some prop := builtinPropagators.up[declName]? then
        prop e
     propagateDown := fun e => do
+     propagateImpliesDown e
      let .const declName _ := e.getAppFn | return ()
      if let some prop := builtinPropagators.down[declName]? then
        prop e