fix: matcher splitter is code (#3815)

It have to keep it as a private definition for now. We currently only
support duplicate theorems in different modules. Splitters are generated
on demand, and are also used to write code.

src/Lean/Meta/Eqns.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.ReservedNameAction
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
+import Lean.Meta.Match.MatcherInfo
 
 namespace Lean.Meta
 /--
@@ -57,7 +58,13 @@ Ensures that `f.eq_def` and `f.eq_<idx>` are reserved names if `f` is a safe def
 -/
 builtin_initialize registerReservedNamePredicate fun env n =>
   match n with
-  | .str p s => (isEqnReservedNameSuffix s || isUnfoldReservedNameSuffix s) && env.isSafeDefinition p
+  | .str p s =>
+    (isEqnReservedNameSuffix s || isUnfoldReservedNameSuffix s)
+    && env.isSafeDefinition p
+    -- Remark: `f.match_<idx>.eq_<idx>` are private definitions and are not treated as reserved names
+    -- Reason: `f.match_<idx>.splitter is generated at the same time, and can eliminate into type.
+    -- Thus, it cannot be defined in different modules since it is not a theorem, and is used to generate code.
+    && !isMatcherCore env p
   | _ => false
 
 def GetEqnsFn := Name → MetaM (Option (Array Name))

src/Lean/Meta/Match/MatchEqs.lean

@@ -649,13 +649,18 @@ where
 private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns := withLCtx {} {} do
   trace[Meta.Match.matchEqs] "mkEquationsFor '{matchDeclName}'"
   withConfig (fun c => { c with etaStruct := .none }) do
-  let baseName := matchDeclName
+  /-
+  Remark: user have requested the `split` tactic to be available for writing code.
+  Thus, the `splitter` declaration must be a definition instead of a theorem.
+  Moreover, the `splitter` is generated on demand, and we currently
+  can't import the same definition from different modules. Thus, we must
+  keep `splitter` as a private declaration to prevent import failures.
+  -/
+  let baseName := mkPrivateName (← getEnv) matchDeclName
   let splitterName := baseName ++ `splitter
   let constInfo ← getConstInfo matchDeclName
   let us := constInfo.levelParams.map mkLevelParam
   let some matchInfo ← getMatcherInfo? matchDeclName | throwError "'{matchDeclName}' is not a matcher function"
-  -- `alreadyDeclared` is `true` if matcher equations were defined in an imported module
-  let alreadyDeclared := (← getEnv).contains splitterName
   let numDiscrEqs := getNumEqsFromDiscrInfos matchInfo.discrInfos
   forallTelescopeReducing constInfo.type fun xs matchResultType => do
     let mut eqnNames := #[]
@@ -690,59 +695,51 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
         for discr in discrs.toArray.reverse, pattern in patterns.reverse do
           notAlt ← mkArrow (← mkEqHEq discr pattern) notAlt
         notAlt ← mkForallFVars (discrs ++ ys) notAlt
-        if alreadyDeclared then
-          -- If the matcher equations and splitter have already been declared, the only
-          -- values we are `notAlt` and `splitterAltNumParam`. This code is a bit hackish.
-          return (notAlt, default, splitterAltNumParam, default)
-        else
-          /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant.
-             Thus, we need to create new `alts`. -/
-          withNewAlts numDiscrEqs discrs patterns alts fun alts => do
-            let alt := alts[i]!
-            let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
-            let rhs := mkAppN alt rhsArgs
-            let thmType ← mkEq lhs rhs
-            let thmType ← hs.foldrM (init := thmType) (mkArrow · ·)
-            let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
-            let thmType ← unfoldNamedPattern thmType
-            let thmVal ← proveCondEqThm matchDeclName thmType
-            addDecl <| Declaration.thmDecl {
-              name        := thmName
-              levelParams := constInfo.levelParams
-              type        := thmType
-              value       := thmVal
-            }
-            return (notAlt, splitterAltType, splitterAltNumParam, argMask)
+        /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant.
+           Thus, we need to create new `alts`. -/
+        withNewAlts numDiscrEqs discrs patterns alts fun alts => do
+          let alt := alts[i]!
+          let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
+          let rhs := mkAppN alt rhsArgs
+          let thmType ← mkEq lhs rhs
+          let thmType ← hs.foldrM (init := thmType) (mkArrow · ·)
+          let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
+          let thmType ← unfoldNamedPattern thmType
+          let thmVal ← proveCondEqThm matchDeclName thmType
+          addDecl <| Declaration.thmDecl {
+            name        := thmName
+            levelParams := constInfo.levelParams
+            type        := thmType
+            value       := thmVal
+          }
+          return (notAlt, splitterAltType, splitterAltNumParam, argMask)
       notAlts := notAlts.push notAlt
       splitterAltTypes := splitterAltTypes.push splitterAltType
       splitterAltNumParams := splitterAltNumParams.push splitterAltNumParam
       altArgMasks := altArgMasks.push argMask
       trace[Meta.Match.matchEqs] "splitterAltType: {splitterAltType}"
       idx := idx + 1
-    if alreadyDeclared then
-      return { eqnNames, splitterName, splitterAltNumParams }
-    else
-      -- Define splitter with conditional/refined alternatives
-      withSplitterAlts splitterAltTypes fun altsNew => do
-        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 template := template.headBeta
-        let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks)
-        addAndCompile <| Declaration.defnDecl {
-          name        := splitterName
-          levelParams := constInfo.levelParams
-          type        := splitterType
-          value       := splitterVal
-          hints       := .abbrev
-          safety      := .safe
-        }
-        setInlineAttribute splitterName
-        let result := { eqnNames, splitterName, splitterAltNumParams }
-        registerMatchEqns matchDeclName result
-        return result
+    -- Define splitter with conditional/refined alternatives
+    withSplitterAlts splitterAltTypes fun altsNew => do
+      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 template := template.headBeta
+      let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks)
+      addAndCompile <| Declaration.defnDecl {
+        name        := splitterName
+        levelParams := constInfo.levelParams
+        type        := splitterType
+        value       := splitterVal
+        hints       := .abbrev
+        safety      := .safe
+      }
+      setInlineAttribute splitterName
+      let result := { eqnNames, splitterName, splitterAltNumParams }
+      registerMatchEqns matchDeclName result
+      return result
 
 /- See header at `MatchEqsExt.lean` -/
 @[export lean_get_match_equations_for]
@@ -753,23 +750,4 @@ def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
 
 builtin_initialize registerTraceClass `Meta.Match.matchEqs
 
-private def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
-  unless (← isMatcher declName) do
-    return none
-  let result ← getEquationsForImpl declName
-  return some result.eqnNames
-
-builtin_initialize
-  registerGetEqnsFn getEqnsFor?
-
-/-
-We register `foo.match_<idx>.splitter` as a reserved name, but
-we do not install a realizer. The `splitter` will be generated by the
-`foo.match_<idx>.eq_<idx>` realizer.
--/
-builtin_initialize registerReservedNamePredicate fun env n =>
-  match n with
-  | .str p "splitter" => isMatcherCore env p
-  | _ => false
-
 end Lean.Meta.Match

tests/lean/run/matchEqsBug.lean

@@ -26,10 +26,6 @@ set_option trace.Meta.Match.matchEqs true
 test% f.match_1
 #check f.match_1.splitter
 
-/--
-error: 'g.match_1.splitter' is a reserved name
--/
-#guard_msgs (error) in
 def g.match_1.splitter := 4
 
 test% g.match_1