feat: enable new E-matching pattern inference procedure in grind (#10432)

This PR enables the new E-matching pattern inference heuristic for
`grind`, implemented in PR #10422.
**Important**: Users can still use the old pattern inference heuristic
by setting:

```lean
set_option backward.grind.inferPattern true
```

In PR #10422, we introduced the new modifier `@[grind!]` for enabling
the minimal indexable subexpression condition. This option can now also
be set in `grind` parameters. Example:

```lean
opaque f : Nat → Nat
opaque fInv : Nat → Nat 
axiom fInv_f : fInv (f x) = x

/-- trace: [grind.ematch.pattern] fInv_f: [f #0] -/
#guard_msgs in 
set_option trace.grind.ematch.pattern true in
example {x y} : f x = f y → x = y := by
  /-
  The modifier `!` instructs `grind` to use the minimal indexable subexpression 
  (i.e., `f x` in this case).   
  -/
  grind [!fInv_f] 
```

src/Init/Data/Vector/Attach.lean

@@ -193,7 +193,7 @@ theorem attachWith_map_subtype_val {p : α → Prop} {xs : Vector α n} (H : ∀
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind]
+@[simp, grind ←]
 theorem mem_attach (xs : Vector α n) : ∀ x, x ∈ xs.attach
   | ⟨a, h⟩ => by
     have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)

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

@@ -1176,7 +1176,7 @@ where
     | _ => return ()
 
 register_builtin_option backward.grind.inferPattern : Bool := {
-  defValue := true
+  defValue := false
   group    := "backward compatibility"
   descr    := "use old E-matching pattern inference"
 }

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Josh Clune
 -/
 module
-
 prelude
 public import Init.Data.List.Erase
 public import Init.Data.Array.Lemmas
@@ -13,7 +12,6 @@ public import Std.Sat.CNF.Basic
 public import Std.Tactic.BVDecide.LRAT.Internal.PosFin
 public import Std.Tactic.BVDecide.LRAT.Internal.Assignment
 public import Init.Grind
-
 @[expose] public section
 
 namespace Std.Tactic.BVDecide
@@ -61,7 +59,8 @@ namespace Clause
 
 grind_pattern empty_eq => toList (empty : β)
 grind_pattern unit_eq => @toList _ _ self (unit l)
-attribute [grind] isUnit_iff negate_eq delete_iff contains_iff
+attribute [grind =] isUnit_iff negate_eq delete_iff
+attribute [grind ←] contains_iff
 
 instance : Entails α (Literal α) where
   eval := fun p l => p l.1 = l.2
@@ -108,7 +107,7 @@ namespace DefaultClause
 
 @[grind] def toList (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause
 
-attribute [local grind] DefaultClause.nodup DefaultClause.nodupkey
+attribute [local grind! ←] DefaultClause.nodup DefaultClause.nodupkey
 
 theorem not_tautology (c : DefaultClause n) (l : Literal (PosFin n)) :
     l ∉ toList c ∨ ¬Literal.negate l ∈ toList c := by
@@ -160,7 +159,7 @@ theorem negate_eq (c : DefaultClause n) : negate c = (toList c).map Literal.nega
 attribute [local grind] DefaultClause.ofArray.folder
 
 -- This isn't a good global `grind` lemma, because it can cause a loop with `Pairwise.sublist`.
-attribute [local grind] List.pairwise_iff_forall_sublist
+attribute [local grind =] List.pairwise_iff_forall_sublist
 
 def ofArray (ls : Array (Literal (PosFin n))) : Option (DefaultClause n) :=
   let mapOption := ls.foldl ofArray.folder (some (HashMap.emptyWithCapacity ls.size))
@@ -174,14 +173,14 @@ def ofArray (ls : Array (Literal (PosFin n))) : Option (DefaultClause n) :=
 theorem ofArray.foldl_folder_none_eq_none : List.foldl ofArray.folder none ls = none := by
   apply List.foldlRecOn (motive := (· = none)) <;> grind
 
-attribute [local grind] ofArray.foldl_folder_none_eq_none
+attribute [local grind =] ofArray.foldl_folder_none_eq_none
 
 theorem ofArray.mem_of_mem_of_foldl_folder_eq_some
     (h : List.foldl DefaultClause.ofArray.folder (some acc) ls = some acc') (l) (h : l ∈ acc.toList) :
       l ∈ acc'.toList := by
   induction ls generalizing acc with grind
 
-attribute [local grind] ofArray.mem_of_mem_of_foldl_folder_eq_some
+grind_pattern ofArray.mem_of_mem_of_foldl_folder_eq_some => l ∈ acc'.toList, List.foldl ofArray.folder (some acc) ls
 
 theorem ofArray.folder_foldl_mem_of_mem
     (h : List.foldl DefaultClause.ofArray.folder acc ls = some map) :
@@ -191,8 +190,7 @@ theorem ofArray.folder_foldl_mem_of_mem
   | nil => grind
   | cons x xs ih =>
     simp at hl h
-    rw [DefaultClause.ofArray.folder.eq_def] at h -- TODO why doesn't `grind` handle this?
-    rcases hl <;> grind
+    rcases hl <;> grind [DefaultClause.ofArray.folder.eq_def]
 
 @[inline, local grind]
 def delete (c : DefaultClause n) (l : Literal (PosFin n)) : DefaultClause n where

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean

@@ -62,7 +62,8 @@ class Formula (α : outParam (Type u)) (β : outParam (Type v)) [Clause α β] (
 
 open Formula
 
-attribute [grind] insert_iff delete_subset
+attribute [grind =] insert_iff
+attribute [grind →] delete_subset
 
 grind_pattern readyForRupAdd_insert => ReadyForRupAdd (insert f c)
 grind_pattern readyForRupAdd_delete => ReadyForRupAdd (delete f arr)

stage0/src/stdlib_flags.h

@@ -1,9 +1,11 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {
 options get_default_options() {
     options opts;
     // see https://github.com/leanprover/lean4/blob/master/doc/dev/bootstrap.md#further-bootstrapping-complications
+    opts = opts.update({"backward", "grind", "inferPattern"}, false);
 #if LEAN_IS_STAGE0 == 1
     // set to true to generally avoid bootstrapping issues limited to proofs
     opts = opts.update({"debug", "proofAsSorry"}, false);

tests/lean/run/grind_9610.lean

@@ -7,4 +7,4 @@ theorem foo (x: UInt32) :
 
 theorem aa (x : UInt32) :
   x.toNat ≤ sixteen.toNat := by
-  grind [foo]
+  grind [!foo]

tests/lean/run/grind_attrs.lean

@@ -31,19 +31,19 @@ axiom Expr.constProp : Expr → State → Expr
 /-- trace: [grind.ematch.pattern] eval_constProp_of_sub: [State.le #3 #2, constProp #1 #3] -/
 #guard_msgs (trace) in
 set_option trace.grind.ematch.pattern true in
-@[grind =>] theorem Expr.eval_constProp_of_sub (e : Expr) (h : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ :=
+@[grind! =>] theorem Expr.eval_constProp_of_sub (e : Expr) (h : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ :=
   sorry
 
 /-- trace: [grind.ematch.pattern] eval_constProp_of_eq_of_sub: [State.le #3 #2, constProp #1 #3] -/
 #guard_msgs (trace) in
 set_option trace.grind.ematch.pattern true in
-@[grind =>] theorem Expr.eval_constProp_of_eq_of_sub {e : Expr} (h₂ : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ :=
+@[grind! =>] theorem Expr.eval_constProp_of_eq_of_sub {e : Expr} (h₂ : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ :=
   sorry
 
 /-- trace: [grind.ematch.pattern] update_le_update: [le #4 #3, update #4 #2 #1] -/
 #guard_msgs (trace) in
 set_option trace.grind.ematch.pattern true in
-@[grind =>] theorem State.update_le_update (h : State.le σ' σ) : State.le (σ'.update x v) (σ.update x v) :=
+@[grind! =>] theorem State.update_le_update (h : State.le σ' σ) : State.le (σ'.update x v) (σ.update x v) :=
   sorry
 
 

tests/lean/run/grind_ctor_ematch.lean

@@ -69,6 +69,6 @@ attribute [grind] fax
 example : f (f (f x)) = f x := by
   grind
 
-/-- error: invalid E-matching theorem `Nat.succ`, type is not a proposition -/
+/-- error: invalid `grind` theorem, failed to find an usable pattern using different modifiers -/
 #guard_msgs in
 attribute [grind] Nat.succ

tests/lean/run/grind_eq_pattern.lean

@@ -6,14 +6,14 @@ trace: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppe
 -/
 #guard_msgs (trace) in
 set_option trace.grind.ematch.pattern true in
-attribute [grind] List.append_ne_nil_of_left_ne_nil
+attribute [grind ←] List.append_ne_nil_of_left_ne_nil
 
 /--
 trace: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #1 #2]
 -/
 #guard_msgs (trace) in
 set_option trace.grind.ematch.pattern true in
-attribute [grind] List.append_ne_nil_of_right_ne_nil
+attribute [grind ←] List.append_ne_nil_of_right_ne_nil
 /-- trace: [grind.ematch.pattern] List.getLast?_eq_some_iff: [@List.getLast? #2 #1, @some _ #0] -/
 #guard_msgs (trace) in
 set_option trace.grind.ematch.pattern true in

tests/lean/run/grind_try_trace.lean

@@ -202,7 +202,7 @@ info: Try these:
   • fun_induction bla <;> simp_all
   • fun_induction bla <;> simp [*]
   • fun_induction bla <;> simp only [List.length_reverse, *]
-  • fun_induction bla <;> grind only [List.length_reverse]
+  • fun_induction bla <;> grind only [= List.length_reverse]
 -/
 #guard_msgs (info) in
 example : (bla xs ys).length = ys.length := by

tests/lean/run/grind_usr.lean

@@ -12,7 +12,7 @@ public theorem fthm : f (f x) = f x := sorry
 #guard_msgs (trace) in
 set_option trace.grind.ematch.pattern true in
 example : f (f (f x)) = f x := by
-  grind only [fthm]
+  grind only [!fthm]
 
 /--
 trace: [grind.ematch.instance] fthm: f (f x) = f x
@@ -22,7 +22,7 @@ trace: [grind.ematch.instance] fthm: f (f x) = f x
 #guard_msgs (trace) in
 set_option trace.grind.ematch.instance true in
 example : f (f (f x)) = f x := by
-  grind only [fthm]
+  grind only [!fthm]
 
 /--
 trace: [grind.ematch.instance] fthm: f (f x) = f x
@@ -32,7 +32,7 @@ trace: [grind.ematch.instance] fthm: f (f x) = f x
 -- should not instantiate anything using pattern `f (f #0)`
 set_option trace.grind.ematch.instance true in
 example : f x = x := by
-  fail_if_success grind only [fthm]
+  fail_if_success grind only [!fthm]
   sorry
 
 /--
@@ -68,7 +68,7 @@ trace: [grind.ematch.instance] fthm: f (f x) = f x
 #guard_msgs (trace) in
 set_option trace.grind.ematch.instance true in
 example : f x = x := by
-  fail_if_success grind only [fthm]
+  fail_if_success grind only [!fthm]
   sorry
 
 /--