[Merged by Bors] - feat(data): port finsupp.ne_locus/lex to dfinsupp #16777
Conversation
alreadydone
added
awaiting-review
mathlib-dependent-issues-bot
added
blocked-by-other-PR
There was a problem hiding this comment.
Your lemmas look very much like the dist ones in a normed group (dist_add_right, dist_neg_neg, dist_neg, dist_sub_left, ...) so I would align this API on that one (and you can see we're missing lemmas about ne_locus f (f + g) and similar) and leave a note to this effect.
Please also multiplicativize everything.
I understand this API is based off the finsupp.ne_locus one, but it is very recent and not imported further than data.finsupp.lex so I think it's fair changing.
src/data/dfinsupp/lex.lean
Outdated
| lemma lex.le_of_forall_le {a b : lex (Π₀ i, α i)} (h : ∀ i, of_lex a i ≤ of_lex b i) : a ≤ b := | ||
| le_of_lt_or_eq $ or_iff_not_imp_right.2 $ λ hne, by classical; exact | ||
| ⟨finset.min' _ (nonempty_ne_locus_iff.2 hne), | ||
| λ j hj, not_mem_ne_locus.1 (λ h, (finset.min'_le _ _ h).not_lt hj), | ||
| (h _).lt_of_ne (mem_ne_locus.1 $ finset.min'_mem _ _)⟩ | ||
|
|
||
| lemma lex.le_of_of_lex_le {a b : lex (Π₀ i, α i)} (h : of_lex a ≤ of_lex b) : a ≤ b := | ||
| lex.le_of_forall_le h | ||
|
|
||
| lemma to_lex_monotone : monotone (@to_lex (Π₀ i, α i)) := | ||
| λ _ _, lex.le_of_forall_le |
There was a problem hiding this comment.
Out of these four, the only one I would expect is to_lex_monotone and I would add its counterpart to_lex_strict_mono. The other ones have confusing names and if I were to discover the API for the first time I would wonder what their use is given that we already have to_lex_monotone and to_lex_strict_mono.
lex_lt_of_lt_of_preorder and lex_lt_of_lt are similarly unsettling because they mix bundled relations with unbundled ones.
There was a problem hiding this comment.
Git blame tells me that all three were introduced by @urkud for pi.lex, with the first one in #9129 and the other two in #14389, and you've also touched the first one in #14164 before the other two were added. @adomani was probably just copying from pi.lex like what I do here. I'm happy to have the first two removed because all are defeq.
There was a problem hiding this comment.
Just to confirm: I did simply copy a bunch of lemmas and fix as instructed by Lean!
There was a problem hiding this comment.
lex_lt_of_lt_of_preorderandlex_lt_of_ltare similarly unsettling because they mix bundled relations with unbundled ones.
It's the only way to state them succinctly while still allowing complete generality on the relation on ι ; I'd like to use unbundled relation for the order on α i as well, but although a ≤ a' is just ∀ i, a i ≤ a' i (product order), a < a' is defined to be a ≤ a' ∧ a' ≰ a; we don't have a definition for this operation on relations, and I think writing (∀ i, r (a i) (a' i)) ∧ (∃ i, ¬ r (a' i) (a i)) is too long, so I rely on the typeclass system to generate the (<) for me, and that requires the use of preorder.
And really these are just 3 x 2 technical lemmas used to transfer well-foundedness of lex order to product order (in fact only the first of the dfinsupp lemmas is actually used, I believe).
There was a problem hiding this comment.
Hi @YaelDillies I've removed the 3x2 lemmas lex.le_of_forall_le/le_of_of_lex_le from pi/finsupp/dfinsupp and CI now passed. I also renamed the dfinsupp.ne_locus lemmas following your PR #17036. So the only thing not yet resolved is about lex_lt_of_lt(_of_preorder); do you have a better suggestion, or should I leave them as is?
|
Just a heads-up that Anne delegated to me #16236 and I will merge is as soon as CI is happy with it. I'm mentioning this since the PR touches the |
|
Oh nevermind we can't multiplicativize because we don't have finitely multiplicatively supported functions. I will open a PR matching the |
There was a problem hiding this comment.
I will open a PR matching the finsupp.ne_locus and dist APIs shortly.
You other naming suggestions in ne_locus all look good, but don't you want to do those changes for finsupp and add the dfinsupp.ne_locus file together in your PR? If you do that part, I'll wait for it and only deal with this comment and not the others in this PR.
|
Here's the PR #17036. I don't care whether the current is merged first. |
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
+ Add new files *dfinsupp/ne_locus* and *dfinsupp/lex* mostly by copying the finsupp counterparts and making trivial adaptions. Use the `dfinsupp` lemmas/constructions to golf the `finsupp` counterpart, e.g. the `linear_order` on `finsupp.lex`. + Add lemmas `lex_lt_of_lt(_of_preorder)` for each of pi/finsupp/dfinsupp that shows the (<) relation on the product of a family of partial orders is a subrelation of the lexicographic (<), for any choice of well-founded relation (in the case of pi) or strict total order (in the case of (d)finsupp) on the set of coordinates. Useful to deduce well-foundedness of the product order from the well-foundedness of the lexicographic order in #16772. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
eric-wieser
added
the
hacktoberfest-accepted
Add new files dfinsupp/ne_locus and dfinsupp/lex mostly by copying the finsupp counterparts and making trivial adaptions. Use the
dfinsupplemmas/constructions to golf thefinsuppcounterpart, e.g. thelinear_orderonfinsupp.lex.Add lemmas
lex_lt_of_lt(_of_preorder)for each of pi/finsupp/dfinsupp that shows the (<) relation on the product of a family of partial orders is a subrelation of the lexicographic (<), for any choice of well-founded relation (in the case of pi) or strict total order (in the case of (d)finsupp) on the set of coordinates. Useful to deduce well-foundedness of the product order from the well-foundedness of the lexicographic order in [Merged by Bors] - feat(data/(d)finsupp): well-foundedness of lexicographic and product orders #16772.