Skip to content

chore: adjust BEq classes#7855

Merged
TwoFX merged 30 commits intoleanprover:masterfrom
Rob23oba:beq-class-adjustments
Apr 16, 2025
Merged

chore: adjust BEq classes#7855
TwoFX merged 30 commits intoleanprover:masterfrom
Rob23oba:beq-class-adjustments

Conversation

@Rob23oba
Copy link
Contributor

@Rob23oba Rob23oba commented Apr 7, 2025 •
edited
Loading

This PR moves ReflBEq to Init.Core and changes LawfulBEq to extend ReflBEq.

BREAKING CHANGES:

  • The refl field of ReflBEq has been renamed to rfl to match LawfulBEq
  • LawfulBEq extends ReflBEq, so in particular LawfulBEq.rfl is no longer valid

@Rob23oba Rob23oba requested a review from kim-em as a code owner April 7, 2025 10:02
@Rob23oba Rob23oba requested review from TwoFX and digama0 as code owners April 7, 2025 10:30
TwoFX
TwoFX reviewed Apr 7, 2025
View reviewed changes
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How about you provide a lemma LawfulBEq.rfl with a deprecation pointing to BEq.rfl?

@TwoFX TwoFX added the changelog-library Library label Apr 7, 2025
@TwoFX TwoFX self-assigned this Apr 7, 2025
@Rob23oba
Copy link
Contributor Author

Rob23oba commented Apr 7, 2025 •
edited
Loading

I can't add LawfulBEq.rfl, it will complain that structure 'LawfulBEq' has field 'rfl'.

@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 Apr 7, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 7, 2025
Update lean-toolchain for testing leanprover/lean4#7855
79ea517
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 7, 2025
Update lean-toolchain for testing leanprover/lean4#7855
36d0aac
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 7, 2025
@ghost
Copy link

ghost commented Apr 7, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 7, 2025
Trigger CI for leanprover/lean4#7855
b13dc2b
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 7, 2025
Trigger CI for leanprover/lean4#7855
aadee85
@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Apr 9, 2025
@TwoFX TwoFX added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Apr 10, 2025
@Rob23oba
Copy link
Contributor Author

Rob23oba commented Apr 10, 2025

Okay, there were too many instances where I would've needed to add have : DecidableEq α := instDecidableEqOfLawfulBEq in the proof -- for now I'll revert most of the changes to decidability. For future reference though, a1f5e67 is the commit with all fixes with the new membership decidability instance.

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2025
Trigger CI for leanprover/lean4#7855
a7cb6a0
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 10, 2025
Trigger CI for leanprover/lean4#7855
76a0f9f
@TwoFX TwoFX mentioned this pull request Apr 14, 2025
Merged
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 16, 2025
Trigger CI for leanprover/lean4#7855
0e26dcd
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 16, 2025
Trigger CI for leanprover/lean4#7855
c959984
@Rob23oba
Copy link
Contributor Author

Rob23oba commented Apr 16, 2025

I have found a workaround regarding LawfulBEq.rfl:

@[deprecated BEq.rfl (since := "2025-04-16")]
abbrev LawfulBEq.LawfulBEq.rfl := @BEq.rfl
export LawfulBEq (LawfulBEq.rfl)

It's not pretty but works, should we do something like this?

@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 Apr 16, 2025
@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Apr 16, 2025
TwoFX
TwoFX approved these changes Apr 16, 2025
View reviewed changes
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nicely done, thanks!

@TwoFX
Copy link
Member

TwoFX commented Apr 16, 2025 •
edited
Loading

It's not pretty but works, should we do something like this?

That's a fun workaround. I think in this case it's fine to just skip the deprecation. Proper support for deprecating structure fields is on the radar.

@TwoFX TwoFX added this pull request to the merge queue Apr 16, 2025
Merged via the queue into leanprover:master with commit 7cca594 Apr 16, 2025
22 checks passed
@Rob23oba Rob23oba mentioned this pull request Aug 19, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX approved these changes

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

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

@hargoniX hargoniX Awaiting requested review from hargoniX

Assignees

@TwoFX TwoFX

Labels

awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library 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.

2 participants

@Rob23oba @TwoFX