fix: forall propagation in grind (#6578)

This PR fixes and improves the propagator for forall-expressions in the
`grind` tactic.

---------

Co-authored-by: Kim Morrison <[email protected]>

src/Init/Grind/Lemmas.lean

@@ -73,6 +73,8 @@ theorem forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = Tr
   · intro h'; exact Eq.mp h₂ (h' (of_eq_true h₁))
   · intro h'; intros; exact Eq.mpr h₂ h'
 
+theorem of_forall_eq_false (α : Sort u) (p : α → Prop) (h : (∀ x : α, p x) = False) : ∃ x : α, ¬ p x := by simp_all
+
 /-! dite -/
 
 theorem dite_cond_eq_true' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c → α} {b : ¬ c → α} {r : α} (h₁ : c = True) (h₂ : a (of_eq_true h₁) = r) : (dite c a b) = r := by simp [h₁, h₂]

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

@@ -46,11 +46,21 @@ where
       -- 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
+def propagateForallPropDown (e : Expr) : GoalM Unit := do
+  let .forallE n a b bi := e | return ()
   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
+    if b.hasLooseBVars then
+      let α := a
+      let p := b
+      -- `e` is of the form `∀ x : α, p x`
+      -- Add fact `∃ x : α, ¬ p x`
+      let u ← getLevel α
+      let prop := mkApp2 (mkConst ``Exists [u]) α (mkLambda n bi α (mkNot p))
+      let proof := mkApp3 (mkConst ``Grind.of_forall_eq_false [u]) α (mkLambda n bi α p) (← mkEqFalseProof e)
+      addNewFact proof prop (← getGeneration e)
+    else
+      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/Main.lean

@@ -30,7 +30,7 @@ def mkMethods (fallback : Fallback) : CoreM Methods := do
      if let some prop := builtinPropagators.up[declName]? then
        prop e
     propagateDown := fun e => do
-     propagateImpliesDown e
+     propagateForallPropDown e
      let .const declName _ := e.getAppFn | return ()
      if let some prop := builtinPropagators.down[declName]? then
        prop e
@@ -70,7 +70,7 @@ def all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List Goa
 
 /-- A very simple strategy -/
 private def simple (goals : List Goal) : GrindM (List Goal) := do
-  applyToAll (ematchStar >> (splitNext >> ematchStar).iterate) goals
+  applyToAll (assertAll >> ematchStar >> (splitNext >> assertAll >> ematchStar).iterate) goals
 
 def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List MVarId) := do
   let go : GrindM (List MVarId) := do

tests/lean/run/grind_cat.lean

@@ -122,4 +122,61 @@ def hcomp {H I : Functor D E} (α : F ⟶ G) (β : H ⟶ I) : F.comp H ⟶ G.com
   -- rw [Functor.comp_map, Functor.comp_map, ← assoc, naturality, assoc, ← I.map_comp, naturality,
   --   map_comp, assoc]
 
+structure Iso {C : Type u} [Category.{v} C] (X Y : C) where
+  hom : X ⟶ Y
+  inv : Y ⟶ X
+  hom_inv_id : hom ≫ inv = 𝟙 X := by cat_tac
+  inv_hom_id : inv ≫ hom = 𝟙 Y := by cat_tac
+
+attribute [grind =] Iso.hom_inv_id Iso.inv_hom_id
+
+/-- Notation for an isomorphism in a category. -/
+infixr:10 " ≅ " => Iso -- type as \cong or \iso
+
+variable {C : Type u} [Category.{v} C] {X Y Z : C}
+
+namespace Iso
+
+@[ext]
+theorem ext ⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β :=
+  suffices α.inv = β.inv by
+    cases α
+    cases β
+    cases w
+    cases this
+    rfl
+  calc
+    α.inv = α.inv ≫ β.hom ≫ β.inv   := by grind
+    _     = β.inv                    := by grind
+
+
+/-- `LeftInverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/
+def Function.LeftInverse (g : β → α) (f : α → β) : Prop :=
+  ∀ x, g (f x) = x
+
+/-- `RightInverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/
+def Function.RightInverse (g : β → α) (f : α → β) : Prop :=
+  LeftInverse f g
+
+open Function
+
+/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
+structure Equiv (α : Sort _) (β : Sort _) where
+  protected toFun : α → β
+  protected invFun : β → α
+  protected left_inv : LeftInverse invFun toFun
+  protected right_inv : RightInverse invFun toFun
+
+@[inherit_doc]
+infixl:25 " ≃ " => Equiv
+
+attribute [local grind] Function.LeftInverse in
+/-- The bijection `(Z ⟶ X) ≃ (Z ⟶ Y)` induced by `α : X ≅ Y`. -/
+def homToEquiv (α : X ≅ Y) {Z : C} : (Z ⟶ X) ≃ (Z ⟶ Y) where
+  toFun f := f ≫ α.hom
+  invFun g := g ≫ α.inv
+  left_inv := by cat_tac
+  right_inv := sorry
+
+end Iso
 end CategoryTheory