Skip to content

feat: clear_value tactic#8449

Merged
kmill merged 2 commits intoleanprover:masterfrom
kmill:kmill_clear_value
May 27, 2025
Merged

feat: clear_value tactic#8449
kmill merged 2 commits intoleanprover:masterfrom
kmill:kmill_clear_value

Conversation

@kmill
Copy link
Copy Markdown
Collaborator

@kmill kmill commented May 23, 2025

This PR upstreams and extends the Mathlib clear_value tactic. Given a local definition x : T := v, the tactic clear_value x replaces it with a hypothesis x : T, or throws an error if the goal does not depend on the value v. The syntax clear_value x with h creates a hypothesis h : x = v before clearing the value of x. Furthermore, clear_value * clears all values that can be cleared, or throws an error if none can be cleared.

@kmill
feat: clear_value tactic
d98f25c 
This PR upstreams and extends the Mathlib `clear_value` tactic. Given a local definition `x : T := v`, the tactic `clear_value x` replaces it with a hypothesis `x : T`, or throws an error if the goal does not depend on the value `v`. The syntax `clear_value x with h` creates a hypothesis `h : x = v` before clearing the value of `x`. Furthermore, `clear_value *` clears all values that can be cleared, or throws an error if none can be cleared.
@kmill kmill requested review from kim-em and leodemoura as code owners May 23, 2025 09:40
@kmill kmill added the changelog-language Language features and metaprograms label May 23, 2025
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 23, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 23, 2025
Update lean-toolchain for testing leanprover/lean4#8449
e1f28a9
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 23, 2025
Update lean-toolchain for testing leanprover/lean4#8449
12fcc22
@ghost
Copy link
Copy Markdown

ghost commented May 23, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label May 23, 2025
@Rob23oba
Copy link
Copy Markdown
Contributor

Rob23oba commented May 23, 2025

This doesn't fix leanprover-community/mathlib4#25053, does it? I think we need let tgt ← instantiateMVars tgt after the getType to fix it.

@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels May 23, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 26, 2025
Trigger CI for leanprover/lean4#8449
9c5ba15
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 26, 2025
Trigger CI for leanprover/lean4#8449
e0adc74
@kmill
Copy link
Copy Markdown
Collaborator Author

kmill commented May 27, 2025

Thanks for pointing out that issue @Rob23oba. Using instantiateMVars shouldn't be needed here, though it does fix this particular example. I've made #8488 to keep track of the deeper issue.

@kmill kmill mentioned this pull request May 27, 2025
Open
3 tasks
@kmill kmill added this pull request to the merge queue May 27, 2025
Merged via the queue into leanprover:master with commit a6dd6a4 May 27, 2025
15 checks passed
@digama0
Copy link
Copy Markdown
Collaborator

digama0 commented May 27, 2025

The syntax clear_value x with h creates a hypothesis h : x = v before clearing the value of x.

Can I suggest the notation clear_value h : x instead? I would like us to get away from the with h pattern currently only used in mathlib tactics, since lean core usually uses with for clauses instead, and h : is used to add equality assumptions in cases, generalize and match.

@kmill
Copy link
Copy Markdown
Collaborator Author

kmill commented May 27, 2025

Discussion for syntax started on Zulip.

@kmill kmill mentioned this pull request May 27, 2025
Closed
3 tasks
kmill added a commit to kmill/lean4 that referenced this pull request May 28, 2025
@kmill
feat: different syntax for new clear_value tactic
435dce6 
This PR is a followup to leanprover#8449 to refine the syntax of `clear_value`. Now the syntax for adding equality hypotheses before clearing values is `clear_value (h : x = _)`.

This syntax was developed in a [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60clear_value.60.20syntax.20request.20for.20comments/near/520704290).
@kmill kmill mentioned this pull request May 28, 2025
Merged
kmill added a commit to kmill/lean4 that referenced this pull request May 28, 2025
@kmill
feat: different syntax for new clear_value tactic
5d1268d 
This PR is a followup to leanprover#8449 to refine the syntax of `clear_value`. Now the syntax for adding equality hypotheses before clearing values is `clear_value (h : x = _)`.

This syntax was developed in a [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60clear_value.60.20syntax.20request.20for.20comments/near/520704290).
github-merge-queue bot pushed a commit that referenced this pull request May 28, 2025
@kmill
feat: different syntax for new clear_value tactic (#8516)
4dd8648 
This PR is a followup to #8449 to refine the syntax of `clear_value`.
The syntax for adding equality hypotheses before clearing values is now
`clear_value (h : x = _)`. Any expression definitionally equal to `x`
can be used in place of the underscore.

This syntax was developed in a [Zulip
discussion](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60clear_value.60.20syntax.20request.20for.20comments/near/520704290).
jcommelin pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 4, 2025
@kim-em @Vierkantor
@Kha @eric-wieser @Rob23oba @jrr6
chore: adaptations for nightly-2025-06-04 (#25431)
3780f5f 
* Update lean-toolchain for testing leanprover/lean4#8347

* fixes for leanprover/lean4#8347

* Update lean-toolchain for testing leanprover/lean4#8397

* deprecations for leanprover/lean4#8397

* chore: bump to nightly-2025-05-19

* chore: adaptations for nightly-2025-05-19

* Trigger CI for leanprover/lean4#8347

* Update the style linter to use LinterOptions

* Fix test

* chore: adaptations for nightly-2025-05-19 (#25017)



Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

* chore: bump to nightly-2025-05-20

* Merge master into nightly-testing

* feat: a `grind` test case (#25037)

Adds a test case for `grind` that was previously failing in the presence of Mathlib's typeclass shortcuts. Let's just keep it in Mathlib as a regression test.

Note that this is a PR to `bump/v4.21.0`, as it requires a recent nightly toolchain. (It can still be reviewed and bors'd as any other PR.)

* lake update

* fixes

* fixes

* fixes

* fixes

* fix

* fixes

* fixes

* shake --update

* chore: bump to nightly-2025-05-21

* Update lean-toolchain for testing leanprover/lean4#7352

* lake update

* Trigger CI for leanprover/lean4#7352

* chore: adaptations for nightly-2025-05-21

* chore: adaptations for nightly-2025-05-21 (#25079)



Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
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: Anne C.A. Baanen <vierkantor@vierkantor.com>

* chore: adaptations for nightly-2025-05-21

* fix for leanprover/lean4#7352

* remove unneeded List.ofFn_succ from simp sets

* Merge master into nightly-testing

* Merge master into nightly-testing

* Revert "fix for leanprover/lean4#7352"

This reverts commit 38ca408.

* chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.

* chore: bump to nightly-2025-05-22

* update batteries

* chore: bump to nightly-2025-05-23

* Update lean-toolchain for testing leanprover/lean4#8449

* chore: adaptations for nightly-2025-05-22 (#25110)



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: github-actions <github-actions@github.com>

* remove now upstreamed `clear_value`

* Update lean-toolchain for testing leanprover/lean4#8457

* chore: update tests for `Format` bug fix

* Trigger CI for leanprover/lean4#8457

* lake update

* lake update

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-24

* fix

* chore: adaptations for nightly-2025-05-24 (#25147)



Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>

* chore: adaptations for nightly-2025-05-24

* Merge master into nightly-testing

* Update lean-toolchain for testing leanprover/lean4#8470

* chore: bump to nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25 (#25184)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>

* unsimp `List.getElem?_length`

This is solved using `getElem?_neg` now.

* chore: adaptations for nightly-2025-05-25

* Trigger CI for leanprover/lean4#8470

* chore: bump to nightly-2025-05-26

* lake update

* deprecations

* Trigger CI for leanprover/lean4#8449

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-27

* chore: adaptations for nightly-2025-05-27

* Update lean-toolchain for testing leanprover/lean4#8504

* chore: bump to nightly-2025-05-28

* chore: adaptations for nightly-2025-05-27 (#25234)



Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>

* fix

* fix merge

* fix merge again

* deprecations

* deprecations

* fix Archive

* comment out test

* Fix and re-enable directory dependency lint test.

* chore: bump to nightly-2025-05-29

* Use the formatting from the master branch. (Seems to have been a merge that went wrong.)

* lake update

* chore: adaptations for nightly-2025-05-28 (#25295)



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: github-actions <github-actions@github.com>

* fix

* Trigger CI for leanprover/lean4#8337

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-30

* chore: adaptations for nightly-2025-05-29 (#25306)



Co-authored-by: Kim Morrison <kim@tqft.net>
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: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>

* chore: bump to nightly-2025-05-31

* chore: bump to nightly-2025-06-01

* fix Archive

* chore: adaptations for nightly-2025-06-01 (#25355)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

* chore: bump to nightly-2025-06-02

* chore: adaptations for nightly-2025-06-02 (#25360)



Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>

* Update lean-toolchain for testing leanprover/lean4#8584

* chore: adaptations for nightly-2025-06-02

* chore: bump to nightly-2025-06-03

* fix

* fix

* Update lean-toolchain for testing leanprover/lean4#8610

* fix

* chore: bump to nightly-2025-06-04

* bump toolchain

---------

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: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
jcommelin added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 6, 2025
@kim-em @eric-wieser
@Rob23oba @jrr6 @Vierkantor @Kha @jcommelin @JovanGerb @nomeata
chore: adaptations for nightly-2025-06-05 (#25490)
5a9a408 
* chore: adaptations for nightly-2025-05-21

* fix for leanprover/lean4#7352

* remove unneeded List.ofFn_succ from simp sets

* Merge master into nightly-testing

* Merge master into nightly-testing

* Revert "fix for leanprover/lean4#7352"

This reverts commit 38ca408.

* chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.

* chore: bump to nightly-2025-05-22

* update batteries

* chore: bump to nightly-2025-05-23

* Update lean-toolchain for testing leanprover/lean4#8449

* chore: adaptations for nightly-2025-05-22 (#25110)



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: github-actions <github-actions@github.com>

* remove now upstreamed `clear_value`

* Update lean-toolchain for testing leanprover/lean4#8457

* chore: update tests for `Format` bug fix

* Trigger CI for leanprover/lean4#8457

* lake update

* lake update

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-24

* fix

* chore: adaptations for nightly-2025-05-24 (#25147)



Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>

* chore: adaptations for nightly-2025-05-24

* Merge master into nightly-testing

* Update lean-toolchain for testing leanprover/lean4#8470

* chore: bump to nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25 (#25184)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>

* unsimp `List.getElem?_length`

This is solved using `getElem?_neg` now.

* chore: adaptations for nightly-2025-05-25

* Trigger CI for leanprover/lean4#8470

* chore: bump to nightly-2025-05-26

* lake update

* deprecations

* Trigger CI for leanprover/lean4#8449

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-27

* chore: adaptations for nightly-2025-05-27

* Update lean-toolchain for testing leanprover/lean4#8504

* chore: bump to nightly-2025-05-28

* chore: adaptations for nightly-2025-05-27 (#25234)



Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>

* fix

* Update lean-toolchain for testing leanprover/lean4#8519

* fix merge

* fix merge again

* deprecations

* deprecations

* fix Archive

* comment out test

* Fix and re-enable directory dependency lint test.

* chore: bump to nightly-2025-05-29

* Use the formatting from the master branch. (Seems to have been a merge that went wrong.)

* lake update

* chore: adaptations for nightly-2025-05-28 (#25295)



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: github-actions <github-actions@github.com>

* fix

* Trigger CI for leanprover/lean4#8337

* Trigger CI for leanprover/lean4#8519

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-30

* chore: adaptations for nightly-2025-05-29 (#25306)



Co-authored-by: Kim Morrison <kim@tqft.net>
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: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>

* chore: bump to nightly-2025-05-31

* chore: bump to nightly-2025-06-01

* chore: remove simp attribute when value of argument can not be inferred by simp

* fix Archive

* chore: adaptations for nightly-2025-06-01 (#25355)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

* chore: bump to nightly-2025-06-02

* chore: adaptations for nightly-2025-06-02 (#25360)



Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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

* cleanup lakefile

---------

Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
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: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.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: Joachim Breitner <mail@joachim-breitner.de>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kmill @Rob23oba @digama0