From 71cf266cd7e75b39c3b3e1e5bf75565d4e3e19db Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 23 Jun 2025 18:33:53 -0700 Subject: [PATCH] feat: add `Meta.letToHave` and the `let_to_have` tactic (#8954) This PR adds a procedure that efficiently transforms `let` expressions into `have` expressions (`Meta.letToHave`). This is exposed as the `let_to_have` tactic. It uses the `withTrackingZetaDelta` technique: the expression is typechecked, and any `let` variables that don't enter the zeta delta set are nondependent. The procedure uses a number of heuristics to limit the amount of typechecking performed. For example, it is ok to skip subexpressions that do not contain fvars, mvars, or `let`s. --- src/Init/Conv.lean | 6 + src/Init/Tactics.lean | 7 + src/Lean/Elab/Tactic/Conv/Lets.lean | 13 + src/Lean/Elab/Tactic/Lets.lean | 11 + src/Lean/Meta.lean | 1 + src/Lean/Meta/Basic.lean | 6 + src/Lean/Meta/LetToHave.lean | 443 ++++++++++++++++++++++++++++ src/Lean/Meta/Tactic/Lets.lean | 31 ++ src/Lean/Meta/WHNF.lean | 2 +- tests/lean/run/letToHave.lean | 325 ++++++++++++++++++++ 10 files changed, 844 insertions(+), 1 deletion(-) create mode 100644 src/Lean/Meta/LetToHave.lean create mode 100644 tests/lean/run/letToHave.lean diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index ceebc39f73..49dde3c540 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -339,6 +339,12 @@ This is the conv mode version of the `lift_lets` tactic. -/ syntax (name := liftLets) "lift_lets " optConfig : conv +/-- +Transforms `let` expressions into `have` expressions within th etarget expression when possible. +This is the conv mode version of the `let_to_have` tactic. +-/ +syntax (name := letToHave) "let_to_have" : conv + /-- `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis, by focusing on particular subexpressions. diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 5433f7c2b8..c16ee25dba 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -573,6 +573,13 @@ example : (let x := 1; x) = 1 := by -/ syntax (name := liftLets) "lift_lets " optConfig (location)? : tactic +/-- +Transforms `let` expressions into `have` expressions when possible. +- `let_to_have` transforms `let`s in the target. +- `let_to_have at h` transforms `let`s in the given local hypothesis. +-/ +syntax (name := letToHave) "let_to_have" (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/Conv/Lets.lean b/src/Lean/Elab/Tactic/Conv/Lets.lean index b4dae5c723..dfec982662 100644 --- a/src/Lean/Elab/Tactic/Conv/Lets.lean +++ b/src/Lean/Elab/Tactic/Conv/Lets.lean @@ -57,4 +57,17 @@ namespace Lean.Elab.Tactic.Conv throwTacticEx `lift_lets (← getMainGoal) m!"made no progress" changeLhs lhs' +/-! +### `let_to_have` +-/ + +@[builtin_tactic Lean.Parser.Tactic.Conv.letToHave] elab_rules : tactic + | `(conv| let_to_have) => do + withMainContext do + let lhs ← getLhs + let lhs' ← Meta.letToHave lhs + if lhs == lhs' then + throwTacticEx `let_to_have (← 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 index fef1e8cde0..5bc00990fc 100644 --- a/src/Lean/Elab/Tactic/Lets.lean +++ b/src/Lean/Elab/Tactic/Lets.lean @@ -65,4 +65,15 @@ declare_config_elab elabLiftLetsConfig LiftLetsConfig (atTarget := liftMetaTactic1 fun mvarId => mvarId.liftLets config) (failed := fun _ => throwError "'lift_lets' tactic failed") +/-! +### `let_to_have` +-/ + +@[builtin_tactic letToHave] elab_rules : tactic + | `(tactic| let_to_have $[$loc?:location]?) => do + withLocation (expandOptLocation (Lean.mkOptionalNode loc?)) + (atLocal := fun h => liftMetaTactic1 fun mvarId => mvarId.letToHaveLocalDecl h) + (atTarget := liftMetaTactic1 fun mvarId => mvarId.letToHave) + (failed := fun _ => throwError "'let_to_have' tactic failed") + end Lean.Elab.Tactic diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean index 619a4ad64d..f53aec60eb 100644 --- a/src/Lean/Meta.lean +++ b/src/Lean/Meta.lean @@ -26,6 +26,7 @@ import Lean.Meta.Match import Lean.Meta.ReduceEval import Lean.Meta.Closure import Lean.Meta.AbstractNestedProofs +import Lean.Meta.LetToHave import Lean.Meta.ForEachExpr import Lean.Meta.Transform import Lean.Meta.PPGoal diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 04a60a8242..e3e352376e 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -1152,6 +1152,12 @@ See `withTrackingZetaDelta` and `withTrackingZetaDeltaSet`. def getZetaDeltaFVarIds : MetaM FVarIdSet := return (← get).zetaDeltaFVarIds +/-- +Inserts `fvarId` into the `zetaDeltaFVarIds` set. +-/ +def addZetaDeltaFVarId (fvarId : FVarId) : MetaM Unit := + modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId } + /-- `withResetZetaDeltaFVarIds x` executes `x` in a context where the `zetaDeltaFVarIds` is temporarily cleared. diff --git a/src/Lean/Meta/LetToHave.lean b/src/Lean/Meta/LetToHave.lean new file mode 100644 index 0000000000..19045910d9 --- /dev/null +++ b/src/Lean/Meta/LetToHave.lean @@ -0,0 +1,443 @@ +/- +Copyright (c) 2025 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.Check +import Lean.ReservedNameAction +import Lean.AddDecl +import Lean.Meta.Transform +import Lean.Util.CollectFVars +import Lean.Util.CollectMVars + +/-! +# Transforming nondependent `let`s into `have`s + +A `let` expression `let x : t := v; b` is *nondependent* if `fun x : t => b` is type correct. +Nondependent `let`s are those that can be transformed into `have x := v; b`. +This module has a procedure that detects which `let`s are nondependent and does the transformation, +attempting to do so efficiently. + +Dependence checking is approximated using the `withTrackingZetaDelta` technique: +given `let x := v; b`, we add a `x := v` declaration to the local context, +and then type check `b` with `withTrackingZetaDelta` enabled to record whether `x` is unfolded. +If `x` is not unfolded, then we know that `b` does not depend on `v`. +This is a conservative check, since `isDefEq` may unfold local definitions unnecessarily. + +We do not use `Lean.Meta.check` directly. A naive algorithm would be to do `Meta.check (b.instantiate1 x)` +for each `let` body, which would involve rechecking subexpressions multiple times when there are nested `let`s, +and furthermore we do not need to fully typecheck the body when evaluating dependence. +Instead, we re-implement a type checking algorithm here to be able to interleave checking and transformation. + +The trace class `trace.Meta.letToHave` reports statistics. + +The transformation has very limited support for metavariables. +Any `let` that contains a metavariable remains a `let` for now. + +Optimizations, present and future: +- We can avoid doing the transformation if the expression has no `let`s. +- We can also avoid doing the transformation to `let`-free subexpressions that are not inside a `let`, + however checking for `let`s is O(n), so we only try this for expressions with a small `approxDepth`. + (We can consider precomputing this somehow.) + - The cache is currently responsible for the check. + - We also do it before entering telescopes, to avoid unnecesasry fvar overhead. +- If we are not currently inside a `let`, then we do not need to do full typechecking. +- We try to reuse Exprs to promote subexpression sharing. +- We might consider not transforming lets to haves if we are in a proof that is not inside a `let`. + For now we assume `abstractNestedProofs` has already been applied. +-/ + +namespace Lean.Meta + +namespace LetToHave + +/-- +Returns `true` if there are any `letE (nondep := false)` subexpressions. +If true, then we must be sure to visit the subexpression. +If false, then we might still need to visit the subexpression, +but if we are not currently under any nondependent lets it is safe to skip it. +-/ +private def hasDepLet (e : Expr) : Bool := + Option.isSome <| e.find? (· matches .letE (nondep := false) ..) + +/-- +Heuristic for skipping subexpressions. If true, we definitely can skip. + +The default max depth of `5` was not experimentally optimized, except to see that it was faster than `0`. +-/ +private def canSkip (e : Expr) (maxDepth : UInt32 := 5) : Bool := + !e.hasFVar && !e.hasExprMVar && (e.approxDepth ≤ maxDepth && !hasDepLet e) + +private structure Result where + /-- The transformed expression. -/ + expr : Expr + /-- The type of `expr`, if it has been computed. -/ + type? : Option Expr + deriving Inhabited + +private local instance : Coe Result Expr where coe := Result.expr + +private structure Context where + /-- The dependent lets we are currently under. + If this list is nonempty, then full typechecking is necessary. -/ + letFVars : List FVarId := [] + +private structure State where + /-- The number of transformed `let` expressions. See `incCount`. -/ + count : Nat := 0 + /-- Cached results for `visit`. -/ + results : Std.HashMap ExprStructEq Result := {} + +private abbrev M := ReaderT Context (StateRefT State MetaM) + +/-- Gives the type of `r.expr`. If it has not been computed yet, updates the cache. -/ +private def Result.type (r : Result) : M Expr := do + if let some type := r.type? then + return type + else + let type ← inferType r.expr + let r := { r with type? := type } + modify fun s => { s with results := s.results.insert r.expr r } + return type + +/-- Returns `true` if we need to do full typechecking due to `let` variables being in scope. -/ +private def Context.check (ctx : Context) : Bool := !ctx.letFVars.isEmpty + +/-- If we don't need full typechecking, returns `e`, otherwise evaluates `m`. -/ +private def whenCheck (e : Expr) (m : M Result) : M Result := do + if (← read).check then m else return { expr := e, type? := none } + +/-- Executes `m` in a context where `letFVars := fvars`. -/ +private def withLetFVars (fvars : List FVarId) (m : M α) : M α := do + withReader (fun ctx => { ctx with letFVars := fvars }) m + +/-- Increments the count of the number of `let`s transformed into `have`s. -/ +private def incCount : M Unit := + modify fun s => { s with count := s.count + 1 } + +/-- +Finds a pre-existing result in the cache. +Note that the result might have no type, which happens for example if it was visited when `check` is false. +-/ +private def findCache? (e : Expr) : M (Option Result) := do + return (← get).results[(e : ExprStructEq)]? + +/-- +Finds `e` in the cache, or otherwise computes `m`. + +If not in the cache, applies a cheap check to see if we can skip descending into the expression. +-/ +private def checkCache (e : Expr) (m : M Result) : M Result := do + if let some r ← findCache? e then + return r + else + -- `2` was not experimentally optimized + let r ← if canSkip (maxDepth := 2) e then + pure { expr := e, type? := none } + else + m + modify fun st => { st with results := st.results.insert e r } + return r + +/-- Like `findMCache?` but checks that `e` doesn't have any loose bvars. -/ +private def findCacheNoBVars? (e : Expr) : M (Option Result) := + if e.hasLooseBVars then pure none else findCache? e + +private def visitFVar (e : Expr) : MetaM Result := do + let some decl ← e.fvarId!.findDecl? | e.fvarId!.throwUnknown + return { expr := e, type? := decl.type } + +/-- +Give an expression `e` whose definition may be used in an unknown manner (for example, through a metavariable), +marks all fvars in `e` (or accessible through `e`) that can potentially be unfolded. + +Assumption: while there may be metavariables in `e` (or in types of fvars present in `e`), +they have already been processed by `checkMVar` or will be processed by it. +-/ +private def visitDepExpr (e : Expr) : M Unit := do + let mut visited : FVarIdSet := {} + let mut worklist := #[e] + while !worklist.isEmpty do + let e ← instantiateMVars worklist.back! + worklist := worklist.pop + for fvarId in (collectFVars {} e).fvarIds do + unless visited.contains fvarId do + visited := visited.insert fvarId + if ← fvarId.isLetVar then + addZetaDeltaFVarId fvarId + worklist := worklist.push (← fvarId.getType) + +/-- +Checks whether the mvar creates a dependency on any let fvars. +Note: the local context of `mvarId` cannot depend on `letFVars`, since it was created outside these `let`s. +The only consideration is delayed assignments and which variables they depend on; +if the fvar is not passed among the `args`, the mvar cannot depend on it. +-/ +private def checkMVar (mvarId : MVarId) (args : Array Expr) : M Unit := do + if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then + let letFVars := (← read).letFVars + unless fvars.size ≤ args.size do + -- This is an invalid delayed assignment. Mark all `letFVars` to inhibit transformation. + letFVars.forM (addZetaDeltaFVarId ·) + return + let pendingDecl ← mvarIdPending.getDecl + for fvar in fvars, arg in args do + let fvarDecl := pendingDecl.lctx.getFVar! fvar + if fvarDecl.isLet then + visitDepExpr arg + +private def visitMVar (e : Expr) : M Result := do + let some decl ← e.mvarId!.findDecl? | throwUnknownMVar e.mvarId! + if (← read).check then checkMVar e.mvarId! #[] + return { expr := e, type? := decl.type } + +private def visitConst (e : Expr) : M Result := do + whenCheck e do + let .const constName us := e | unreachable! + let cinfo ← getConstVal constName + if cinfo.levelParams.length == us.length then + let type ← instantiateTypeLevelParams cinfo us + return { expr := e, type? := type } + else + throwIncorrectNumberOfLevels constName us + +/-- +When checking, makes sure that `r.type?` is of the form `Expr.sort _`. +-/ +private def ensureType (r : Result) : M Result := do + if (← read).check then + let type ← r.type + let r := { r with type? := type } + if type.isSort then + return r + else + let .sort u ← whnf type | throwTypeExpected r + let r := { r with type? := Expr.sort u } + modify fun s => { s with results := s.results.insert r.expr r } + return r + else + return r + +/-- +Note: We want to cache all prefixes of each application, hence no `instantiateRevRange`-type logic here. +-/ +private def visitApp (e : Expr) (f a : Result) : M Result := do + if (← read).check then + let mut fType ← f.type + unless fType.isForall do + fType ← whnf fType + match fType with + | Expr.forallE _ d b _ => + unless (← isDefEq d (← a.type)) do + throwAppTypeMismatch f a + return { expr := e.updateApp! f a, type? := b.instantiate1 a } + | _ => throwFunctionExpected (mkApp f a) + else + return { expr := e.updateApp! f a, type? := none } + +mutual + +private partial def visitType (e : Expr) : M Result := do + let r ← visit e + ensureType r + +private partial def visitAppArgs (e : Expr) : M Result := do + if (← read).check then + if let .mvar mvarId := e.getAppFn then + checkMVar mvarId e.getAppArgs + let rec go (e : Expr) : M Result := do + let Expr.app f a := e | visit e + visitApp e (← checkCache f <| go f) (← visit a) + go e + else + -- If not checking, skip caching each prefix. + let rec go' (e : Expr) : M Expr := do + let Expr.app f a := e | visit e + return e.updateApp! (← go' f) (← visit a) + return { expr := ← go' e, type? := none } + +private partial def visitForall (e : Expr) : M Result := do + if canSkip e then + return { expr := e, type? := none } + else + go (← getLCtx) #[] #[] e +where + go (lctx : LocalContext) (fvars : Array Expr) (doms : Array Result) (e : Expr) : M Result := do + if let some e' ← findCacheNoBVars? e then + return ← withLCtx lctx {} do finalize fvars doms e' + else + match e with + | .forallE n t b bi => + let t ← withLCtx lctx {} do visitType (t.instantiateRev fvars) + let fvarId ← mkFreshFVarId + let lctx := lctx.mkLocalDecl fvarId n t.expr bi + go lctx (fvars.push (.fvar fvarId)) (doms.push t) b + | _ => + withLCtx lctx {} do + let e' ← visit (e.instantiateRev fvars) + finalize fvars doms e' + finalize (fvars : Array Expr) (doms : Array Result) (body : Result) : M Result := do + let e' := (← getLCtx).mkForall fvars body + if (← read).check then + let bodyLevel := (← ensureType body).type?.get!.sortLevel! + let u ← doms.foldrM (init := bodyLevel) fun dom u => + return mkLevelIMax' (← dom.type).sortLevel! u + return { expr := e', type? := Expr.sort u } + else + return { expr := e', type? := none } + +/-- +Visits lambdas, lets, and haves. + +Enters the entire telescope at once. +We do not check the cache at each step of the telescope since we assume that there are no unused variables. +-/ +private partial def visitLambdaLet (e : Expr) : M Result := do + if canSkip e then + return { expr := e, type? := none } + else + go (← getLCtx) #[] e (← read).letFVars +where + /-- + Enters a lambda/let/have telescope, checking that each domain type is a type. + For let/have, checks that each value has a type defeq to the domain type. + Calls `finalize` once the telescope is constructed. + -/ + go (lctx : LocalContext) (fvars : Array Expr) (e : Expr) (letFVars : List FVarId) : M Result := do + let inCtx (v : Expr → M Result) (e : Expr) : M Result := + withLCtx lctx {} <| withLetFVars letFVars <| v (e.instantiateRev fvars) + match e with + | .lam n t b bi => + let t ← inCtx visitType t + let fvarId ← mkFreshFVarId + let lctx := lctx.mkLocalDecl fvarId n t.expr bi + go lctx (fvars.push (.fvar fvarId)) b letFVars + | .letE n t v b nondep => + let t ← inCtx visitType t + let v ← inCtx visit v + unless letFVars.isEmpty do withLCtx' lctx do + let vType ← v.type + unless (← isDefEq t vType) do + throwError "invalid let declaration, term{indentExpr v}{← mkHasTypeButIsExpectedMsg vType t}" + let fvarId ← mkFreshFVarId + let lctx := lctx.mkLetDecl fvarId n t v nondep + let letFVars := if nondep then letFVars else fvarId :: letFVars + go lctx (fvars.push (.fvar fvarId)) b letFVars + | _ => + inCtx (finalize fvars <=< visit) e + /-- + This function rebuilds the expression and converts `let`s to `have`s when possible. + -/ + finalize (fvars : Array Expr) (body : Result) : M Result := do + trace[Meta.letToHave.debug] "finalize {fvars},{indentD m!"{body.expr} : {body.type?}"}" + let body' := { + expr := body.expr.abstract fvars + type? := body.type?.map (·.abstract fvars) + } + Nat.foldRevM fvars.size (init := body') fun i _ res => do + let .fvar fvarId := fvars[i] | unreachable! + let some decl ← fvarId.findDecl? | fvarId.throwUnknown + match decl with + | .cdecl _ _ n t bi _ => do + let t := t.abstractRange i fvars + pure { + expr := Expr.lam n t res.expr bi + type? := res.type?.map fun type => Expr.forallE n t type bi + } + | .ldecl _ _ n t v nondep _ => do + let nondep ← + if nondep then pure true + else if !(← getZetaDeltaFVarIds).contains fvarId then incCount; pure true + else pure false + let t := t.abstractRange i fvars + let v := v.abstractRange i fvars + pure { + expr := Expr.letE n t v res.expr nondep + type? := res.type?.map fun type => + if type.hasLooseBVar 0 then + Expr.letE n t v type nondep + else + type.lowerLooseBVars 1 1 + } + +private partial def visitProj (e : Expr) (structName : Name) (idx : Nat) (struct : Result) : M Result := do + unless (← read).check do + return { expr := e.updateProj! struct, type? := none } + let structType ← whnf (← struct.type) + let prop ← isProp structType + let failed {α} (_ : Unit) : M α := throwError "invalid projection{indentExpr (mkProj structName idx struct)}\nfrom type{indentExpr structType}" + matchConstStructure structType.getAppFn failed fun structVal structLvls ctorVal => do + unless structVal.name == structName do failed () + let structTypeArgs := structType.getAppArgs + if structVal.numParams + structVal.numIndices != structTypeArgs.size then + failed () + let mut ctorType ← inferType <| mkAppN (mkConst ctorVal.name structLvls) structTypeArgs[:structVal.numParams] + let mut args := #[] + let mut j := 0 + let mut lastFieldTy : Expr := default + for i in [:idx+1] do + unless ctorType.isForall do + ctorType ← whnf <| ctorType.instantiateRevRange j i args + j := i + let .forallE _ dom body _ := ctorType | failed () + let dom := dom.instantiateRevRange j i args + if prop then unless ← isProp dom do failed () + args := args.push <| Expr.proj structName i struct + ctorType := body + lastFieldTy := dom + lastFieldTy := lastFieldTy.cleanupAnnotations + return { expr := e.updateProj! struct, type? := lastFieldTy } + +private partial def visit (e : Expr) : M Result := do + withTraceNode `Meta.letToHave.debug (fun res => + return m!"{if res.isOk then checkEmoji else crossEmoji} visit (check := {(← read).check}){indentExpr e}") do + match e with + | .bvar .. => throwError "unexpected bound variable {e}" + | .fvar .. => visitFVar e + | .mvar .. => visitMVar e + | .sort u => return { expr := e, type? := Expr.sort u.succ } + | .const .. => visitConst e + | .app .. => checkCache e do visitAppArgs e + | .forallE .. => checkCache e do visitForall e + | .lam .. | .letE .. => checkCache e do visitLambdaLet e + | .lit v => return { expr := e, type? := v.type } + | .mdata _ e' => let e' ← visit e'; return { e' with expr := e.updateMData! e' } + | .proj structName idx struct => checkCache e do visitProj e structName idx (← visit struct) + +end + +private def main (e : Expr) : MetaM Expr := do + Prod.fst <$> withTraceNode `Meta.letToHave (fun + | .ok (_, msg) => pure m!"{checkEmoji} {msg}" + | .error ex => pure m!"{crossEmoji} {ex.toMessageData}") do + if hasDepLet e then + withTrackingZetaDelta <| + withTransparency TransparencyMode.all <| + withInferTypeConfig do + let (r, s) ← visit e |>.run {} |>.run {} + if s.count == 0 then + trace[Meta.letToHave] "result: (no change)" + else + trace[Meta.letToHave] "result:{indentExpr r.expr}" + return (r.expr, m!"transformed {s.count} `let` expressions into `have` expressions") + else + return (e, "no `let` expressions") + +end LetToHave + +/-- +Transforms nondependent `let` expressions into `have` expressions. +If `e` is not type correct, returns `e`. +The `Meta.letToHave` trace class logs errors and messages. +-/ +def letToHave (e : Expr) : MetaM Expr := do + profileitM Exception "let-to-have transformation" (← getOptions) do + let e ← instantiateMVars e + LetToHave.main e + +builtin_initialize + registerTraceClass `Meta.letToHave + registerTraceClass `Meta.letToHave.debug + +end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Lets.lean b/src/Lean/Meta/Tactic/Lets.lean index c67eb8023e..90cf2f670f 100644 --- a/src/Lean/Meta/Tactic/Lets.lean +++ b/src/Lean/Meta/Tactic/Lets.lean @@ -5,6 +5,7 @@ Authors: Kyle Miller -/ prelude import Lean.Meta.Tactic.Replace +import Lean.Meta.LetToHave /-! # Tactics to manipulate `let` expressions @@ -432,3 +433,33 @@ def Lean.MVarId.liftLetsLocalDecl (mvarId : MVarId) (fvarId : FVarId) (config : throwMadeNoProgress `lift_lets mvarId finalize (.letE n t' v' b ndep) | _ => throwTacticEx `lift_lets mvarId "unexpected auxiliary target" + +/-! +### Let-to-have transformation + +A meta tactic version of `Lean.Meta.letToHave`. +-/ + +/-- +Transforms lets to haves in the target. Throws an error if no progress is made. +-/ +def Lean.MVarId.letToHave (mvarId : MVarId) (failIfUnchanged := true) : MetaM MVarId := + mvarId.withContext do + mvarId.checkNotAssigned `let_to_have + let ty ← mvarId.getType + let ty' ← Meta.letToHave ty + if failIfUnchanged && ty == ty' then + throwMadeNoProgress `let_to_have mvarId + mvarId.replaceTargetDefEq ty' + +/-- +Transforms lets to haves in the type of `fvarId`. Throws an error if no progress is made. +-/ +def Lean.MVarId.letToHaveLocalDecl (mvarId : MVarId) (fvarId : FVarId) (failIfUnchanged := true) : MetaM MVarId := do + mvarId.withContext do + mvarId.checkNotAssigned `let_to_have + let ty ← fvarId.getType + let ty' ← Meta.letToHave ty + if failIfUnchanged && ty == ty' then + throwMadeNoProgress `let_to_have mvarId + mvarId.replaceLocalDeclDefEq fvarId ty' diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 53af950a18..83a4985fae 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -380,7 +380,7 @@ end if !(← read).zetaDeltaSet.contains fvarId then return e if (← read).trackZetaDelta then - modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId } + addZetaDeltaFVarId fvarId whnfEasyCases v k | _ => return e | .mvar mvarId => diff --git a/tests/lean/run/letToHave.lean b/tests/lean/run/letToHave.lean new file mode 100644 index 0000000000..9c622d3d5a --- /dev/null +++ b/tests/lean/run/letToHave.lean @@ -0,0 +1,325 @@ +import Lean +/-! +# Tests of the `letToHave` transformation +-/ + +set_option pp.letVarTypes true +set_option pp.mvars.anonymous false + +open Lean Elab Command in +/-- +`#let_to_have t` elaborates `t` then applies let-to-have. It typechecks `t` before and after. +-/ +elab "#let_to_have " t:term : command => runTermElabM fun _ => do + let e ← Term.elabTermAndSynthesize t none + Meta.check e + let e' ← Meta.letToHave e + Meta.check e' + unless ← Meta.isDefEq e e' do + throwError "result is not definitionally equal" + if e == e' then + logInfo m!"no change" + else + logInfo m!"{e'}" + +set_option linter.unusedVariables false + +/-! +Very basic tests where there are no lets. +-/ +/-- info: no change -/ +#guard_msgs in #let_to_have true +/-- info: no change -/ +#guard_msgs in #let_to_have fun (x : Nat) => x + 1 +/-- info: no change -/ +#guard_msgs in #let_to_have ∀ (x : Nat), x = x +/-- info: no change -/ +#guard_msgs in #let_to_have have x := 1; x + 1 + +/-! +Basic tests of nondependent `let`s. +-/ +/-- +info: have x : Nat := 1; +true +-/ +#guard_msgs in #let_to_have let x := 1; true +/-- +info: have x : Nat := 1; +x + 1 +-/ +#guard_msgs in #let_to_have let x := 1; x + 1 +/-- +info: have x : Nat := 1; +have x' : Nat := x; +have x'' : Nat := x + x'; +have x''' : Nat := x + x' + x''; +x + x' + x'' + x''' +-/ +#guard_msgs in #let_to_have + let x : Nat := 1; let x' := x; let x'' := x + x'; let x''' := x + x' + x''; x + x' + x'' + x''' +/-- +info: fun x => + have x' : Nat := x; + have x'' : Nat := x + x'; + have x''' : Nat := x + x' + x''; + x + x' + x'' + x''' +-/ +#guard_msgs in #let_to_have + fun x : Nat => let x' := x; let x'' := x + x'; let x''' := x + x' + x''; x + x' + x'' + x''' +/-- +info: (x : Nat) → + have x' : Nat := x; + have x'' : Nat := x + x'; + have x''' : Nat := x + x' + x''; + Fin (x + x' + x'' + x''') +-/ +#guard_msgs in #let_to_have + ∀ x : Nat, let x' := x; let x'' := x + x'; let x''' := x + x' + x''; Fin (x + x' + x'' + x''') + +/-! +Testing the cache. Reports one expression transformed. +-/ +/-- +info: (have x : Nat := 1; + x + 1) + + have x : Nat := 1; + x + 1 +--- +trace: [Meta.letToHave] ✅️ transformed 1 `let` expressions into `have` expressions + [Meta.letToHave] result: + (have x : Nat := 1; + x + 1) + + have x : Nat := 1; + x + 1 +-/ +#guard_msgs in +set_option trace.Meta.letToHave true in +#let_to_have (let x := 1; x + 1) + (let x := 1; x + 1) + +/-! +Cache uses strict equality. Preserves binder names. +-/ +/-- +info: (have x : Nat := 1; + x + 1) + + have y : Nat := 1; + y + 1 +-/ +#guard_msgs in +#let_to_have (let x := 1; x + 1) + (let y := 1; y + 1) + +/-! +The expression `(1 + 2 + 3 + 4 + 5 + 6)` enters the cache first without a type, +but then a type needs to be computed under the `let`. +-/ +/-- +info: 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + + have y : Nat := 1; + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + y +-/ +#guard_msgs in +#let_to_have (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8) + (let y := 1; (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8) + y) + +/-! +Dependence in a let value. +-/ +/-- +info: let x : Nat := 1; +have h : x = 1 := ⋯; +x +-/ +#guard_msgs in #let_to_have let x := 1; let h : x = 1 := rfl; x + +/-! +Dependence in a let type. +-/ +/-- +info: let x : Nat := 1; +have h : 0 = 0 := ⋯; +x +-/ +#guard_msgs in #let_to_have let x := 1; let h : (0 : Fin x) = (0 : Fin x) := rfl; x + +/-! +No dependence from the let type. +-/ +/-- +info: have x : Nat := 1; +have h : 0 = 0 := ⋯; +x +-/ +#guard_msgs in #let_to_have let x := 1; let h : (0 : Fin (x + 1)) = (0 : Fin (x + 1)) := rfl; x +/-! +Another dependence in the let type. +-/ +/-- +info: let x : Nat := 1; +have h : 0 = 0 := ⋯; +x +-/ +#guard_msgs in #let_to_have let x := 1; let h : (0 : Fin (x + 1)) = (0 : Fin (1 + 1)) := rfl; x + +/-! +Dependence in a forall type +-/ +/-- +info: let U : Type 1 := Type; +have α : U := Nat; +∀ (n : α), n = n +-/ +#guard_msgs in #let_to_have let U := Type; let α : U := Nat; ∀ (n : α), n = n + +/-! +Dependence in a forall body +-/ +/-- +info: let U : Type 1 := Type; +have α : U := Nat; +Bool → α +-/ +#guard_msgs in #let_to_have let U := Type; let α : U := Nat; Bool → α + +/-! +Dependence in a lambda type +-/ +/-- +info: let U : Type 1 := Type; +have α : U := Nat; +fun n => n +-/ +#guard_msgs in #let_to_have let U := Type; let α : U := Nat; fun (n : α) => n + +/-! +Metavariable under binder, might be dependent, doesn't change. +-/ +/-- info: no change -/ +#guard_msgs in #let_to_have let x := 1; ?m +/-! +Metavariable has a context that doesn't include `x`, so it doesn't depend on it. +-/ +/-- +info: have x : ?_ := ?m; +?m +-/ +#guard_msgs in #let_to_have let x := ?m; ?m +/-! +Similar, but we see that the outer `let` remains dependent. +-/ +/-- +info: let x : Nat := 1; +have y : ?_ := ?m; +?m +-/ +#guard_msgs in #let_to_have let x := 1; let y := ?m; ?m + +/-! +Test with a deep let expression. +-/ +syntax "deepLets% " num term:arg term:arg : term +macro_rules + | `(deepLets% 0 $b $e) => `(if $b then $e else 0) + | `(deepLets% $n $b $e) => + let n' : Lean.Syntax.NumLit := Lean.quote (n.getNat - 1) + `(let b' : Bool := !$b; let x : Nat := 1*$e; deepLets% $n' b' x) +/-- +info: fun a => + let b' : Bool := !true; + let x : Nat := 1 * (0 + a); + let b' : Bool := !b'; + let x : Nat := 1 * x; + let b' : Bool := !b'; + let x : Nat := 1 * x; + let b' : Bool := !b'; + let x : Nat := 1 * x; + let b' : Bool := !b'; + let x : Nat := 1 * x; + if b' = true then x else 0 : Nat → Nat +-/ +#guard_msgs in #check fun a => deepLets% 5 true (0 + a) +/-- +info: fun a => + have b' : Bool := !true; + have x : Nat := 1 * (0 + a); + have b' : Bool := !b'; + have x : Nat := 1 * x; + have b' : Bool := !b'; + have x : Nat := 1 * x; + have b' : Bool := !b'; + have x : Nat := 1 * x; + have b' : Bool := !b'; + have x : Nat := 1 * x; + if b' = true then x else 0 +-/ +#guard_msgs in #let_to_have fun a => deepLets% 5 true (0 + a) + +/-- +info: fun a => + have b' : Bool := !true; + have x : Nat := 1 * (0 + a); + have b' : Bool := !b'; + have x : Nat := 1 * x; + have b' : Bool := !b'; + have x : Nat := 1 * x; + have b' : Bool := !b'; + have x : Nat := 1 * x; + have b' : Bool := !b'; + have x : Nat := ⋯; + ⋯ +-/ +#guard_msgs in set_option pp.deepTerms.threshold 10 in #let_to_have fun a => deepLets% 33 true (0 + a) +/-- +info: fun a => + have b' : Bool := !true; + have x : Nat := 1 * (0 + a); + have b' : Bool := !b'; + have x : Nat := 1 * x; + have b' : Bool := !b'; + have x : Nat := 1 * x; + have b' : Bool := !b'; + have x : Nat := 1 * x; + have b' : Bool := !b'; + have x : Nat := ⋯; + ⋯ +-/ +#guard_msgs in set_option pp.deepTerms.threshold 10 in #let_to_have fun a => deepLets% 150 true (0 + a) + +/-! +Tests of the `let_to_have` tactic. +-/ +/-- +trace: h : + have x : Nat := 1; + x = x +⊢ have y : Nat := 1; + y = y +-/ +#guard_msgs in +example (h : let x := 1; x = x) : let y := 1; y = y := by + let_to_have at * + trace_state + rfl +/-- +trace: h : + let x : Nat := 1; + x = x +⊢ have y : Nat := 1; + y = y +-/ +#guard_msgs in +example (h : let x := 1; x = x) : let y := 1; y = y := by + let_to_have + trace_state + rfl +/-- +trace: h : + have x : Nat := 1; + x = x +⊢ let y : Nat := 1; + y = y +-/ +#guard_msgs in +example (h : let x := 1; x = x) : let y := 1; y = y := by + let_to_have at h + trace_state + rfl