From e442fbbf54cfad6eb65bfb5569795e84b41e137a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Jun 2022 16:35:18 -0700
Subject: [PATCH] fix: remove `kabstractWithPred`

The function `kabstractWithPred` was never used, and introduced the
bug exposed by issue #1235.

fixes #1235
---
 src/Lean/Meta/KAbstract.lean         | 31 ----------------------------
 src/Lean/Meta/Tactic/Generalize.lean |  4 ++--
 tests/lean/1235.lean                 |  8 +++++++
 tests/lean/1235.lean.expected.out    |  4 ++++
 4 files changed, 14 insertions(+), 33 deletions(-)
 create mode 100644 tests/lean/1235.lean
 create mode 100644 tests/lean/1235.lean.expected.out

diff --git a/src/Lean/Meta/KAbstract.lean b/src/Lean/Meta/KAbstract.lean
index ee534ac938..38f60e9a63 100644
--- a/src/Lean/Meta/KAbstract.lean
+++ b/src/Lean/Meta/KAbstract.lean
@@ -41,35 +41,4 @@ def kabstract (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : Me
         visitChildren ()
     visit e 0 |>.run' 1
 
-/--
-  Similar to `kabstract`, but only abstracts occurrences of `p` s.t. `pred parent? p` is true where `parent?`
-  is the parent expression for `p` if any.
--/
-partial def kabstractWithPred (e : Expr) (p : Expr) (pred : (parent? : Option Expr) → (e : Expr) → MetaM Bool) : MetaM Expr := do
-  let e ← instantiateMVars e
-  let pHeadIdx := p.toHeadIndex
-  let pNumArgs := p.headNumArgs
-  let rec visit (parent? : Option Expr) (e : Expr) (offset : Nat) : MetaM Expr := do
-    let visitChildren : Unit → MetaM Expr := fun _ => do
-      match e with
-      | Expr.app ..          => e.withApp fun f args => return mkAppN (← visit e f offset) (← args.mapM (visit e . offset))
-      | Expr.mdata _ b _     => return e.updateMData! (← visit e b offset)
-      | Expr.proj _ _ b _    => return e.updateProj! (← visit e b offset)
-      | Expr.letE _ t v b _  => return e.updateLet! (← visit e t offset) (← visit e v offset) (← visit e b (offset+1))
-      | Expr.lam _ d b _     => return e.updateLambdaE! (← visit e d offset) (← visit e b (offset+1))
-      | Expr.forallE _ d b _ => return e.updateForallE! (← visit e d offset) (← visit e b (offset+1))
-      | e                    => return e
-    if e.hasLooseBVars then
-      visitChildren ()
-    else if e.toHeadIndex != pHeadIdx || e.headNumArgs != pNumArgs then
-      visitChildren ()
-    else if (← isDefEq e p) then
-      if (← pred parent? e) then
-        return mkBVar offset
-      else
-        visitChildren ()
-    else
-      visitChildren ()
-  visit none e 0
-
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Generalize.lean b/src/Lean/Meta/Tactic/Generalize.lean
index 90f8d3c430..8c560467b6 100644
--- a/src/Lean/Meta/Tactic/Generalize.lean
+++ b/src/Lean/Meta/Tactic/Generalize.lean
@@ -18,7 +18,7 @@ structure GeneralizeArg where
 
 partial def generalize
     (mvarId : MVarId) (args : Array GeneralizeArg)
-    (pred : (parent? : Option Expr) → (e : Expr) → MetaM Bool := fun _ _ => return true)
+    -- (pred : (parent? : Option Expr) → (e : Expr) → MetaM Bool := fun _ _ => return true)
     : MetaM (Array FVarId × MVarId) :=
   withMVarContext mvarId do
     checkNotAssigned mvarId `generalize
@@ -31,7 +31,7 @@ partial def generalize
         let eType ← instantiateMVars (← inferType e)
         let type ← go (i+1)
         let xName ← if let some xName := arg.xName? then pure xName else mkFreshUserName `x
-        return Lean.mkForall xName BinderInfo.default eType (← kabstractWithPred type e pred)
+        return Lean.mkForall xName BinderInfo.default eType (← kabstract type e)
       else
         return target
     let targetNew ← go 0
diff --git a/tests/lean/1235.lean b/tests/lean/1235.lean
new file mode 100644
index 0000000000..b9e0f4b994
--- /dev/null
+++ b/tests/lean/1235.lean
@@ -0,0 +1,8 @@
+opaque f (a b : Nat) : Nat
+example : f 1 2 = f 2 1 := by
+  generalize h : f 1 = g
+  /- g : ℕ → ℕ
+  h : f 1 = g
+  ⊢ g 2 = f 2 1 -/
+  trace_state
+  sorry
diff --git a/tests/lean/1235.lean.expected.out b/tests/lean/1235.lean.expected.out
new file mode 100644
index 0000000000..aa7dcb6381
--- /dev/null
+++ b/tests/lean/1235.lean.expected.out
@@ -0,0 +1,4 @@
+1235.lean:2:0-2:7: warning: declaration uses 'sorry'
+g : Nat → Nat
+h : f 1 = g
+⊢ g 2 = f 2 1