From 517899da7be31fa33f8b15bf0ad3c7e090d59445 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 21 Apr 2025 01:57:01 -0700 Subject: [PATCH] feat: `extract_lets` and `lift_lets` tactics (#6432) This PR implements tactics called `extract_lets` and `lift_lets` that manipulate `let`/`let_fun` expressions. The `extract_lets` tactic creates new local declarations extracted from any `let` and `let_fun` expressions in the main goal. For top-level lets in the target, it is like the `intros` tactic, but in general it can extract lets from deeper subexpressions as well. The `lift_lets` tactic moves `let` and `let_fun` expressions as far out of an expression as possible, but it does not extract any new local declarations. The option `extract_lets +lift` combines these behaviors. This is a re-implementation of `extract_lets` and `lift_lets` from mathlib. The new `extract_lets` is like doing `lift_lets; extract_lets`, but it does not lift unextractable lets like `lift_lets`. The `lift_lets; extract_lets` behavior is now handled by `extract_lets +lift`. The new `lift_lets` tactic is a frontend to `extract_lets +lift` machinery, which rather than creating new local definitions instead represents the accumulated local declarations as top-level lets. There are also conv tactics for both of these. The `extract_lets` has a limitation due to the conv architecture; it can extract lets for a given conv goal, but the local declarations don't survive outside conv. They get zeta reduced immediately upon leaving conv. --- src/Init/Conv.lean | 19 + src/Init/MetaTypes.lean | 40 ++ src/Init/Tactics.lean | 32 ++ src/Lean/Elab/Tactic.lean | 1 + src/Lean/Elab/Tactic/Conv.lean | 1 + src/Lean/Elab/Tactic/Conv/Lets.lean | 60 +++ src/Lean/Elab/Tactic/Lets.lean | 68 +++ src/Lean/Meta/AppBuilder.lean | 10 +- src/Lean/Meta/Basic.lean | 73 +++ src/Lean/Meta/Tactic.lean | 1 + src/Lean/Meta/Tactic/Lets.lean | 437 ++++++++++++++++ tests/lean/run/extract_lets.lean | 785 ++++++++++++++++++++++++++++ tests/lean/run/lift_lets.lean | 432 +++++++++++++++ 13 files changed, 1956 insertions(+), 3 deletions(-) create mode 100644 src/Lean/Elab/Tactic/Conv/Lets.lean create mode 100644 src/Lean/Elab/Tactic/Lets.lean create mode 100644 src/Lean/Meta/Tactic/Lets.lean create mode 100644 tests/lean/run/extract_lets.lean create mode 100644 tests/lean/run/lift_lets.lean diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 7cd51782f7..ddb769fabe 100644 --- a/src/Init/Conv.lean +++ b/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. diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index 00b218ed01..ef39aa56b3 100644 --- a/src/Init/MetaTypes.lean +++ b/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 diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 1517f65795..d68bd3eaae 100644 --- a/src/Init/Tactics.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index befae3eaf9..9036f1cb0c 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Conv.lean b/src/Lean/Elab/Tactic/Conv.lean index 4065765fc6..f4ba8c0e21 100644 --- a/src/Lean/Elab/Tactic/Conv.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Conv/Lets.lean b/src/Lean/Elab/Tactic/Conv/Lets.lean new file mode 100644 index 0000000000..b4dae5c723 --- /dev/null +++ b/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 diff --git a/src/Lean/Elab/Tactic/Lets.lean b/src/Lean/Elab/Tactic/Lets.lean new file mode 100644 index 0000000000..fef1e8cde0 --- /dev/null +++ b/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 diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index aacbe84ad1..15d1a684e9 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/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] diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 3533959d41..a006e9bb45 100644 --- a/src/Lean/Meta/Basic.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean index 8ce1c492ce..e6f6a588c1 100644 --- a/src/Lean/Meta/Tactic.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Lets.lean b/src/Lean/Meta/Tactic/Lets.lean new file mode 100644 index 0000000000..7edd5621fa --- /dev/null +++ b/src/Lean/Meta/Tactic/Lets.lean @@ -0,0 +1,437 @@ +/- +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.Replace + +/-! +# Tactics to manipulate `let` expressions +-/ + +open Lean Meta + +namespace Lean.Meta + +/-! +### `let` extraction + +Extracting `let`s means to locate `let`/`letFun`s in a term and to extract them +from the term, extending the local context with new declarations in the process. +A related process is lifting `lets`, which means to move `let`/`letFun`s toward the root of a term. +-/ + +namespace ExtractLets + +structure LocalDecl' where + decl : LocalDecl + /-- + If true, is a `let`, if false, is a `letFun`. + Used in `lift` mode. + -/ + isLet : Bool + +structure State where + /-- Names to use for local definitions for the extracted lets. -/ + givenNames : List Name + /-- Saved declarations for the extracted `let`s. -/ + decls : Array LocalDecl' := #[] + /-- Map from `let` values to fvars. To support the `merge` option. -/ + valueMap : ExprStructMap FVarId := {} + deriving Inhabited + +-- The `Bool` in the cache key is whether we are looking at a "top-level" expression. +abbrev M := ReaderT ExtractLetsConfig <| MonadCacheT (Bool × ExprStructEq) Expr <| StateRefT State MetaM + +/-- Returns `true` if `nextName?` would return a name. -/ +def hasNextName : M Bool := do + return !(← read).onlyGivenNames || !(← get).givenNames.isEmpty + +/-- Gets the next name to use for extracted `let`s -/ +def nextName? : M (Option Name) := do + let s ← get + match s.givenNames, (← read).onlyGivenNames with + | n :: ns, _ => set { s with givenNames := ns }; return n + | [] , true => return none + | [] , false => return `_ + +/-- +Generate a name to use for a new local declaration, derived possibly from the given binder name. +Returns `none` iff `hasNextName` is false. +-/ +def nextNameForBinderName? (binderName : Name) : M (Option Name) := do + if let some n ← nextName? then + if n != `_ then + return n + else + if binderName.isAnonymous then + -- Use a nicer binder name than `[anonymous]`, which can appear for example in `letFun x f` when `f` is not a lambda expression. + mkFreshUserName `a + else if (← read).preserveBinderNames || n.hasMacroScopes then + return n + else + mkFreshUserName binderName + else + return none + +/-- +Returns 'true' if `e` does not depend on any of the fvars in `fvars`. +-/ +def extractable (fvars : List Expr) (e : Expr) : Bool := + !e.hasAnyFVar (fvars.contains <| .fvar ·) + +/-- +Returns whether a let-like expression with the given type and value is extractable, +given the list `fvars` of binders that inhibit extraction. +-/ +def isExtractableLet (fvars : List Expr) (n : Name) (t v : Expr) : M (Bool × Name) := do + if (← hasNextName) && extractable fvars t && extractable fvars v then + if let some n ← nextNameForBinderName? n then + return (true, n) + -- In lift mode, we temporarily extract non-extractable lets, but we do not make use of `givenNames` for them. + -- These will be flushed as let/letFun expressions, and we wish to preserve the original binder name. + if (← read).lift then + return (true, n) + return (false, n) + +/-- +Adds the `decl` to the `decls` list. Assumes that `decl` is an ldecl. +-/ +def addDecl (decl : LocalDecl) (isLet : Bool) : M Unit := do + let cfg ← read + modify fun s => { s with + decls := s.decls.push { decl, isLet } + valueMap := if cfg.merge then s.valueMap.insert decl.value decl.fvarId else s.valueMap + } + +/-- +Removes and returns all local declarations that (transitively) depend on `fvar`. +-/ +def flushDecls (fvar : FVarId) : M (Array LocalDecl') := do + let mut fvarSet : FVarIdSet := {} + fvarSet := fvarSet.insert fvar + let mut toSave := #[] + let mut toFlush := #[] + for ldecl in (← get).decls do + if ldecl.decl.type.hasAnyFVar (fvarSet.contains ·) || ldecl.decl.value.hasAnyFVar (fvarSet.contains ·) then + toFlush := toFlush.push ldecl + fvarSet := fvarSet.insert ldecl.decl.fvarId + else + toSave := toSave.push ldecl + modify fun s => { s with decls := toSave } + return toFlush + +/-- +Ensures that the given local declarations are in context. Runs `k` in that context. +-/ +def withEnsuringDeclsInContext [Monad m] [MonadControlT MetaM m] [MonadLCtx m] (decls : Array LocalDecl') (k : m α) : m α := do + let lctx ← getLCtx + let decls := decls |>.filter (!lctx.contains ·.decl.fvarId) |>.map (·.decl) + withExistingLocalDecls decls.toList k + +/-- +Closes all the local declarations in `e`, creating `let` and `letFun` expressions. +Does not require that any of the declarations are in context. +Assumes that `e` contains no metavariables with local contexts that contain any of these metavariables +(the extraction procedure creates no new metavariables, so this is the case). + +This should *not* be used when closing lets for new goal metavariables, since +1. The goal contains the decls in its local context, violating the assumption. +2. We need to use true `let`s in that case, since tactics may zeta-delta reduce these declarations. +-/ +def mkLetDecls (decls : Array LocalDecl') (e : Expr) : MetaM Expr := do + withEnsuringDeclsInContext decls do + decls.foldrM (init := e) fun { decl, isLet } e => do + if isLet then + return .letE decl.userName decl.type decl.value (e.abstract #[decl.toExpr]) false + else + mkLetFun decl.toExpr decl.value e + +/-- +Makes sure the declaration for `fvarId` is marked with `isLet := true`. +Used in `lift + merge` mode to ensure that, after merging, if any version was a `let` then it's a `let` rather than a `letFun`. +-/ +def ensureIsLet (fvarId : FVarId) : M Unit := do + modify fun s => { s with + decls := s.decls.map fun d => + if d.decl.fvarId == fvarId then { d with isLet := true } else d + } + +/-- +Ensures that the given `fvarId` is in context by adding `decls` from the state. +Simplification: since we are not recording which decls depend on which, but we do know all dependencies +come before a particular decl, we add all the decls up to and including `fvarId`. + +Used for `merge` feature. +-/ +def withDeclInContext (fvarId : FVarId) (k : M α) : M α := do + let decls := (← get).decls + if (← getLCtx).contains fvarId then + -- Is either pre-existing or already added. + k + else if let some idx := decls.findIdx? (·.decl.fvarId == fvarId) then + withEnsuringDeclsInContext decls[0:idx+1] k + else + k + +/-- +Initializes the `valueMap` with all the local definitions that aren't implementation details. +Used for `merge` feature when `useContext` is enabled. +-/ +def initializeValueMap : M Unit := do + let lctx ← getLCtx + lctx.forM fun decl => do + if decl.isLet && !decl.isImplementationDetail then + let value ← instantiateMVars decl.value + modify fun s => { s with valueMap := s.valueMap.insert value decl.fvarId } + +/-- +Returns `true` if the expression contains a `let` expression or a `letFun` +(this does not verify that the `letFun`s are well-formed). +Its purpose is to be a check for whether a subexpression can be skipped. +-/ +def containsLet (e : Expr) : Bool := + Option.isSome <| e.find? fun e' => e'.isLet || e'.isConstOf ``letFun + +/-- +Extracts lets from `e`. +- `fvars` is an array of all the local variables from going under binders, + used to detect whether an expression is extractable. Extracted `let`s do not have their fvarids in this list. + This is not part of the cache key since it's an optimization and in principle derivable. +- `topLevel` is whether we are still looking at the top-level expression. + The body of an extracted top-level let is also considered to be top-level. + This is part of the cache key since it affects what is extracted. + +Note: the return value may refer to fvars that are not in the current local context, but they are in the `decls` list. +-/ +partial def extractCore (fvars : List Expr) (e : Expr) (topLevel : Bool := false) : M Expr := do + let cfg ← read + if e.isAtomic then + return e + else if !cfg.descend && !topLevel then + return e + else + checkCache (topLevel, (e : ExprStructEq)) fun _ => do + if !containsLet e then + return e + -- Don't honor `proofs := false` or `types := false` for top-level lets, since it's confusing not having them be extracted. + unless topLevel && (e.isLet || e.isLetFun || e.isMData) do + if !cfg.proofs then + if ← isProof e then + return e + if !cfg.types then + if ← isType e then + return e + let whenDescend (k : M Expr) : M Expr := do if cfg.descend then k else pure e + match e with + | .bvar .. | .fvar .. | .mvar .. | .sort .. | .const .. | .lit .. => unreachable! + | .mdata _ e' => return e.updateMData! (← extractCore fvars e' (topLevel := topLevel)) + | .letE n t v b _ => extractLetLike true n t v b (fun t v b => pure <| e.updateLet! t v b) (topLevel := topLevel) + | .app .. => + if e.isLetFun then + extractLetFun e (topLevel := topLevel) + else + whenDescend do extractApp e.getAppFn e.getAppArgs + | .proj _ _ s => whenDescend do return e.updateProj! (← extractCore fvars s) + | .lam n t b i => whenDescend do extractBinder n t b i (fun t b => e.updateLambda! i t b) + | .forallE n t b i => whenDescend do extractBinder n t b i (fun t b => e.updateForall! i t b) +where + extractBinder (n : Name) (t b : Expr) (i : BinderInfo) (mk : Expr → Expr → Expr) : M Expr := do + let t ← extractCore fvars t + if (← read).underBinder then + withLocalDecl n i t fun x => do + let b ← extractCore (x :: fvars) (b.instantiate1 x) + if (← read).lift then + let toFlush ← flushDecls x.fvarId! + let b ← mkLetDecls toFlush b + return mk t (b.abstract #[x]) + else + return mk t (b.abstract #[x]) + else + return mk t b + extractLetLike (isLet : Bool) (n : Name) (t v b : Expr) (mk : Expr → Expr → Expr → M Expr) (topLevel : Bool) : M Expr := do + let cfg ← read + let t ← extractCore fvars t + let v ← extractCore fvars v + if cfg.usedOnly && !b.hasLooseBVars then + return ← extractCore fvars b (topLevel := topLevel) + if cfg.merge then + if let some fvarId := (← get).valueMap.get? v then + if isLet && cfg.lift then ensureIsLet fvarId + return ← withDeclInContext fvarId <| + extractCore fvars (b.instantiate1 (.fvar fvarId)) (topLevel := topLevel) + let (extract, n) ← isExtractableLet fvars n t v + if !extract && (!cfg.underBinder || !cfg.descend) then + return ← mk t v b + withLetDecl n t v fun x => do + if extract then + addDecl (← x.fvarId!.getDecl) isLet + extractCore fvars (b.instantiate1 x) (topLevel := topLevel) + else + let b ← extractCore (x :: fvars) (b.instantiate1 x) + mk t v (b.abstract #[x]) + /-- `e` is the letFun expression -/ + extractLetFun (e : Expr) (topLevel : Bool) : M Expr := do + let letFunE := e.getAppFn + let β := e.getArg! 1 + let (n, t, v, b) := e.letFun?.get! + extractLetLike false n t v b (topLevel := topLevel) + (fun t v b => + -- Strategy: construct letFun directly rather than use `mkLetFun`. + -- We don't update the `β` argument. + return mkApp4 letFunE t β v (.lam n t b .default)) + extractApp (f : Expr) (args : Array Expr) : M Expr := do + let cfg ← read + if f.isConstOf ``letFun && args.size ≥ 4 then + extractApp (mkAppN f args[0:4]) args[4:] + else + let f' ← extractCore fvars f + if cfg.implicits then + return mkAppN f' (← args.mapM (extractCore fvars)) + else + let (paramInfos, _) ← instantiateForallWithParamInfos (← inferType f) args + let mut args := args + for i in [0:args.size] do + if paramInfos[i]!.binderInfo.isExplicit then + args := args.set! i (← extractCore fvars args[i]!) + return mkAppN f' args + +def extractTopLevel (e : Expr) : M Expr := do + let e ← instantiateMVars e + extractCore [] e (topLevel := true) + +/-- +Main entry point for extracting lets. +-/ +def extract (es : Array Expr) : M (Array Expr) := do + let cfg ← read + if cfg.merge && cfg.useContext then + initializeValueMap + es.mapM extractTopLevel + +end ExtractLets + +/-- +Implementation of the `extractLets` function. +- `es` is an array of terms that are valid in the current local context. +- `k` is a callback that is run in the updated local context with all relevant `let`s extracted + and with the post-extraction expressions, and the remaining names from `givenNames`. +-/ +private def extractLetsImp (es : Array Expr) (givenNames : List Name) + (k : Array FVarId → Array Expr → List Name → MetaM α) (config : ExtractLetsConfig) : MetaM α := do + let (es, st) ← ExtractLets.extract es |>.run config |>.run' {} |>.run { givenNames } + let givenNames' := st.givenNames + let decls := st.decls.map (·.decl) + withExistingLocalDecls decls.toList <| k (decls.map (·.fvarId)) es givenNames' + +/-- +Extracts `let` and `letFun` expressions into local definitions, +evaluating `k` at the post-extracted expressions and the extracted fvarids, within a context containing those local declarations. +- The `givenNames` is a list of explicit names to use for extracted local declarations. + If a name is `_` (or if there is no provided given name and `config.onlyGivenNames` is true) then uses a hygienic name + based on the existing binder name. +-/ +def extractLets [Monad m] [MonadControlT MetaM m] (es : Array Expr) (givenNames : List Name) + (k : Array FVarId → Array Expr → List Name → m α) (config : ExtractLetsConfig := {}) : m α := + map3MetaM (fun k => extractLetsImp es givenNames k config) k + +/-- +Lifts `let` and `letFun` expressions in the given expression as far out as possible. +-/ +def liftLets (e : Expr) (config : LiftLetsConfig := {}) : MetaM Expr := do + let (es, st) ← ExtractLets.extract #[e] |>.run { config with onlyGivenNames := true } |>.run' {} |>.run { givenNames := [] } + ExtractLets.mkLetDecls st.decls es[0]! + +end Lean.Meta + +private def throwMadeNoProgress (tactic : Name) (mvarId : MVarId) : MetaM α := + throwTacticEx tactic mvarId m!"made no progress" + +/-- +Extracts `let` and `letFun` expressions from the target, +returning `FVarId`s for the extracted let declarations along with the new goal. +- The `givenNames` is a list of explicit names to use for extracted local declarations. + If a name is `_` (or if there is no provided given name and `config.onlyGivenNames` is true) then uses a hygienic name + based on the existing binder name. +-/ +def Lean.MVarId.extractLets (mvarId : MVarId) (givenNames : List Name) (config : ExtractLetsConfig := {}) : + MetaM ((Array FVarId × List Name) × MVarId) := + mvarId.withContext do + mvarId.checkNotAssigned `extract_lets + let ty ← mvarId.getType + Meta.extractLets #[ty] givenNames (config := config) fun fvarIds es givenNames' => do + let ty' := es[0]! + if fvarIds.isEmpty && ty == ty' then + throwMadeNoProgress `extract_lets mvarId + let g ← mkFreshExprSyntheticOpaqueMVar ty' (← mvarId.getTag) + mvarId.assign <| ← mkLetFVars (usedLetOnly := false) (fvarIds.map .fvar) g + return ((fvarIds, givenNames'), g.mvarId!) + +/-- +Like `Lean.MVarId.extractLets` but extracts lets from a local declaration. +If the local declaration has a value, then both its type and value are modified. +-/ +def Lean.MVarId.extractLetsLocalDecl (mvarId : MVarId) (fvarId : FVarId) (givenNames : List Name) (config : ExtractLetsConfig := {}) : + MetaM ((Array FVarId × List Name) × MVarId) := do + mvarId.checkNotAssigned `extract_lets + mvarId.withReverted #[fvarId] fun mvarId fvars => mvarId.withContext do + let finalize (fvarIds : Array FVarId) (givenNames' : List Name) (targetNew : Expr) := do + let g ← mkFreshExprSyntheticOpaqueMVar targetNew (← mvarId.getTag) + mvarId.assign <| ← mkLetFVars (usedLetOnly := false) (fvarIds.map .fvar) g + return ((fvarIds, givenNames'), fvars.map .some, g.mvarId!) + match ← mvarId.getType with + | .forallE n t b i => + Meta.extractLets #[t] givenNames (config := config) fun fvarIds es givenNames' => do + let t' := es[0]! + if fvarIds.isEmpty && t == t' then + throwMadeNoProgress `extract_lets mvarId + finalize fvarIds givenNames' (.forallE n t' b i) + | .letE n t v b ndep => + Meta.extractLets #[t, v] givenNames (config := config) fun fvarIds es givenNames' => do + let t' := es[0]! + let v' := es[1]! + if fvarIds.isEmpty && t == t' && v == v' then + throwMadeNoProgress `extract_lets mvarId + finalize fvarIds givenNames' (.letE n t' v' b ndep) + | _ => throwTacticEx `extract_lets mvarId "unexpected auxiliary target" + +/-- +Lifts `let` and `letFun` expressions in target as far out as possible. +Throws an exception if nothing is lifted. + +Like `Lean.MVarId.extractLets`, but top-level lets are not added to the local context. +-/ +def Lean.MVarId.liftLets (mvarId : MVarId) (config : LiftLetsConfig := {}) : MetaM MVarId := + mvarId.withContext do + mvarId.checkNotAssigned `lift_lets + let ty ← mvarId.getType + let ty' ← Meta.liftLets ty (config := config) + if ty == ty' then + throwMadeNoProgress `lift_lets mvarId + mvarId.replaceTargetDefEq ty' + +/-- +Like `Lean.MVarId.liftLets` but lifts lets in a local declaration. +If the local declaration has a value, then both its type and value are modified. +-/ +def Lean.MVarId.liftLetsLocalDecl (mvarId : MVarId) (fvarId : FVarId) (config : LiftLetsConfig := {}) : MetaM MVarId := do + mvarId.checkNotAssigned `lift_lets + -- Revert to make sure the resulting type/value refers fvars that come after `fvarId`. + -- (Note: reverting isn't necessary unless both `merge := true` and `useContext := true`.) + Prod.snd <$> mvarId.withReverted #[fvarId] fun mvarId fvars => mvarId.withContext do + let finalize (targetNew : Expr) := do + return ((), fvars.map .some, ← mvarId.replaceTargetDefEq targetNew) + match ← mvarId.getType with + | .forallE n t b i => + let t' ← Meta.liftLets t (config := config) + if t == t' then + throwMadeNoProgress `lift_lets mvarId + finalize (.forallE n t' b i) + | .letE n t v b ndep => + let t' ← Meta.liftLets t (config := config) + let v' ← Meta.liftLets v (config := config) + if t == t' && v == v' then + throwMadeNoProgress `lift_lets mvarId + finalize (.letE n t' v' b ndep) + | _ => throwTacticEx `lift_lets mvarId "unexpected auxiliary target" diff --git a/tests/lean/run/extract_lets.lean b/tests/lean/run/extract_lets.lean new file mode 100644 index 0000000000..54df22882c --- /dev/null +++ b/tests/lean/run/extract_lets.lean @@ -0,0 +1,785 @@ +/-! +# Tests of the `extract_lets` tactic +-/ + +set_option linter.tactic.unusedName true +set_option linter.unusedVariables false +axiom test_sorry {α : Sort _} : α + +/-! +Extract a top-level let, no names given. +-/ +/-- +info: x✝ : Nat := 2 +⊢ x✝ = 2 +-/ +#guard_msgs in +example : let x := 2; x = 2 := by + extract_lets + trace_state + rfl + +/-! +Extract a top-level let, name given. +-/ +/-- +info: z : Nat := 2 +⊢ z = 2 +-/ +#guard_msgs in +example : let x := 2; x = 2 := by + extract_lets z + trace_state + rfl + +/-! +Extract a top-level let, placeholder name given. +-/ +/-- +info: x✝ : Nat := 2 +⊢ x✝ = 2 +-/ +#guard_msgs in +example : let x := 2; x = 2 := by + extract_lets _ + trace_state + rfl + +/-! +Extract an embedded let, name given. +-/ +/-- +info: z : Nat := 2 +⊢ z = 2 +-/ +#guard_msgs in +example : (let x := 2; x) = 2 := by + extract_lets z + trace_state + rfl + +/-! +Extract multiple embedded lets, no names given. +-/ +/-- +info: x✝ : Nat := 2 +y✝ : Nat := 1 + 1 +⊢ x✝ = y✝ +-/ +#guard_msgs in +example : (let x := 2; x) = (let y := 1 + 1; y) := by + extract_lets + trace_state + rfl + +/-! +Names extracted lets in order, but keeps extracting even after list is exhausted. +-/ +/-- +info: z : Nat := 2 +y✝ : Nat := 1 + 1 +⊢ z = y✝ +-/ +#guard_msgs in +example : (let x := 2; x) = (let y := 1 + 1; y) := by + extract_lets z + trace_state + rfl + +/-! +Too many names, linter warning. +-/ +/-- +warning: unused name +note: this linter can be disabled with `set_option linter.tactic.unusedName false` +--- +info: z : Nat := 2 +z' : Nat := 1 + 1 +⊢ z = z' +-/ +#guard_msgs in +example : (let x := 2; x) = (let y := 1 + 1; y) := by + extract_lets z z' z'' + trace_state + rfl + +/-! +Length of name list controls number of lets in `+onlyGivenNames` mode. +-/ +/-- +info: z : Nat := 2 +⊢ z = + let y := 1 + 1; + y +-/ +#guard_msgs in +example : (let x := 2; x) = (let y := 1 + 1; y) := by + extract_lets +onlyGivenNames z + trace_state + rfl +/-- +info: z : Nat := 2 +w : Nat := 1 + 1 +⊢ z = w +-/ +#guard_msgs in +example : (let x := 2; x) = (let y := 1 + 1; y) := by + extract_lets +onlyGivenNames z w + trace_state + rfl + +/-! +Merging. +-/ +/-- +info: x✝ : Nat := 2 +⊢ x✝ = x✝ +-/ +#guard_msgs in +example : (let x := 2; x) = (let y := 2; y) := by + extract_lets + trace_state + rfl + +/-! +Merging, even if we run out of names. +-/ +/-- +info: z : Nat := 2 +⊢ z = z +-/ +#guard_msgs in +example : (let x := 2; x) = (let y := 2; y) := by + extract_lets z + trace_state + rfl + +/-! +Merging reuses pre-existing declarations +-/ +/-- +info: z : Nat := 2 +⊢ z = z +-/ +#guard_msgs in +example : (let x := 2; x) = (let y := 2; y) := by + let z := 2 + extract_lets + trace_state + rfl + +/-! +Merging doesn't reuse pre-existing declarations when `-useContext`. +-/ +/-- +info: z : Nat := 2 +x✝ : Nat := 2 +⊢ x✝ = x✝ +-/ +#guard_msgs in +example : (let x := 2; x) = (let y := 2; y) := by + let z := 2 + extract_lets -useContext + trace_state + rfl + +/-! +Works with `have` (`let_fun`) +-/ +/-- +info: a✝ : Nat := 2 +x✝ : Nat := a✝ +y✝ : Nat := a✝ + 0 +⊢ x✝ = y✝ +-/ +#guard_msgs in +example : have a := 2; (have x := a; x) = (have y := a + 0; y) := by + extract_lets + trace_state + rfl + +/-! +Extracts at both the type and the value of a local definition. +-/ +/-- +info: α✝ : Type := Nat +y✝ : Nat := 2 +x : α✝ := 2 +⊢ x = x +-/ +#guard_msgs in +example : let x : (let α := Nat; α) := (let y := 2; 2); x = x := by + intro x + extract_lets at x + trace_state + rfl +-- Essentially same state: +/-- +info: α✝ : Type := Nat +y✝ : Nat := 2 +x✝ : α✝ := 2 +⊢ x✝ = x✝ +-/ +#guard_msgs in +example : let x : (let α := Nat; α) := (let y := 2; 2); x = x := by + extract_lets + trace_state + rfl + +/-! +Basic `descend := false` test. +-/ +/-- +info: x✝ : Nat := 2 +⊢ x✝ = 2 +-/ +#guard_msgs in +example : let x := 2; x = 2 := by + extract_lets -descend + trace_state + rfl + +/-! +Make sure `descend := false` is not obstructed by metadata. +-/ +/-- +info: this : True +x✝ : Nat := 2 +⊢ x✝ = 2 +-/ +#guard_msgs in +example : let x := 2; x = 2 := by + have : True := trivial + extract_lets -descend + trace_state + rfl + +/- +In `-descend` mode, does not extract embedded let. +-/ +/-- +error: tactic 'extract_lets' failed, made no progress +⊢ (let x := 2; + x) = + 2 +-/ +#guard_msgs in +example : (let x := 2; x) = 2 := by + extract_lets -descend z + +/-! +In `-descend` mode, merges using pre-existing declarations. +-/ +/-- +info: w : Nat := 2 +y✝ : Nat := 3 +⊢ w = 2 + y✝ - y✝ +-/ +#guard_msgs in +example : let x := 2; let y := 3; let z := 3; x = 2 + y - z := by + let w := 2 + extract_lets -descend + trace_state + rfl + +/-! +`-descend` works with `have` (`let_fun`) +-/ +/-- +info: a✝ : Nat := 2 +⊢ (let_fun x := a✝; + x) = + let_fun y := a✝ + 0; + y +-/ +#guard_msgs in +example : have a := 2; (have x := a; x) = (have y := a + 0; y) := by + extract_lets -descend + trace_state + rfl + +/-! +Extracting at a hypothesis +-/ +/-- +info: x✝ : Nat := 1 +h : x✝ = x✝ +⊢ True +-/ +#guard_msgs in +example (h : let x := 1; x = x) : True := by + extract_lets at h + fail_if_success extract_lets a at h + trace_state + trivial + +/-! +Extracting at a hypothesis, with names +-/ +/-- +info: y : Nat := 1 +h : y = y +⊢ True +-/ +#guard_msgs in +example (h : let x := 1; x = x) : True := by + extract_lets y at h + fail_if_success extract_lets a at h + trace_state + trivial + +/-! +Extracting at a hypothesis, reorders hypotheses +-/ +/-- +info: h' : Nat +y : Nat := 1 +h : y = y +⊢ True +-/ +#guard_msgs in +example (h : let x := 1; x = x) (h' : Nat) : True := by + extract_lets y at h + fail_if_success extract_lets a at h + trace_state + trivial + +/-! +Extracting at a hypothesis, not all top level. +-/ +/-- +info: x✝ : Nat := 1 +y✝ : Nat := 2 +h : x✝ + 1 = y✝ +⊢ True +-/ +#guard_msgs in +example (h : let x := 1; x + 1 = let y := 2; y) : True := by + extract_lets at h + trace_state + trivial + +/-! +Extracting at a hypothesis, not all top level, in `-descend` mode. +-/ +/-- +info: x✝ : Nat := 1 +h : + x✝ + 1 = + let y := 2; + y +⊢ True +-/ +#guard_msgs in +example (h : let x := 1; x + 1 = let y := 2; y) : True := by + extract_lets -descend at h + trace_state + trivial + +/-! +At multiple locations with `merge := true`. +-/ +/-- +info: _z✝ : Nat := 3 +x✝ : Nat := 1 +h : x✝ + 2 = _z✝ +⊢ ∀ (x : Nat), True +-/ +#guard_msgs in +example (h : let x := 1; let y := 3; x + 2 = y) : let _z := 3; ∀ (_ : Nat), True := by + extract_lets at * + trace_state + intro + trivial + +/-! +At multiple locations with `merge := false`. +-/ +/-- +info: _z✝ : Nat := 3 +x✝ : Nat := 1 +y✝ : Nat := 3 +h : x✝ + 2 = y✝ +⊢ ∀ (x : Nat), True +-/ +#guard_msgs in +example (h : let x := 1; let y := 3; x + 2 = y) : let _z := 3; ∀ (_ : Nat), True := by + extract_lets -merge at * + trace_state + intro + trivial + +/-! +Merging can chain. This tests how extracted let declarations are recalled and can handle dependence. +-/ +/-- +info: x✝ : Nat := 2 +y✝ : Nat := x✝ +⊢ y✝ = y✝ +-/ +#guard_msgs in +example : (let x := 2; let y := x; y) = (let x' := 2; let y' := x'; y') := by + extract_lets + trace_state + rfl + +/-! +Same merging example, but with `-merge`. +-/ +/-- +info: x✝ : Nat := 2 +y✝ : Nat := x✝ +x'✝ : Nat := 2 +y'✝ : Nat := x'✝ +⊢ y✝ = y'✝ +-/ +#guard_msgs in +example : (let x := 2; let y := x; y) = (let x' := 2; let y' := x'; y') := by + extract_lets -merge + trace_state + rfl + +/-! +This tests an issue reported about the mathlib version of `extract_lets`. +Reported at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60extract_lets.60.20fails.20in.20a.20hypothesis.20if.20the.20name.20is.20unused/near/439675718 +Unused lets are handled properly. +-/ +/-- +info: ok✝ : Prop := True +h : + let _not_ok := False; + ok✝ +⊢ let _also_ok := 3; + True +--- +info: ok✝ : Prop := True +h : + let _not_ok := False; + ok✝ +_also_ok✝ : Nat := 3 +⊢ True +--- +info: ok✝ : Prop := True +_also_ok✝ : Nat := 3 +_not_ok✝ : Prop := False +h : ok✝ +⊢ True +-/ +#guard_msgs in +example (h : let ok := True; let _not_ok := False; ok) : let _also_ok := 3; True := by + extract_lets +onlyGivenNames _ at h + trace_state + extract_lets +onlyGivenNames _ + trace_state + extract_lets +onlyGivenNames _ at h + trace_state + trivial + +/-! +Testing `+usedOnly` +-/ +/-- +info: ok✝ : Prop := True +h : ok✝ +⊢ let _also_ok := 3; + True +--- +info: ok✝ : Prop := True +h : ok✝ +⊢ True +-/ +#guard_msgs in +example (h : let ok := True; let _not_ok := False; ok) : let _also_ok := 3; True := by + extract_lets +onlyGivenNames +usedOnly _ at h + trace_state + extract_lets +usedOnly + trace_state + trivial + +/-! +Testing `+usedOnly` with `-descend` +-/ +/-- +info: ok✝ : Prop := True +h : ok✝ +⊢ let _also_ok := 3; + True +--- +info: ok✝ : Prop := True +h : ok✝ +⊢ True +-/ +#guard_msgs in +example (h : let ok := True; let _not_ok := False; ok) : let _also_ok := 3; True := by + extract_lets -descend +onlyGivenNames +usedOnly _ at h + trace_state + extract_lets -descend +usedOnly + trace_state + trivial + +/-! +`+proofs` +-/ +/-- +info: this✝ : (some true).isSome = true := of_eq_true (eq_self true) +⊢ (some true).get this✝ = true +-/ +#guard_msgs in +example : Option.get (some true) (have := (by simp); this) = true := by + fail_if_success extract_lets -proofs + extract_lets +proofs + trace_state + rfl + +/-! +`+implicits` +-/ +/-- +info: α✝ : Type := Nat +⊢ id 2 = 2 +-/ +#guard_msgs in +example : @id (let α := Nat; α) 2 = 2 := by + fail_if_success extract_lets -implicits + extract_lets +implicits + trace_state + rfl + +/-! +`-types`, works both to inhibit when the top level is a type and when the subterm is a type. +(This option isn't so useful outside of `conv` mode.) +-/ +example : (let x := Nat; x) = Nat := by + fail_if_success extract_lets -types + extract_lets +types + rfl +example : (let x := 2; x) = 2 := by + fail_if_success extract_lets -types + extract_lets +types + rfl + +/-! +Let value depends on binder, fails. +-/ +example : ∀ n : Nat, let x := n; x = x := by + fail_if_success extract_lets + intros + rfl + +/-! +Can extract from underneath another `let`. +-/ +/-- +info: y✝ : Nat := 2 +⊢ ∀ (n : Nat), + let x := n; + x + y✝ = x + y✝ +-/ +#guard_msgs in +example : ∀ n : Nat, let x := n; let y := 2; x + y = x + y := by + extract_lets + trace_state + intros + rfl + +/-! +Can't extract from underneath another `let` when `underBinder := false`. +-/ +/-- +error: tactic 'extract_lets' failed, made no progress +⊢ ∀ (n : Nat), + let x := n; + let y := 2; + x + y = x + y +-/ +#guard_msgs in +example : ∀ n : Nat, let x := n; let y := 2; x + y = x + y := by + extract_lets -underBinder + +/-! +Testing lots of `let`s +-/ +set_option maxHeartbeats 300 in +example : + let x := 2 + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + let x := let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; let x := x; x + x = x := by + extract_lets + rename_i a + guard_target =ₛ a = a + rfl + +/-! +### `+lift` mode + +See also the `lift_lets.lean` test file. +-/ + +/-! +Lifts, does not make use of name generator. +-/ +/-- +info: ⊢ ∀ (n : Nat), + let x := n; + n = x +-/ +#guard_msgs in +example : ∀ n : Nat, n = (let x := n; x) := by + fail_if_success extract_lets + extract_lets +lift + trace_state + intros + rfl + +/-! +Same example, but testing `letFun`. +-/ +/-- +info: ⊢ ∀ (n : Nat), + let_fun x := n; + n = x +-/ +#guard_msgs in +example : ∀ n : Nat, n = (have x := n; x) := by + fail_if_success extract_lets + extract_lets +lift + trace_state + intros + rfl + +/-! +Merging of merely-lifted lets. Four cases to this test, depending on whether a `have` or `let` is seen first, +and whether the second is a `have` or `let`. +-/ +/-- +info: ⊢ ∀ (n : Nat), + let_fun x := n; + x = x +-/ +#guard_msgs in +example : ∀ n : Nat, (have x := n; x) = (have x' := n; x') := by + fail_if_success extract_lets + extract_lets +lift + trace_state + intros + rfl +/-- +info: ⊢ ∀ (n : Nat), + let x := n; + x = x +-/ +#guard_msgs in +example : ∀ n : Nat, (let x := n; x) = (have x' := n; x') := by + fail_if_success extract_lets + extract_lets +lift + trace_state + intros + rfl +/-- +info: ⊢ ∀ (n : Nat), + let x := n; + x = x +-/ +#guard_msgs in +example : ∀ n : Nat, (have x := n; x) = (let x' := n; x') := by + fail_if_success extract_lets + extract_lets +lift + trace_state + intros + rfl +/-- +info: ⊢ ∀ (n : Nat), + let x := n; + x = x +-/ +#guard_msgs in +example : ∀ n : Nat, (let x := n; x) = (let x' := n; x') := by + fail_if_success extract_lets + extract_lets +lift + trace_state + intros + rfl + +/-! +Without merging +-/ +/-- +info: ⊢ ∀ (n : Nat), + let_fun x := n; + let_fun x' := n; + x = x' +-/ +#guard_msgs in +example : ∀ n : Nat, (have x := n; x) = (have x' := n; x') := by + fail_if_success extract_lets + extract_lets +lift -merge + trace_state + intros + rfl + +/-! +Make sure `+lift` doesn't lift things that transitively depend on a binder. +-/ +example : ∀ n : Nat, let x := n; let y := x; y = n := by + fail_if_success extract_lets +lift + intros + rfl + +/-! +Extracting `let`s in proofs in `+proof` mode. +-/ +/-- +info: m : Nat +h : ∃ n, n + 1 = m +x : Fin m +y : Fin (h.choose + 1) +he : m = h.choose + 1 := Eq.symm (Exists.choose_spec h) +⊢ cast ⋯ x = y +-/ +#guard_msgs in +example (m : Nat) (h : ∃ n, n + 1 = m) (x : Fin m) (y : Fin _) : + cast (let h' := h.choose_spec.symm; congrArg Fin h') x = y := by + fail_if_success extract_lets -proofs + extract_lets +proofs he + trace_state + exact test_sorry + +/-! +### Conv mode +-/ + +/-! +Limitation: we can use `extract_lets` within `conv`, but the let bindings do not persist. +-/ +/-- +info: y : Type := Nat +| y = Int +--- +info: ⊢ Nat = Int +-/ +#guard_msgs in +example : let x := Nat; x = Int := by + conv => + extract_lets y + trace_state + trace_state + exact test_sorry diff --git a/tests/lean/run/lift_lets.lean b/tests/lean/run/lift_lets.lean new file mode 100644 index 0000000000..e8142a9829 --- /dev/null +++ b/tests/lean/run/lift_lets.lean @@ -0,0 +1,432 @@ +/-! +# Tests of the `lift_lets` tactic +-/ + +set_option linter.unusedVariables false +axiom test_sorry {α : Sort _} : α + +/-! +Basic test of let in expression. +-/ +/-- +info: ⊢ let x := 1; + x = 1 +-/ +#guard_msgs in +example : (let x := 1; x) = 1 := by + lift_lets + trace_state + intro + rfl + +/-! +Merging +-/ +/-- +info: ⊢ let x := 1; + x = x +-/ +#guard_msgs in +example : (let x := 1; x) = (let y := 1; y) := by + lift_lets + trace_state + intro + rfl + +/-! +Merging off. +-/ +/-- +info: ⊢ let x := 1; + let y := 1; + x = y +-/ +#guard_msgs in +example : (let x := 1; x) = (let y := 1; y) := by + lift_lets -merge + trace_state + intros + rfl + +/-! +Not mergable, since they must match syntactically. +-/ +/-- +info: ⊢ let x := 2; + let y := 1 + 1; + x = y +-/ +#guard_msgs in +example : (let x := 2; x) = (let y := 1 + 1; y) := by + lift_lets + trace_state + rfl + +/-! +Merging with local context. +-/ +/-- +info: y : Nat := 1 +⊢ y = 1 +-/ +#guard_msgs in +example : (let x := 1; x) = 1 := by + let y := 1 + lift_lets + trace_state + rfl + +/-! +Merging with local context, for top-level. +-/ +/-- +info: y : Nat := 1 +⊢ y = 1 +-/ +#guard_msgs in +example : let x := 1; x = 1 := by + let y := 1 + lift_lets + trace_state + rfl + +/-! +Recursive lifting +-/ +/-- +info: ⊢ let y := 1; + let x := y + 1; + x + 1 = 3 +-/ +#guard_msgs in +example : (let x := (let y := 1; y + 1); x + 1) = 3 := by + lift_lets + trace_state + intros + rfl + +/-! +Lifting under a binder, dependency. +-/ +/-- +info: ⊢ ∀ (n : Nat), + let x := n; + n = x +-/ +#guard_msgs in +example : ∀ n : Nat, n = (let x := n; x) := by + lift_lets + trace_state + intros + rfl + +/-! +Lifting under a binder, no dependency. +-/ +/-- +info: ⊢ let x := 0; + ∀ (n : Nat), n = n + x +-/ +#guard_msgs in +example : ∀ n : Nat, n = (let x := 0; n + x) := by + lift_lets + trace_state + intros + rfl + +/-! +Lifting `letFun` under a binder, dependency. +-/ +/-- +info: ⊢ ∀ (n : Nat), + let_fun x := n; + n = x +-/ +#guard_msgs in +example : ∀ n : Nat, n = (have x := n; x) := by + lift_lets + trace_state + intros + rfl + +/-! +Lifting `letFun` under a binder, no dependency. +-/ +/-- +info: ⊢ let_fun x := 0; + ∀ (n : Nat), n = n + x +-/ +#guard_msgs in +example : ∀ n : Nat, n = (have x := 0; n + x) := by + lift_lets + trace_state + intros + rfl + +/-! +Recursive lifting, one of the internal lets can leave the binder. +-/ +/-- +info: ⊢ let y := 1; + (fun x => + let a := x; + a + y) + 2 = + 2 + 1 +-/ +#guard_msgs in +example : (fun x => let a := x; let y := 1; a + y) 2 = 2 + 1 := by + lift_lets + trace_state + intro + rfl + +/-! +Lifting out of binder type. +-/ +/-- +info: ⊢ let ty := Nat; + (fun x => Nat) 2 +-/ +#guard_msgs in +example : (fun (_ : let ty := Nat; ty) => Nat) (2 : Nat) := by + lift_lets + trace_state + exact 0 + +/-! +When `-types`, doesn't lift out of binder type. +-/ +/-- +error: tactic 'lift_lets' failed, made no progress +⊢ (fun x => Nat) 2 +-/ +#guard_msgs in +example : (fun (_ : let ty := Nat; ty) => Nat) (2 : Nat) := by + lift_lets -types + +/-! +Merging of lets of different kinds. +Four cases to this test, depending on whether a `have` or `let` is seen first, +and whether the second is a `have` or `let`. +-/ +/-- +info: ⊢ ∀ (n : Nat), + let_fun x := n; + x = x +-/ +#guard_msgs in +example : ∀ n : Nat, (have x := n; x) = (have x' := n; x') := by + lift_lets + trace_state + intros + rfl +/-- +info: ⊢ ∀ (n : Nat), + let x := n; + x = x +-/ +#guard_msgs in +example : ∀ n : Nat, (let x := n; x) = (have x' := n; x') := by + lift_lets + trace_state + intros + rfl +/-- +info: ⊢ ∀ (n : Nat), + let x := n; + x = x +-/ +#guard_msgs in +example : ∀ n : Nat, (have x := n; x) = (let x' := n; x') := by + lift_lets + trace_state + intros + rfl +/-- +info: ⊢ ∀ (n : Nat), + let x := n; + x = x +-/ +#guard_msgs in +example : ∀ n : Nat, (let x := n; x) = (let x' := n; x') := by + lift_lets + trace_state + intros + rfl + +/-! +Make sure it doesn't lift things that transitively depend on a binder. +-/ +example : ∀ n : Nat, let x := n; let y := x; y = n := by + fail_if_success lift_lets + intros + rfl + +/-! +Lifting from underneath an unliftable let is OK. +-/ +/-- +info: ⊢ let y := 0; + ∀ (n : Nat), + let x := n; + x + y = n +-/ +#guard_msgs in +example : ∀ n : Nat, let x := n; let y := 0; x + y = n := by + lift_lets + trace_state + intros + rfl + +/-! +Doesn't lift from implicit arguments by default +-/ +/-- +error: tactic 'lift_lets' failed, made no progress +⊢ id = id +-/ +#guard_msgs in +example : (id : (let ty := Nat; ty) → Nat) = @id Nat := by + lift_lets + +/-! +Enable lifting from implicit arguments using `+implicit`. +-/ +/-- +info: ⊢ let ty := Nat; + id = id +-/ +#guard_msgs in +example : (id : (let ty := Nat; ty) → Nat) = @id Nat := by + lift_lets +implicits + trace_state + rfl + +/-! +Lifting at a local hypothesis. +-/ +/-- +info: y : Nat +h : + let x := 1; + x = y +⊢ True +-/ +#guard_msgs in +example (h : (let x := 1; x) = y) : True := by + lift_lets at h + trace_state + trivial + +/-! +Lifting in both the type and value for local declarations. +-/ +/-- +info: v : let ty := Nat; +id ty := + let x := 2; + id x +⊢ True +-/ +#guard_msgs in +example : True := by + let v : id (let ty := Nat; ty) := id (let x : Nat := 2; x) + lift_lets at v + trace_state + trivial + +/-! +Merges using local context, even if the local declaration comes after. +-/ +/-- +info: y : Type := Nat +h : y +⊢ True +-/ +#guard_msgs in +example (h : let x := Nat; x) : True := by + let y := Nat + lift_lets at h + trace_state + trivial + +/-! +A test to make sure `lift_lets` works after other tactics. +-/ +/-- +info: y : Nat +⊢ let x := 1; + x = y → True +-/ +#guard_msgs in +example (h : (let x := 1; x) = y) : True := by + refine ?_ + revert h + lift_lets + trace_state + intros + trivial + +/-! +Lifting `let`s in proofs in `+proof` mode. +-/ +/-- +info: m : Nat +h : ∃ n, n + 1 = m +x : Fin m +y : Fin (h.choose + 1) +⊢ let h' := ⋯; + cast ⋯ x = y +-/ +#guard_msgs in +example (m : Nat) (h : ∃ n, n + 1 = m) (x : Fin m) (y : Fin _) : + cast (let h' := h.choose_spec.symm; congrArg Fin h') x = y := by + fail_if_success lift_lets -proofs + lift_lets +proofs + trace_state + exact test_sorry + + +/-! +### conv mode +-/ + +/-! +Unlike `extract_lets`, the `lift_lets` conv tactic's modifications persist, +since the local context remains the same. +-/ +/-- +info: | let x := Nat; + x = Int +--- +info: ⊢ let x := Nat; + x = Int +-/ +#guard_msgs in +example : (let x := Nat; x) = Int := by + conv => + lift_lets + trace_state + trace_state + exact test_sorry + +/-! +Merging with local context. +-/ +/-- +info: y : Type := Nat +| y +--- +info: y : Type := Nat +⊢ y = Int +-/ +#guard_msgs in +example : (let x := Nat; x) = Int := by + let y := Nat + conv => + lhs + lift_lets + trace_state + trace_state + exact test_sorry