chore: revert "feat: abstract metavariables when generalizing match motives (#8099) (#11696)"

This PR reverts #11696.

Author: sgraf812

src/Init/Grind/Ring/CommSolver.lean

@@ -766,7 +766,7 @@ def Poly.cancelVar (c : Int) (x : Var) (p : Poly) : Poly :=
           (fun _ _ _ _ => a.toPoly_k.pow k)
           (fun _ _ _ _ => a.toPoly_k.pow k)
           (fun _ _ _ => a.toPoly_k.pow k)
-          a) = match (generalizing := false) a with
+          a) = match a with
             | num n => Poly.num (n ^ k)
             | .intCast n => .num (n^k)
             | .natCast n => .num (n^k)

src/Lean/Elab/Match.lean

@@ -886,7 +886,7 @@ private def generalize (discrs : Array Discr) (matchType : Expr) (altViews : Arr
       let matchType' ← forallBoundedTelescope matchType discrs.size fun ds type => do
         let type ← mkForallFVars ys type
         let (discrs', ds') := Array.unzip <| Array.zip discrExprs ds |>.filter fun (di, _) => di.isFVar
-        let type ← type.replaceFVarsM discrs' ds'
+        let type := type.replaceFVars discrs' ds'
         mkForallFVars ds type
       if (← isTypeCorrect matchType') then
         let discrs := discrs ++  ys.map fun y => { expr := y : Discr }
@@ -1119,11 +1119,11 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
       withRef altLHS.ref do
         for d in altLHS.fvarDecls do
           if d.hasExprMVar then
-            -- This code path is a vestige prior to fixing #8099, but it is still appears to be
-            -- important for testcase 1300.lean.
             tryPostpone
             withExistingLocalDecls altLHS.fvarDecls do
               runPendingTacticsAt d.type
+              if (← instantiateMVars d.type).hasExprMVar then
+                throwMVarError m!"Invalid match expression: The type of pattern variable '{d.toExpr}' contains metavariables:{indentExpr d.type}"
         for p in altLHS.patterns do
           if (← Match.instantiatePatternMVars p).hasExprMVar then
             tryPostpone

src/Lean/Elab/Tactic/Do/VCGen.lean

@@ -196,18 +196,8 @@ where
     -- context = fun e => H ⊢ₛ wp⟦e⟧ Q
     let context ← withLocalDecl `e .default (mkApp m α) fun e => do
       mkLambdaFVars #[e] (goal.withNewProg e).toExpr
-    return ← info.splitWith goal.toExpr (useSplitter := true) fun altSuff expAltType idx params => do
-      burnOne
-      let e ← mkFreshExprMVar (mkApp m α)
-      unless ← isDefEq (goal.withNewProg e).toExpr expAltType do
-        throwError "The alternative type {expAltType} returned by `splitWith` does not match {(goal.withNewProg e).toExpr}. This is a bug in `mvcgen`."
-      let e ← instantiateMVarsIfMVarApp e
+    return ← info.splitWithConstantMotive goal.toExpr (useSplitter := true) fun altSuff idx params => do
       let res ← liftMetaM <| rwIfOrMatcher idx e
-      -- When `FunInd.rwMatcher` fails, it returns the original expression. We'd loop in that case,
-      -- so we rather throw an error.
-      if res.expr == e then
-        throwError "`rwMatcher` failed to rewrite {indentExpr e}\n\
-          Check the output of `trace.Elab.Tactic.Do.vcgen.split` for more info and submit a bug report."
       let goal' := goal.withNewProg res.expr
       let prf ← withAltCtx idx params <| onWPApp goal' (name ++ altSuff)
       let res ← Simp.mkCongrArg context res
@@ -253,7 +243,7 @@ where
       mkFreshExprSyntheticOpaqueMVar hypsTy (name.appendIndexAfter i)
 
     let (joinPrf, joinGoal) ← forallBoundedTelescope joinTy numJoinParams fun joinParams _body => do
-      let φ ← info.splitWith (mkSort .zero) fun _suff _expAltType idx altParams =>
+      let φ ← info.splitWithConstantMotive (mkSort .zero) fun _suff idx altParams =>
         return mkAppN hypsMVars[idx]! (joinParams ++ altParams)
       withLocalDecl (← mkFreshUserName `h) .default φ fun h => do
         -- NB: `mkJoinGoal` is not quite `goal.withNewProg` because we only take 4 args and clear

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -16,7 +16,6 @@ namespace Lean.Elab.Tactic.Do
 open Lean Parser Elab Tactic Meta Do SpecAttr
 
 builtin_initialize registerTraceClass `Elab.Tactic.Do.vcgen
-builtin_initialize registerTraceClass `Elab.Tactic.Do.vcgen.split
 
 register_builtin_option mvcgen.warning : Bool := {
   defValue := true

src/Lean/Elab/Tactic/Do/VCGen/Split.lean

@@ -6,10 +6,8 @@ Authors: Sebastian Graf
 module
 
 prelude
-public import Lean.Meta.Tactic.Simp.Types
+public import Lean.Meta.Tactic.FunInd
 public import Lean.Meta.Match.MatcherApp.Transform
-public import Lean.Data.Array
-import Lean.Meta.Match.Rewrite
 import Lean.Meta.Tactic.Simp.Rewrite
 import Lean.Meta.Tactic.Assumption
 
@@ -51,40 +49,36 @@ def altInfos (info : SplitInfo) : Array (Nat × Expr) := match info with
   | matcher matcherApp => matcherApp.altNumParams.mapIdx fun idx numParams =>
       (numParams, matcherApp.alts[idx]!)
 
-def splitWith
+def splitWithConstantMotive
   {n} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadEnv n] [MonadLog n]
   [AddMessageContext n] [MonadOptions n]
-  (info : SplitInfo) (resTy : Expr) (onAlt : Name → Expr → Nat → Array Expr → n Expr) (useSplitter := false) : n Expr := match info with
+  (info : SplitInfo) (resTy : Expr) (onAlt : Name → Nat → Array Expr → n Expr) (useSplitter := false) : n Expr := match info with
   | ite e => do
     let u ← getLevel resTy
     let c := e.getArg! 1
     let h := e.getArg! 2
     if useSplitter then -- dite is the "splitter" for ite
       let n ← liftMetaM <| mkFreshUserName `h
-      let t ← withLocalDecl n .default c fun h => do mkLambdaFVars #[h] (← onAlt `isTrue resTy 0 #[])
-      let e ← withLocalDecl n .default (mkNot c) fun h => do mkLambdaFVars #[h] (← onAlt `isFalse resTy 1 #[])
+      let t ← withLocalDecl n .default c fun h => do mkLambdaFVars #[h] (← onAlt `isTrue 0 #[])
+      let e ← withLocalDecl n .default (mkNot c) fun h => do mkLambdaFVars #[h] (← onAlt `isFalse 1 #[])
       return mkApp5 (mkConst ``_root_.dite [u]) resTy c h t e
     else
-      let t ← onAlt `isTrue resTy 0 #[]
-      let e ← onAlt `isFalse resTy 1 #[]
+      let t ← onAlt `isTrue 0 #[]
+      let e ← onAlt `isFalse 1 #[]
       return mkApp5 (mkConst ``_root_.ite [u]) resTy c h t e
   | dite e => do
     let u ← getLevel resTy
     let c := e.getArg! 1
     let h := e.getArg! 2
     let n ← liftMetaM <| mkFreshUserName `h
-    let t ← withLocalDecl n .default c fun h => do mkLambdaFVars #[h] (← onAlt `isTrue resTy 0 #[h])
-    let e ← withLocalDecl n .default (mkNot c) fun h => do mkLambdaFVars #[h] (← onAlt `isFalse resTy 1 #[h])
+    let t ← withLocalDecl n .default c fun h => do mkLambdaFVars #[h] (← onAlt `isTrue 0 #[h])
+    let e ← withLocalDecl n .default (mkNot c) fun h => do mkLambdaFVars #[h] (← onAlt `isFalse 1 #[h])
     return mkApp5 (mkConst ``_root_.dite [u]) resTy c h t e
   | matcher matcherApp => do
-    let mask := matcherApp.discrs.map (·.isFVar)
-    let maskedDiscrs := Array.mask mask matcherApp.discrs
-    let absMotiveBody ← resTy.abstractM maskedDiscrs
     (·.toExpr) <$> matcherApp.transform
       (useSplitter := useSplitter) (addEqualities := useSplitter) -- (freshenNames := true)
-      (onMotive := fun xs _body => pure (absMotiveBody.instantiateRev (Array.mask mask xs)))
-      (onAlt := fun idx expAltType params _alt => do
-        onAlt ((`h).appendIndexAfter (idx+1)) expAltType idx params)
+      (onMotive := fun _xs _motive => pure resTy)
+      (onAlt := fun idx _ty params _alt => onAlt ((`h).appendIndexAfter (idx+1)) idx params)
 
 def simpDiscrs? (info : SplitInfo) (e : Expr) : SimpM (Option Simp.Result) := match info with
   | dite _ | ite _ => return none -- Tricky because we need to simultaneously rewrite  `[Decidable c]`
@@ -108,6 +102,6 @@ def rwIfOrMatcher (idx : Nat) (e : Expr) : MetaM Simp.Result := do
     let c := if idx = 0 then c else mkNot c
     let .some fv ← findLocalDeclWithType? c
       | throwError "Failed to find proof for if condition {c}"
-    rwIfWith (mkFVar fv) e
+    FunInd.rwIfWith (mkFVar fv) e
   else
-    rwMatcher idx e
+    FunInd.rwMatcher idx e

src/Lean/Meta/Basic.lean

@@ -1097,13 +1097,6 @@ Similar to `Expr.abstract`, but handles metavariables correctly.
 def _root_.Lean.Expr.abstractM (e : Expr) (xs : Array Expr) : MetaM Expr :=
   e.abstractRangeM xs.size xs
 
-/--
-Replace occurrences of the free variables `fvars` in `e` with `vs`.
-Similar to `Expr.replaceFVars`, but handles metavariables correctly.
--/
-def _root_.Lean.Expr.replaceFVarsM (e : Expr) (fvars : Array Expr) (vs : Array Expr) : MetaM Expr :=
-  return (← e.abstractM fvars).instantiateRev vs
-
 /--
 Collect forward dependencies for the free variables in `toRevert`.
 Recall that when reverting free variables `xs`, we must also revert their forward dependencies.

src/Lean/Meta/Match/Rewrite.lean

@@ -51,13 +51,6 @@ def MVarId.congr? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
     let some congrThm ← mkCongrSimp? lhs.getAppFn (subsingletonInstImplicitRhs := false) (maxArgs? := lhs.getAppNumArgs) | return none
     applyCongrThm? mvarId congrThm
 
-/--
-Try to apply a `simp` congruence theorem and throw an error if it fails.
--/
-def MVarId.congr (mvarId : MVarId) : MetaM (List MVarId) := do
-  let some mvarIds ← mvarId.congr? | throwError "Failed to apply `simp` congruence theorem"
-  return mvarIds
-
 /--
 Try to apply a `hcongr` congruence theorem, and then tries to close resulting goals
 using `Eq.refl`, `HEq.refl`, and assumption.