feat: add splitter theorem

src/Lean/Meta/Match/MatchEqs.lean

@@ -10,6 +10,8 @@ import Lean.Meta.Tactic.SplitIf
 
 namespace Lean.Meta.Match
 
+-- TODO enviroment extension for caching conditional equation lemmas and splitter for match auxiliary declarations.
+
 private def isMatchValue (e : Expr) : Bool :=
   e.isNatLit || e.isCharLit || e.isStringLit
 
@@ -125,7 +127,7 @@ where
 
 
 /-- Construct new local declarations `xs` with types `altTypes`, and then execute `f xs`  -/
-private partial def withElimAlts (altTypes : Array Expr) (f : Array Expr → MetaM α) : MetaM α := do
+private partial def withSplitterAlts (altTypes : Array Expr) (f : Array Expr → MetaM α) : MetaM α := do
   let rec go (i : Nat) (xs : Array Expr) : MetaM α := do
     if h : i < altTypes.size then
       let hName := (`h).appendIndexAfter (i+1)
@@ -136,21 +138,26 @@ private partial def withElimAlts (altTypes : Array Expr) (f : Array Expr → Met
   go 0 #[]
 
 /--
-  Construct a proof for the elimination principle generated by `mkEquationsfor`.
+  Construct a proof for the splitter generated by `mkEquationsfor`.
   The proof uses the definition of the `match`-declaration as a template (argument `template`).
   - `alts` are free variables corresponding to alternatives of the `match` auxiliary declaration being processed.
   - `altNews` are the new free variables which contains aditional hypotheses that ensure they are only used
      when the previous overlapping alternatives are not applicable. -/
-private partial def mkElimProof (template : Expr) (alts altsNew : Array Expr) : MetaM Expr := do
+private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (alts altsNew : Array Expr) : MetaM Expr := do
   trace[Meta.Match.matchEqs] "proof template: {template}"
   let map := mkMap
   let (proof, mvarIds) ← convertTemplate map |>.run #[]
-  trace[Meta.Match.matchEqs] "elim proof: {proof}"
+  trace[Meta.Match.matchEqs] "splitter proof: {proof}"
   for mvarId in mvarIds do
-    trace[Meta.Match.matchEqs] "elim subgoal:\n{MessageData.ofGoal mvarId}"
-    -- TODO: close goal `mvarId`
-  check proof -- TODO remove
-  return proof
+    trace[Meta.Match.matchEqs] "subgoal {mkMVar mvarId}, {repr (← getMVarDecl mvarId).kind}, {← isExprMVarAssigned mvarId}\n{MessageData.ofGoal mvarId}"
+    let (_, mvarId) ← intros mvarId
+    let mvarId ← tryClearMany mvarId (alts.map (·.fvarId!))
+    unless (← contradictionCore mvarId {}) do
+      -- TODO
+      trace[Meta.Match.matchEqs] "failed to generate splitter, unsolved subgoal\n{MessageData.ofGoal mvarId}"
+      admit mvarId
+      -- throwError "failed to generate splitter for match auxiliary declaration '{matchDeclName}', unsolved subgoal:\n{MessageData.ofGoal mvarId}"
+  instantiateMVars proof
 where
   mkMap : NameMap Expr := do
     let mut m := {}
@@ -186,14 +193,14 @@ where
 
   addExtraParams (e : Expr) : StateRefT (Array MVarId) MetaM Expr := do
     trace[Meta.Match.matchEqs] "addExtraParams {e}"
-    let (mvars, _, _) ← forallMetaTelescope (← inferType e) (kind := MetavarKind.syntheticOpaque)
+    let (mvars, _, _) ← forallMetaTelescopeReducing (← inferType e) (kind := MetavarKind.syntheticOpaque)
     modify fun s => s ++ (mvars.map (·.mvarId!))
     return mkAppN e mvars
 
 /--
-  Create conditional equations and elimination principle for the given
-  match auxiliary declaration. -/
+  Create conditional equations and splitter for the given match auxiliary declaration. -/
 partial def mkEquationsFor (matchDeclName : Name) :  MetaM Unit := do
+  -- TODO: do not assume `mkEquationsFor` was not already generated
   let constInfo ← getConstInfo matchDeclName
   let us := constInfo.levelParams.map mkLevelParam
   let some matchInfo ← getMatcherInfo? matchDeclName | throwError "'{matchDeclName}' is not a matcher function"
@@ -205,11 +212,11 @@ partial def mkEquationsFor (matchDeclName : Name) :  MetaM Unit := do
     let discrs := xs[firstDiscrIdx : firstDiscrIdx + matchInfo.numDiscrs]
     let mut notAlts := #[]
     let mut idx := 1
-    let mut elimAltTypes := #[]
+    let mut splitterAltTypes := #[]
     for alt in alts do
       let altType ← inferType alt
       trace[Meta.debug] ">> {altType}"
-      let (notAlt, elimAltType) ← forallTelescopeReducing altType fun ys altResultType => do
+      let (notAlt, splitterAltType) ← forallTelescopeReducing altType fun ys altResultType => do
         let (ys, rhsArgs) ← toFVarsRHSArgs ys altResultType
         let patterns := altResultType.getAppArgs
         let mut hs := #[]
@@ -217,7 +224,7 @@ partial def mkEquationsFor (matchDeclName : Name) :  MetaM Unit := do
           hs := hs.push (← instantiateForall notAlt patterns)
         hs ← simpHs hs patterns.size
         trace[Meta.Match.matchEqs] "hs: {hs}"
-        let elimAltType ← mkForallFVars ys (← hs.foldrM (init := altResultType) mkArrow)
+        let splitterAltType ← mkForallFVars ys (← hs.foldrM (init := altResultType) mkArrow)
         -- Create a proposition for representing terms that do not match `patterns`
         let mut notAlt := mkConst ``False
         for discr in discrs.toArray.reverse, pattern in patterns.reverse do
@@ -238,20 +245,26 @@ partial def mkEquationsFor (matchDeclName : Name) :  MetaM Unit := do
           type        := thmType
           value       := thmVal
         }
-        return (notAlt, elimAltType)
+        return (notAlt, splitterAltType)
       notAlts := notAlts.push notAlt
-      elimAltTypes := elimAltTypes.push elimAltType
-      trace[Meta.Match.matchEqs] "elimAltType: {elimAltType}"
+      splitterAltTypes := splitterAltTypes.push splitterAltType
+      trace[Meta.Match.matchEqs] "splitterAltType: {splitterAltType}"
       idx := idx + 1
-    -- Define eliminator with conditional/refined alternatives
-    withElimAlts elimAltTypes fun altsNew => do
-      let elimType ← mkForallFVars (params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew) matchResultType
-      trace[Meta.Match.matchEqs] "elimType: {elimType}"
+    -- Define splitter with conditional/refined alternatives
+    withSplitterAlts splitterAltTypes fun altsNew => do
+      let elimParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
+      let elimType ← mkForallFVars elimParams matchResultType
+      trace[Meta.Match.matchEqs] "splitterType: {elimType}"
       let template ← mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
       let template ← deltaExpand template (. == constInfo.name)
-      let elimVal ← mkElimProof template alts altsNew
-      -- TODO: construct value of type `elimType`
-      return ()
+      let elimVal ← mkLambdaFVars elimParams (← mkSplitterProof matchDeclName template alts altsNew)
+      let elimName := matchDeclName ++ `elim
+      addDecl <| Declaration.thmDecl {
+        name        := elimName
+        levelParams := constInfo.levelParams
+        type        := elimType
+        value       := elimVal
+      }
 
 builtin_initialize registerTraceClass `Meta.Match.matchEqs