fix: more robust match equation generation

[nomeata]

This PR performs a large refactoring to how match equations are generated, to fix issues like #11342 (which would arise more frequently once we have #11105).

When proving a matcher equation, we previously could encounter casesOn that do not reduce right away (it is not applied to a constructor), and that we thus want to split. But splitting can be blocked when the scrutinee is not a free variable, which can be the case when this target is also the index of a later target, see #11342.

A more robust approach is to first prove the “congruence equation” from #8284, where the arguments to the matcher are free variables, and the information that these arguments are actually equal to the current pattern is put into hypotheses. In this form, we should be able to reliably split the match into all its branches, avoiding the issue above. At each branch there are three possibilities:

• We are in the right branch. We may need to substitute some variable and apply injection to the assumed assumption to unify the goal, and then are done. This can be handled by a (restrictively configured) call to grind, now that grind handles heterogeneous equality between constructors better (feat: heterogeneous contructor injectivity in grind #11491).

• We are in a wrong branch and the patterns do not unify. Then we should have a (possibly heterogeneous) equality between different constructors somewhere in the context, and grind can handle it.

• We are in a wrong branch and it’s overlapping the one we care about. Then there should be a no-overlap assumption in the context, and we need to use that. The code for that exists in contradiction { genDiseq := true }.

  This could be made more surgical if instead of using contradiction we use some bookkeeping or makers for the overlap assumptions to know which one to belongs to which arm, and use it directly.

This is a more expensive approach than the current one, which can avoid many case splits. However it only affects equations that are not by rfl anyways, so the common case is unaffected. Therefore I decided the performance hit in the rarer overlapping is worth the uniformity and the robustness in the code (as opposed to, say, keeping the old code around).

It should be possible to (later, when needed) regain some of the performance loss by, before splitting, search the context for equalities between the scrutinee and a constructor, and use the per-constructor elimination form to avoid the unreachable branches directly.

To avoid bootstrapping problems, when compiling core grind is not used, but instead a naive eager injectivity-applying tactic similar to solveOverlap is used. This is neither fast nor complete, but good enough for Core (where there are no larger matches and no tricky dependencies). The flag bootstrap.grindInMatchEqns can be used to trigger this.

The flag debug.Meta.Match.MatchEqs.unrestrictedGrind switches grind to the default configuration. This can be used to test if the restricted configuration is the reason for a failing match compliation.

Fixes #11342.

[nomeata]

Just a note to future myself:

The next issue is that during proveCondEqThm we want the overlap assumptions to be applied to the abstract discrs, but the final theorem needs them applied to the concrete pattern and simpHlified, to match the splitter and be convenient.

This requires a bit of refactoring, and in particular simpH needs to return an actual proof of equivalence between the two (possibly only since this week since #11474).

[nomeata]

!radar

[leanprover-radar]

Benchmark results for 6c0bbc8 against 95a7c76 are in! @nomeata

Major changes (3)

• 🟥 Init.Data.List.Basic re-elab//instructions: +2.0G (+1.1%)
• 🟥 big_match_nat_split//instructions: +3.1G (+24.9%)
• 🟥 big_match_partial//instructions: +4.8G (+26.0%)

Minor changes (1)

• 🟥 size/init/.olean//bytes: +352kiB (+0.4%)