feat: missing normalization rules in grind (#8413)

This PR implements normalization rules that pull universal quantifiers
across disjunctions. This is a common normalization step performed by
first-order theorem provers.

Author: leodemoura

src/Init/Grind/Norm.lean

@@ -104,6 +104,26 @@ theorem flip_bool_eq (a b : Bool) : (a = b) = (b = a) := by
 theorem bool_eq_to_prop (a b : Bool) : (a = b) = ((a = true) = (b = true)) := by
   simp
 
+theorem forall_or_forall {α : Sort u} {β : α → Sort v} (p : α → Prop) (q : (a : α) → β a → Prop)
+    : (∀ a : α, p a ∨ ∀ b : β a, q a b) =
+      (∀ (a : α) (b : β a), p a ∨ q a b) := by
+  apply propext; constructor
+  · intro h a b; cases h a <;> simp [*]
+  · intro h a
+    apply Classical.byContradiction
+    intro h'; simp at h'; have ⟨h₁, b, h₂⟩ := h'
+    replace h := h a b; simp [h₁, h₂] at h
+
+theorem forall_forall_or {α : Sort u} {β : α → Sort v} (p : α → Prop) (q : (a : α) → β a → Prop)
+    : (∀ a : α, (∀ b : β a, q a b) ∨ p a) =
+      (∀ (a : α) (b : β a), q a b ∨ p a) := by
+  apply propext; constructor
+  · intro h a b; cases h a <;> simp [*]
+  · intro h a
+    apply Classical.byContradiction
+    intro h'; simp at h'; have ⟨⟨b, h₁⟩, h₂⟩ := h'
+    replace h := h a b; simp [h₁, h₂] at h
+
 init_grind_norm
   /- Pre theorems -/
   not_and not_or not_ite not_forall not_exists
@@ -113,6 +133,7 @@ init_grind_norm
   /- Post theorems -/
   Classical.not_not
   ne_eq iff_eq eq_self heq_eq_eq
+  forall_or_forall forall_forall_or
   -- Prop equality
   eq_true_eq eq_false_eq not_eq_prop
   -- True

tests/lean/run/grind_palindrome2.lean

@@ -25,13 +25,4 @@ theorem checkPalin1_correct' : checkPalin1 xs = true ↔ IsPalindrome xs := by
     -- TODO: `IsPalindrome` (without `.eq_1`) produces bad error message.
     grind +extAll [IsPalindrome.eq_1]
   intro i
-  fun_induction checkPalin1.go
-  case case1 j h₁ h₂ ih =>
-    -- TODO: make sure we don't need `constructor` here. This is a normalization issue.
-    constructor <;> grind
-  case case2 j h₁ h₂ =>
-    -- TODO: fix normalization
-    simp only [Bool.false_eq_true, false_iff, Classical.not_forall]
-    grind
-  case case3 x h =>
-    grind
+  fun_induction checkPalin1.go <;> grind

tests/lean/run/grind_t1.lean

@@ -439,3 +439,21 @@ example [BEq α] [LawfulBEq α] (a b : α) : a ≠ b → foo a b = 0 := by
 
 example (p q : Prop) : (p → q) → (¬ p → q) → (p → ¬ q) → (¬p → ¬q) → False := by
   grind (splitImp := true)
+
+
+/-! Pull universal over disjunction -/
+
+opaque p : (i : Nat) → i ≠ 10 → Prop
+
+-- This example does not require pulling quantifiers
+example (h : ∀ i, i > 0 → ∀ h : i ≠ 10, p i h) : p 5 (by decide) := by
+  grind
+
+-- This one is semantically equivalent to the previous example, but can only be proved by `grind` after
+-- we pull universal over disjunctions during normalization.
+example (h : ∀ i, (¬i > 0) ∨ ∀ h : i ≠ 10, p i h) : p 5 (by decide) := by
+  grind
+
+-- Similar to previous test.
+example (h : ∀ i, (∀ h : i ≠ 10, p i h) ∨ (¬i > 0)) : p 5 (by decide) := by
+  grind