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

[haitian-yuki]

add Dershowitz-Manna Ordering and Theorem for Multisets

Co-authored-by: Malvin Gattinger [email protected]

---

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Dershowitz-Manna.20Ordering.20theorem/near/434390710

[github-actions[bot]]

PR summary 85739c0726

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Multiset.DershowitzManna (new file)	393

---

Declarations diff

+ IsDershowitzMannaLT + IsDershowitzMannaLT.trans + instWellFoundedisDershowitzMannaLT + wellFounded_isDershowitzMannaLT ++ add_add_tsub_cancel

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

[riccardobrasca]

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

[kim-em]

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#15645~~ By Dependent Issues (🤖). Happy coding!

[haitian-yuki]

Thanks for the PR!

Am I right in saying that DMLT_singleton and TransLT are auxiliary to the proof? If so, can you make them as well as all lemmas about them private?

Thanks about the quick review! Yes, they are auxiliary to the proof. May I ask what do you mean by saying to make them private?

[YaelDillies]

I mean replacing def/lemma by private def/private lemma

[YaelDillies]

I have just pushed a golf. I am running out of time today, but you should feel free to have a look for yourself at my commit and try golfing further using the tricks you will have learned. 😃

[haitian-yuki]

I have just pushed a golf. I am running out of time today, but you should feel free to have a look for yourself at my commit and try golfing further using the tricks you will have learned. 😃

Hi Thanks for showing some of the golfing tricks;-) @YaelDillies . I tried golfing a little bit more and maybe now it is in a better form. One thing that I am still unsure about is whether I am allowed to use aesop in the proof as long as it doesn't show 'time run out' thing? Is that what you meant by 'so long as performance is not too terrible'? Thanks!

Ah I just saw some checks were not successful and I'm trying to understand what happened to the branch...

[YaelDillies]

Can you please merge master to get rid of the obscure CI error?

[haitian-yuki]

Thanks again for another golf @YaelDillies ! I have to say it looks pretty clean to me now and I cannot see much to improve here ;-) Does it mean the PR is done now? Thanks!

[YaelDillies]

I'm hoping to do a third golf pass at some point next week (I am completely submerged right now), then yes it should be good 😄

[YaelDillies]

Sorry for the delay, but here's the final golf. Thank you for your patience!

maintainer merge

[github-actions[bot]]

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

[kim-em]

There's still an unresolved review comment above.

[kim-em]

bors merge

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mathlib-bors[bot]]

Build failed:

• Build

[bryangingechen]

bors r+ bors d+

[mathlib-bors[bot]]

:v: haitian-yuki can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style