perf: in CaseValues, subst only once

src/Lean/Elab/Match.lean

@@ -12,6 +12,7 @@ public import Lean.Elab.BindersUtil
 public import Lean.Elab.PatternVar
 public import Lean.Elab.Quotation.Precheck
 public import Lean.Elab.SyntheticMVars
+import Lean.Meta.Match.Value
 import Lean.Meta.Match.NamedPatterns
 
 public section

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -8,10 +8,12 @@ module
 prelude
 public import Lean.Elab.PreDefinition.FixedParams
 import Lean.Elab.PreDefinition.EqnsUtils
-import Lean.Meta.Tactic.Split
+import Lean.Meta.Tactic.CasesOnStuckLHS
+import Lean.Meta.Tactic.Delta
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Delta
 import Lean.Meta.Tactic.CasesOnStuckLHS
+import Lean.Meta.Tactic.Split
 
 namespace Lean.Elab
 open Meta

src/Lean/Meta/Constructions/CasesOnSameCtor.lean

@@ -213,7 +213,9 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit :=
           numDiscrs := info.numIndices + 3
           altInfos
           uElimPos? := some 0
-          discrInfos := #[{}, {}, {}]}
+          discrInfos := #[{}, {}, {}]
+          overlaps := {}
+        }
 
         -- Compare attributes with `mkMatcherAuxDefinition`
         withExporting (isExporting := !isPrivateName declName) do

src/Lean/Meta/IndPredBelow.lean

@@ -319,7 +319,7 @@ public partial def mkBelowMatcher (matcherApp : MatcherApp) (belowParams : Array
     (ctx : RecursionContext) (transformAlt : RecursionContext → Expr → MetaM Expr) :
     MetaM (Option (Expr × MetaM Unit)) :=
   withTraceNode `Meta.IndPredBelow.match (return m!"{exceptEmoji ·} {matcherApp.toExpr} and {belowParams}") do
-  let mut input ← getMkMatcherInputInContext matcherApp
+  let mut input ← getMkMatcherInputInContext matcherApp (unfoldNamed := false)
   let mut discrs := matcherApp.discrs
   let mut matchTypeAdd := #[] -- #[(discrIdx, ), ...]
   let mut i := discrs.size

src/Lean/Meta/Match/Basic.lean

@@ -6,8 +6,14 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Lean.Meta.Basic
+public import Lean.Meta.Tactic.FVarSubst
 public import Lean.Meta.CollectFVars
-public import Lean.Meta.Match.CaseArraySizes
+import Lean.Meta.Match.Value
+import Lean.Meta.AppBuilder
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Assert
+import Lean.Meta.Tactic.Subst
 import Lean.Meta.Match.NamedPatterns
 
 public section
@@ -150,6 +156,11 @@ structure Alt where
   After we perform additional case analysis, their types become definitionally equal.
   -/
   cnstrs    : List (Expr × Expr)
+  /--
+  Indices of previous alternatives that this alternative expects a not-that-proofs.
+  (When producing a splitter, and in the future also for source-level overlap hypotheses.)
+  -/
+  notAltIdxs : Array Nat
   deriving Inhabited
 
 namespace Alt

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -6,32 +6,36 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.Match.CaseValues
-
-public section
+public import Lean.Meta.Basic
+public import Lean.Meta.Tactic.FVarSubst
+import Lean.Meta.Match.CaseValues
+import Lean.Meta.AppBuilder
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Assert
+import Lean.Meta.Tactic.Subst
 
 namespace Lean.Meta
 
-structure CaseArraySizesSubgoal where
+public structure CaseArraySizesSubgoal where
   mvarId : MVarId
   elems  : Array FVarId := #[]
   diseqs : Array FVarId := #[]
   subst  : FVarSubst := {}
   deriving Inhabited
 
-def getArrayArgType (a : Expr) : MetaM Expr := do
+public def getArrayArgType (a : Expr) : MetaM Expr := do
   let aType ← inferType a
   let aType ← whnfD aType
   unless aType.isAppOfArity ``Array 1 do
     throwError "array expected{indentExpr a}"
   pure aType.appArg!
 
-private def mkArrayGetLit (a : Expr) (i : Nat) (n : Nat) (h : Expr) : MetaM Expr := do
+def mkArrayGetLit (a : Expr) (i : Nat) (n : Nat) (h : Expr) : MetaM Expr := do
   let lt    ← mkLt (mkRawNatLit i) (mkRawNatLit n)
   let ltPrf ← mkDecideProof lt
   mkAppM `Array.getLit #[a, mkRawNatLit i, h, ltPrf]
 
-private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr) : MetaM MVarId := do
+partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr) : MetaM MVarId := do
   let α ← getArrayArgType a
   let rec loop (i : Nat) (xs : Array Expr) (args : Array Expr) := do
     if i < n then
@@ -61,7 +65,7 @@ private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNameP
   n) `..., x_1 ... x_{sizes[n-1]}  |- C #[x_1, ..., x_{sizes[n-1]}]`
   n+1) `..., (h_1 : a.size != sizes[0]), ..., (h_n : a.size != sizes[n-1]) |- C a`
   where `n = sizes.size` -/
-def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) :=
+public def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) :=
   mvarId.withContext do
     let a := mkFVar fvarId
     let aSize ← mkAppM `Array.size #[a]
@@ -72,22 +76,20 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
     subgoals.mapIdxM fun i subgoal => do
       let subst  := subgoal.subst
       let mvarId := subgoal.mvarId
-      let hEqSz  := (subst.get hEq).fvarId!
       if h : i < sizes.size then
-         let n := sizes[i]
-         let mvarId ← mvarId.clear subgoal.newHs[0]!
-         let mvarId ← mvarId.clear (subst.get aSizeFVarId).fvarId!
-         mvarId.withContext do
-           let hEqSzSymm ← mkEqSymm (mkFVar hEqSz)
-           let mvarId ← introArrayLit mvarId a n xNamePrefix hEqSzSymm
-           let (xs, mvarId)  ← mvarId.introN n
-           let (hEqLit, mvarId) ← mvarId.intro1
-           let mvarId ← mvarId.clear hEqSz
-           let (subst, mvarId) ← substCore mvarId hEqLit false subst
-           pure { mvarId := mvarId, elems := xs, subst := subst }
+        let hEqSz  := (subst.get hEq).fvarId!
+        let n := sizes[i]
+        mvarId.withContext do
+          let hEqSzSymm ← mkEqSymm (mkFVar hEqSz)
+          let mvarId ← introArrayLit mvarId a n xNamePrefix hEqSzSymm
+          let (xs, mvarId)  ← mvarId.introN n
+          let (hEqLit, mvarId) ← mvarId.intro1
+          let mvarId ← mvarId.clear hEqSz
+          let (subst, mvarId) ← substCore mvarId hEqLit (symm := false) subst
+          pure { mvarId := mvarId, elems := xs, subst := subst }
       else
-         let (subst, mvarId) ← substCore mvarId hEq false subst
-         let diseqs := subgoal.newHs.map fun fvarId => (subst.get fvarId).fvarId!
-         pure { mvarId := mvarId, diseqs := diseqs, subst := subst }
+        let (subst, mvarId) ← substCore mvarId hEq (symm := false) subst
+        let diseqs := subgoal.newHs.map fun fvarId => (subst.get fvarId).fvarId!
+        pure { mvarId := mvarId, diseqs := diseqs, subst := subst }
 
 end Lean.Meta

src/Lean/Meta/Match/CaseValues.lean

@@ -6,28 +6,25 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.Tactic.Subst
-public import Lean.Meta.Match.Value
-
-public section
+public import Lean.Meta.Basic
+public import Lean.Meta.Tactic.FVarSubst
+import Lean.Meta.Tactic.Subst
 
 namespace Lean.Meta
 
 structure CaseValueSubgoal where
   mvarId : MVarId
   newH   : FVarId
-  subst  : FVarSubst := {}
   deriving Inhabited
 
 /--
   Split goal `... |- C x` into two subgoals
-  `..., (h : x = value)  |- C value`
+  `..., (h : x = value)  |- C x`
   `..., (h : x != value) |- C x`
   where `fvarId` is `x`s id.
   The type of `x` must have decidable equality.
-
-  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 := {})
+ -/
+def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h)
     : MetaM (CaseValueSubgoal × CaseValueSubgoal) :=
   mvarId.withContext do
     let tag ← mvarId.getTag
@@ -42,27 +39,16 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
     let val ← mkAppOptM `dite #[none, xEqValue, none, thenMVar, elseMVar]
     mvarId.assign val
     let (elseH, elseMVarId) ← elseMVar.mvarId!.intro1P
-    let elseSubgoal := { mvarId := elseMVarId, newH := elseH, subst := subst : CaseValueSubgoal }
+    let elseSubgoal := { mvarId := elseMVarId, newH := elseH }
     let (thenH, thenMVarId) ← thenMVar.mvarId!.intro1P
-    let symm   := false
-    let clearH := false
-    let (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH
     thenMVarId.withContext do
-      trace[Meta] "subst domain: {thenSubst.domain.map (·.name)}"
-      let thenH := (thenSubst.get thenH).fvarId!
       trace[Meta] "searching for decl"
       let _ ← thenH.getDecl
       trace[Meta] "found decl"
-    let thenSubgoal := { mvarId := thenMVarId, newH := (thenSubst.get thenH).fvarId!, subst := thenSubst : CaseValueSubgoal }
+    let thenSubgoal := { mvarId := thenMVarId, newH := thenH }
     pure (thenSubgoal, elseSubgoal)
 
-def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) : MetaM (CaseValueSubgoal × CaseValueSubgoal) := do
-  let s ← caseValueAux mvarId fvarId value
-  appendTagSuffix s.1.mvarId `thenBranch
-  appendTagSuffix s.2.mvarId `elseBranch
-  pure s
-
-structure CaseValuesSubgoal where
+public structure CaseValuesSubgoal where
   mvarId : MVarId
   newHs  : Array FVarId := #[]
   subst  : FVarSubst := {}
@@ -83,22 +69,15 @@ 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) :=
+public def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) : 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) ← caseValue mvarId fvarId v (hNamePrefix.appendIndexAfter i)
       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
-         pure <| subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
-      else
-         pure <| subgoals.push { mvarId := thenMVarId, newHs := #[thenSubgoal.newH], subst := thenSubgoal.subst }
+      let thenMVarId ← thenSubgoal.mvarId.tryClearMany  hs
+      let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH (symm := false) {} (clearH := true)
+      let subgoals := subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
       match vs with
       | [] => do
         appendTagSuffix elseSubgoal.mvarId ((`case).appendIndexAfter (i+1))