Skip to content

chore(Order/UpperLower/Basic): use to_dual #34640

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
vihdzp wants to merge 4 commits into
base: master
Choose a base branch
from
Open

chore(Order/UpperLower/Basic): use to_dual #34640

vihdzp wants to merge 4 commits into from
+27 −78

Conversation

@vihdzp
Copy link
Collaborator

@vihdzp vihdzp commented Jan 31, 2026 •
edited
Loading

@vihdzp vihdzp added the t-order Order theory label Jan 31, 2026
@vihdzp vihdzp requested a review from JovanGerb January 31, 2026 10:12
@github-actions
Copy link

github-actions bot commented Jan 31, 2026 •
edited
Loading

PR summary b8dad038b1

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

- IsLowerSet.Iic_subset
- IsLowerSet.Iio_subset
- IsLowerSet.eq_empty_or_Iic
- IsLowerSet.lowerBounds_subset
- IsLowerSet.not_bddBelow
- IsUpperSet.eq_univ_or_Ioi
- OrderEmbedding.image_Iic
- OrderEmbedding.image_Iio
- compl_Ici
- compl_Ioi
- isLowerSet_Iic
- isLowerSet_Iio
- isLowerSet_iff_Iic_subset
- isLowerSet_iff_Iio_subset
- notMem_Iic
- notMem_Iio
- not_bddBelow_Iic
- not_bddBelow_Iio
- preimage_Iic
- preimage_Iio

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).

@JovanGerb
Copy link
Contributor

JovanGerb commented Feb 3, 2026

This overlaps with #33964, no?

@vihdzp
Copy link
Collaborator Author

vihdzp commented Feb 3, 2026

There's some overlap, yes. I'll make it a dependent PR.

@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 3, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 10, 2026
@mathlib-dependent-issues
Copy link

mathlib-dependent-issues bot commented Feb 10, 2026

This PR/issue depends on:

JovanGerb
JovanGerb reviewed Feb 11, 2026
View reviewed changes
Mathlib/Order/Interval/Set/LinearOrder.lean

@[simp]
@[to_dual (attr := simp)]
theorem compl_Iic : (Iic a)ᶜ = Ioi a :=
Copy link
Contributor

@JovanGerb JovanGerb Feb 11, 2026

Choose a reason for hiding this comment

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

I have this other PR #33543 where I teach to_dual that compl should be translated to hnot. I guess that that is a bad idea...

Copy link
Collaborator Author

@vihdzp vihdzp Feb 11, 2026

Choose a reason for hiding this comment

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

We already avoid translating the order on sets, don't we? So I don't think this should cause any conflict.

Copy link
Contributor

@JovanGerb JovanGerb Feb 11, 2026

Choose a reason for hiding this comment

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

Yes, but I mean that the name translation will get messed up.

Copy link
Collaborator

@Komyyy Komyyy Feb 11, 2026

Choose a reason for hiding this comment

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

Ideally, compl should be translated to hnot only when the type is not a boolean algebra.
However, we need to implement a new feature for the to_dual attribute to do this...

Copy link
Collaborator

@Komyyy Komyyy Feb 11, 2026

Choose a reason for hiding this comment

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

Rather than doing that, I think it would be better to stop using compl in the definition of Heyting algebras and make compl a notation exclusively for Boolean algebras.

JovanGerb
JovanGerb approved these changes Feb 12, 2026
View reviewed changes
Mathlib/Order/UpperLower/Basic.lean
theorem IsUpperSet.ordConnected (h : IsUpperSet s) : s.OrdConnected :=
⟨fun _ ha _ _ => Icc_subset_Ici_self.trans <| h.Ici_subset ha⟩

@[to_dual existing]
Copy link
Contributor

@JovanGerb JovanGerb Feb 12, 2026

Choose a reason for hiding this comment

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

Can you add a comment here saying that to_dual cannot yet reorder arguments of arguments? That way it'll be easier to clean up later

Mathlib/Order/WellFounded.lean
Comment on lines +142 to 143
@[to_dual none]
theorem WellFounded.min_le (h : WellFounded ((· < ·) : β → β → Prop))
Copy link
Contributor

@JovanGerb JovanGerb Feb 12, 2026

Choose a reason for hiding this comment

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

Why is this in this PR? And shouldn't we just change it to h : WellFoundedLT β?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@JovanGerb JovanGerb JovanGerb approved these changes

+1 more reviewer

@Komyyy Komyyy Komyyy left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@vihdzp @JovanGerb @Komyyy