feat: generalized Option theorems for grind (#8572)

This PR adds some generalized `Option` theorems for `grind` . The avoid
`casts` operations during E-matching.

src/Init/Data/Option/Lemmas.lean

@@ -1163,8 +1163,11 @@ end ite
 
 /-! ### pbind -/
 
-@[simp, grind] theorem pbind_none : pbind none f = none := rfl
-@[simp, grind] theorem pbind_some : pbind (some a) f = f a rfl := rfl
+@[simp] theorem pbind_none : pbind none f = none := rfl
+@[simp] theorem pbind_some : pbind (some a) f = f a rfl := rfl
+
+@[grind = gen] theorem pbind_none' (h : x = none) : pbind x f = none := by subst h; rfl
+@[grind = gen] theorem pbind_some' (h : x = some a) : pbind x f = f a h := by subst h; rfl
 
 @[simp, grind] theorem map_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
     {g : β → γ} : (o.pbind f).map g = o.pbind (fun a h => (f a h).map g) := by
@@ -1227,12 +1230,18 @@ theorem get_pbind {o : Option α} {f : (a : α) → o = some a → Option β} {h
 
 /-! ### pmap -/
 
-@[simp, grind] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+@[simp] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f none h = none := rfl
 
-@[simp, grind] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+@[simp] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f (some a) h = some (f a (h a rfl)) := rfl
 
+@[grind = gen] theorem pmap_none' {p : α → Prop} {f : ∀ (a : α), p a → β} (he : x = none) {h} :
+    pmap f x h = none := by subst he; rfl
+
+@[grind = gen] theorem pmap_some' {p : α → Prop} {f : ∀ (a : α), p a → β} (he : x = some a) {h} :
+    pmap f x h = some (f a (h a he)) := by subst he; rfl
+
 @[simp] theorem pmap_eq_none_iff {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f o h = none ↔ o = none := by
   cases o <;> simp
@@ -1315,8 +1324,11 @@ theorem get_pmap {p : α → Bool} {f : (x : α) → p x → β} {o : Option α}
 
 /-! ### pelim -/
 
-@[simp, grind] theorem pelim_none : pelim none b f = b := rfl
-@[simp, grind] theorem pelim_some : pelim (some a) b f = f a rfl := rfl
+@[simp] theorem pelim_none : pelim none b f = b := rfl
+@[simp] theorem pelim_some : pelim (some a) b f = f a rfl := rfl
+
+@[grind = gen] theorem pelim_none' (h : x = none) : pelim x b f = b := by subst h; rfl
+@[grind = gen] theorem pelim_some' (h : x = some a) : pelim x b f = f a h := by subst h; rfl
 
 @[simp] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
   cases o <;> simp

src/Init/Grind/Tactics.lean

@@ -8,6 +8,57 @@ module
 prelude
 import Init.Tactics
 
+namespace Lean.Grind
+/--
+Gadget for representing generalization steps `h : x = val` in patterns
+This gadget is used to represent patterns in theorems that have been generalized to reduce the
+number of casts introduced during E-matching based instantiation.
+
+For example, consider the theorem
+```
+Option.pbind_some {α1 : Type u_1} {a : α1} {α2 : Type u_2}
+    {f : (a_1 : α1) → some a = some a_1 → Option α2}
+    : (some a).pbind f = f a rfl
+```
+Now, suppose we have a goal containing the term `c.pbind g` and the equivalence class
+`{c, some b}`. The E-matching module generates the instance
+```
+(some b).pbind (cast ⋯ g)
+```
+The `cast` is necessary because `g`'s type contains `c` instead of `some b.
+This `cast` problematic because we don't have a systematic way of pushing casts over functions
+to its arguments. Moreover, heterogeneous equality is not effective because the following theorem
+is not provable in DTT:
+```
+theorem hcongr (h₁ : f ≍ g) (h₂ : a ≍ b)  : f a ≍ g b := ...
+```
+The standard solution is to generalize the theorem above and write it as
+```
+theorem Option.pbind_some'
+        {α1 : Type u_1} {a : α1} {α2 : Type u_2}
+        {x : Option α1}
+        {f : (a_1 : α1) → x = some a_1 → Option α2}
+        (h : x = some a)
+        : x.pbind f = f a h := by
+  subst h
+  apply Option.pbind_some
+```
+Internally, we use this gadget to mark the E-matching pattern as
+```
+(genPattern h x (some a)).pbind f
+```
+This pattern is matched in the same way we match `(some a).pbind f`, but it saves the proof
+for the actual term to the `some`-application in `f`, and the actual term in `x`.
+
+In the example above, `c.pbind g` also matches the pattern `(genPattern h x (some a)).pbind f`,
+and stores `c` in `x`, `b` in `a`, and the proof that `c = some b` in `h`.
+-/
+def genPattern {α : Sort u} (_h : Prop) (x : α) (_val : α) : α := x
+
+/-- Similar to `genPattern` but for the heterogenous case -/
+def genHEqPattern {α β : Sort u} (_h : Prop) (x : α) (_val : β) : α := x
+end Lean.Grind
+
 namespace Lean.Parser
 /--
 Reset all `grind` attributes. This command is intended for testing purposes only and should not be used in applications.

src/Init/Grind/Util.lean

@@ -32,55 +32,6 @@ def offset (a b : Nat) : Nat := a + b
 /-- Gadget for representing `a = b` in patterns for backward propagation. -/
 def eqBwdPattern (a b : α) : Prop := a = b
 
-/--
-Gadget for representing generalization steps `h : x = val` in patterns
-This gadget is used to represent patterns in theorems that have been generalized to reduce the
-number of casts introduced during E-matching based instantiation.
-
-For example, consider the theorem
-```
-Option.pbind_some {α1 : Type u_1} {a : α1} {α2 : Type u_2}
-    {f : (a_1 : α1) → some a = some a_1 → Option α2}
-    : (some a).pbind f = f a rfl
-```
-Now, suppose we have a goal containing the term `c.pbind g` and the equivalence class
-`{c, some b}`. The E-matching module generates the instance
-```
-(some b).pbind (cast ⋯ g)
-```
-The `cast` is necessary because `g`'s type contains `c` instead of `some b.
-This `cast` problematic because we don't have a systematic way of pushing casts over functions
-to its arguments. Moreover, heterogeneous equality is not effective because the following theorem
-is not provable in DTT:
-```
-theorem hcongr (h₁ : f ≍ g) (h₂ : a ≍ b)  : f a ≍ g b := ...
-```
-The standard solution is to generalize the theorem above and write it as
-```
-theorem Option.pbind_some'
-        {α1 : Type u_1} {a : α1} {α2 : Type u_2}
-        {x : Option α1}
-        {f : (a_1 : α1) → x = some a_1 → Option α2}
-        (h : x = some a)
-        : x.pbind f = f a h := by
-  subst h
-  apply Option.pbind_some
-```
-Internally, we use this gadget to mark the E-matching pattern as
-```
-(genPattern h x (some a)).pbind f
-```
-This pattern is matched in the same way we match `(some a).pbind f`, but it saves the proof
-for the actual term to the `some`-application in `f`, and the actual term in `x`.
-
-In the example above, `c.pbind g` also matches the pattern `(genPattern h x (some a)).pbind f`,
-and stores `c` in `x`, `b` in `a`, and the proof that `c = some b` in `h`.
--/
-def genPattern {α : Sort u} (_h : Prop) (x : α) (_val : α) : α := x
-
-/-- Similar to `genPattern` but for the heterogenous case -/
-def genHEqPattern {α β : Sort u} (_h : Prop) (x : α) (_val : β) : α := x
-
 /--
 Gadget for annotating the equalities in `match`-equations conclusions.
 `_origin` is the term used to instantiate the `match`-equation using E-matching.

tests/lean/run/grind_ematch_gen_pattern.lean

@@ -1,15 +1,25 @@
 set_option grind.warning false
-reset_grind_attrs%
-
-@[grind gen] theorem pbind_some' {α β} {x : Option α} {a : α} {f : (a : α) → x = some a → Option β}
-     (h : x = some a) : Option.pbind x f = f a h := by
-  subst h; rfl
 
 def f (x : Option Nat) (h : x ≠ none) : Nat :=
   match x with
   | none => by contradiction
   | some a => a
 
+-- The following should work out-of-the-box with `Option.pbind_some'
+example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
+  grind [f]
+
+/-- info: Try this: grind only [= gen Option.pbind_some', f, cases Or] -/
+#guard_msgs (info) in
+example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
+  grind? [f]
+
+reset_grind_attrs%
+
+@[grind gen] theorem pbind_some' {α β} {x : Option α} {a : α} {f : (a : α) → x = some a → Option β}
+     (h : x = some a) : Option.pbind x f = f a h := by
+  subst h; rfl
+
 example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
   grind only [gen pbind_some', f]