Skip to content
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

feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem #14411

Open
wants to merge 17 commits into
base: master
Choose a base branch
from
Open

feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem #14411

wants to merge 17 commits into from
+410 −0

Conversation

haitian-yuki
Copy link
Collaborator

@haitian-yuki haitian-yuki commented Jul 4, 2024 •
edited by YaelDillies
Loading

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 4, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Jul 4, 2024 •
edited
Loading

PR summary 61d70ce689

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Data.Multiset.DershowitzManna 574

Declarations diff

+ AccM
+ MultisetDMLT
+ MultisetRedLT
+ MultisetTransLT
+ acc_cons
+ acc_cons_of_acc
+ acc_cons_of_acc_of_lt
+ acc_of_acc_lt
+ dmLT_of_redLT
+ dmLT_wf
+ dmlt_trans
+ not_redLT_zero
+ redLT_wf
+ red_insert
+ transLT_eq_dmLT
+ transLT_of_dmLT
+ transLT_wf

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.

@riccardobrasca
Copy link
Member

Can you please mark this PR WIP or awaiting-review? Thanks!

@riccardobrasca riccardobrasca added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 4, 2024
Rida-Hamadani
Rida-Hamadani reviewed Jul 5, 2024
View reviewed changes
Copy link
Collaborator

@Rida-Hamadani Rida-Hamadani 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! Some comments are general and need to be applied in other places in PR (instead of just committing the suggested portions).

Mathlib/Data/Multiset/Order.lean Outdated Show resolved Hide resolved
Mathlib/Data/Multiset/Order.lean Outdated Show resolved Hide resolved
Mathlib/Data/Multiset/Order.lean Outdated Show resolved Hide resolved
Mathlib/Data/Multiset/Order.lean Outdated Show resolved Hide resolved
Mathlib/Data/Multiset/Order.lean Outdated Show resolved Hide resolved
Mathlib/Data/Multiset/Order.lean Outdated Show resolved Hide resolved
Mathlib/Data/Multiset/Order.lean Outdated Show resolved Hide resolved
Mathlib/Data/Multiset/Order.lean Outdated Show resolved Hide resolved
Mathlib/Data/Multiset/Order.lean Outdated Show resolved Hide resolved
Mathlib/Data/Multiset/Order.lean Outdated Show resolved Hide resolved
@haitian-yuki haitian-yuki removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 10, 2024
@kim-em
Copy link
Contributor

kim-em commented Jul 17, 2024

Obviously my review is far from complete, but I'm not an expert here so hopefully someone else will come along, but these will give you something to start with.

@kim-em kim-em added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 18, 2024
@grunweg grunweg added the t-data Data (lists, quotients, numbers, etc) label Aug 15, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Aug 26, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Sep 19, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@m4lvin m4lvin mentioned this pull request Oct 16, 2024
Closed
@haitian-yuki haitian-yuki removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 18, 2024
goens
goens reviewed Oct 29, 2024
View reviewed changes
Copy link
Collaborator

@goens goens left a comment

Choose a reason for hiding this comment

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

It looks like some proofs can be golfed a little bit more, and I'm not sure about the namings/namespaces (might be worth reading the naming conventions for that), that's the best feedback I can give so far (before a maintainer looks at it)

Mathlib/Data/Multiset/DershowitzManna.lean

/-- The standard Dershowitz–Manna ordering: -/
inductive MultisetDMLT [DecidableEq α] [Preorder α] (M N : Multiset α) : Prop :=
| DMLT : ∀ (X Y Z : Multiset α),
Copy link
Collaborator

Choose a reason for hiding this comment

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

not clear why this needs to be an inductive (with one constructor), couldn't it just be a def?

Mathlib/Data/Multiset/DershowitzManna.lean
/-- MultisetRedLT is a special case of MultisetDMLT. The transitive closure of it is used to define
an equivalent (proved later) version of the ordering. -/
inductive MultisetRedLT [DecidableEq α] [LT α] (M N : Multiset α) : Prop :=
| RedLT : ∀ (X Y : Multiset α) (a : α) ,
Copy link
Collaborator

Choose a reason for hiding this comment

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

Also here, why is this a one-constructor inductive without self reference? Seems to complicate things, no?

Mathlib/Data/Multiset/DershowitzManna.lean

/-- MultisetTransLT is the transitive closure of MultisetRedLT and is equivalent to MultisetDMLT
(proved later). -/
def MultisetTransLT [DecidableEq α] [LT α] : Multiset α → Multiset α → Prop :=
Copy link
Collaborator

Choose a reason for hiding this comment

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

I'm not 100% sure exactly what the Mathlib convention is, but shouldn't the Multiset be a namespace instead of part of the name in CammelCase? i.e. Multiset.transLT and Multiset.DMLT above, etc?

Mathlib/Data/Multiset/DershowitzManna.lean
simp [Multiset.ext, Multiset.count_cons] at h0
by_cases h : b = a
· have := h0 b
aesop
Copy link
Collaborator

Choose a reason for hiding this comment

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

does aesop? work (not sure if you want to leave the aesop calls, in the same spirit as simp vs simp only)

Mathlib/Data/Multiset/DershowitzManna.lean Show resolved Hide resolved
Mathlib/Data/Multiset/DershowitzManna.lean
aesop
· have := h0 b
simp [Multiset.sub_singleton]
aesop
Copy link
Collaborator

Choose a reason for hiding this comment

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

another instance of an aesop call that may be replaced with the result of aesop? (I think)

Mathlib/Data/Multiset/DershowitzManna.lean
Comment on lines +155 to +157
· constructor
simpa
· simpa
Copy link
Collaborator

Choose a reason for hiding this comment

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

can these be replaced with something like constructor <;> simpa? (don't have an enviroment to test this right now)

Mathlib/Data/Multiset/DershowitzManna.lean Show resolved Hide resolved
Mathlib/Data/Multiset/DershowitzManna.lean
exact this
exact y_in
let _ := h y_in_Y1
aesop
Copy link
Collaborator

Choose a reason for hiding this comment

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

aesop?

@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 30, 2024
@YaelDillies YaelDillies self-assigned this Oct 30, 2024
YaelDillies
YaelDillies reviewed Oct 30, 2024
View reviewed changes
Mathlib/Data/Multiset/DershowitzManna.lean
Comment on lines +19 to +21
- `MultisetDMLT` : the standard definition fo the `Dershowitz-Manna ordering`.
- `dm_wf` : the main theorem about the `Dershowitz-Manna ordering` being well-founded.
- `TransLT_eq_DMLT` : two definitions of the `Dershowitz-Manna ordering` are equivalent.
Copy link
Collaborator

Choose a reason for hiding this comment

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

The alignment looks off 😅

Mathlib/Data/Multiset/DershowitzManna.lean Show resolved Hide resolved
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

@goens goens goens left review comments

@m4lvin m4lvin m4lvin left review comments

@YaelDillies YaelDillies YaelDillies left review comments

@Rida-Hamadani Rida-Hamadani Rida-Hamadani left review comments

Assignees

@YaelDillies YaelDillies

Labels
awaiting-author A reviewer has asked the author a question or requested changes new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-data Data (lists, quotients, numbers, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
10 participants
@haitian-yuki @riccardobrasca @kim-em @mathlib4-dependent-issues-bot @goens @m4lvin @YaelDillies @Rida-Hamadani @grunweg @leanprover-community-mathlib4-bot