max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add Meta.letToHave and the let_to_have tactic (#8954)

Browse source 
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.
This commit is contained in:
Kyle Miller 2025-06-23 18:33:53 -07:00 • committed by GitHub
parent 0941d53f6a
commit 71cf266cd7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 844 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Conv.lean
View file

@ -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.

7
src/Init/Tactics.lean
View file

@ -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

13
src/Lean/Elab/Tactic/Conv/Lets.lean
View file

@ -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

11
src/Lean/Elab/Tactic/Lets.lean
View file

@ -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

1
src/Lean/Meta.lean
View file

@ -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

6
src/Lean/Meta/Basic.lean
View file

@ -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.

443
src/Lean/Meta/LetToHave.lean Normal file
View file

@ -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

31
src/Lean/Meta/Tactic/Lets.lean
View file

@ -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'

2
src/Lean/Meta/WHNF.lean
View file

@ -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 =>

325
tests/lean/run/letToHave.lean Normal file
View file

@ -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