Skip to content

[Merged by Bors] - feat: port Order.Lattice#642

Closed
Ruben-VandeVelde wants to merge 38 commits intomasterfrom
order.lattice
Closed

[Merged by Bors] - feat: port Order.Lattice#642
Ruben-VandeVelde wants to merge 38 commits intomasterfrom
order.lattice

Conversation

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde commented Nov 18, 2022 •
edited
Loading

Tracking mathlib commit: fd47bdf09e90f553519c712378e651975fe8c829

@Ruben-VandeVelde Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 18, 2022
@Ruben-VandeVelde Ruben-VandeVelde added the help-wanted The author needs attention to resolve issues label Nov 18, 2022
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor Author

Ruben-VandeVelde commented Nov 18, 2022

Anyone should feel free to work on this; I'll take another look later.

kim-em
kim-em reviewed Nov 18, 2022
View reviewed changes
Ruben-VandeVelde
Ruben-VandeVelde commented Nov 19, 2022
View reviewed changes
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor Author

Ruben-VandeVelde commented Nov 19, 2022 •
edited by dwarn
Loading

To do:

  • In SemilatticeSup.ext, SemilatticeInf.ext & Lattice.ext, the cases invocations yield different goals than in lean3
  • In Lattice.mk', rw [partial_order_eq] doesn't work
  • SemilatticeSup, SemilatticeInf & DistribLattice instances for pi types rely on the unported refine_struct and pi_instance_derive_field
  • The Lattice instance for pi types has a type mismatch I don't understand, but might be because the SemilatticeSup & SemilatticeInf instances are broken

I don't know how to fix these issues, so help very much welcome

@dwarn dwarn added the mathlib-port This is a port of a theory file from mathlib. label Nov 23, 2022
kim-em
kim-em reviewed Nov 23, 2022
View reviewed changes
@kim-em kim-em added the help-wanted The author needs attention to resolve issues label Nov 23, 2022
@Ruben-VandeVelde Ruben-VandeVelde mentioned this pull request Nov 23, 2022
Closed
2 tasks
urkud
urkud reviewed Nov 24, 2022
View reviewed changes
Mathlib/Order/Basic.lean Outdated
(The lexicographic ordering is defined in `Order.Lexicographic`, and the instances are
available via the type synonym `α ×ₗ β = α × β`.) -/
instance (α : Type u) (β : Type v) [PartialOrder α] [PartialOrder β] : PartialOrder (α × β) where
instance partialOrder (α : Type u) (β : Type v) [PartialOrder α] [PartialOrder β] :
Copy link
Copy Markdown
Member

@urkud urkud Nov 24, 2022

Choose a reason for hiding this comment

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

What is the reason to force lowercase p here?

Copy link
Copy Markdown
Contributor Author

@Ruben-VandeVelde Ruben-VandeVelde Nov 24, 2022

Choose a reason for hiding this comment

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

It was my understanding that instances are named like defs with lowerCamelCase, is that wrong? Alternatively I could try to drop the explicit names

Copy link
Copy Markdown
Member

@urkud urkud Nov 24, 2022

Choose a reason for hiding this comment

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

I don't know. I started looking at mathlib 4 port less than 24h ago. So, I'm asking stupid questions. It seems strange to me to use explicit names for all instances.

Copy link
Copy Markdown
Contributor Author

@Ruben-VandeVelde Ruben-VandeVelde Nov 24, 2022

Choose a reason for hiding this comment

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

I removed the explicit names for everything except

OrderDual.semilatticeSup
OrderDual.semilatticeInf
OrderDual.distribLattice

Copy link
Copy Markdown
Contributor

@kim-em kim-em Nov 25, 2022

Choose a reason for hiding this comment

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

If you wanted to name this instance, this would be the correct name. The rule is that CamelCase names get turned into lowerCamelCase when used in definitions referring to them.

urkud
urkud reviewed Nov 24, 2022
View reviewed changes
urkud
urkud reviewed Nov 24, 2022
View reviewed changes
@Ruben-VandeVelde Ruben-VandeVelde removed the help-wanted The author needs attention to resolve issues label Nov 24, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 25, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 25, 2022
bors bot pushed a commit that referenced this pull request Nov 25, 2022
@Ruben-VandeVelde @dwarn @kim-em
feat: port Order.Lattice (#642)
4510beb 
Tracking mathlib commit: [fd47bdf09e90f553519c712378e651975fe8c829](leanprover-community/mathlib3@fd47bdf)

Co-authored-by: David Wärn <codwarn@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
@bors
Copy link
Copy Markdown

bors bot commented Nov 25, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Order.Lattice [Merged by Bors] - feat: port Order.Lattice Nov 25, 2022
@bors bors bot closed this Nov 25, 2022
@bors bors bot deleted the order.lattice branch November 25, 2022 17:55
@github-actions github-actions bot mentioned this pull request Nov 27, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 27, 2022
chore(*): add mathlib4 synchronization comments (#17736)
28295cd 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.group.semiconj`: leanprover-community/mathlib4#717
* `algebra.group_with_zero.basic`: leanprover-community/mathlib4#669
* `algebra.group_with_zero.inj_surj`: leanprover-community/mathlib4#722
* `algebra.ring.inj_surj`: leanprover-community/mathlib4#734
* `algebra.ring.units`: leanprover-community/mathlib4#746
* `data.finite.defs`: leanprover-community/mathlib4#698
* `order.lattice`: leanprover-community/mathlib4#642
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 27, 2022
chore(*): add mathlib4 synchronization comments (#17736)
c7e627f 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.group.semiconj`: leanprover-community/mathlib4#717
* `algebra.group_with_zero.basic`: leanprover-community/mathlib4#669
* `algebra.group_with_zero.inj_surj`: leanprover-community/mathlib4#722
* `algebra.ring.inj_surj`: leanprover-community/mathlib4#734
* `algebra.ring.units`: leanprover-community/mathlib4#746
* `data.finite.defs`: leanprover-community/mathlib4#698
* `order.lattice`: leanprover-community/mathlib4#642
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 28, 2022
chore(*): add mathlib4 synchronization comments (#17736)
1fc36cc 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.group.semiconj`: leanprover-community/mathlib4#717
* `algebra.group_with_zero.basic`: leanprover-community/mathlib4#669
* `algebra.group_with_zero.inj_surj`: leanprover-community/mathlib4#722
* `algebra.ring.inj_surj`: leanprover-community/mathlib4#734
* `algebra.ring.units`: leanprover-community/mathlib4#746
* `data.finite.defs`: leanprover-community/mathlib4#698
* `order.lattice`: leanprover-community/mathlib4#642
bors bot pushed a commit that referenced this pull request Nov 28, 2022
@Ruben-VandeVelde @dwarn @kim-em
feat: port Order.BoundedOrder (#697)
74deab3 
- [x] depends on: #642
- [x] depends on: leanprover-community/mathlib3#17730

Tracking mathlib commit: [e50b8c261b0a000b806ec0e1356b41945eda61f7](leanprover-community/mathlib3@e50b8c2)

Co-authored-by: David Wärn <codwarn@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
@github-actions github-actions bot mentioned this pull request Nov 29, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@urkud urkud urkud left review comments

@kim-em kim-em kim-em left review comments

@digama0 digama0 digama0 left review comments

@j-loreaux j-loreaux j-loreaux left review comments

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@Ruben-VandeVelde @kim-em @urkud @digama0 @j-loreaux @dwarn