feat: add the nondep field of Expr.letE to the C++ data model
#8751
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This PR adds the `nonDep` field of `Expr.letE` to the C++ data model. Previously this was unused, and in followup PRs the elaborator will use it to encode `have` expressions (non-dependent `let`s). The kernel does not verify that `nonDep` is correctly applied during typechecking. Breaking change: now `Expr.updateLet!` is `Expr.updateLetE!`. This PR also fixes a bug in `Expr.letFun?` and `Expr.letFunAppArgs?` when the body is not a lambda. In any case, these functions will be removed once the `Expr.letE (nonDep := true)` encoding of `have` expressions is complete.
|
Mathlib CI status (docs):
|
Rob23oba
reviewed
Jun 12, 2025
zwarich
reviewed
Jun 12, 2025
src/kernel/expr.cpp
Outdated
| @@ -295,6 +295,12 @@ bool is_default_var_name(name const & n) { | |||
| return n == *g_default_name; | |||
| } | |||
|
|
|||
| extern "C" uint8 lean_expr_isHave(object * e); | |||
| bool let_nonDep_core(expr const & e) { | |||
There was a problem hiding this comment.
Similarly to lean_expr_isHave making more sense as lean_expr_is_have, I think let_nonDep_core makes more sense as let_non_dep_core, and similarly for other uses of non_dep. The camel case really sticks out like a sore thumb (hump?) in the C++ code.
There was a problem hiding this comment.
Given that nondependent is a word, I went with let_nondep and let_nondep_core. Any objection to that? (I might switch nonDep to nondep in Lean later.)
There was a problem hiding this comment.
Yeah that seems fine. There's already an is_nondep_elim in lcnf.cpp.
nonDep field of Expr.letE to the C++ data modelnondep field of Expr.letE to the C++ data model
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 13, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 13, 2025
leodemoura
reviewed
Jun 14, 2025
| @@ -1965,7 +1984,7 @@ def letFun? (e : Expr) : Option (Name × Expr × Expr × Expr) := | |||
| | .app (.app (.app (.app (.const ``letFun _) t) _β) v) f => | |||
| match f with | |||
| | .lam n _ b _ => some (n, t, v, b) | |||
| | _ => some (.anonymous, t, v, .app f (.bvar 0)) | |||
| | _ => some (.anonymous, t, v, .app (f.liftLooseBVars 0 1) (.bvar 0)) | |||
There was a problem hiding this comment.
Did you hit this bug when implementing this PR?
There was a problem hiding this comment.
Sorry, this wasn't good PR hygiene. I found this bug in other work, and I was extracting changes to Expr.lean to make this PR.
I plan to deprecate/delete this function anyway, but I left in the change because it does fix a bug.
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Jun 14, 2025
This PR adds `have` forms of simp lemmas that will be used in a future `have` simplifier. This depends on leanprover#8751 and future elaboration changes, since these are meant to elaborate using `Expr.letE (nondep := true) ..` expressions; otherwise they are duplicates of the `letFun_*` lemmas.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Jun 14, 2025
This PR adds `have` forms of simp lemmas that will be used in a future `have` simplifier. This depends on #8751 and future elaboration changes, since these are meant to elaborate using `Expr.letE (nondep := true) ..` expressions; for now they are duplicates of the `letFun_*` lemmas.
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Jun 16, 2025
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.
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 16, 2025
* Update lean-toolchain for testing leanprover/lean4#8584 * chore: adaptations for nightly-2025-06-02 * change phrasing of comments * chore(Geometry/Manifold): two simp-lemmas can be proven by simp * fix two lint problems * Trigger CI for leanprover/lean4#8519 * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but f 8000 or a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 17, 2025
* chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 17, 2025
* revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 --------- Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de>
algebraic-dev
pushed a commit
to algebraic-dev/lean4
that referenced
this pull request
Jun 18, 2025
…anprover#8751) This PR adds the `nondep` field of `Expr.letE` to the C++ data model. Previously this field has been unused, and in followup PRs the elaborator will use it to encode `have` expressions (non-dependent `let`s). The kernel does not verify that `nondep` is correctly applied during typechecking. The `letE` delaborator now prints `have`s when `nondep` is true, though `have` still elaborates as `letFun` for now. Breaking change: `Expr.updateLet!` is renamed to `Expr.updateLetE!`. This PR also fixes a bug in `Expr.letFun?` and `Expr.letFunAppArgs?` when the body is not a lambda. In any case, these functions will be removed once the `Expr.letE (nondep := true)` encoding of `have` expressions is complete.
algebraic-dev
pushed a commit
to algebraic-dev/lean4
that referenced
this pull request
Jun 18, 2025
This PR adds `have` forms of simp lemmas that will be used in a future `have` simplifier. This depends on leanprover#8751 and future elaboration changes, since these are meant to elaborate using `Expr.letE (nondep := true) ..` expressions; for now they are duplicates of the `letFun_*` lemmas.
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Jun 18, 2025
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.
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 19, 2025
* bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptatio F438 ns for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 20, 2025
* Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * chore: bump to nightly-2025-06-19 * fix * remove mul_hmul * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Jun 22, 2025
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.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Jun 22, 2025
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 #8751, which made sure the nondep flag was preserved in the C++ interface.
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Jun 24, 2025
…anprover#8751) This PR adds the `nondep` field of `Expr.letE` to the C++ data model. Previously this field has been unused, and in followup PRs the elaborator will use it to encode `have` expressions (non-dependent `let`s). The kernel does not verify that `nondep` is correctly applied during typechecking. The `letE` delaborator now prints `have`s when `nondep` is true, though `have` still elaborates as `letFun` for now. Breaking change: `Expr.updateLet!` is renamed to `Expr.updateLetE!`. This PR also fixes a bug in `Expr.letFun?` and `Expr.letFunAppArgs?` when the body is not a lambda. In any case, these functions will be removed once the `Expr.letE (nondep := true)` encoding of `have` expressions is complete.
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Jun 24, 2025
This PR adds `have` forms of simp lemmas that will be used in a future `have` simplifier. This depends on leanprover#8751 and future elaboration changes, since these are meant to elaborate using `Expr.letE (nondep := true) ..` expressions; for now they are duplicates of the `letFun_*` lemmas.
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Jun 24, 2025
…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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds the
nondepfield ofExpr.letEto the C++ data model. Previously this field has been unused, and in followup PRs the elaborator will use it to encodehaveexpressions (non-dependentlets). The kernel does not verify thatnondepis correctly applied during typechecking. TheletEdelaborator now printshaves whennondepis true, thoughhavestill elaborates asletFunfor now. Breaking change:Expr.updateLet!is renamed toExpr.updateLetE!.This PR also fixes a bug in
Expr.letFun?andExpr.letFunAppArgs?when the body is not a lambda. In any case, these functions will be removed once theExpr.letE (nondep := true)encoding ofhaveexpressions is complete.