feat: use nondep flag in Expr.letE and LocalContext.ldecl
#8804
Conversation
|
Mathlib CI status (docs):
|
5a5650a to
0b63061
Compare
This PR makes changes for compatibility with leanprover/lean4#8804. The key difference is that `nondep := true` should be treated as a cdecl. The `LocalDecl.isLet` will return false for such ldecls.
| let result ← if useLetExpr then | ||
| withLetDecl id.getId (kind := kind) type val fun x => do | ||
| let result ← | ||
| withLetDecl id.getId (kind := kind) type val (nondep := !useLetExpr) fun x => do | ||
| addLocalVarInfo id x |
There was a problem hiding this comment.
Nice. @kmill No action needed here. I am just marking non trivial changes that I have already checked.
| if !zetaDeltaFVarIds.contains fvarId then | ||
| /- Non-dependent let-decl. See comment at src/Lean/Meta/Closure.lean -/ | ||
| if nondep || !zetaDeltaFVarIds.contains fvarId then | ||
| /- Nondependent let-decl. See comment at src/Lean/Meta/Closure.lean -/ |
There was a problem hiding this comment.
@kmill This is an optimization, correct? I am assuming that if fvarId is in zetaDeltaFVarIds and nondep is true, then the nondep annotation is incorrect.
There was a problem hiding this comment.
Correct, if nondep is true then it is not possible for zetaDeltaFVarIds to contain fvarId. This is just a small optimization.
There was a problem hiding this comment.
Added a comment mentioning this invariant.
| | Expr.letE n type val body nondep => | ||
| -- Turn `have`s into `let`s if they are not propositions. | ||
| let nondep ← pure nondep <&&> not <$> Meta.isProp type | ||
| mapLetDecl n (← loop below type) (← loop below val) (nondep := nondep) (usedLetOnly := false) fun x => do |
There was a problem hiding this comment.
Remind me of the rationale for turning have to let in structural recursion, Kyle?
| @@ -110,14 +110,68 @@ builtin_dsimproc paramMatcher (_) := fun e => do | |||
| let matcherApp' := { matcherApp with discrs := discrs', alts := alts' } | |||
| return .continue <| matcherApp'.toExpr | |||
|
|
|||
| /-- `let x := (wfParam e); body[x] ==> let x := e; body[wfParam y] -/ | |||
| private def anyLetValueIsWfParam (e : Expr) : Bool := | |||
There was a problem hiding this comment.
@nomeata I am assuming you are happy with these changes. I am asking because you own this file.
src/Lean/LocalContext.lean
Outdated
| Instead, `revert x` *must* produce the goal `⊢ ∀ x : α, b`. | ||
| Furthermore, given a goal `⊢ have x : α := v; b`, the `intro x` tactic should yield a *dependent* `ldecl`, | ||
| since users expect to be able to make use of the value of `x`, | ||
| and also the value creates a hidden source of dependencies on other local variables. |
There was a problem hiding this comment.
@kmill You justified well the design decisions, but it would be great to include a note saying how one gets a nondep ldecl into the local context x : α := v (nondep) ⊢ b since intro will introduce a dependent one for have.
| since users expect to be able to make use of the value of `x`, | ||
| and also the value creates a hidden source of dependencies on other local variables. | ||
| - Also: `value` might not be type correct. Metaprograms may decide to pretend that all `nondep := true` | ||
| `ldecl`s are `cdecl`s (for example, when reverting variables). As a consequence, nondep `ldecl`s may |
There was a problem hiding this comment.
Should we have a debugging flag to force Lean to type check the value at functions such as withLetDecl?
There was a problem hiding this comment.
I'll keep this in mind. Thinking about possible metaprogramming mistakes, maybe mkBinding could check that the value's fvars are all in context?
| def setValue : LocalDecl → Expr → LocalDecl | ||
| | ldecl idx id n t _ nd k, v => ldecl idx id n t v nd k | ||
| | d, _ => d | ||
|
|
||
| /-- Sets the `nondep` flag of an `ldecl`, otherwise returns `cdecl`s unchanged. -/ | ||
| def setNondep : LocalDecl → Bool → LocalDecl |
There was a problem hiding this comment.
@kmill Should we add a note saying that it is the caller responsibility to ensure dep => nondep transitions are correct?
There was a problem hiding this comment.
Added some guidelines to the docstring
| -/ | ||
| def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α := | ||
| map2MetaM (fun k => lambdaTelescopeImp e true .none k (cleanupAnnotations := cleanupAnnotations)) k | ||
| def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) (preserveNondepLet := true) : n α := |
There was a problem hiding this comment.
In the current master, lambdaLetTelescope stops at have. For example, the following example prints 1.
import Lean
def c : Nat → Nat → Bool := fun x => have y := 1; fun z => x == y + z
open Lean Meta in
run_meta do
let decl ← getConstInfo ``c
lambdaLetTelescope decl.value! fun xs _ => IO.println xs.size I am not defending the current behavior.
The comment above suggests that this example will print 3 if preserveNondepLet := false. What happens if preserveNondepLet := true. I am assuming it will "consume" the have and mark it as nondep in the local context.
There was a problem hiding this comment.
Yes, now haves are always consumed and that prints 3. Setting preserveNondepLet controls whether the nondep flag will be cleared. I've added this to the tests:
def c : Nat → Nat → Bool := fun x => have y := 1; fun z => x == y + z
/--
info: #[false, true, false]
#[false, false, false]
-/
#guard_msgs in
open Lean Meta in
run_meta do
let decl ← getConstInfo ``c
lambdaLetTelescope decl.value! fun xs _ => do
IO.println <| ← xs.mapM fun x => return (← x.fvarId!.getDecl).isNondep
lambdaLetTelescope decl.value! (preserveNondepLet := false) fun xs _ => do
IO.println <| ← xs.mapM fun x => return (← x.fvarId!.getDecl).isNondep|
|
||
| See also `mapLetTelescope` for entering and rebuilding the telescope. | ||
| -/ | ||
| def letTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) (preserveNondepLet := true) (nondepLetOnly := false) : n α := |
There was a problem hiding this comment.
I am assuming there is no way to consume only dependent lets.
There was a problem hiding this comment.
Correct, there's no way to do that at the moment (I haven't needed it yet).
| let zetaDeltaFVarIds ← getZetaDeltaFVarIds | ||
| if !zetaDeltaFVarIds.contains fvarId then | ||
| if nondep || !zetaDeltaFVarIds.contains fvarId then | ||
| /- Non-dependent let-decl |
There was a problem hiding this comment.
Same as comment above. I am assuming this is an optimization.
There was a problem hiding this comment.
Added a comment about the invariant
| @@ -728,7 +728,7 @@ mutual | |||
| else | |||
| let lctx := ctxMeta.lctx | |||
| match lctx.findFVar? fvar with | |||
| | some (.ldecl (value := v) ..) => check v | |||
| | some (.ldecl (nondep := false) (value := v) ..) => check v | |||
| | _ => | |||
There was a problem hiding this comment.
@kmill Could you please document this change? We need a why? and example showing why the previous behavior was incorrect.
There was a problem hiding this comment.
Added an explanation and example.
| @@ -917,7 +917,7 @@ unsafe def checkImpl | |||
| | .fvar fvarId .. => | |||
| if mvarDecl.lctx.contains fvarId then | |||
| return true | |||
| if let some (LocalDecl.ldecl ..) := lctx.find? fvarId then | |||
| if let some (LocalDecl.ldecl (nondep := false) ..) := lctx.find? fvarId then | |||
There was a problem hiding this comment.
Added a comment pointing to the new comment in CheckAssignment.checkFVar.
| @@ -379,13 +379,13 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E | |||
| let body' ← foldAndCollect oldIH newIH isRecCall (body.instantiate1 x) | |||
| mkForallFVars #[x] body' | |||
|
|
|||
| | .letE n t v b _ => | |||
| | .letE n t v b nondep => | |||
There was a problem hiding this comment.
@nomeata Are you happy with the changes to this file?
| mkLetFun decl.toExpr decl.value e | ||
| def mkLetDecls (decls : Array LocalDecl') (e : Expr) : Expr := | ||
| decls.foldr (init := e) fun { decl, isLet } e => | ||
| Expr.letE decl.userName decl.type decl.value (e.abstract #[decl.toExpr]) (nondep := !isLet) |
| withLocalDeclD n t fun x => do | ||
| let bx := b.instantiate1 x | ||
| if nondep then | ||
| let bxType ← whnf (← inferType bx) | ||
| if (← dependsOn bxType x.fvarId!) then |
There was a problem hiding this comment.
@kmill Could you please add a comment here explaining this part? We will forget.
There was a problem hiding this comment.
Added an explanation.
By the way, I have a followup PR that intends to replace this code. Brief preview: if simp comes across a nondep := false let, then it can run letToHave on it (which is slightly cheaper than isTypeCorrect, and it addresses the "TODO" comment in this function, by handling all lets simultaneously), and otherwise we can do the nondepDepVar/nondep determination on an entire telescope at once, using code similar to what you wrote for letFun.
| @@ -721,8 +729,8 @@ def simpApp (e : Expr) : SimpM Result := do | |||
| if isOfNatNatLit e || isOfScientificLit e || isCharLit e then | |||
| -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n` | |||
| return { expr := e } | |||
| 4D32 else if isNonDepLetFun e then | |||
| simpNonDepLetFun e | |||
| else if let some (args, n, t, v, b) := e.letFunAppArgs? then | |||
There was a problem hiding this comment.
Added a comment/explanation that this piece of code is in flux. (It should be addressed in time for the next release, so hopefully this comment is short-lived!)
There was a problem hiding this comment.
Leo asked me to give this a read-through, too.
High-level thought: I’m a bit worried about the complexities around ldecl behaving one way or another depending on their flag and various flags on the functions acting on them. If it wasn’t for backwards compat, would we do it this way, or would entering a have just leave a cdecl in the context, and leave it to whoever rebuilds the expression to remember to use a nondep expression? But you probably considered that design and chose this one for a reason.
In a few cases my brain has trouble keeping up with an optional boolean flag that is called non-something, too much negation and boolean blindness. In terms of API design, at least for those functions where one flag is common and the other is very rare and possibly dangerous or at least hairy to get right, if it’d be better to have separate functions with more speaking names.
| | Expr.letE n type val body nondep => | ||
| -- Turn `have`s into `let`s if they are not propositions. | ||
| let nondep ← pure nondep <&&> not <$> Meta.isProp type | ||
| mapLetDecl n (← loop below type) (← loop below val) (nondep := nondep) (usedLetOnly := false) fun x => do |
There was a problem hiding this comment.
Remind me of the rationale for turning have to let in structural recursion, Kyle?
| withLetDecl n (← loop type) (← loop val) fun x => do | ||
| mkLetFVars #[x] (← loop (body.instantiate1 x)) | ||
| | Expr.letE n type val body nondep => | ||
| mapLetDecl n (← loop type) (← loop val) (nondep := nondep) fun x => do |
There was a problem hiding this comment.
I like the mapLetDecl combinator to capture that idioms here, I think I wanted something like that before. Maybe later we’ll want it for mapForall etc. as well. (And then generalize the result from Expr to a HasExpr type class so that we can return (Bool, Expr) or (Expr, Expr) … :-))
| @@ -110,14 +110,68 @@ builtin_dsimproc paramMatcher (_) := fun e => do | |||
| let matcherApp' := { matcherApp with discrs := discrs', alts := alts' } | |||
| return .continue <| matcherApp'.toExpr | |||
|
|
|||
| /-- `let x := (wfParam e); body[x] ==> let x := e; body[wfParam y] -/ | |||
| private def anyLetValueIsWfParam (e : Expr) : Bool := | |||
src/Lean/LocalContext.lean
Outdated
| /-- Returns true if this is an `ldecl`. If `allowNondep` is false (the default), then requires that `nondep` be false. -/ | ||
| def isLet : LocalDecl → (allowNondep : Bool := false) → Bool | ||
| | cdecl .., _ => false | ||
| | ldecl (nondep := false) .., _ => true | ||
| | ldecl (nondep := true) .., allowNondep => allowNondep |
There was a problem hiding this comment.
The only use of the optional parameter is through isLetVar, and there it is isn’t used, it seems.
I wonder if we get easier to understand code if isLet and isLetVar doesn’t take an optional parameter, and we have separate functions isLetOrHave and isLetOrHaveVar for what’s now (allowNonDep := true). Especially if we don’t expect meta-code to be “dynamically generic” in the allowNonDep flag.
I guess we’d also need letOrHaveValue?. Up to you.
There was a problem hiding this comment.
Sorry, had to step away before your last message — I was going to say that I'll review this part of the API again after a couple PRs.
Any thoughts about generalizeNondepLet? I'm wondering if I got the polarity wrong on that one, but I couldn't think of anything else to call it. At least it's used infrequently enough that it wouldn't be hard to change it later.
There was a problem hiding this comment.
I had to think when I read it, but then concluded that the name is correct 🤷🏻
src/Lean/LocalContext.lean
Outdated
| - If the declaration is for a variable whose dependencies are not completely under the caller's control, | ||
| then setting `nondep := false` must not be done. | ||
| - Even if the caller does have complete control, setting `nondep := false` should not be done. | ||
| The cautions about caches and metavariables still apply. |
There was a problem hiding this comment.
This sounds like there isn’t a need to even support nondep := false, if it shouldn't be done. Do we need it?
Although, the only use case I see in this diff is
-- Clear the flag if it's not a prop.
let decl' := decl.setNondep <| ← pure decl.isNondep <&&> Meta.isProp decl.type
And it seems that this may do a (nondep := true) → (nondep := false) transition… if this is something that shouldn’t be done, do we need a comment there why we do it?
I wonder again if the code was clearer if we have separate setNondep and clearNonDep functions, and write it like this:
-- Clear the flag if it's not a prop.
if (← Meta.isProp decl.type) the
decl := decl.clearNondep
assuming we can afford the Meta.isProp check, or
-- Clear the flag if it's not a prop.
if (← decl.isNondep <&&> Meta.isProp decl.type) the
decl := decl.clearNondep
There was a problem hiding this comment.
I've tried to clarify this docstring.
I was trying to use "must not" vs "should not" technically, but that's too confusing. There's an example of ok nondep := false usage and why, taken from the WF changes.
It's reasonable to worry about whether backwards compatibility was a consideration, but I tried to make the design be from first principles. A case study we have is what it's been like to work with letFun, where you have to enter it as a cdecl and then awkwardly apply the letfun constructor at the correct points in a telescope. In an earlier version of There seems to be something fundamental here with there being variables where in different situations the value is either known or not known, and I wish I had some more theory to support it. That lack of supporting theory is a weakness of this design in my opinion. Another design idea I had was to add an
In any case, so long as metaprograms use
It seems like a negation, but I think in practice "nondependent" is a positive quality. It could have been called "simple"/"fun"/"have"/etc. The default value for the flag is
Yes, this is the purpose of the Something that helped me feel like the approach in the PR was on the right track is that none of the uses of the
I'll check this one again. I know there was a motivating test case, but I don't remember if it was (1) because of changes to simp in this PR, which caches nondependence in the letE expression or (2) if it is necessary once letToHave is being universally applied in a future PR. (I'll respond to your other comments directly.) |
|
Thanks, that's convincing.
Hm, but isn't that even more reason to make it not look as if But we are entering superficial bike shedding territory, and it's not like the rest of Lean's API is designed with psychological nudges in mind, so it's ok as is. |
|
What's the situation around kernel changes here? Should the kernel now treat |
|
@digama0 Quoting the PR summary: "Note that nondependence of lets is not checked by the kernel." For the time being, we'll rely on the elaborator typechecker to spot-check nondep usage. (Or, possibly, in some contexts such as proofs we might have the elaborator use a letFun/beta-redex encoding to keep the variable from being unfolded during checking, for performance.) If you want to implement checking it in an external checker, then I think there are two main options: either convert |
This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x := v; b` is called *nondependent* if `fun x => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been fully supported throughout the metaprogramming interface and the elaborator. Note that nondependence of lets is not checked by the kernel. Follows up from leanprover#8751, which made sure the nondep flag was preserved in the C++ interface.
8c4d1cf to
2f02cad
Compare
…prover#8804) This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x : t := v; b` is called *nondependent* if `fun x : t => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been given full support throughout the metaprogramming interface and the elaborator. Key changes to the metaprogramming interface: - Local context `ldecl`s with `nondep := true` are generally treated as `cdecl`s. This is because in the body of a `have` expression the variable is opaque. Functions like `LocalDecl.isLet` by default return `false` for nondependent `ldecl`s. In the rare case where it is needed, they take an additional optional `allowNondep : Bool` flag (defaults to `false`) if the variable is being processed in a context where the value is relevant. - Functions such as `mkLetFVars` by default generalize nondependent let variables and create lambda expressions for them. The `generalizeNondepLet` flag (default true) can be set to false if `have` expressions should be produced instead. **Breaking change:** Uses of `letLambdaTelescope`/`mkLetFVars` need to use `generalizeNondepLet := false`. See the next item. - There are now some mapping functions to make telescoping operations more convenient. See `mapLetTelescope` and `mapLambdaLetTelescope`. There is also `mapLetDecl` as a counterpart to `withLetDecl` for creating `let`/`have` expressions. - Important note about the `generalizeNondepLet` flag: it should only be used for variables in a local context that the metaprogram "owns". Since nondependent let variables are treated as constants in most cases, the `value` field might refer to variables that do not exist, if for example those variables were cleared or reverted. Using `mapLetDecl` is always fine. - The simplifier will cache its let dependence calculations in the nondep field of let expressions. - The `intro` tactic still produces *dependent* local variables. Given that the simplifier will transform lets into haves, it would be surprising if that would prevent `intro` from creating a local variable whose value cannot be used. Note that nondependence of lets is not checked by the kernel. To external checker authors: If the elaborator gets the nondep flag wrong, we consider this to be an elaborator error. Feel free to typecheck `letE n t v b true` as if it were `app (lam n t b default) v` and please report issues. This PR follows up from leanprover#8751, which made sure the nondep flag was preserved in the C++ interface.
This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression
let x : t := v; bis called nondependent iffun x : t => btypechecks, and the notation for a nondependent let expression ishave x := v; b. Previously we encodedhaveusing theletFunfunction, but now we make use of thenondepflag in theExpr.letEconstructor for the encoding. This has been given full support throughout the metaprogramming interface and the elaborator. Key changes to the metaprogramming interface:ldecls withnondep := trueare generally treated ascdecls. This is because in the body of ahaveexpression the variable is opaque. Functions likeLocalDecl.isLetby default returnfalsefor nondependentldecls. In the rare case where it is needed, they take an additional optionalallowNondep : Boolflag (defaults tofalse) if the variable is being processed in a context where the value is relevant.mkLetFVarsby default generalize nondependent let variables and create lambda expressions for them. ThegeneralizeNondepLetflag (default true) can be set to false ifhaveexpressions should be produced instead. Breaking change: Uses ofletLambdaTelescope/mkLetFVarsneed to usegeneralizeNondepLet := false. See the next item.mapLetTelescopeandmapLambdaLetTelescope. There is alsomapLetDeclas a counterpart towithLetDeclfor creatinglet/haveexpressions.generalizeNondepLetflag: it should only be used for variables in a local context that the metaprogram "owns". Since nondependent let variables are treated as constants in most cases, thevaluefield might refer to variables that do not exist, if for example those variables were cleared or reverted. UsingmapLetDeclis always fine.introtactic still produces dependent local variables. Given that the simplifier will transform lets into haves, it would be surprising if that would preventintrofrom creating a local variable whose value cannot be used.Note that nondependence of lets is not checked by the kernel. To external checker authors: If the elaborator gets the nondep flag wrong, we consider this to be an elaborator error. Feel free to typecheck
letE n t v b trueas if it wereapp (lam n t b default) vand please report issues.This PR follows up from #8751, which made sure the nondep flag was preserved in the C++ interface.