leanprover-community
feat(data/finsupp/lex): linear order on finsupps
This PR constructs a linear order on finsupps where both source and target are linearly ordered. This is useful for #15983, where these linear orders are used to prove that add_monoid_algebras have no non-trivial zero-divisors.
This PR is work in progress and comments or suggestions are as usual really really appreciated!
Can you copy over as many of the
pilemmas about lex as possible?
If I understand correctly, in the pi.lex file there is an underlying order on the Pi type (on line 66) and this instance is then used to prove monotonicity and various other lemmas. Should I port over this instance as well?
I think the suggestion is to prove the finsupp analogues of these pi theorems.
Sure, but those lemmas involve inequalities on the non-lex type, which does not have an order currently.
Sure, but those lemmas involve inequalities on the non-lex type, which does not have an order currently.
What about this one?
https://github.com/leanprover-community/mathlib/blob/a21a8bc69c0484508b53e5c5c9c5208b700518a6/src/data/finsupp/order.lean#L37
Eric, thanks! I was missing the import! I added lt/strict_order instances as well. I copied over some of the pi.lex lemmas. I omitted the bot ones, since the instances for bot on finsupp seem to be on canonically_ordered stuff, which seems not too relevant. Let me know what you think!
Don't forget the lemmas
finsupp.to_lex_applyandfinsupp.of_lex_apply!
These lemmas are in!
I tried to use the linear_order.lift, but failed. If I understand your suggestion correctly, I was trying to lift the order from the pi.lex instance. However, that instance has an extra instance of well-order that is not needed here, thanks to the finite support.
#check @pi.lex.linear_order
pi.lex.linear_order :
Π {ι : Type u_3} {β : ι → Type u_4} [_inst_1 : linear_order ι]
[_inst_2 : is_well_order ι has_lt.lt] -- <-- here
[_inst_3 : Π (a : ι), linear_order (β a)], linear_order (lex (Π (i : ι), β i))
This PR/issue depends on:
- leanprover-community/mathlib#16026
- leanprover-community/mathlib#16122 By Dependent Issues (🤖). Happy coding!
@eric-wieser, if you are happy with this version feel free to push it!
I am partly in favour of wit since it is a common way of arguing: you want to prove something, you find a minimal representative where you can test what happens and you decide your statement there. I agree that wit probably does not achieve this in a very general way.
Also, my eventual goal is to be able to prove that several add_monoid_algebras have no zero-divisors and the linear order is just a convenient tool that will actually self-eliminate from the final statement: the order on the source of the finsupp is completely arbitrary, while the order on the target is tied in with covariant assumptions. Since the target is nat in cases of interest, this is ok. For the source, I simply plan to take any linear order on the source, as this is all that is needed.
I've pushed a slightly cleaner version.
I think the problem with your wit is that it has to repeatedly deal with a junk value that doesn't make anything easier. It's not really much more work to write (f.diff g).min or (f.diff g).min' or whatever variant of junk-handling the user actually wants, and the spelling is arguably still very readable.
@eric-wieser, do you mind if I PR the finset.lattice lemmas separately? I am about to open a PR with a proof of covariance that does not use wit (and is much simpler than I thought), so those lemmas would have to be part of the other PR as well.