Skip to content

[Merged by Bors] - chore(Order/Hom/WithTopBot): use to_dual#37274

Closed
JovanGerb wants to merge 2 commits intoleanprover-community:masterfrom
JovanGerb:Jovan-to_dual-WithTop-Hom
Closed

[Merged by Bors] - chore(Order/Hom/WithTopBot): use to_dual#37274
JovanGerb wants to merge 2 commits intoleanprover-community:masterfrom
JovanGerb:Jovan-to_dual-WithTop-Hom

Conversation

@JovanGerb
Copy link
Copy Markdown
Contributor

@JovanGerb JovanGerb commented Mar 27, 2026

Use to_dual on WithBot/WithTop morphism definitions. This removes one backward.isDefEq.respectTransparency option.

Intentionally remove simps! from LatticeHom.withTopWithBot and LatticeHom.withTop', instead putting simp on the equivalent manual lemma`.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 27, 2026 •
edited
Loading

PR summary f92dcbb69b

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

- _root_.Function.Embedding.coeWithBot
- coeOrderHom
- coe_toDualTopEquiv_eq
- coe_withBot
- subtypeOrderIso
- subtypeOrderIso_apply_coe
- subtypeOrderIso_symm_apply
- toDualTopEquiv
- toDualTopEquiv_bot
- toDualTopEquiv_coe
- toDualTopEquiv_symm_bot
- toDualTopEquiv_symm_coe
- withBot
- withBot'
- withBotCongr
- withBot_apply
- withTop
- withTop'
- withTop_comp
- withTop_id
-- withBot_comp
-- withBot_id
-- withTopMap

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

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

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

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)
Current number Change Type
452 -1 porting notes
7435 -1 backward.isDefEq

Current commit 6783a2eb26
Reference commit f92dcbb69b

You can run this locally as

./scripts/reporting/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 Mar 27, 2026
@Komyyy Komyyy self-assigned this Apr 5, 2026
Komyyy
Komyyy approved these changes Apr 5, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@Komyyy Komyyy left a comment

Choose a reason for hiding this comment

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

Thank you for your contribution!

I carefully confirmed that all declarations are dualized correctly.

maintainer merge

For maintainers: What I confirmed
  1. All declarations are dualized correctly.
  2. Definitions related to LatticeHom could not be directly dualized easily as to_dual cannot handle extended structure constructor LatticeHom.mk.
  3. withTopCongr could not be directly dualized easily as e.toEquiv uses RelIso.toEquiv and the order relations of RelIso are flipped. We can use EquivLike.toEquiv instead, but this is not robust because of type class ambiguity: EquivLike (α ≃o β) α β and EquivLike ((· ≤ ·) ≃r (· ≤ ·)) α β.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 5, 2026

🚀 Pull request has been placed on the maintainer queue by Komyyy.

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 5, 2026
@Komyyy Komyyy assigned bryangingechen and unassigned bryangingechen and Komyyy Apr 5, 2026
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Apr 5, 2026

!radar

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 5, 2026 •
edited
Loading

Benchmark results for 6783a2e against f92dcbb are in. There are no significant changes. @riccardobrasca

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

  • Bench repo commit hashes for run main differ between commits.
  • 🟥 build//instructions: +8.2G (+0.00%)

Small changes (1✅, 1🟥)

  • ✅ build/module/Mathlib.LinearAlgebra.Alternating.Curry//instructions: -250.6M (-3.05%)
  • 🟥 build/module/Mathlib.Order.Hom.WithTopBot//instructions: +647.1M (+4.28%)

@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Apr 5, 2026

Thanks!

bors merge

@mathlib-triage mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 5, 2026
mathlib-bors bot pushed a commit that referenced this pull request Apr 5, 2026
@JovanGerb
chore(Order/Hom/WithTopBot): use to_dual (#37274)
c8b8884 
Use `to_dual` on `WithBot`/`WithTop` morphism definitions. This removes one `backward.isDefEq.respectTransparency` option.

Intentionally remove `simps!` from `LatticeHom.withTopWithBot` and `LatticeHom.withTop'`, instead putting `simp` on the equivalent manual lemma`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 5, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Order/Hom/WithTopBot): use to_dual [Merged by Bors] - chore(Order/Hom/WithTopBot): use to_dual Apr 5, 2026
@mathlib-bors mathlib-bors bot closed this Apr 5, 2026
riccardobrasca pushed a commit to riccardobrasca/mathlib4 that referenced this pull request Apr 6, 2026
@JovanGerb @riccardobrasca
chore(Order/Hom/WithTopBot): use to_dual (leanprover-community#37274)
569f1ef 
Use `to_dual` on `WithBot`/`WithTop` morphism definitions. This removes one `backward.isDefEq.respectTransparency` option.

Intentionally remove `simps!` from `LatticeHom.withTopWithBot` and `LatticeHom.withTop'`, instead putting `simp` on the equivalent manual lemma`.
YellPika pushed a commit to YellPika/mathlib4 that referenced this pull request Apr 6, 2026
@JovanGerb @YellPika
chore(Order/Hom/WithTopBot): use to_dual (leanprover-community#37274)
0702389 
Use `to_dual` on `WithBot`/`WithTop` morphism definitions. This removes one `backward.isDefEq.respectTransparency` option.

Intentionally remove `simps!` from `LatticeHom.withTopWithBot` and `LatticeHom.withTop'`, instead putting `simp` on the equivalent manual lemma`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Komyyy Komyyy Komyyy approved these changes

Assignees

@bryangingechen bryangingechen

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.

5 participants

@JovanGerb @riccardobrasca @leanprover-radar @Komyyy @bryangingechen