chore: fixes for leanprover/lean4#2783 #8023

kim-em · 2023-10-30T01:42:01Z

These are the adaptations required by leanprover/lean4#2783

Note that this PR is pointing at nightly-testing-2023-11-06, and cannot actually be merged. I will merge it into nightly-testing when it is needed.

A delegation or approving review would be helpful, so I know it is ready for the next Lean version bump!

…sting-2783

kim-em · 2023-10-30T01:44:07Z

I have not finished making everything work, because the changes seem pretty sad to me.

@eric-wieser, is this what you were expecting from leanprover/lean4#2042?

eric-wieser · 2023-10-30T09:20:20Z

After a quick skim, I think having a nicer way to unfold Function.comp would help here. We didn't need that in lean 3 because it was reducible.

One option would be to restore the "colon position determines unfolding" behavior we had in lean 3 (rather than I believe is the new "look for lambdas" heuristic), then define comp f g x with x after the colon.

Another would just be to add comp_def if it doesn't already exist, and use that throughout mathlib.

kim-em · 2023-10-30T13:58:08Z

Leo has also suggested that we could implement a simp [!f] syntax, that unfolds partial applications of f.

I'm hesitant to go that path, as many things interact with the simp syntax and surely there would be some annoying fallout with other tactics trying to reuse the simp syntax.

If we don't mind the additional complexity it is a concise solution at the point of use.

comp_def is probably also fine. I guess tomorrow I will continue fixing up this PR.

eric-wieser · 2023-10-30T16:10:28Z

My guess would be that in almost all cases in mathlib, it's the case that if we are relying on simp unfolding f and it's not doing so, this is because we always want f to unfold in this way, not because we want it to do so at this particular call site. So I think our options are:

Add new lemmas for these cases (or use existing ones)
Register custom equation lemmas for these cases uses @[eqns]
Have a way to indicate what unfolding is desired in the definition; perhaps if the :-detection is considered ugly, it could be something like an fun x => unfold_unapplied (fun y => ...) syntax, where unfold_unapplied is metadata like no_index, and tells simp that lambdas inside it do not need to be applied in order to allow unfolding.

kim-em · 2023-11-01T03:41:02Z

@eric-wieser I think my preference would be to go with option 1 or 2 on your list, with the alternative of revisiting option 3 (but via a new RFC / PR, rather than changing leanprover/lean4#2783).

That would mean:

finish adding the workarounds as in the PR
merge fix: issue 2042 leanprover/lean4#2783
at leisure, Mathlib adds the additional simp or eqns annotations and cleans up the workarounds?

…ean4#2783

This reverts commit 34670747bdc0a5b4f5bcd8ea40f3279431faf9ca.

eric-wieser · 2023-11-12T11:41:57Z

scripts/count-transitive-imports.lean

Is this supposed to be here?

This will mostly be a no-op in the current version of Lean, but will override the new behavior from leanprover/lean4#2783. Once consequence of this is that `rw [comp]` no longer uses "smart unfolding"; it introduces a non-beta reduced term if the composition was applied. As a result, these places need to use `rw [comp_apply]` instead. My claim is that this is no big deal. This is split from the lean bump PR #8023, targeting master, to make clear what the fallout is.

# PR contents This is the supremum of - #8284 - #8056 - #8023 - #8332 - #8226 (already approved) - #7834 (already approved) along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it. Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380. I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime. # Lean PRs involved in this bump In particular this includes adjustments for the Lean PRs * leanprover/lean4#2778 * leanprover/lean4#2790 * leanprover/lean4#2783 * leanprover/lean4#2825 * leanprover/lean4#2722 ## leanprover/lean4#2778 We can get rid of all the ``` local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 ``` macros across Mathlib (and in any projects that want to write natural number powers of reals). ## leanprover/lean4#2722 Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. ## leanprover/lean4#2783 This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes: * switching to using explicit lemmas that have the intended level of application * `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour * Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`. This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes! Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Mauricio Collares <[email protected]>

This will mostly be a no-op in the current version of Lean, but will override the new behavior from leanprover/lean4#2783. Once consequence of this is that `rw [comp]` no longer uses "smart unfolding"; it introduces a non-beta reduced term if the composition was applied. As a result, these places need to use `rw [comp_apply]` instead. My claim is that this is no big deal. This is split from the lean bump PR #8023, targeting master, to make clear what the fallout is.

# PR contents This is the supremum of - #8284 - #8056 - #8023 - #8332 - #8226 (already approved) - #7834 (already approved) along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it. Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380. I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime. # Lean PRs involved in this bump In particular this includes adjustments for the Lean PRs * leanprover/lean4#2778 * leanprover/lean4#2790 * leanprover/lean4#2783 * leanprover/lean4#2825 * leanprover/lean4#2722 ## leanprover/lean4#2778 We can get rid of all the ``` local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 ``` macros across Mathlib (and in any projects that want to write natural number powers of reals). ## leanprover/lean4#2722 Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. ## leanprover/lean4#2783 This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes: * switching to using explicit lemmas that have the intended level of application * `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour * Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`. This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes! Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Mauricio Collares <[email protected]>

This will mostly be a no-op in the current version of Lean, but will override the new behavior from leanprover/lean4#2783. Once consequence of this is that `rw [comp]` no longer uses "smart unfolding"; it introduces a non-beta reduced term if the composition was applied. As a result, these places need to use `rw [comp_apply]` instead. My claim is that this is no big deal. This is split from the lean bump PR #8023, targeting master, to make clear what the fallout is.

This is the supremum of - #8284 - #8056 - #8023 - #8332 - #8226 (already approved) - #7834 (already approved) along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it. Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380. I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime. In particular this includes adjustments for the Lean PRs * leanprover/lean4#2778 * leanprover/lean4#2790 * leanprover/lean4#2783 * leanprover/lean4#2825 * leanprover/lean4#2722 We can get rid of all the ``` local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 ``` macros across Mathlib (and in any projects that want to write natural number powers of reals). Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes: * switching to using explicit lemmas that have the intended level of application * `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour * Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`. This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes! Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Mauricio Collares <[email protected]>

This will mostly be a no-op in the current version of Lean, but will override the new behavior from leanprover/lean4#2783. Once consequence of this is that `rw [comp]` no longer uses "smart unfolding"; it introduces a non-beta reduced term if the composition was applied. As a result, these places need to use `rw [comp_apply]` instead. My claim is that this is no big deal. This is split from the lean bump PR #8023, targeting master, to make clear what the fallout is.

# PR contents This is the supremum of - #8284 - #8056 - #8023 - #8332 - #8226 (already approved) - #7834 (already approved) along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it. Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380. I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime. # Lean PRs involved in this bump In particular this includes adjustments for the Lean PRs * leanprover/lean4#2778 * leanprover/lean4#2790 * leanprover/lean4#2783 * leanprover/lean4#2825 * leanprover/lean4#2722 ## leanprover/lean4#2778 We can get rid of all the ``` local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 ``` macros across Mathlib (and in any projects that want to write natural number powers of reals). ## leanprover/lean4#2722 Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. ## leanprover/lean4#2783 This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes: * switching to using explicit lemmas that have the intended level of application * `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour * Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`. This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes! Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Mauricio Collares <[email protected]>

leanprover-community-mathlib4-bot and others added 3 commits October 29, 2023 18:39

Update lean-toolchain for testing leanprover/lean4#2783

2c40980

Merge remote-tracking branch 'origin/nightly-testing' into lean-pr-te…

59553b4

…sting-2783

many fixes

21aebb9

kim-em added awaiting-review awaiting-CI labels Oct 30, 2023

kim-em requested a review from eric-wieser October 30, 2023 01:42

kim-em changed the base branch from master to nightly-testing October 30, 2023 01:43

kim-em mentioned this pull request Oct 30, 2023

fix: issue 2042 leanprover/lean4#2783

Merged

Trigger CI for leanprover/lean4#2783

e24201f

github-actions bot removed the awaiting-CI label Oct 30, 2023

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 30, 2023

kim-em changed the base branch from nightly-testing to bump/v4.4.0 November 1, 2023 03:38

kim-em added the v4.4.0 label Nov 1, 2023

merge bump/v4.4.0

ce91563

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 1, 2023

?

b1bb29d

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 3, 2023

fgdorais and others added 7 commits November 4, 2023 21:01

fix: patch for std4#195

b821f80

fix: patch for std4#194 (more order lemmas for Nat)

ec68bfa

fix imports

b014d9b

revert use of ← Nat.one_add

f463547

two more

b0dfc61

Merge branch 'fgdorais-nat-succ-pred' into fgdorais-nat-order

ac3cc4f

merge nightly-testing-2023-11-04; trigger Mathlib CI for leanprover/l…

aaa40f0

…ean4#2783

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 5, 2023

cleanup?

dcccc2b

kim-em changed the title ~~chore: partial fixes for leanprover/lean4#2783~~ chore: fixes for leanprover/lean4#2783 Nov 9, 2023

kim-em added 2 commits November 9, 2023 15:27

long line

2a05f0a

fix

acdd208

kim-em added the blocked-by-core-release Not relevant for the current Lean release candidate, but will be needed for the next. label Nov 9, 2023

fix test

12d1cc4

kim-em added the merged-into-nightly-testing label Nov 10, 2023

kim-em mentioned this pull request Nov 12, 2023

[Merged by Bors] - chore: bump to v4.3.0-rc2 #8366

Closed

eric-wieser mentioned this pull request Nov 12, 2023

refactor: replace (· ∘ ·) with Function.comp_def #8367

Closed

Revert "cherry-pick all the comp_defs"

d6c5536

This reverts commit 34670747bdc0a5b4f5bcd8ea40f3279431faf9ca.

eric-wieser reviewed Nov 12, 2023

View reviewed changes

eric-wieser force-pushed the lean-pr-testing-2783 branch from 84e1578 to 1f2d1e7 Compare November 12, 2023 15:23

eric-wieser added 5 commits November 12, 2023 15:25

use eqns for flip and comp

cd4033c

eqns doesn't work for dsimp

ec44d9e

other fixes

54ab98c

golf a little

66b1e23

removed unrelated script

34b6622

eric-wieser force-pushed the lean-pr-testing-2783 branch from 1f2d1e7 to 34b6622 Compare November 12, 2023 15:32

fix in the archive

6c39953

eric-wieser mentioned this pull request Nov 12, 2023

[Merged by Bors] - refactor: add explicit equation lemmas for comp and flip #8371

Closed

kim-em closed this Nov 19, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: fixes for leanprover/lean4#2783 #8023

chore: fixes for leanprover/lean4#2783 #8023

kim-em commented Oct 30, 2023 •

edited

Loading

kim-em commented Oct 30, 2023

eric-wieser commented Oct 30, 2023

kim-em commented Oct 30, 2023

eric-wieser commented Oct 30, 2023 •

edited

Loading

kim-em commented Nov 1, 2023

eric-wieser Nov 12, 2023

eric-wieser Nov 12, 2023

chore: fixes for leanprover/lean4#2783 #8023

chore: fixes for leanprover/lean4#2783 #8023

Conversation

kim-em commented Oct 30, 2023 • edited Loading

kim-em commented Oct 30, 2023

eric-wieser commented Oct 30, 2023

kim-em commented Oct 30, 2023

eric-wieser commented Oct 30, 2023 • edited Loading

kim-em commented Nov 1, 2023

eric-wieser Nov 12, 2023

Choose a reason for hiding this comment

eric-wieser Nov 12, 2023

Choose a reason for hiding this comment

kim-em commented Oct 30, 2023 •

edited

Loading

eric-wieser commented Oct 30, 2023 •

edited

Loading