feat: add support for splitting on <-> to grind

src/Init/Grind/Lemmas.lean

@@ -66,6 +66,12 @@ theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by s
 theorem eq_congr  {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) : (a₁ = b₁) = (a₂ = b₂) := by simp [*]
 theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) : (a₁ = b₁) = (a₂ = b₂) := by rw [h₁, h₂, Eq.comm (a := a₂)]
 
+/- The following two helper theorems are used to case-split `a = b` representing `iff`. -/
+theorem of_eq_eq_true {a b : Prop} (h : (a = b) = True) : (¬a ∨ b) ∧ (¬b ∨ a) := by
+  by_cases a <;> by_cases b <;> simp_all
+theorem of_eq_eq_false {a b : Prop} (h : (a = b) = False) : (¬a ∨ ¬b) ∧ (b ∨ a) := by
+  by_cases a <;> by_cases b <;> simp_all
+
 /-! Forall -/
 
 theorem forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = True) (h₂ : q (of_eq_true h₁) = q') : (∀ hp : p, q hp) = q' := by

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

@@ -217,14 +217,22 @@ def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
 where
   go (p : Expr) (isNeg : Bool) : GoalM Unit := do
     match_expr p with
-    | Eq _ lhs rhs => goEq p lhs rhs isNeg false
-    | HEq _ lhs _ rhs => goEq p lhs rhs isNeg true
-    | _ =>
-      internalize p generation
-      if isNeg then
-        addEq p (← getFalseExpr) (← mkEqFalse proof)
+    | Eq α lhs rhs =>
+      if α.isProp then
+        -- It is morally an iff.
+        -- We do not use the `goEq` optimization because we want to register `p` as a case-split
+        goFact p isNeg
       else
-        addEq p (← getTrueExpr) (← mkEqTrue proof)
+        goEq p lhs rhs isNeg false
+    | HEq _ lhs _ rhs => goEq p lhs rhs isNeg true
+    | _ => goFact p isNeg
+
+  goFact (p : Expr) (isNeg : Bool) : GoalM Unit := do
+    internalize p generation
+    if isNeg then
+      addEq p (← getFalseExpr) (← mkEqFalse proof)
+    else
+      addEq p (← getTrueExpr) (← mkEqTrue proof)
 
   goEq (p : Expr) (lhs rhs : Expr) (isNeg : Bool) (isHEq : Bool) : GoalM Unit := do
     if isNeg then

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

@@ -53,12 +53,20 @@ private def addSplitCandidate (e : Expr) : GoalM Unit := do
 -- TODO: add attribute to make this extensible
 private def forbiddenSplitTypes := [``Eq, ``HEq, ``True, ``False]
 
+/-- Returns `true` if `e` is of the form `@Eq Prop a b` -/
+def isMorallyIff (e : Expr) : Bool :=
+  let_expr Eq α _ _ := e | false
+  α.isProp
+
 /-- Inserts `e` into the list of case-split candidates if applicable. -/
 private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
   unless e.isApp do return ()
   if (← getConfig).splitIte && (e.isIte || e.isDIte) then
     addSplitCandidate e
     return ()
+  if isMorallyIff e then
+    addSplitCandidate e
+    return ()
   if (← getConfig).splitMatch then
     if (← isMatcherApp e) then
       if let .reduced _ ← reduceMatcher? e then

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

@@ -39,6 +39,11 @@ private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
         return .ready
     else
       return .notReady
+  | Eq _ _ _ =>
+    if (← isEqTrue e <||> isEqFalse e) then
+      return .ready
+    else
+      return .notReady
   | ite _ c _ _ _ =>
     if (← isEqTrue c <||> isEqFalse c) then
       return .resolved
@@ -94,6 +99,11 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
   | And a b => return mkApp3 (mkConst ``Grind.or_of_and_eq_false) a b (← mkEqFalseProof c)
   | ite _ c _ _ _ => return mkEM c
   | dite _ c _ _ _ => return mkEM c
+  | Eq _ a b =>
+    if (← isEqTrue c) then
+      return mkApp3 (mkConst ``Grind.of_eq_eq_true) a b (← mkEqTrueProof c)
+    else
+      return mkApp3 (mkConst ``Grind.of_eq_eq_false) a b (← mkEqFalseProof c)
   | _ => return mkApp2 (mkConst ``of_eq_true) c (← mkEqTrueProof c)
 
 /-- Introduces new hypotheses in each goal. -/

tests/lean/run/grind_implies.lean

@@ -28,10 +28,13 @@ example (p q : Prop) : (p → q) → ¬q → ¬p := by
   grind
 
 /--
-info: [grind.internalize] p → q
+info: [grind.internalize] (p → q) = r
+[grind.internalize] Prop
+[grind.internalize] p → q
 [grind.internalize] p
 [grind.internalize] q
 [grind.internalize] r
+[grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] p = False
 [grind.eqc] (p → q) = True
@@ -43,10 +46,13 @@ example (p q : Prop) : (p → q) = r → ¬p → r := by
 
 
 /--
-info: [grind.internalize] p → q
+info: [grind.internalize] (p → q) = r
+[grind.internalize] Prop
+[grind.internalize] p → q
 [grind.internalize] p
 [grind.internalize] q
 [grind.internalize] r
+[grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] q = True
 [grind.eqc] (p → q) = True
@@ -57,10 +63,13 @@ example (p q : Prop) : (p → q) = r → q → r := by
   grind
 
 /--
-info: [grind.internalize] p → q
+info: [grind.internalize] (p → q) = r
+[grind.internalize] Prop
+[grind.internalize] p → q
 [grind.internalize] p
 [grind.internalize] q
 [grind.internalize] r
+[grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] q = False
 [grind.eqc] r = True
@@ -72,10 +81,13 @@ example (p q : Prop) : (p → q) = r → ¬q → r → ¬p := by
   grind
 
 /--
-info: [grind.internalize] p → q
+info: [grind.internalize] (p → q) = r
+[grind.internalize] Prop
+[grind.internalize] p → q
 [grind.internalize] p
 [grind.internalize] q
 [grind.internalize] r
+[grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] q = False
 [grind.eqc] r = False

tests/lean/run/grind_pre.lean

@@ -86,13 +86,28 @@ example (p : Prop) (a b c : Nat) : p → a = 0 → a = b → h a = h c → a = c
 set_option trace.grind.debug.proof true
 /--
 error: `grind` failed
-case grind
+case grind.1
+α : Type
+a : α
+p q r : Prop
+h₁ : HEq p a
+h₂ : HEq q a
+h₃ : p = r
+left : ¬p ∨ r
+right : ¬r ∨ p
+h : ¬r
+⊢ False
+
+case grind.2
 α : Type
 a : α
 p q r : Prop
 h₁ : HEq p a
 h₂ : HEq q a
 h₃ : p = r
+left : ¬p ∨ r
+right : ¬r ∨ p
+h : p
 ⊢ False
 -/
 #guard_msgs (error) in

tests/lean/run/grind_t1.lean

@@ -213,3 +213,15 @@ example (P Q R : α → Prop) (h₁ : ∀ x, Q x → P x) (h₂ : ∀ x, R x →
 
 example (w : Nat → Type) (h : ∀ n, Subsingleton (w n)) : True := by
   grind
+
+example {P1 P2 : Prop} : (P1 ∧ P2) ↔ (P2 ∧ P1) := by
+  grind
+
+example {P U V W : Prop} (h : P ↔ (V ↔ W)) (w : ¬ U ↔ V) : ¬ P ↔ (U ↔ W) := by
+  grind (splits := 6)
+
+example {P Q : Prop} (q : Q) (w : P = (P = ¬ Q)) : False := by
+  grind
+
+example (P Q : Prop) : (¬P → ¬Q) ↔ (Q → P) := by
+  grind