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.
This commit is contained in:
Kyle Miller
GitHub
parent
02f7a1dd41
commit
517899da7b
13 changed files with 1956 additions and 3 deletions
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
60
src/Lean/Elab/Tactic/Conv/Lets.lean
Normal file
60
src/Lean/Elab/Tactic/Conv/Lets.lean
Normal file
|
|
@ -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
|
||||
68
src/Lean/Elab/Tactic/Lets.lean
Normal file
68
src/Lean/Elab/Tactic/Lets.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
437
src/Lean/Meta/Tactic/Lets.lean
Normal file
437
src/Lean/Meta/Tactic/Lets.lean
Normal file
|
|
@ -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"
|
||||
785
tests/lean/run/extract_lets.lean
Normal file
785
tests/lean/run/extract_lets.lean
Normal file
|
|
@ -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
|
||||
432
tests/lean/run/lift_lets.lean
Normal file
432
tests/lean/run/lift_lets.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue