Skip to content

[Merged by Bors] - chore(Order/WithBot): golf, clean up#21274

Closed
YaelDillies wants to merge 5 commits intomasterfrom
golf_with_bot_top
Closed

[Merged by Bors] - chore(Order/WithBot): golf, clean up#21274
YaelDillies wants to merge 5 commits intomasterfrom
golf_with_bot_top

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Jan 30, 2025

  • Shorten proofs
  • Make the WithBot and WithTop sections analogous
  • Avoid relying on the defeq (WithTop α)ᵒᵈ = WithBot αᵒᵈ
  • Pull more implicit variables to variable statements
  • Stick to the convention that a b : α and x y : WithBot α

Open in Gitpod

@YaelDillies
chore(Order/WithBot): golf, clean up
48acaea 
* Shorten proofs
* Make the `WithBot` and `WithTop` sections analogous
* Avoid relying on the defeq `(WithTop α)ᵒᵈ = WithBot αᵒᵈ`
* Pull more implicit variables to `variable` statements
* Stick to the convention that `a b : α` and `x y : WithBot α`
@YaelDillies YaelDillies mentioned this pull request Jan 30, 2025
Closed
4 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 30, 2025 •
edited
Loading

PR summary 2630c8e335

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ WithBot.le_ofDual_iff
+ WithBot.le_toDual_iff
+ WithBot.lt_ofDual_iff
+ WithBot.lt_toDual_iff
+ WithBot.ofDual_le_iff
+ WithBot.ofDual_le_ofDual_iff
+ WithBot.ofDual_lt_iff
+ WithBot.ofDual_lt_ofDual_iff
+ WithBot.toDual_le_iff
+ WithBot.toDual_le_toDual_iff
+ WithBot.toDual_lt_iff
+ WithBot.toDual_lt_toDual_iff
+ WithTop.le_ofDual_iff
+ WithTop.le_toDual_iff
+ WithTop.lt_ofDual_iff
+ WithTop.lt_toDual_iff
+ WithTop.ofDual_le_iff
+ WithTop.ofDual_le_ofDual_iff
+ WithTop.ofDual_lt_iff
+ WithTop.ofDual_lt_ofDual_iff
+ WithTop.toDual_le_iff
+ WithTop.toDual_le_toDual_iff
+ WithTop.toDual_lt_iff
+ WithTop.toDual_lt_toDual_iff
++ le_def
++ lt_def
++-- coe_le_coe
++-- coe_le_iff
++-- coe_lt_coe
++-- coe_max
++-- coe_min
++-- ge_of_forall_gt_iff_ge
++-- le_coe_iff
++-- le_of_forall_lt_iff_le
++-- lt_iff_exists_coe
+-+- linearOrder
+-+- orderBot
+-+- orderTop
-+-+ distribLattice
-+-+ isTotal_le
-+-+ semilatticeInf
-- le_ofDual_iff
-- le_toDual_iff
-- lt_ofDual_iff
-- lt_toDual_iff
-- ofDual_le_iff
-- ofDual_le_ofDual_iff
-- ofDual_lt_iff
-- ofDual_lt_ofDual_iff
-- toDual_le_iff
-- toDual_le_toDual_iff
-- toDual_lt_iff
-- toDual_lt_toDual_iff

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-order Order theory label Jan 30, 2025
vihdzp
vihdzp reviewed Feb 5, 2025
View reviewed changes
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp left a comment •
edited
Loading

Choose a reason for hiding this comment

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

If only we had a to_order_dual tactic to generate all the WithTop proofs automatically...

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Feb 5, 2025

Violeta, the context is that I am removing the defeq in #19668, so I am happy to revert changes here and there, but they will likely be done eventually.

bryangingechen
bryangingechen approved these changes Feb 12, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

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

Thanks!
bors r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Feb 12, 2025
@bryangingechen bryangingechen mentioned this pull request Feb 12, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Feb 12, 2025
@YaelDillies
chore(Order/WithBot): golf, clean up (#21274)
f5fe987 
* Shorten proofs
* Make the `WithBot` and `WithTop` sections analogous
* Avoid relying on the defeq `(WithTop α)ᵒᵈ = WithBot αᵒᵈ`
* Pull more implicit variables to `variable` statements
* Stick to the convention that `a b : α` and `x y : WithBot α`
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 12, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Order/WithBot): golf, clean up [Merged by Bors] - chore(Order/WithBot): golf, clean up Feb 12, 2025
@mathlib-bors mathlib-bors bot closed this Feb 12, 2025
@mathlib-bors mathlib-bors bot deleted the golf_with_bot_top branch February 12, 2025 12:37
joneugster pushed a commit that referenced this pull request Feb 12, 2025
@YaelDillies @joneugster
chore(Order/WithBot): golf, clean up (#21274)
e1969b5 
* Shorten proofs
* Make the `WithBot` and `WithTop` sections analogous
* Avoid relying on the defeq `(WithTop α)ᵒᵈ = WithBot αᵒᵈ`
* Pull more implicit variables to `variable` statements
* Stick to the convention that `a b : α` and `x y : WithBot α`
YaelDillies added a commit that referenced this pull request Feb 20, 2025
@YaelDillies
chore(Algebra/Order/Monoid/Unbundled/WithTop): golf, clean up
8ec30e1 
* Shorten proofs
* Make the `WithBot` and `WithTop` sections analogous
* Avoid relying on the defeq `(WithTop α)ᵒᵈ = WithBot αᵒᵈ`
* Pull more implicit variables to `variable` statements
* Stick to the convention that `a b : α` and `x y : WithBot α`

This is a follow-up to #21274.
@YaelDillies YaelDillies mentioned this pull request Feb 20, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Feb 21, 2025
@YaelDillies
chore(Algebra/Order/Monoid/Unbundled/WithTop): golf, clean up (#22109)
3faeb59 
* Shorten proofs
* Make the `WithBot` and `WithTop` sections analogous
* Avoid relying on the defeq `(WithTop α)ᵒᵈ = WithBot αᵒᵈ`
* Pull more implicit variables to `variable` statements
* Stick to the convention that `a b : α` and `x y : WithBot α`

This is a follow-up to #21274.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@bryangingechen bryangingechen bryangingechen approved these changes

+1 more reviewer

@vihdzp vihdzp vihdzp left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@YaelDillies @bryangingechen @vihdzp