perf: when matching on values, avoid generating hyps when not needed

This PR avoids generating hyps when not needed (i.e. if there is a
catch-all so no completeness checking needed) during matching on values.

This tweak was made possible by #11220.

Author: nomeata

src/Lean/Meta/Match/CaseValues.lean

@@ -82,8 +82,11 @@ structure CaseValuesSubgoal where
   Remark: the field `newHs` has size 1 forall but the last subgoal.
 
   If `substNewEqs = true`, then the new `h_i` equality hypotheses are substituted in the first `n` cases.
+
+  If `needsHyps = false` then the else case has the hypotheses cleared.
 -/
-def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) (substNewEqs := false) : MetaM (Array CaseValuesSubgoal) :=
+def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h)
+    (substNewEqs := false) (needHyps := true) : MetaM (Array CaseValuesSubgoal) :=
   let rec loop : Nat → MVarId → List Expr → Array FVarId → Array CaseValuesSubgoal → MetaM (Array CaseValuesSubgoal)
     | _, mvarId, [],    _,  _        => throwTacticEx `caseValues mvarId "list of values must not be empty"
     | i, mvarId, v::vs, hs, subgoals => do
@@ -103,7 +106,14 @@ def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNameP
       | [] => do
         appendTagSuffix elseSubgoal.mvarId ((`case).appendIndexAfter (i+1))
         pure $ subgoals.push { mvarId := elseSubgoal.mvarId, newHs := hs.push elseSubgoal.newH, subst := {} }
-      | vs => loop (i+1) elseSubgoal.mvarId vs (hs.push elseSubgoal.newH) subgoals
+      | vs =>
+        let (mvarId', hs') ←
+          if needHyps then
+            pure (elseSubgoal.mvarId, hs.push elseSubgoal.newH)
+          else
+            pure (← elseSubgoal.mvarId.tryClear elseSubgoal.newH, hs)
+        loop (i+1) mvarId' vs hs' subgoals
+
   loop 1 mvarId values.toList #[] #[]
 
 end Lean.Meta

src/Lean/Meta/Match/Match.lean

@@ -720,11 +720,23 @@ private def isFirstPatternVar (alt : Alt) : Bool :=
   | .var _ :: _ => true
   | _           => false
 
+private def Pattern.isRefutable : Pattern → Bool
+  | .var _           => false
+  | .inaccessible _  => false
+  | .as _ p _        => p.isRefutable
+  | .arrayLit ..     => true
+  | .ctor ..         => true
+  | .val ..          => true
+
+private def triviallyComplete (p : Problem) : Bool :=
+  !p.alts.isEmpty && p.alts.getLast!.patterns.all (!·.isRefutable)
+
 private def processValue (p : Problem) : MetaM (Array Problem) := do
   trace[Meta.Match.match] "value step"
   let x :: xs := p.vars | unreachable!
   let values := collectValues p
-  let subgoals ← caseValues p.mvarId x.fvarId! values (substNewEqs := true)
+  let needHyps := !triviallyComplete p || p.alts.any (!·.notAltIdxs.isEmpty)
+  let subgoals ← caseValues p.mvarId x.fvarId! values (substNewEqs := true) (needHyps := needHyps)
   subgoals.mapIdxM fun i subgoal => do
     trace[Meta.Match.match] "processValue subgoal\n{MessageData.ofGoal subgoal.mvarId}"
     if h : i < values.size then
@@ -898,14 +910,6 @@ private def moveToFront (p : Problem) (i : Nat) : Problem :=
   else
     p
 
-def Pattern.isRefutable : Pattern → Bool
-  | .var _           => false
-  | .inaccessible _  => false
-  | .as _ p _        => p.isRefutable
-  | .arrayLit ..     => true
-  | .ctor ..         => true
-  | .val ..          => true
-
 /--
 Returns the index of the first pattern in the first alternative that is refutable
 (i.e. not a variable or inaccessible pattern). We want to handle these first

tests/lean/run/match_nat.lean

@@ -0,0 +1,40 @@
+def f : Nat → Nat
+  | 0 => 0
+  | 10 => 1
+  | 100 => 2
+  | _ => 3
+
+
+/--
+info: def f.match_1.{u_1} : (motive : Nat → Sort u_1) →
+  (x : Nat) → (Unit → motive 0) → (Unit → motive 10) → (Unit → motive 100) → ((x : Nat) → motive x) → motive x
+-/
+#guard_msgs in
+#print sig f.match_1
+
+
+/--
+info: private def f.match_1.splitter.{u_1} : (motive : Nat → Sort u_1) →
+  (x : Nat) →
+    (Unit → motive 0) →
+      (Unit → motive 10) →
+        (Unit → motive 100) → ((x : Nat) → (x = 0 → False) → (x = 10 → False) → (x = 100 → False) → motive x) → motive x
+-/
+#guard_msgs in
+#print sig f.match_1.splitter
+
+/--
+info: private theorem f.match_1.eq_4.{u_1} : ∀ (motive : Nat → Sort u_1) (x : Nat) (h_1 : Unit → motive 0)
+  (h_2 : Unit → motive 10) (h_3 : Unit → motive 100) (h_4 : (x : Nat) → motive x),
+  (x = 0 → False) →
+    (x = 10 → False) →
+      (x = 100 → False) →
+        (match x with
+          | 0 => h_1 ()
+          | 10 => h_2 ()
+          | 100 => h_3 ()
+          | x => h_4 x) =
+          h_4 x
+-/
+#guard_msgs in
+#print sig f.match_1.eq_4