perf: in CaseValues, subst only once

This PR avoids running `substCore` twice in `caseValues`.

Author: nomeata

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -68,7 +68,7 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
     let mvarId ← mvarId.assertExt `aSize (mkConst `Nat) aSize
     let (aSizeFVarId, mvarId) ← mvarId.intro1
     let (hEq, mvarId) ← mvarId.intro1
-    let subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkRawNatLit) hNamePrefix
+    let subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkRawNatLit) hNamePrefix (substNewEqs := false)
     subgoals.mapIdxM fun i subgoal => do
       let subst  := subgoal.subst
       let mvarId := subgoal.mvarId

src/Lean/Meta/Match/CaseValues.lean

@@ -26,8 +26,11 @@ structure CaseValueSubgoal where
   where `fvarId` is `x`s id.
   The type of `x` must have decidable equality.
 
+  If `substNewEq = false`, then the first case remains `C x`.
+
   Remark: `subst` field of the second subgoal is equal to the input `subst`. -/
-private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h) (subst : FVarSubst := {})
+private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h)
+    (subst : FVarSubst := {}) (substNewEq : Bool)
     : MetaM (CaseValueSubgoal × CaseValueSubgoal) :=
   mvarId.withContext do
     let tag ← mvarId.getTag
@@ -44,9 +47,11 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
     let (elseH, elseMVarId) ← elseMVar.mvarId!.intro1P
     let elseSubgoal := { mvarId := elseMVarId, newH := elseH, subst := subst : CaseValueSubgoal }
     let (thenH, thenMVarId) ← thenMVar.mvarId!.intro1P
-    let symm   := false
-    let clearH := false
-    let (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH
+    let (thenSubst, thenMVarId) ←
+      if substNewEq then
+        substCore thenMVarId thenH (symm := false) subst (clearH := false)
+      else
+        pure (subst, thenMVarId)
     thenMVarId.withContext do
       trace[Meta] "subst domain: {thenSubst.domain.map (·.name)}"
       let thenH := (thenSubst.get thenH).fvarId!
@@ -57,7 +62,7 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
     pure (thenSubgoal, elseSubgoal)
 
 def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) : MetaM (CaseValueSubgoal × CaseValueSubgoal) := do
-  let s ← caseValueAux mvarId fvarId value
+  let s ← caseValueAux mvarId fvarId value (substNewEq := true)
   appendTagSuffix s.1.mvarId `thenBranch
   appendTagSuffix s.2.mvarId `elseBranch
   pure s
@@ -83,19 +88,19 @@ structure CaseValuesSubgoal where
 
   If `substNewEqs = true`, then the new `h_i` equality hypotheses are substituted in the first `n` cases.
 -/
-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 : Bool) : 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
-      let (thenSubgoal, elseSubgoal) ← caseValueAux mvarId fvarId v (hNamePrefix.appendIndexAfter i) {}
+      let (thenSubgoal, elseSubgoal) ← caseValueAux mvarId fvarId v (hNamePrefix.appendIndexAfter i) (substNewEq := !substNewEqs) {}
       appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i)
       let thenMVarId ← hs.foldlM
         (fun thenMVarId h => match thenSubgoal.subst.get h with
           | Expr.fvar fvarId => thenMVarId.tryClear fvarId
           | _                => pure thenMVarId)
         thenSubgoal.mvarId
       let subgoals ← if substNewEqs then
-         let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH false thenSubgoal.subst true
+         let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH (symm := false) thenSubgoal.subst (clearH := true)
          pure <| subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
       else
          pure <| subgoals.push { mvarId := thenMVarId, newHs := #[thenSubgoal.newH], subst := thenSubgoal.subst }

tests/lean/run/meta6.lean

@@ -71,7 +71,7 @@ withLocalDeclD `y nat fun y => do
 let vType ← mkAppM `Vec #[nat, x];
 withLocalDeclD `v vType fun v => do
 let m ← mkFreshExprSyntheticOpaqueMVar vType;
-let subgoals ← caseValues m.mvarId! x.fvarId! #[mkNatLit 2, mkNatLit 3, mkNatLit 5];
+let subgoals ← caseValues m.mvarId! x.fvarId! #[mkNatLit 2, mkNatLit 3, mkNatLit 5] (substNewEqs := false);
 subgoals.forM fun s => do {
   print (MessageData.ofGoal s.mvarId);
   s.mvarId.assumption