refactor: use match compilation to generate splitter (#11220)

This PR changes how match splitters are generated: Rather than rewriting
the match statement, the match compilation pipeline is used again.


The benefits are:

* Re-doing the match compilation means we can do more intelligent book
keeping, e.g. prove overlap assumptions only once and re-use the proof,
or prune the context of the MVar to speed up `contradiction`. This may
have allowed a different solution than #11200.
 
* It would unblock #11105, as the existing splitter implementation would
have trouble dealing with the matchers produced that way.
 
* It provides the necessary machinery also for source-exposed “none of
the above” bindings, a feature that we probably want at some point (and
we mostly need to find good syntax for, see #3136, although maybe I
should open a dedicated RFC).

* It allows us to skip costly things during matcher creation that would
only be useful for the splitter, and thus allows performance
improvements like #11508.
 
 * We can drop the existing implementation.
 
It’s not entirely free:

* We have to run `simpH` twice, once for the match equations and once
for the splitter.

Author: nomeata

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -8,10 +8,12 @@ module
 prelude
 public import Lean.Elab.PreDefinition.FixedParams
 import Lean.Elab.PreDefinition.EqnsUtils
-import Lean.Meta.Tactic.Split
+import Lean.Meta.Tactic.CasesOnStuckLHS
+import Lean.Meta.Tactic.Delta
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Delta
 import Lean.Meta.Tactic.CasesOnStuckLHS
+import Lean.Meta.Tactic.Split
 
 namespace Lean.Elab
 open Meta

src/Lean/Meta/Constructions/CasesOnSameCtor.lean

@@ -213,7 +213,9 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit :=
           numDiscrs := info.numIndices + 3
           altInfos
           uElimPos? := some 0
-          discrInfos := #[{}, {}, {}]}
+          discrInfos := #[{}, {}, {}]
+          overlaps := {}
+        }
 
         -- Compare attributes with `mkMatcherAuxDefinition`
         withExporting (isExporting := !isPrivateName declName) do

src/Lean/Meta/IndPredBelow.lean

@@ -319,7 +319,7 @@ public partial def mkBelowMatcher (matcherApp : MatcherApp) (belowParams : Array
     (ctx : RecursionContext) (transformAlt : RecursionContext → Expr → MetaM Expr) :
     MetaM (Option (Expr × MetaM Unit)) :=
   withTraceNode `Meta.IndPredBelow.match (return m!"{exceptEmoji ·} {matcherApp.toExpr} and {belowParams}") do
-  let mut input ← getMkMatcherInputInContext matcherApp
+  let mut input ← getMkMatcherInputInContext matcherApp (unfoldNamed := false)
   let mut discrs := matcherApp.discrs
   let mut matchTypeAdd := #[] -- #[(discrIdx, ), ...]
   let mut i := discrs.size

src/Lean/Meta/Match/Basic.lean

@@ -150,6 +150,11 @@ structure Alt where
   After we perform additional case analysis, their types become definitionally equal.
   -/
   cnstrs    : List (Expr × Expr)
+  /--
+  Indices of previous alternatives that this alternative expects a not-that-proofs.
+  (When producing a splitter, and in the future also for source-level overlap hypotheses.)
+  -/
+  notAltIdxs : Array Nat
   deriving Inhabited
 
 namespace Alt

src/Lean/Meta/Match/Match.lean

@@ -67,6 +67,7 @@ def matchMatcherApp? [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCases
         matcherName   := declName
         matcherLevels := declLevels.toArray
         uElimPos?, discrInfos, params, motive, discrs, alts, remaining, altInfos
+        overlaps := {} -- CasesOn constructor have no overlaps
       }
 
   return none

src/Lean/Meta/Match/MatchEqs.lean

@@ -23,6 +23,9 @@ structure Overlaps where
   map : Std.HashMap Nat (Std.TreeSet Nat) := {}
 deriving Inhabited, Repr
 
+def Overlaps.isEmpty (o : Overlaps) : Bool :=
+  o.map.isEmpty
+
 def Overlaps.insert (o : Overlaps) (overlapping overlapped : Nat) : Overlaps where
   map := o.map.alter overlapped fun s? => some ((s?.getD {}).insert overlapping)
 
@@ -41,29 +44,32 @@ structure AltParamInfo where
   numOverlaps : Nat
   /-- Whether this alternatie has an artifcial `Unit` parameter -/
   hasUnitThunk : Bool
-deriving Inhabited, Repr
+deriving Inhabited, Repr, BEq
 
 /--
-A "matcher" auxiliary declaration has the following structure:
-- `numParams` parameters
-- motive
-- `numDiscrs` discriminators (aka major premises)
-- `altInfos.size` alternatives (aka minor premises) with parameter structure information
-- `uElimPos?` is `some pos` when the matcher can eliminate in different universe levels, and
-   `pos` is the position of the universe level parameter that specifies the elimination universe.
-   It is `none` if the matcher only eliminates into `Prop`.
-- `overlaps` indicates which alternatives may overlap another
+Information about the structure of a matcher declaration
 -/
 structure MatcherInfo where
+  /-- Number of parameters -/
   numParams    : Nat
+  /-- Number of discriminants -/
   numDiscrs    : Nat
+  /-- Parameter structure information for each alternative -/
   altInfos     : Array AltParamInfo
+  /--
+  `uElimPos?` is `some pos` when the matcher can eliminate in different universe levels, and
+  `pos` is the position of the universe level parameter that specifies the elimination universe.
+  It is `none` if the matcher only eliminates into `Prop`.
+  -/
   uElimPos?    : Option Nat
   /--
-    `discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`.
+  `discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`.
   -/
   discrInfos   : Array DiscrInfo
-  overlaps     : Overlaps := {}
+  /--
+  (Conservative approximation of) which alternatives may overlap another.
+  -/
+  overlaps     : Overlaps
 deriving Inhabited, Repr
 
 @[expose] def MatcherInfo.numAlts (info : MatcherInfo) : Nat :=

src/Lean/Meta/Match/MatcherApp/Basic.lean

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

src/Lean/Meta/Match/MatcherInfo.lean

@@ -38,8 +38,8 @@ info: Vec.match_on_same_ctor.{u_1, u} {α : Type u}
 /--
 info: Vec.match_on_same_ctor.splitter.{u_1, u} {α : Type u}
   {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} {a✝ : Nat} (t t✝ : Vec α a✝)
-  (h : t.ctorIdx = t✝.ctorIdx) (h_1 : Unit → motive nil nil ⋯)
-  (h_2 : (a : α) → (n : Nat) → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
+  (h : t.ctorIdx = t✝.ctorIdx) (nil : Unit → motive nil nil ⋯)
+  (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
   motive t t✝ h
 -/
 #guard_msgs in