feat: add procedure for solving subgoals generated by mkSplitterProof

src/Lean/Meta/Match/MatchEqs.lean

@@ -137,6 +137,27 @@ private partial def withSplitterAlts (altTypes : Array Expr) (f : Array Expr →
       f xs
   go 0 #[]
 
+inductive InjectionAnyResult where
+  | solved
+  | failed
+  | subgoal (mvarId : MVarId)
+
+private def injenctionAny (mvarId : MVarId) : MetaM InjectionAnyResult :=
+  withMVarContext mvarId do
+    for localDecl in (← getLCtx) do
+      if let some (_, lhs, rhs) ← matchEq? localDecl.type then
+        unless (← isDefEq lhs rhs) do
+          let lhs ← whnf lhs
+          let rhs ← whnf rhs
+          unless lhs.isNatLit && rhs.isNatLit do
+            try
+              match (← injection mvarId localDecl.fvarId) with
+              | InjectionResult.solved  => return InjectionAnyResult.solved
+              | InjectionResult.subgoal mvarId .. => return InjectionAnyResult.subgoal mvarId
+            catch _ =>
+              pure ()
+    return InjectionAnyResult.failed
+
 /--
   Construct a proof for the splitter generated by `mkEquationsfor`.
   The proof uses the definition of the `match`-declaration as a template (argument `template`).
@@ -149,14 +170,7 @@ private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (al
   let (proof, mvarIds) ← convertTemplate map |>.run #[]
   trace[Meta.Match.matchEqs] "splitter proof: {proof}"
   for mvarId in mvarIds do
-    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}"
+    proveSubgoal mvarId
   instantiateMVars proof
 where
   mkMap : NameMap Expr := do
@@ -197,6 +211,20 @@ where
     modify fun s => s ++ (mvars.map (·.mvarId!))
     return mkAppN e mvars
 
+  proveSubgoalLoop (mvarId : MVarId) : MetaM Unit := do
+    if (← contradictionCore mvarId {}) then
+      return ()
+    match (← injenctionAny mvarId) with
+    | InjectionAnyResult.solved => return ()
+    | InjectionAnyResult.failed => throwError "failed to generate splitter for match auxiliary declaration '{matchDeclName}', unsolved subgoal:\n{MessageData.ofGoal mvarId}"
+    | InjectionAnyResult.subgoal mvarId => proveSubgoalLoop mvarId
+
+  proveSubgoal (mvarId : MVarId) : MetaM Unit := do
+    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!))
+    proveSubgoalLoop mvarId
+
 /--
   Create conditional equations and splitter for the given match auxiliary declaration. -/
 partial def mkEquationsFor (matchDeclName : Name) :  MetaM Unit := do
@@ -252,18 +280,18 @@ partial def mkEquationsFor (matchDeclName : Name) :  MetaM Unit := do
       idx := idx + 1
     -- 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 splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
+      let splitterType ← mkForallFVars splitterParams matchResultType
+      trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
       let template ← mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
       let template ← deltaExpand template (. == constInfo.name)
-      let elimVal ← mkLambdaFVars elimParams (← mkSplitterProof matchDeclName template alts altsNew)
-      let elimName := matchDeclName ++ `elim
+      let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew)
+      let splitterName := matchDeclName ++ `splitter
       addDecl <| Declaration.thmDecl {
-        name        := elimName
+        name        := splitterName
         levelParams := constInfo.levelParams
-        type        := elimType
-        value       := elimVal
+        type        := splitterType
+        value       := splitterVal
       }
 
 builtin_initialize registerTraceClass `Meta.Match.matchEqs

tests/playground/matchEqs.lean

@@ -33,12 +33,13 @@ theorem ex2 : h 10002 1 = 3 := rfl
 -- set_option trace.Meta.debug true
 -- set_option pp.proofs true
 -- set_option trace.Meta.debug truen
+set_option trace.Meta.Match.matchEqs true in
 test% f.match_1
-set_option pp.analyze false
 #check @f.match_1.eq_1
 #check @f.match_1.eq_2
 #check @f.match_1.eq_3
 #check @f.match_1.eq_4
+#check @f.match_1.splitter
 
 test% h.match_1
 #check @h.match_1.eq_1
@@ -47,6 +48,7 @@ test% h.match_1
 #check @h.match_1.eq_4
 #check @h.match_1.eq_5
 #check @h.match_1.eq_6
+#check @h.match_1.splitter
 
 def g (xs ys : List (Nat × String)) : Nat :=
   match xs, ys with
@@ -54,7 +56,11 @@ def g (xs ys : List (Nat × String)) : Nat :=
   | [(c, d)], _ => 1
   | _,  _       => 2
 
+set_option pp.analyze false
+set_option pp.proofs true
+set_option trace.Meta.Match.matchEqs true in
 test% g.match_1
 #check @g.match_1.eq_1
 #check @g.match_1.eq_2
 #check @g.match_1.eq_3
+#check @g.match_1.splitter