This PR implements the new E-matching pattern inference heuristic for
`grind`. It is not enabled yet. You can activate the new behavior using
`set_option backward.grind.inferPattern false`. Here is a summary of the
new behavior.
* `[grind =]`, `[grind =_]`, `[grind _=_]`, `[grind <-=]`: no changes;
we keep the current behavior.
* `[grind ->]`, `[grind <-]`, `[grind =>]`, `[grind <=]`: we stop using
the *minimal indexable subexpression* and instead use the first
indexable one.
* `[grind! <mod>]`: behaves like `[grind <mod>]` but uses the minimal
indexable subexpression restriction. We generate an error if the user
writes `[grind! =]`, `[grind! =_]`, `[grind! _=_]`, or `[grind! <-=]`,
since there is no pattern search in these cases.
* `[grind]`: it tries `=`, `=_`, `<-`, `->`, `<=`, `=>` with and without
the minimal indexable subexpression restriction. For the ones that work,
we generate a code action to encourage users to select the one they
prefer.
* `[grind!]`: it tries `<-`, `->`, `<=`, `=>` using the minimal
indexable subexpression restriction. For the ones that work, we generate
a code action to encourage users to select the one they prefer.
* `[grind? <mod>]`: where `<mod>` is one of the modifiers above, it
behaves like `[grind <mod>]` but also displays the pattern.
Example:
```lean
/--
info: Try these:
• [grind =] for pattern: [f (g #0)]
• [grind =_] for pattern: [r #0#0]
• [grind! ←] for pattern: [g #0]
-/
#guard_msgs in
@[grind] axiom fg₇ : f (g x) = r x x
```
efb398b040