fix: add expected type hints to Sym rules modified by preprocessing

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

@@ -460,7 +460,9 @@ def analyzeFrameRule (rule : BackwardRule) (opHead : Name) (numExcess : Nat) :
   -- entries of `resultPos`, which reorders the subgoal binders (non-dependent first) into the
   -- applied rule's goal list.
   let resultPos := rule.resultPos.toArray
-  forallTelescope (← Meta.inferType rule.expr) fun xs _ => do
+  -- Look through the expected type hint: `opHead` may be unfolded in the preprocessed statement.
+  let e := match_expr rule.expr with | id _ e => e | _ => rule.expr
+  forallTelescope (← Meta.inferType e) fun xs _ => do
     let premiseType (listIdx : Nat) : MetaM Expr :=
       Meta.inferType xs[resultPos[listIdx]!]!
     let mut found := none

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

@@ -94,7 +94,8 @@ public def Lean.Meta.Sym.BackwardRule.applyChecked (rule : BackwardRule) (goal :
       | .failed => return false
     if succeeded then
       let ruleDesc := ruleDesc?.getD <|
-        match rule.expr.getAppFn with
+        let e := match_expr rule.expr with | id _ e => e | _ => rule.expr
+        match e.getAppFn with
         | .const declName _ => m!"`{.ofConstName declName}`"
         | _ => m!"<rule constructed from expression>"
       throwError m!"[vcgen +debug] BackwardRule {ruleDesc} failed to \

src/Lean/Meta/Sym/Apply.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Pattern
+import Lean.Meta.AppBuilder
 import Lean.Util.CollectFVars
 import Init.Data.Range.Polymorphic.Iterators
 namespace Lean.Meta.Sym
@@ -18,7 +19,11 @@ will unify `T` with `P`, assign the goal to the theorem application,
 and return new goals for the unassigned arguments in `xs`.
 -/
 public structure BackwardRule where
-  /-- The theorem used to create the rule. It is often of the form `Expr.const declName`. -/
+  /--
+  The theorem used to create the rule. It is often of the form `Expr.const declName`. If
+  preprocessing changed the statement of a proof, it carries an expected type hint, see
+  `Simp.Theorem.expr`.
+  -/
   expr      : Expr
   /-- Precomputed pattern for efficient unification. -/
   pattern   : Pattern
@@ -84,9 +89,15 @@ The `num?` parameter optionally limits how many arguments are included in the pa
 (useful for partially applying theorems).
 -/
 public def mkBackwardRuleFromDecl (declName : Name) (num? : Option Nat := none) : MetaM BackwardRule := do
-  let pattern ← mkPatternFromDecl declName num?
+  let (levelParams, type, modified) ← preprocessDeclPattern declName (num? := num?)
+  let pattern ← mkPatternFromType levelParams type num?
   let resultPos := mkResultPos pattern
-  return { expr := mkConst declName, pattern, resultPos }
+  -- Proofs only: the value of a data rule can occur in later goals, where `id` blocks matching.
+  let expr := if modified && (← isProp type) then
+    mkExpectedPropHint (mkConst declName (levelParams.map mkLevelParam)) type
+  else
+    mkConst declName
+  return { expr, pattern, resultPos }
 
 /--
 Creates a `BackwardRule` from an expression.
@@ -98,10 +109,14 @@ The `num?` parameter optionally limits how many arguments are included in the pa
 (useful for partially applying theorems).
 -/
 public def mkBackwardRuleFromExpr (e : Expr) (levelParams : List Name := []) (num? : Option Nat := none) : MetaM BackwardRule := do
-  let pattern ← mkPatternFromExpr e levelParams num?
+  let (levelParams', type, modified) ← preprocessExprPattern e levelParams (num? := num?)
+  let pattern ← mkPatternFromType levelParams' type num?
   let resultPos := mkResultPos pattern
-  let e := e.instantiateLevelParams levelParams (pattern.levelParams.map mkLevelParam)
-  return { expr := e, pattern, resultPos }
+  let e := e.instantiateLevelParams levelParams (levelParams'.map mkLevelParam)
+  -- When `e` contains free variables, `preprocessLCtx` may have already unfolded reducible
+  -- constants in their local declarations even though the outer goal retains the original types.
+  let expr := if (modified || e.hasFVar) && (← isProp type) then mkExpectedPropHint e type else e
+  return { expr, pattern, resultPos }
 
 /--
 Creates a value to assign to input goal metavariable using unification result.

src/Lean/Meta/Sym/Pattern.lean

@@ -107,26 +107,33 @@ def isUVar? (n : Name) : Option Nat := Id.run do
   unless p == uvarPrefix do return none
   return some idx
 
-/-- Helper function for implementing `mkPatternFromDecl` and `mkEqPatternFromDecl` -/
-def preprocessDeclPattern (declName : Name) (zetaReduceLHSOnly := false) (num? : Option Nat := none) :
-    MetaM (List Name × Expr) := do
+/--
+Preprocesses the type of `declName` for use as a pattern, with its universe parameters renamed to
+`_uvar`s. Returns those parameters, the type, and whether preprocessing changed the statement
+beyond normalizing universe levels.
+-/
+public def preprocessDeclPattern (declName : Name) (zetaReduceLHSOnly := false) (num? : Option Nat := none) :
+    MetaM (List Name × Expr × Bool) := do
   let info ← getConstInfo declName
   let levelParams := info.levelParams.mapIdx fun i _ => Name.num uvarPrefix i
   let us := levelParams.map mkLevelParam
-  let type ← instantiateTypeLevelParams info.toConstantVal us
-  let type ← preprocessType type (zetaReduceLHSOnly := zetaReduceLHSOnly) (num? := num?)
+  let origType ← instantiateTypeLevelParams info.toConstantVal us
+  let type ← preprocessType origType (zetaReduceLHSOnly := zetaReduceLHSOnly) (num? := num?)
+  let modified := type != origType
   let type ← normalizeLevels type
-  return (levelParams, type)
+  return (levelParams, type, modified)
 
-def preprocessExprPattern (e : Expr) (levelParams₀ : List Name) (zetaReduceLHSOnly := false)
-    (num? : Option Nat := none) : MetaM (List Name × Expr) := do
-  let type ← inferType e
+/-- Like `preprocessDeclPattern`, for the type of `e` with universe parameters `levelParams₀`. -/
+public def preprocessExprPattern (e : Expr) (levelParams₀ : List Name) (zetaReduceLHSOnly := false)
+    (num? : Option Nat := none) : MetaM (List Name × Expr × Bool) := do
+  let origType ← inferType e
   let levelParams := levelParams₀.mapIdx fun i _ => Name.num uvarPrefix i
   let us := levelParams.map mkLevelParam
-  let type := type.instantiateLevelParams levelParams₀ us
-  let type ← preprocessType type (zetaReduceLHSOnly := zetaReduceLHSOnly) (num? := num?)
+  let origType := origType.instantiateLevelParams levelParams₀ us
+  let type ← preprocessType origType (zetaReduceLHSOnly := zetaReduceLHSOnly) (num? := num?)
+  let modified := type != origType
   let type ← normalizeLevels type
-  return (levelParams, type)
+  return (levelParams, type, modified)
 
 /--
 Creates a mask indicating which pattern variables require type checking during matching.
@@ -188,7 +195,7 @@ def mkPatternCore (type : Expr) (levelParams : List Name) (varTypes : Array Expr
     mkProofInstArgInfo? xs
   return { levelParams, varTypes, pattern, fnInfos, varInfos?, checkTypeMask? }
 
-def mkPatternFromType (levelParams : List Name) (type : Expr) (num? : Option Nat) : MetaM Pattern := do
+public def mkPatternFromType (levelParams : List Name) (type : Expr) (num? : Option Nat) : MetaM Pattern := do
   let hugeNumber := 10000000
   let num := num?.getD hugeNumber
   let rec go (i : Nat) (pattern : Expr) (varTypes : Array Expr) : MetaM Pattern := do
@@ -212,15 +219,15 @@ If `num?` is `some n`, at most `n` leading quantifiers are stripped.
 If `num?` is `none`, all leading quantifiers are stripped.
 -/
 public def mkPatternFromDecl (declName : Name) (num? : Option Nat := none) : MetaM Pattern := do
-  let (levelParams, type) ← preprocessDeclPattern declName (num? := num?)
+  let (levelParams, type, _) ← preprocessDeclPattern declName (num? := num?)
   mkPatternFromType levelParams type num?
 
 public def mkPatternFromExpr (e : Expr) (levelParams : List Name := []) (num? : Option Nat := none) : MetaM Pattern := do
-  let (levelParams, type) ← preprocessExprPattern e levelParams (num? := num?)
+  let (levelParams, type, _) ← preprocessExprPattern e levelParams (num? := num?)
   mkPatternFromType levelParams type num?
 
 @[inline]
-def mkPatternFromTypeWithKey (levelParams : List Name) (type : Expr) (selectKey : Expr → MetaM (Expr × α)) : MetaM (Pattern × α) := do
+public def mkPatternFromTypeWithKey (levelParams : List Name) (type : Expr) (selectKey : Expr → MetaM (Expr × α)) : MetaM (Pattern × α) := do
   let rec go (pattern : Expr) (varTypes : Array Expr) : MetaM (Pattern × α) := do
     if let .forallE _ d b _ := pattern then
       return (← go b (varTypes.push d))
@@ -244,7 +251,7 @@ with `n` pattern variables.
 -/
 @[inline]
 public def mkPatternFromDeclWithKey (declName : Name) (selectKey : Expr → MetaM (Expr × α)) (zetaReduceLHSOnly := false) : MetaM (Pattern × α) := do
-  let (levelParams, type) ← preprocessDeclPattern declName zetaReduceLHSOnly
+  let (levelParams, type, _) ← preprocessDeclPattern declName zetaReduceLHSOnly
   mkPatternFromTypeWithKey levelParams type selectKey
 
 /--
@@ -253,7 +260,7 @@ theorem.
 -/
 @[inline]
 public def mkPatternFromExprWithKey (e : Expr) (levelParams : List Name := []) (selectKey : Expr → MetaM (Expr × α)) (zetaReduceLHSOnly := false) : MetaM (Pattern × α) := do
-  let (levelParams, type) ← preprocessExprPattern e levelParams zetaReduceLHSOnly
+  let (levelParams, type, _) ← preprocessExprPattern e levelParams zetaReduceLHSOnly
   mkPatternFromTypeWithKey levelParams type selectKey
 
 /--

src/Lean/Meta/Sym/Simp/Theorems.lean

@@ -25,7 +25,11 @@ Contains both the theorem expression and a precomputed pattern for efficient uni
 during rewriting.
 -/
 structure Theorem where
-  /-- The theorem expression, typically `Expr.const declName` for a named theorem. -/
+  /--
+  The theorem expression, typically `Expr.const declName` for a named theorem. If preprocessing
+  changed the statement, it carries an expected type hint, so that the kernel checks the change once
+  on the theorem rather than at each instantiation, where it can re-evaluate `match` discriminants.
+  -/
   expr    : Expr
   /-- Precomputed pattern extracted from the theorem's type for efficient matching. -/
   pattern : Pattern
@@ -50,6 +54,16 @@ structure Theorem where
 instance : BEq Theorem where
   beq thm₁ thm₂ := thm₁.expr == thm₂.expr
 
+/--
+Returns the declaration name when the stored proof is a constant,
+optionally wrapped in an expected-type hint.
+-/
+def Theorem.declName? (thm : Theorem) : Option Name :=
+  let e := match_expr thm.expr with | id _ e => e | _ => thm.expr
+  match e with
+  | .const declName _ => some declName
+  | _ => none
+
 /-- Collection of simplification theorems available to the simplifier. -/
 structure Theorems where
   thms : DiscrTree Theorem := {}
@@ -209,17 +223,26 @@ private def ensurePropType (type : Expr) (declName? : Option Name := none) : Met
 def mkTheoremFromDecl (declName : Name) : MetaM Theorem := do
   let info ← getConstInfo declName
   ensurePropType info.type declName
-  let (pattern, (rhs, adaptation)) ← mkPatternFromDeclWithKey declName selectEqKey (zetaReduceLHSOnly := true)
-  let expr ← wrapProof pattern (mkConst declName) adaptation
+  let (levelParams, type, modified) ← preprocessDeclPattern declName (zetaReduceLHSOnly := true)
+  let (pattern, (rhs, adaptation)) ← mkPatternFromTypeWithKey levelParams type selectEqKey
+  let expr := if modified then
+    mkExpectedPropHint (mkConst declName (levelParams.map mkLevelParam)) type
+  else
+    mkConst declName
+  let expr ← wrapProof pattern expr adaptation
   let perm := isPerm pattern.varTypes.size pattern.pattern rhs
   let rhsVarMask := mkRhsVarMask pattern.varTypes.size rhs
   return { expr, pattern, rhs, perm, rhsVarMask }
 
 /-- Create a `Theorem` from a proof expression. Handles equalities, `¬`, `↔`, and propositions. -/
 def mkTheoremFromExpr (e : Expr) : MetaM Theorem := do
   ensurePropType (← inferType e)
-  let (pattern, (rhs, adaptation)) ← mkPatternFromExprWithKey e [] selectEqKey (zetaReduceLHSOnly := true)
-  let expr ← wrapProof pattern e adaptation
+  let (levelParams, type, modified) ← preprocessExprPattern e [] (zetaReduceLHSOnly := true)
+  let (pattern, (rhs, adaptation)) ← mkPatternFromTypeWithKey levelParams type selectEqKey
+  -- When `e` contains free variables, `preprocessLCtx` may have already unfolded reducible
+  -- constants in their local declarations even though the outer goal retains the original types.
+  let expr := if modified || e.hasFVar then mkExpectedPropHint e type else e
+  let expr ← wrapProof pattern expr adaptation
   let perm := isPerm pattern.varTypes.size pattern.pattern rhs
   let rhsVarMask := mkRhsVarMask pattern.varTypes.size rhs
   return { expr, pattern, rhs, perm, rhsVarMask }
@@ -298,11 +321,11 @@ def mkSymSimpExt (name : Name := by exact decl_name%) : IO SymSimpExtension :=
     initial  := {}
     addEntry := fun thms thm => thms.insert thm
     exportEntry? := fun _ thm =>
-      match thm.expr with
-      | .const declName _ =>
+      match thm.declName? with
+      | some declName =>
         if isPrivateName declName then ⟨none, none, some thm⟩
         else .uniform (some thm)
-      | _ => .uniform (some thm)
+      | none => .uniform (some thm)
   }
 
 abbrev SymSimpExtensionMap := Std.HashMap Name SymSimpExtension

src/Lean/Meta/Tactic/Cbv/CbvEvalExt.lean

@@ -24,12 +24,6 @@ via `mkAuxLemma`.
 -/
 
 public section
-namespace Lean.Meta.Sym.Simp
-
-def Theorem.declName (thm : Theorem) : Option Name := thm.expr.getAppFn.constName?
-
-end Lean.Meta.Sym.Simp
-
 namespace Lean.Meta.Tactic.Cbv
 open Lean.Meta.Sym.Simp
 
@@ -105,7 +99,7 @@ builtin_initialize cbvEvalExt : CbvEvalExtension ←
     initial  := {}
     addEntry := CbvEvalState.addEntry
     exportEntry? := fun _ entry =>
-      match entry.thm.declName with
+      match entry.thm.declName? with
       | none => ⟨none, none, none⟩
       | some n =>
         if isPrivateName n then ⟨none, none, some entry⟩

src/Lean/Meta/Tactic/Grind/Attr.lean

@@ -51,9 +51,7 @@ def NormSymTheorems.addEntry (s : NormSymTheorems) : NormSymEntry → NormSymThe
 
 /-- The declaration an entry refers to; entries on private declarations are not exported. -/
 private def NormSymEntry.declName? : NormSymEntry → Option Name
-  | .pre thm | .post thm | .dsimp (.thm thm) => match thm.expr with
-    | .const declName _ => some declName
-    | _ => none
+  | .pre thm | .post thm | .dsimp (.thm thm) => thm.declName?
   | .dsimp (.unfold declName) => some declName
 
 builtin_initialize normSymExt : SimpleScopedEnvExtension NormSymEntry NormSymTheorems ←

tests/elab/sym_preprocess_prop_hint.lean

@@ -0,0 +1,111 @@
+/-!
+Regression test for `Sym` rewrite and backward rules whose statements are modified by
+`Sym.preprocessType` (e.g., unfolding `Unit` to `PUnit` in `match` equation theorems, unfolding
+`@[reducible]` definitions, or beta/eta reduction).
+
+Without an expected type hint (`@id`) on the polymorphic rule before instantiating its parameters,
+the kernel has to check definitional equality between the un-preprocessed and preprocessed rule
+types at the instantiated arguments, which can trigger expensive reduction of `match` discriminants.
+Here that reduction takes 2^100 steps, so the heartbeat limit turns a regression into a kernel
+timeout rather than an out-of-memory failure.
+-/
+
+set_option maxHeartbeats 20000
+
+def tree : Nat → Nat → Bool
+  | 0, _ => true
+  | n + 1, k => tree n (2 * k) && tree n (2 * k + 1)
+
+@[cbv_eval] theorem tree_eq_true (n k : Nat) : tree n k = true := by
+  induction n generalizing k <;> simp [tree, *]
+
+def viaMatch (n : Nat) : Nat :=
+  match tree n 0 with
+  | true => 1
+  | false => 0
+
+@[reducible] def myId (x : Nat) : Nat := x
+
+def viaRed (n : Nat) : Nat :=
+  match tree n 0 with
+  | true => myId 1
+  | false => 0
+
+@[sym_simp, cbv_eval] theorem viaRed_eq (n : Nat) :
+    viaRed n = match tree n 0 with | true => myId 1 | false => 0 := by
+  rfl
+
+def applyFun (f : Nat → Nat) (x : Nat) : Nat := f x
+
+def viaEta (n : Nat) : Nat :=
+  match tree n 0 with
+  | true => applyFun (fun x => Nat.succ x) 0
+  | false => 0
+
+-- 1. `mkTheoremFromDecl` via `Sym.simp` (`Unit` in match equation, reducible unfolding, eta)
+theorem matchSym : viaMatch 100 = 1 := by
+  sym => simp [viaMatch.eq_1, tree_eq_true]
+
+theorem redSym : viaRed 100 = 1 := by
+  sym => simp [tree_eq_true]
+
+theorem etaSym : viaEta 100 = 1 := by
+  sym => simp [viaEta.eq_1, applyFun.eq_1, tree_eq_true]
+
+-- 2. `mkTheoremFromDecl` via `cbv`
+theorem matchCbv : viaMatch 100 = 1 := by
+  cbv
+
+theorem redCbv : viaRed 100 = 1 := by
+  cbv
+
+-- 3. `mkTheoremFromExpr` via `Sym.simp` on local hypotheses
+theorem matchSymLocal (h : ∀ n, viaMatch n = match tree n 0 with | true => 1 | false => 0) :
+    viaMatch 100 = 1 := by
+  sym => simp [h, tree_eq_true]
+
+theorem matchSymLocalEta (h : ∀ n, viaMatch ((fun x => x) n) = match tree n 0 with | true => 1 | false => 0) :
+    viaMatch 100 = 1 := by
+  sym => simp [h, tree_eq_true]
+
+-- 4. Non-equality theorem adapted via `EqAdaptation.eqTrue`
+inductive Hold : Nat → Prop where
+  | mk (n : Nat) : Hold (match tree n 0 with | true => 1 | false => 0)
+
+theorem hold_thm (n : Nat) : Hold (match tree n 0 with | true => 1 | false => 0) :=
+  Hold.mk n
+
+theorem simpProp : Hold (viaMatch 100) := by
+  sym => simp [viaMatch.eq_1, hold_thm]
+
+-- 5. `mkBackwardRuleFromDecl` and `mkBackwardRuleFromExpr` via `sym => apply`
+theorem applyDecl : Hold (viaMatch 100) := by
+  sym =>
+    simp [viaMatch.eq_1]
+    apply Hold.mk
+
+theorem applyExpr (h : ∀ n, Hold (match tree n 0 with | true => 1 | false => 0)) :
+    Hold (viaMatch 100) := by
+  sym =>
+    simp [viaMatch.eq_1]
+    apply h
+
+-- 6. Data rules stay unhinted: their values occur in later goals, where `id` would block matching.
+opaque IsGood : Nat → Prop
+abbrev MyNat := Nat
+def dataRule (x : MyNat) : Nat := x + 1
+axiom isGood_dataRule (x : Nat) : IsGood (dataRule x)
+
+example : ∃ x, IsGood x := by
+  sym =>
+    apply Exists.intro
+    any_goals apply dataRule
+    any_goals apply Nat.zero
+    apply isGood_dataRule
+
+example (f : Nat → Nat) (h : ∀ x, IsGood (f x)) : ∃ x, IsGood x := by
+  sym =>
+    apply Exists.intro
+    any_goals apply f
+    any_goals apply Nat.zero
+    apply h