Try to treat casesOn as matchers almost everywhere

Author: nomeata

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -40,7 +40,7 @@ Inline auxiliary `matcher` applications.
 partial def inlineMatchers (e : Expr) : CoreM Expr :=
   Meta.MetaM.run' <| Meta.transform e fun e => do
     let .const declName us := e.getAppFn | return .continue
-    let some info ← Meta.getMatcherInfo? declName | return .continue
+    let some info ← Meta.getMatcherInfo? declName (alsoCasesOn := false) | return .continue
     let numArgs := e.getAppNumArgs
     if numArgs > info.arity then
       return .continue

src/Lean/Meta/Match/MatchEqs.lean

@@ -46,7 +46,7 @@ private def _root_.Lean.MVarId.contradictionQuick (mvarId : MVarId) : MetaM Bool
     return false
 
 /--
-  Helper method for `proveCondEqThm`. Given a goal of the form `C.rec ... xMajor = rhs`,
+  Helper method for `proveCondEqThm`. Given a goal of the form `C.casesOn ... xMajor ... = rhs`,
   apply `cases xMajor`. -/
 partial def casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId) := do
   let target ← mvarId.getType
@@ -71,14 +71,24 @@ where
           else
             return none
         | none =>
-          matchConstRec f (fun _ => return none) fun recVal _ => do
-            if recVal.getMajorIdx >= args.size then
+          if isCasesOnRecursor (← getEnv) declName then
+            let some matcherInfo := getMatcherInfoForCasesOn (← getEnv) declName | return none
+            if matcherInfo.getFirstDiscrPos >= args.size then
               return none
-            let major := args[recVal.getMajorIdx]!.consumeMData
+            let major := args[matcherInfo.getLastDiscrPos]!.consumeMData
             if major.isFVar then
               return some major.fvarId!
             else
               return none
+          else
+            matchConstRec f (fun _ => return none) fun recVal _ => do
+              if recVal.getMajorIdx >= args.size then
+                return none
+              let major := args[recVal.getMajorIdx]!.consumeMData
+              if major.isFVar then
+                return some major.fvarId!
+              else
+                return none
 
 def casesOnStuckLHS? (mvarId : MVarId) : MetaM (Option (Array MVarId)) := do
   try casesOnStuckLHS mvarId catch _ => return none
@@ -751,7 +761,7 @@ def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
 where go baseName splitterName := withConfig (fun c => { c with etaStruct := .none }) do
   let constInfo ← getConstInfo matchDeclName
   let us := constInfo.levelParams.map mkLevelParam
-  let some matchInfo ← getMatcherInfo? matchDeclName | throwError "`{matchDeclName}` is not a matcher function"
+  let some matchInfo ← getMatcherInfo? matchDeclName (alsoCasesOn := true) | throwError "`{matchDeclName}` is not a matcher function"
   let numDiscrEqs := getNumEqsFromDiscrInfos matchInfo.discrInfos
   forallTelescopeReducing constInfo.type fun xs matchResultType => do
     let mut eqnNames := #[]
@@ -867,7 +877,7 @@ where go baseName := withConfig (fun c => { c with etaStruct := .none }) do
   withConfig (fun c => { c with etaStruct := .none }) do
   let constInfo ← getConstInfo matchDeclName
   let us := constInfo.levelParams.map mkLevelParam
-  let some matchInfo ← getMatcherInfo? matchDeclName | throwError "`{matchDeclName}` is not a matcher function"
+  let some matchInfo ← getMatcherInfo? matchDeclName (alsoCasesOn := true) | throwError "`{matchDeclName}` is not a matcher function"
   let numDiscrEqs := matchInfo.getNumDiscrEqs
   forallTelescopeReducing constInfo.type fun xs _matchResultType => do
     let mut eqnNames := #[]

src/Lean/Meta/Match/MatcherInfo.lean

@@ -46,6 +46,9 @@ def MatcherInfo.arity (info : MatcherInfo) : Nat :=
 def MatcherInfo.getFirstDiscrPos (info : MatcherInfo) : Nat :=
   info.numParams + 1
 
+def MatcherInfo.getLastDiscrPos (info : MatcherInfo) : Nat :=
+  info.numParams + 1 + info.numDiscrs - 1
+
 def MatcherInfo.getDiscrRange (info : MatcherInfo) : Std.Rco Nat :=
   info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs)
 
@@ -89,7 +92,7 @@ builtin_initialize extension : SimplePersistentEnvExtension Entry State ←
     asyncMode     := .async .mainEnv
     exportEntriesFnEx? := some fun env _ entries _ =>
       -- Do not export info for private defs
-      entries.filter (env.contains (skipRealize := false) ·.name) |>.toArray
+      entries.filter (env.contains (skipRealize := true) ·.name) |>.toArray
   }
 
 def addMatcherInfo (env : Environment) (matcherName : Name) (info : MatcherInfo) : Environment :=
@@ -128,36 +131,36 @@ def getMatcherInfoForCasesOn (env : Environment) (declName : Name) : Option Matc
     altNumParams
   }
 
-def getMatcherInfoCore? (env : Environment) (declName : Name) (alsoCasesOn : Bool := false) : Option MatcherInfo :=
+def getMatcherInfoCore? (env : Environment) (declName : Name) (alsoCasesOn : Bool := true) : Option MatcherInfo :=
   if alsoCasesOn && isCasesOnRecursor env declName then
       getMatcherInfoForCasesOn env declName
   else
     Match.Extension.getMatcherInfo? env declName
 
-def getMatcherInfo? [Monad m] [MonadEnv m] (declName : Name) (alsoCasesOn := false) : m (Option MatcherInfo) :=
+def getMatcherInfo? [Monad m] [MonadEnv m] (declName : Name) (alsoCasesOn := true) : m (Option MatcherInfo) :=
   return getMatcherInfoCore? (← getEnv) declName (alsoCasesOn := alsoCasesOn)
 
 @[export lean_is_matcher]
-def isMatcherCore (env : Environment) (declName : Name) : Bool :=
-  getMatcherInfoCore? env declName |>.isSome
+def isMatcherCore (env : Environment) (declName : Name) (alsoCasesOn := true) : Bool :=
+  getMatcherInfoCore? env declName (alsoCasesOn := alsoCasesOn) |>.isSome
 
-def isMatcher [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
-  return isMatcherCore (← getEnv) declName
+def isMatcher [Monad m] [MonadEnv m] (declName : Name) (alsoCasesOn := true) : m Bool :=
+  return isMatcherCore (← getEnv) declName (alsoCasesOn := alsoCasesOn)
 
-def isMatcherAppCore? (env : Environment) (e : Expr) : Option MatcherInfo :=
+def isMatcherAppCore? (env : Environment) (e : Expr) (alsoCasesOn := true) : Option MatcherInfo :=
   let fn := e.getAppFn
   if fn.isConst then
-    if let some matcherInfo := getMatcherInfoCore? env fn.constName! then
+    if let some matcherInfo := getMatcherInfoCore? env fn.constName! (alsoCasesOn := alsoCasesOn) then
       if e.getAppNumArgs ≥ matcherInfo.arity then some matcherInfo else none
     else
       none
   else
     none
 
-def isMatcherAppCore (env : Environment) (e : Expr) : Bool :=
-  isMatcherAppCore? env e |>.isSome
+def isMatcherAppCore (env : Environment) (e : Expr) (alsoCasesOn := true) : Bool :=
+  isMatcherAppCore? env e (alsoCasesOn := alsoCasesOn) |>.isSome
 
-def isMatcherApp [Monad m] [MonadEnv m] (e : Expr) : m Bool :=
-  return isMatcherAppCore (← getEnv) e
+def isMatcherApp [Monad m] [MonadEnv m] (e : Expr) (alsoCasesOn := true) : m Bool :=
+  return isMatcherAppCore (← getEnv) e (alsoCasesOn := alsoCasesOn)
 
 end Lean.Meta

src/Lean/Meta/Tactic/Split.lean

@@ -150,7 +150,7 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N
   if discrs.all (·.isFVar) then
     trace[split.debug] "no need to generalize discriminants, all are fvars"
     return (discrs.map (·.fvarId!), #[], mvarId)
-  let some matcherInfo ← getMatcherInfo? matcherDeclName | unreachable!
+  let some matcherInfo ← getMatcherInfo? matcherDeclName (alsoCasesOn := true) | unreachable!
   let numDiscrEqs := matcherInfo.getNumDiscrEqs -- Number of `h : discr = pattern` equations
   let (targetNew, rfls) ←
     forallTelescope motiveType fun discrVars _ =>
@@ -249,7 +249,7 @@ private def substDiscrEqs (mvarId : MVarId) (fvarSubst : FVarSubst) (discrEqs :
   return mvarId
 
 def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) := do
-  let some info ← getMatcherInfo? matcherDeclName | throwInternalMisuseError m!"Internal error in `split` tactic: `{matcherDeclName}` is not an auxiliary declaration used to encode `match`-expressions"
+  let some info ← getMatcherInfo? matcherDeclName (alsoCasesOn := true) | throwInternalMisuseError m!"Internal error in `split` tactic: `{matcherDeclName}` is not an auxiliary declaration used to encode `match`-expressions"
   let matchEqns ← Match.getEquationsFor matcherDeclName
   -- splitterPre does not have the correct universe elimination level, but this is fine, we only use it to compute the `motiveType`,
   -- and we only care about the `motiveType` arguments, and not the resulting `Sort u`.
@@ -302,7 +302,7 @@ def throwDiscrGenError (e : Expr) : MetaM α :=
   throwError (mkDiscrGenErrorMsg e)
 
 def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withContext do
-  let some app ← matchMatcherApp? e | throwInternalMisuseError m!"Internal error in `split` tactic: Match application expected{indentExpr e}"
+  let some app ← matchMatcherApp? e (alsoCasesOn := true) | throwInternalMisuseError m!"Internal error in `split` tactic: Match application expected{indentExpr e}"
   let matchEqns ← Match.getEquationsFor app.matcherName
   let mvarIds ← applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params app.discrs
   let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do
@@ -315,7 +315,7 @@ end Split
 open Split
 
 /--
-Splits an `if-then-else` of `match`-expression in the goal target.
+Splits an `if-then-else` or `match`-expression in the goal target.
 If `useNewSemantics` is `true`, the flag `backward.split` is ignored. Recall this flag only affects the split of `if-then-else` expressions.
 -/
 partial def splitTarget? (mvarId : MVarId) (splitIte := true) (useNewSemantics := false) : MetaM (Option (List MVarId)) := commitWhenSome? do mvarId.withContext do

src/Lean/Meta/Tactic/SplitIf.lean

@@ -48,7 +48,7 @@ private def isCandidate? (env : Environment) (ctx : Context) (e : Expr) : Option
       if numArgs >= 5 && !(e.getArg! 1 5).hasLooseBVars then
         return ret (e.getBoundedAppFn (numArgs - 5))
   if ctx.kind.considerMatch then
-    if let some info := isMatcherAppCore? env e then
+    if let some info := isMatcherAppCore? env e (alsoCasesOn := true) then
       let args := e.getAppArgs
       for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do
         if args[i]!.hasLooseBVars then

src/Lean/Meta/WHNF.lean

@@ -528,7 +528,7 @@ private def whnfMatcher (e : Expr) : MetaM Expr := do
 def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do
   let .const declName declLevels := e.getAppFn
     | return .notMatcher
-  let some info ← getMatcherInfo? declName
+  let some info ← getMatcherInfo? declName (alsoCasesOn := true)
     | return .notMatcher
   let args := e.getAppArgs
   let prefixSz := info.numParams + 1 + info.numDiscrs
@@ -870,7 +870,7 @@ mutual
                 recordUnfold fInfo.name
                 return some r
             | _ =>
-              if (← getMatcherInfo? fInfo.name).isSome then
+              if (← getMatcherInfo? fInfo.name (alsoCasesOn := false)).isSome then
                 -- Recall that `whnfCore` tries to reduce "matcher" applications.
                 return none
               else

tests/lean/run/diagRec.lean

@@ -8,11 +8,11 @@ termination_by structural n
 info: 573147844013817084101
 ---
 trace: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 596, num: 2):
-    [reduction] Nat.rec ↦ 596
+  [reduction] unfolded declarations (max: 995, num: 2):
+    [reduction] Nat.rec ↦ 995
     [reduction] HAdd.hAdd ↦ 196
-  [reduction] unfolded reducible declarations (max: 397, num: 1):
-    [reduction] Nat.casesOn ↦ 397
+  [reduction] unfolded reducible declarations (max: 399, num: 1):
+    [reduction] Nat.below ↦ 399
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in

tests/lean/run/diagnostics.lean

@@ -19,8 +19,6 @@ trace: [diag] Diagnostics
     [reduction] OfNat.ofNat ↦ 5
   [reduction] unfolded instances (max: 5, num: 1):
     [reduction] instOfNatNat ↦ 5
-  [reduction] unfolded reducible declarations (max: 15, num: 1):
-    [reduction] Nat.casesOn ↦ 15
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
@@ -40,8 +38,6 @@ trace: [diag] Diagnostics
     [reduction] OfNat.ofNat ↦ 5
   [reduction] unfolded instances (max: 5, num: 1):
     [reduction] instOfNatNat ↦ 5
-  [reduction] unfolded reducible declarations (max: 15, num: 1):
-    [reduction] Nat.casesOn ↦ 15
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in

tests/lean/run/grind_indexmap_trace.lean

@@ -147,8 +147,7 @@ example (m : IndexMap α β) (a : α) (h : a ∈ m) :
 info: Try this:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
-    instantiate only [= getElem?_neg, = getElem?_pos, =_ HashMap.contains_iff_mem]
-    instantiate only [=_ HashMap.contains_iff_mem]
+    instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
     cases #4ed2
     next =>
       cases #ffdf
@@ -181,7 +180,8 @@ example (m : IndexMap α β) (a a' : α) (b : β) :
 info: Try this:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
-    instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
+    instantiate only [= getElem?_neg, = getElem?_pos, =_ HashMap.contains_iff_mem]
+    instantiate only [=_ HashMap.contains_iff_mem]
     cases #4ed2
     next =>
       cases #ffdf

tests/lean/run/issue10876.lean

@@ -29,3 +29,25 @@ fun x =>
 -/
 #guard_msgs in
 #print bar
+
+-- Does `split` work?
+
+-- set_option trace.split.debug true
+
+/--
+trace: case h_1
+t✝ : Bool
+⊢ false = false
+
+case h_2
+t✝ : Bool
+⊢ true = true
+-/
+#guard_msgs in
+theorem splitTest (b : Bool) : b = b.casesOn false true := by
+  split
+  trace_state
+  · rfl
+  · rfl
+
+-- #print splitTest