feat: add optional binder limit to mkPatternFromTheorem

This PR adds `num?` parameter to `mkPatternFromTheorem` to control how
many leading quantifiers are stripped when creating a pattern. This
enables matching theorems where only some quantifiers should be
converted to pattern variables.

For example, to match `mk_forall_and : (∀ x, P x) → (∀ x, Q x) → (∀ x, P x ∧ Q x)`
against a goal `∀ x, q x 0 ∧ q (f (f x)) y`, we use `mkPatternFromTheorem ``mk_forall_and (some 5)`
to create the pattern `∀ x, ?P x ∧ ?Q x`, keeping the outermost `∀` in the pattern rather
than converting it to a pattern variable.

src/Lean/Meta/Sym/Pattern.lean

@@ -68,21 +68,35 @@ def isUVar? (n : Name) : Option Nat := Id.run do
   unless p == uvarPrefix do return none
   return some idx
 
-public def mkPatternFromTheorem (declName : Name) : MetaM Pattern := do
+/--
+Creates a `Pattern` from the type of a theorem.
+
+The pattern is constructed by stripping leading universal quantifiers from the theorem's type.
+Each quantified variable becomes a pattern variable, with its type recorded in `varTypes` and
+whether it is a type class instance recorded in `isInstance`. The remaining type after
+stripping quantifiers becomes the `pattern` expression.
+
+Universe level parameters are replaced with fresh unification variables (prefixed with `_uvar`).
+
+If `num?` is `some n`, at most `n` leading quantifiers are stripped.
+If `num?` is `none`, all leading quantifiers are stripped.
+-/
+public def mkPatternFromTheorem (declName : Name) (num? : Option Nat := none) : MetaM Pattern := 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
-  let rec go (type : Expr) (varTypes : Array Expr) (isInstance : Array Bool) : MetaM Pattern := do
-    match type with
-    | .forallE _ d b _ =>
-      go b (varTypes.push d) (isInstance.push (isClass? (← getEnv) d).isSome)
-    | _ =>
-      let pattern := type
-      let fnInfos ← mkProofInstInfoMapFor pattern
-      return { levelParams, varTypes, isInstance, pattern, fnInfos }
-  go type #[] #[]
+  let hugeNumber := 10000000
+  let num := num?.getD hugeNumber
+  let rec go (i : Nat) (type : Expr) (varTypes : Array Expr) (isInstance : Array Bool) : MetaM Pattern := do
+    if i < num then
+      if let .forallE _ d b _ := type then
+        return (← go (i+1) b (varTypes.push d) (isInstance.push (isClass? (← getEnv) d).isSome))
+    let pattern := type
+    let fnInfos ← mkProofInstInfoMapFor pattern
+    return { levelParams, varTypes, isInstance, pattern, fnInfos }
+  go 0 type #[] #[]
 
 structure UnifyM.Context where
   pattern   : Pattern

tests/lean/run/sym_pattern_2.lean

@@ -5,11 +5,11 @@ opaque p [Ring α] : α → α → Prop
 axiom pax [CommRing α] [NoNatZeroDivisors α] (x y : α) : p x y → p (y + 1) x
 opaque a : Int
 opaque b : Int
-def ex := p (a + 1) b
+def ex₁ := p (a + 1) b
 
-def test : SymM Unit := do
+def test₁ : SymM Unit := do
   let pEx ← mkPatternFromTheorem ``pax
-  let e ← shareCommon (← getConstInfo ``ex).value!
+  let e ← shareCommon (← getConstInfo ``ex₁).value!
   let some r₁ ← pEx.match? e | throwError "failed"
   let h := mkAppN (mkConst ``pax r₁.us) r₁.args
   check h
@@ -22,4 +22,39 @@ info: pax b a ?m.1
 info: #[Int, instCommRingInt, instNoNatZeroDivisorsInt, b, a, ?m.1]
 -/
 #guard_msgs in
-#eval SymM.run' test
+#eval SymM.run' test₁
+
+theorem mk_forall_and (P Q : α → Prop) : (∀ x, P x) → (∀ x, Q x) → (∀ x, P x ∧ Q x) := by
+  grind
+
+opaque q : Nat → Nat → Prop
+opaque f : Nat → Nat
+
+def ex₂ := ∀ x, q x 0 ∧ q (f (f x)) (f x + f (f 1))
+
+def test₂ : SymM Unit := do
+  /- We use `some 5` because we want the pattern to be `(∀ x, ?P x ∧ ?Q x)`-/
+  let p ← mkPatternFromTheorem ``mk_forall_and (some 5)
+  let e ← shareCommon (← getConstInfo ``ex₂).value!
+  logInfo p.pattern
+  logInfo e
+  let some r₁ ← p.unify? e | throwError "failed"
+  let h := mkAppN (mkConst ``mk_forall_and r₁.us) r₁.args
+  check h
+  logInfo h
+  logInfo (← inferType r₁.args[3]!)
+  logInfo (← inferType r₁.args[4]!)
+
+/--
+info: ∀ (x : #4), @#3 x ∧ @#2 x
+---
+info: ∀ (x : Nat), q x 0 ∧ q (f (f x)) (f x + f (f 1))
+---
+info: mk_forall_and (fun x => q x 0) (fun x => q (f (f x)) (f x + f (f 1))) ?m.4 ?m.5
+---
+info: ∀ (x : Nat), q x 0
+---
+info: ∀ (x : Nat), q (f (f x)) (f x + f (f 1))
+-/
+#guard_msgs in
+#eval SymM.run' test₂