Zulip Chat Archive

Stream: Is there code for X?

Topic: Correct setting for positive shifts of intervals


view this post on Zulip Peter Nelson (Mar 09 2021 at 17:41):

There are many trivial lemmas in data.set.intervals.image_preimage about images of intervals under various functions, in particular - adding a constant. However, they all require at least a group structure on the linear order, so none imply the obvious fact that adding a constant maps intervals to intervals in nat. I've tried to look through the structures in mathlib that give the right setting for this fact, but they all seem either too weak or too strong. I'm trying to avoid having to deal with nat as a special case.

Specifically, I want lemmas like :

lemma Ioc_add_bij (a b d : ):
set.bij_on (+d) (Ioc a b) (Ioc (a+d) (b+d)) := sorry

I believe what is required is an add_comm_monoid, with an ordering such that for all 0 \le a \le b, there exists c with a + c = b. Is there any instance or combination of instances that gives these properties?

view this post on Zulip Eric Wieser (Mar 09 2021 at 17:42):

Can you link to the statement you'd like to use that seems too restrictive to apply to nat?

view this post on Zulip Eric Wieser (Mar 09 2021 at 17:44):

So docs#set.image_add_const_Ico?

view this post on Zulip Peter Nelson (Mar 09 2021 at 17:44):

Yes, exactly : https://leanprover-community.github.io/mathlib_docs/data/set/intervals/image_preimage.html#images-under-codex--a--xcode

view this post on Zulip Eric Wieser (Mar 09 2021 at 17:45):

(What a beautiful url anchor, thanks doc-gen)

view this post on Zulip Peter Nelson (Mar 09 2021 at 17:45):

(For what it's worth, I've written proofs for my example lemma and various related facts; it just feels a bit weird that I would have to do so).

view this post on Zulip Eric Wieser (Mar 09 2021 at 17:46):

I wonder if some of the lemmas in that file can be reduced to docs#ordered_add_comm_monoid or docs#ordered_cancel_add_comm_monoid

view this post on Zulip Peter Nelson (Mar 09 2021 at 17:47):

Yeah, I'm not sure. At least if you want bijections, I think that you do need a 'partial subtraction' of the type I described, and I don't know if that follows from a more general cancellative property

view this post on Zulip Eric Wieser (Mar 09 2021 at 18:01):

docs#canonically_linear_ordered_add_monoid is sufficient to prove image_const_add_Ici for nat:

@[simp] lemma image_const_add_Ici {G : Type u} [canonically_linear_ordered_add_monoid G] (a b c : G) :
  (λ x, a + x) '' Ici b = Ici (a + b) :=
begin
  ext,
  simp only [mem_image, mem_Ici],
  split,
  { rintros c, hc, hc'⟩,
    exact (add_le_add_left hc a).trans_eq hc', },
  { intro h,
    obtain c, rfl := le_iff_exists_add.mp h,
    refine b + c, self_le_add_right _ _, (add_assoc _ _ _).symm⟩, },
end

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 18:02):

I don't think there's any deep reason why nat (or more general) versions of these lemmas are missing. I suspect that @Yury G. Kudryashov just didn't need them in that generality when he made the PR. They'd certainly be welcome if someone were to PR them!

view this post on Zulip Peter Nelson (Mar 09 2021 at 18:04):

Eric -that's true, but that setting doesn't apply to int, which fails this axiom

le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a + c_1.

A one-sided version of that axiom, with only the forwards implication, is what's needed to apply to both nat and (for example )int.

view this post on Zulip Eric Wieser (Mar 09 2021 at 18:05):

Right, although the existing lemmas covers int right?

view this post on Zulip Yury G. Kudryashov (Mar 09 2021 at 18:16):

Indeed, I added lemmas in the generality I needed. Feel free to generalize them and/or add ' versions that work for canonically ordered (add) comm monoids.

view this post on Zulip Eric Wieser (Mar 09 2021 at 18:18):

A one-sided version of that axiom, with only the forwards implication, is what's needed to apply to both nat and (for example )int.

I'd be loosely in favor of an ad-hoc typeclass in that file to avoid the need for separate primed and unprimed versions, containing the axiom you suggest and instantiated for ordered_add_comm_monoid and canonically_linear_ordered_add_monoid

view this post on Zulip Kevin Buzzard (Mar 09 2021 at 22:50):

(deleted)

view this post on Zulip Peter Nelson (Mar 10 2021 at 06:20):

To get a bijection version (addition translates an interval bijectively) it is even more awkward. A [canonically_linear_ordered_add_monoid] instance is not enough without some sort of cancellation law (otherwise it fails on singleton intervals).

Here is some code that gives the required lemma, proved using a bespoke typecless with (I think) the minimal required assumptions, and instances for both nat and ordered_add_comm_group.

class ordered_cancel_add_comm_exists_sub_monoid (α : Type u)
  extends ordered_cancel_add_comm_monoid α :=
(exists_add_of_le :  (a b : α), a  b   (c : α), b = a + c)

instance ordered_add_comm_group.ordered_cancel_add_comm_exists_sub_monoid
(α : Type u)[ordered_add_comm_group α]:
  ordered_cancel_add_comm_exists_sub_monoid α :=
{ exists_add_of_le := λ a b hab, b - a, (add_sub_cancel'_right a b).symm⟩}

instance nat.ordered_cancel_add_comm_exists_sub_monoid :
  ordered_cancel_add_comm_exists_sub_monoid  :=
{ exists_add_of_le := λ a b hab, _, (nat.add_sub_of_le hab).symm⟩}

open set ordered_cancel_add_comm_exists_sub_monoid

lemma Ioo_add_bij {α : Type}[ordered_cancel_add_comm_exists_sub_monoid α](a b d : α):
  bij_on (+d) (Icc a b) (Icc (a+d) (b+d)) :=
begin
  refine λ x h, _, λ x hx y hy h, _, λ x h, _⟩,
  { rw [mem_Icc] at  h,
    exact add_le_add_right h.1 _, add_le_add_right h.2 _⟩},
  { apply add_right_cancel h, },
  rw mem_image,
  simp_rw mem_Icc at h ,
  cases h with h1 h2,
  obtain c,rfl := exists_add_of_le _ _ h1,
  rw [add_right_comm, add_le_add_iff_right] at h1 h2,
  exact  a+c, h1,h2⟩, by rw add_right_comm⟩,
end

This would also work for nnreal, but I don't know a good typeclass that encapsulates both nnreal and nat, because canonically_linear_ordered_add_monoid is too weak. Thoughts on this would be welcome.

view this post on Zulip Kevin Buzzard (Mar 10 2021 at 06:43):

Can you give me an example of a canonically linear ordered add monoid for which a theorem you want to be true fails?

Johan asked a question about nnreal a few months ago which, after Mario and I discussed it here (I'm sorry I'm on mobile and the link is too fiddly to find) and we boiled the question down to "when is a topological monoid a submonoid of a topological group?". There is the usual algebraic obstruction -- the monoid needs to be cancellative, or else it doesn't embed into any group at all. However there is also a topological obstruction, as observed by Reid's example of nnreal with following topology: every subset which is open with the usual order topology is open, and also every subset of [0,1] is open. This is a topological monoid, but addition of a fixed element is not an open map in contrast to what happens in a topological group. Conversely adding this condition looked like it was precisely the right one to make the group localisation inherit a topological group structure.

What is the counterexample of a canonically ordered monoid which you have in mind which stops your lemmas being true?

view this post on Zulip Damiano Testa (Mar 10 2021 at 08:00):

I am not really sure if this would work, but I think that this might be a great addition to the counterexamples branch, if it works! (This is somewhat shameless self-promotion of my branch :wink:)

In the branch, there is an example of a canonically_ordered_comm_semiring in which multiplication by 2 is not injective. The example is obtained from ℕ × zmod 2, with the ring structure given by the usual componentwise addition and multiplication. The ordering is defined by declaring (a,s) ≤ (b,t) if and only if

  • a < b, or
  • (a,s) = (b,t).

Thus, "far apart", the order ignores the zmod 2 components, but prevents (a,0) and (a,1) from being comparable. [This is actually formalized.]

It seems to me that, if you remove from the ring the "initial segment" of elements of the form (a,1), for 0 ≤ a ≤ 2you still have all the properties above and moreover, the interval [0, 2] now has fewer elements than the interval [2, 4], since in the initial one, you are missing out on all the interesting zmod 2 elements.
[Note: there is a formalization that if you remove just (0,1), you still get a canonically_ordered_comm_semiring, but I had not thought about removing more elements.]

I hope that this makes sense!

view this post on Zulip Damiano Testa (Mar 10 2021 at 08:04):

Also, the cancellation that you want is on addition, right? This should hold for the example above, since it is a subsemiring of the comm_ring ℤ × zmod 2.

view this post on Zulip Damiano Testa (Mar 10 2021 at 08:10):

Ah, I see an issue with my approach: the identity of the semiring ℕ × zmod 2 is (1,1), so you cannot simply remove it. However, it might be possible to tweak this into an example showing that without your axiom, intervals are not "homogeneous".

view this post on Zulip Peter Nelson (Mar 10 2021 at 13:28):

Ah, it looks like canonically ordered monoids have cancellation after all - I was doing something wrong earlier and the instance wasn't firing. This makes me happier.

Potentially this, and some other small things related to intervals, could make my first PR. Can anyone suggest a good name for this typeclass?

/-- an add_comm_monoid with one-sided 'subtraction' in the sense that if a ≤ b,
there is some c for which a + c = b -/
class ordered_cancel_add_exists_add_monoid (α : Type u)
  extends ordered_cancel_add_comm_monoid α :=
(exists_add_of_le :  (a b : α), a  b   (c : α), b = a + c)

instance ordered_add_comm_group.ordered_cancel_add_exists_add_monoid
(α : Type u)[ordered_add_comm_group α]:
  ordered_cancel_add_exists_add_monoid α :=
{ exists_add_of_le := λ a b hab, b - a, (add_sub_cancel'_right a b).symm⟩}

instance canonically_ordered_comm_monoid.ordered_cancel_add_exists_add_monoid
(α : Type u)[canonically_ordered_add_monoid α]:
  ordered_cancel_add_exists_add_monoid  :=
{ exists_add_of_le := λ a b hab, le_iff_exists_add.mp hab}


open set ordered_cancel_add_exists_add_monoid

lemma Icc_add_bij {α : Type}[ordered_cancel_add_exists_add_monoid α](a b d : α):
  bij_on (+d) (Icc a b) (set.Icc (a+d) (b+d)) :=
begin
  refine λ x h, _, λ x hx y hy h, _, λ x h, _⟩,
  { rw [mem_Icc] at  h,
    exact add_le_add_right h.1 _, add_le_add_right h.2 _⟩},
  { apply add_right_cancel h, },
  rw mem_image,
  simp_rw mem_Icc at h ,
  cases h with h1 h2,
  obtain c,rfl := exists_add_of_le _ _ h1,
  rw [add_right_comm, add_le_add_iff_right] at h1 h2,
  exact  a+c, h1,h2⟩, by rw add_right_comm⟩,
end

view this post on Zulip Heather Macbeth (Mar 10 2021 at 17:15):

I think cancel should not appear in the name, since in cancel_monoid the statement like b = a + c appears in the hypothesis rather than the goal. Maybe ordered_has_sub_add_monoid?

Anyway, since these gadgets are remarkably hard to name, I suggest you open the PR and the discussion can continue there! :)

view this post on Zulip Peter Nelson (Mar 10 2021 at 18:31):

@Eric Wieser @Kevin Buzzard the plot thickens! There was a small but important typo in my code just above, where I forgot to change an back into an α. Changing it into an α breaks the code, because canonically ordered additive monoids (even with a linear order) aren't cancellative.

In fact, re Kevin's question, there is a nice example to show this - take the usual ordering on nat with the monoid where addition is (the usual) max. This is a canonical linear ordered monoid (it satisfies all those axioms; in particular a \le b iff there is some c with max a c = b) but it isn't cancellative, and it is also easy to see that adding a constant maps intervals to intervals, but not bijectively.

So it really seems that ordered_cancel_add_comm_monoid together with (exists_add_of_le : ∀ (a b : α), a ≤ b → ∃ (c : α), b = a + c) is the right set of assumptions; this happens to work for both nat and nnreal, but the only existing general class that obviously has an instance for this is ordered_add_comm_group. Maybe the right abstraction is just that this should hold for either an ordered add_comm group, or the submonoid of nonnegative elements of such a group. If this is the answer, it feels unlikely to be worth formalizing.

view this post on Zulip Heather Macbeth (Mar 10 2021 at 18:35):

Well, there is also:
docs#multiset.le_iff_exists_add
docs#cardinal.le_iff_exists_add :)

view this post on Zulip Peter Nelson (Mar 10 2021 at 18:35):

good point!

view this post on Zulip Peter Nelson (Mar 10 2021 at 18:36):

also set union

view this post on Zulip Peter Nelson (Mar 10 2021 at 18:36):

(deleted)

view this post on Zulip Eric Wieser (Mar 10 2021 at 18:37):

I'd argue (perhaps controversially) that if the same lemma statement appears ≥3 times, it's worthy of a typeclass

view this post on Zulip Eric Wieser (Mar 10 2021 at 18:37):

That or one of the lemmas it uses is

view this post on Zulip Peter Nelson (Mar 10 2021 at 18:38):

So would the typeclass correspond to 'the nonnegative elements of some ordered_add_comm_group' and have instances from nat and nnreal?

view this post on Zulip Eric Wieser (Mar 10 2021 at 18:41):

I was thinking you might just be able to get away with:

class has_exists_add_of_le [ordered_cancel_add_comm_monoid α] :=
(exists_add_of_le :  (a b : α), a  b   (c : α), b = a + c)

view this post on Zulip Eric Wieser (Mar 10 2021 at 18:42):

Then your lemma becomes

lemma Icc_add_bij {α : Type} [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] (a b d : α):
  bij_on (+d) (Icc a b) (set.Icc (a+d) (b+d)) :=
begin

view this post on Zulip Peter Nelson (Mar 10 2021 at 18:43):

ok, that seems nicer than the way I was writing it using extends.

view this post on Zulip Eric Wieser (Mar 10 2021 at 18:43):

Heather Macbeth said:

Well, there is also:
docs#multiset.le_iff_exists_add
docs#cardinal.le_iff_exists_add :)

Well, cardinal is an instance of canonically_linear_ordered_add_monoid already, and multiset is a canonically_ordered_add_monoid

view this post on Zulip Eric Wieser (Mar 10 2021 at 18:45):

But I echo Heather's comment that this would be easier to discuss in a PR

view this post on Zulip Peter Nelson (Mar 10 2021 at 18:45):

that'll happen in the next few hours. Thanks everyone!

view this post on Zulip Peter Nelson (Mar 10 2021 at 20:27):

#6629


Last updated: May 07 2021 at 21:10 UTC