-
Notifications
You must be signed in to change notification settings - Fork 331
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.
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
feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem #14411
base: master
Are you sure you want to change the base?
Conversation
PR summary 61d70ce689Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Can you please mark this PR |
There was a problem hiding this 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).
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. |
This PR/issue depends on:
|
partly done Co-authored-by: Rida Hamadani <[email protected]>
125da22
to
1ee6972
Compare
There was a problem hiding this 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)
|
||
/-- The standard Dershowitz–Manna ordering: -/ | ||
inductive MultisetDMLT [DecidableEq α] [Preorder α] (M N : Multiset α) : Prop := | ||
| DMLT : ∀ (X Y Z : Multiset α), |
There was a problem hiding this comment.
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?
/-- 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 : α) , |
There was a problem hiding this comment.
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?
|
||
/-- MultisetTransLT is the transitive closure of MultisetRedLT and is equivalent to MultisetDMLT | ||
(proved later). -/ | ||
def MultisetTransLT [DecidableEq α] [LT α] : Multiset α → Multiset α → Prop := |
There was a problem hiding this comment.
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?
simp [Multiset.ext, Multiset.count_cons] at h0 | ||
by_cases h : b = a | ||
· have := h0 b | ||
aesop |
There was a problem hiding this comment.
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
)
aesop | ||
· have := h0 b | ||
simp [Multiset.sub_singleton] | ||
aesop |
There was a problem hiding this comment.
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)
· constructor | ||
simpa | ||
· simpa |
There was a problem hiding this comment.
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)
exact this | ||
exact y_in | ||
let _ := h y_in_Y1 | ||
aesop |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
aesop?
- `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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The alignment looks off 😅
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