feat: extract_lets and lift_lets tactics

src/Init/Conv.lean

@@ -318,6 +318,25 @@ syntax "repeat " convSeq : conv
 macro_rules
   | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
 
+/--
+Extracts `let` and `let_fun` expressions from within the target expression.
+This is the conv mode version of the `extract_lets` tactic.
+
+- `extract_lets` extracts all the lets from the target.
+- `extract_lets x y z` extracts all the lets from the target and uses `x`, `y`, and `z` for the first names.
+  Using `_` for a name leaves it unnamed.
+
+Limitation: the extracted local declarations do not persist outside of the `conv` goal.
+See also `lift_lets`, which does not extract lets as local declarations.
+-/
+syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* : conv
+
+/--
+Lifts `let` and `let_fun` expressions within the target expression as far out as possible.
+This is the conv mode version of the `lift_lets` tactic.
+-/
+syntax (name := liftLets) "lift_lets " optConfig : conv
+
 /--
 `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,
 by focusing on particular subexpressions.

src/Init/MetaTypes.lean

@@ -286,4 +286,44 @@ inductive Occurrences where
 
 instance : Coe (List Nat) Occurrences := ⟨.pos⟩
 
+/--
+Configuration for the `extract_lets` tactic.
+-/
+structure ExtractLetsConfig where
+  /-- If true (default: false), extract lets from subterms that are proofs.
+  Top-level lets are always extracted. -/
+  proofs : Bool := false
+  /-- If true (default: true), extract lets from subterms that are types.
+  Top-level lets are always extracted. -/
+  types : Bool := true
+  /-- If true (default: false), extract lets from subterms that are implicit arguments. -/
+  implicits : Bool := false
+  /-- If false (default: true), extracts only top-level lets, otherwise allows descending into subterms.
+  When false, `proofs` and `types` are ignored, and lets appearing in the types or values of the
+  top-level lets are not themselves extracted. -/
+  descend : Bool := true
+  /-- If true (default: true), descend into forall/lambda/let bodies when extracting. Only relevant when `descend` is true. -/
+  underBinder : Bool := true
+  /-- If true (default: false), eliminate unused lets rather than extract them. -/
+  usedOnly : Bool := false
+  /-- If true (default: true), reuse local declarations that have syntactically equal values.
+  Note that even when false, the caching strategy for `extract_let`s may result in fewer extracted let bindings than expected. -/
+  merge : Bool := true
+  /-- When merging is enabled, if true (default: true), make use of pre-existing local definitions in the local context. -/
+  useContext : Bool := true
+  /-- If true (default: false), then once `givenNames` is exhausted, stop extracting lets. Otherwise continue extracting lets. -/
+  onlyGivenNames : Bool := false
+  /-- If true (default: false), then when no name is provided for a 'let' expression, the name is used as-is without making it be inaccessible.
+  The name still might be inaccessible if the binder name was. -/
+  preserveBinderNames : Bool := false
+  /-- If true (default: false), lift non-extractable `let`s as far out as possible. -/
+  lift : Bool := false
+
+/--
+Configuration for the `lift_lets` tactic.
+-/
+structure LiftLetsConfig extends ExtractLetsConfig where
+  lift := true
+  preserveBinderNames := true
+
 end Lean.Meta

src/Init/Tactics.lean

@@ -496,6 +496,38 @@ syntax (name := change) "change " term (location)? : tactic
 -/
 syntax (name := changeWith) "change " term " with " term (location)? : tactic
 
+/--
+Extracts `let` and `let_fun` expressions from within the target or a local hypothesis,
+introducing new local definitions.
+
+- `extract_lets` extracts all the lets from the target.
+- `extract_lets x y z` extracts all the lets from the target and uses `x`, `y`, and `z` for the first names.
+  Using `_` for a name leaves it unnamed.
+- `extract_lets x y z at h` operates on the local hypothesis `h` instead of the target.
+
+For example, given a local hypotheses if the form `h : let x := v; b x`, then `extract_lets z at h`
+introduces a new local definition `z := v` and changes `h` to be `h : b z`.
+-/
+syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* (location)? : tactic
+
+/--
+Lifts `let` and `let_fun` expressions within a term as far out as possible.
+It is like `extract_lets +lift`, but the top-level lets at the end of the procedure
+are not extracted as local hypotheses.
+
+- `lift_lets` lifts let expressions in the target.
+- `lift_lets at h` lifts let expressions at the given local hypothesis.
+
+For example,
+```lean
+example : (let x := 1; x) = 1 := by
+  lift_lets
+  -- ⊢ let x := 1; x = 1
+  ...
+```
+-/
+syntax (name := liftLets) "lift_lets " optConfig (location)? : tactic
+
 /--
 If `thm` is a theorem `a = b`, then as a rewrite rule,
 * `thm` means to replace `a` with `b`, and

src/Lean/Elab/Tactic.lean

@@ -50,3 +50,4 @@ import Lean.Elab.Tactic.AsAuxLemma
 import Lean.Elab.Tactic.TreeTacAttr
 import Lean.Elab.Tactic.ExposeNames
 import Lean.Elab.Tactic.SimpArith
+import Lean.Elab.Tactic.Lets

src/Lean/Elab/Tactic/Conv.lean

@@ -8,6 +8,7 @@ import Lean.Elab.Tactic.Conv.Basic
 import Lean.Elab.Tactic.Conv.Congr
 import Lean.Elab.Tactic.Conv.Rewrite
 import Lean.Elab.Tactic.Conv.Change
+import Lean.Elab.Tactic.Conv.Lets
 import Lean.Elab.Tactic.Conv.Simp
 import Lean.Elab.Tactic.Conv.Pattern
 import Lean.Elab.Tactic.Conv.Delta

src/Lean/Elab/Tactic/Conv/Lets.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Elab.Tactic.Lets
+import Lean.Elab.Tactic.Conv.Basic
+
+/-!
+# Conv tactics to manipulate `let` expressions
+-/
+
+open Lean Meta
+
+namespace Lean.Elab.Tactic.Conv
+
+/-!
+### `extract_lets`
+-/
+
+@[builtin_tactic Lean.Parser.Tactic.Conv.extractLets] elab_rules : tactic
+  | `(conv| extract_lets $cfg:optConfig $ids*) => do
+    let mut config ← elabExtractLetsConfig cfg
+    let givenNames := (ids.map getNameOfIdent').toList
+    let (lhs, rhs) ← getLhsRhs
+    let fvars ← liftMetaTacticAux fun mvarId => do
+      mvarId.checkNotAssigned `extract_lets
+      Meta.extractLets #[lhs] givenNames (config := config) fun fvarIds es _ => do
+        let lhs' := es[0]!
+        if fvarIds.isEmpty && lhs == lhs' then
+          throwTacticEx `extract_lets mvarId m!"made no progress"
+        let (rhs', g) ← mkConvGoalFor lhs' (← mvarId.getTag)
+        let fvars := fvarIds.map .fvar
+        let assign (mvar : MVarId) (e : Expr) : MetaM Unit := do
+          let e ← mkLetFVars (usedLetOnly := false) fvars e
+          mvar.withContext do
+            unless ← isDefEq (.mvar mvar) e do
+              throwTacticEx `extract_lets mvarId m!"(internal error) non-defeq in assignment"
+            mvar.assign e
+        assign rhs'.mvarId! rhs
+        assign mvarId g
+        return (fvarIds, [g.mvarId!])
+    extractLetsAddVarInfo ids fvars
+
+/-!
+### `lift_lets`
+-/
+
+@[builtin_tactic Lean.Parser.Tactic.Conv.liftLets] elab_rules : tactic
+  | `(conv| lift_lets $cfg:optConfig) => do
+    let mut config ← elabLiftLetsConfig cfg
+    withMainContext do
+      let lhs ← getLhs
+      let lhs' ← Meta.liftLets lhs config
+      if lhs == lhs' then
+        throwTacticEx `lift_lets (← getMainGoal) m!"made no progress"
+      changeLhs lhs'
+
+end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Lets.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Meta.Tactic.Lets
+import Lean.Elab.Tactic.Location
+
+/-!
+# Tactics to manipulate `let` expressions
+-/
+
+open Lean Meta
+
+namespace Lean.Elab.Tactic
+
+register_builtin_option linter.tactic.unusedName : Bool := {
+  defValue := true,
+  descr := "enable the 'unused name' tactic linter"
+}
+
+/-!
+### `extract_lets`
+-/
+
+def extractLetsAddVarInfo (ids : Array Syntax) (fvars : Array FVarId) : TacticM Unit :=
+  withMainContext do
+    for h : i in [0:ids.size] do
+      if h' : i < fvars.size then
+        Term.addLocalVarInfo ids[i] (mkFVar fvars[i])
+      else
+        Linter.logLintIf linter.tactic.unusedName ids[i] m!"unused name"
+
+declare_config_elab elabExtractLetsConfig ExtractLetsConfig
+
+@[builtin_tactic extractLets] elab_rules : tactic
+  | `(tactic| extract_lets $cfg:optConfig $ids* $[$loc?:location]?) => do
+    let mut config ← elabExtractLetsConfig cfg
+    let givenNames := (ids.map getNameOfIdent').toList
+    withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
+      (atLocal := fun h => do
+        let fvars ← liftMetaTacticAux fun mvarId => do
+          let ((fvars, _), mvarId) ← mvarId.extractLetsLocalDecl h givenNames config
+          return (fvars, [mvarId])
+        extractLetsAddVarInfo ids fvars)
+      (atTarget := do
+        let fvars ← liftMetaTacticAux fun mvarId => do
+          let ((fvars, _), mvarId) ← mvarId.extractLets givenNames config
+          return (fvars, [mvarId])
+        extractLetsAddVarInfo ids fvars)
+      (failed := fun _ => throwError "'extract_lets' tactic failed")
+
+/-!
+### `lift_lets`
+-/
+
+declare_config_elab elabLiftLetsConfig LiftLetsConfig
+
+@[builtin_tactic liftLets] elab_rules : tactic
+  | `(tactic| lift_lets $cfg:optConfig $[$loc?:location]?) => do
+    let mut config ← elabLiftLetsConfig cfg
+    withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
+      (atLocal := fun h => liftMetaTactic1 fun mvarId => mvarId.liftLetsLocalDecl h config)
+      (atTarget := liftMetaTactic1 fun mvarId => mvarId.liftLets config)
+      (failed := fun _ => throwError "'lift_lets' tactic failed")
+
+end Lean.Elab.Tactic

src/Lean/Meta/AppBuilder.lean

@@ -27,13 +27,17 @@ def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
 /--
 `mkLetFun x v e` creates the encoding for the `let_fun x := v; e` expression.
 The expression `x` can either be a free variable or a metavariable, and the function suitably abstracts `x` in `e`.
-NB: `x` must not be a let-bound free variable.
 -/
 def mkLetFun (x : Expr) (v : Expr) (e : Expr) : MetaM Expr := do
-  let f ← mkLambdaFVars #[x] e
+  -- If `x` is an `ldecl`, then the result of `mkLambdaFVars` is a let expression.
+  let ensureLambda : Expr → Expr
+    | .letE n t _ b _ => .lam n t b .default
+    | e@(.lam ..)     => e
+    | _               => unreachable!
+  let f ← ensureLambda <$> mkLambdaFVars (usedLetOnly := false) #[x] e
   let ety ← inferType e
   let α ← inferType x
-  let β ← mkLambdaFVars #[x] ety
+  let β ← ensureLambda <$> mkLambdaFVars (usedLetOnly := false) #[x] ety
   let u1 ← getLevel α
   let u2 ← getLevel ety
   return mkAppN (.const ``letFun [u1, u2]) #[α, β, v, f]

src/Lean/Meta/Basic.lean

@@ -604,6 +604,9 @@ export Core (instantiateTypeLevelParams instantiateValueLevelParams)
 @[inline] def map2MetaM [MonadControlT MetaM m] [Monad m] (f : forall {α}, (β → γ → MetaM α) → MetaM α) {α} (k : β → γ → m α) : m α :=
   controlAt MetaM fun runInBase => f fun b c => runInBase <| k b c
 
+@[inline] def map3MetaM [MonadControlT MetaM m] [Monad m] (f : forall {α}, (β → γ → δ → MetaM α) → MetaM α) {α} (k : β → γ → δ → m α) : m α :=
+  controlAt MetaM fun runInBase => f fun b c d => runInBase <| k b c d
+
 section Methods
 variable [MonadControlT MetaM n] [Monad n]
 
@@ -1926,6 +1929,76 @@ private partial def instantiateLambdaAux (ps : Array Expr) (i : Nat) (e : Expr)
 def instantiateLambda (e : Expr) (ps : Array Expr) : MetaM Expr :=
   instantiateLambdaAux ps 0 e
 
+/--
+A simpler version of `ParamInfo` for information about the parameter of a forall or lambda.
+-/
+structure ExprParamInfo where
+  /-- The name of the parameter. -/
+  name : Name
+  /-- The type of the parameter. -/
+  type : Expr
+  /-- The binder annotation for the parameter. -/
+  binderInfo : BinderInfo := BinderInfo.default
+  deriving Inhabited
+
+/--
+Given `e` of the form `∀ (p₁ : P₁) … (p₁ : P₁), B[p_1,…,p_n]` and `arg₁ : P₁, …, argₙ : Pₙ`, returns
+* the names `p₁, …, pₙ`,
+* the binder infos,
+* the binder types `P₁, P₂[arg₁], …, P[arg₁,…,argₙ₋₁]`, and
+* the type `B[arg₁,…,argₙ]`.
+
+It uses `whnf` to reduce `e` if it is not a forall.
+
+See also `Lean.Meta.instantiateForall`.
+-/
+def instantiateForallWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnotations : Bool := false) :
+    MetaM (Array ExprParamInfo × Expr) := do
+  let mut e := e
+  let mut res := Array.mkEmpty args.size
+  let mut j := 0
+  for i in [0:args.size] do
+    unless e.isForall do
+      e ← whnf (e.instantiateRevRange j i args)
+      j := i
+    match e with
+    | .forallE name type e' binderInfo =>
+      let type := type.instantiateRevRange j i args
+      let type := if cleanupAnnotations then type.cleanupAnnotations else type
+      res := res.push { name, type, binderInfo }
+      e := e'
+    | _ => throwError "invalid `instantiateForallWithParams`, too many parameters{indentExpr e}"
+  return (res, e)
+
+/--
+Given `e` of the form `fun (p₁ : P₁) … (p₁ : P₁) => t[p_1,…,p_n]` and `arg₁ : P₁, …, argₙ : Pₙ`, returns
+* the names `p₁, …, pₙ`,
+* the binder infos,
+* the binder types `P₁, P₂[arg₁], …, P[arg₁,…,argₙ₋₁]`, and
+* the term `t[arg₁,…,argₙ]`.
+
+It uses `whnf` to reduce `e` if it is not a lambda.
+
+See also `Lean.Meta.instantiateLambda`.
+-/
+def instantiateLambdaWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnotations : Bool := false) :
+    MetaM (Array ExprParamInfo × Expr) := do
+  let mut e := e
+  let mut res := Array.mkEmpty args.size
+  let mut j := 0
+  for i in [0:args.size] do
+    unless e.isLambda do
+      e ← whnf (e.instantiateRevRange j i args)
+      j := i
+    match e with
+    | .forallE name type e' binderInfo =>
+      let type := type.instantiateRevRange j i args
+      let type := if cleanupAnnotations then type.cleanupAnnotations else type
+      res := res.push { name, type, binderInfo }
+      e := e'
+    | _ => throwError "invalid `instantiateForallWithParams`, too many parameters{indentExpr e}"
+  return (res, e)
+
 /-- Pretty-print the given expression. -/
 def ppExprWithInfos (e : Expr) : MetaM FormatWithInfos := do
   let ctxCore  ← readThe Core.Context

src/Lean/Meta/Tactic.lean

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Tactic.Generalize
 import Lean.Meta.Tactic.Replace
+import Lean.Meta.Tactic.Lets
 import Lean.Meta.Tactic.Induction
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.ElimInfo