Addition on intervals?

Stream: mathlib4

[Michael Stoll]

Would it make sense to provide Add instances for @Set.Ioc T(when T has an addition that is compatible with the order structure) etc., such that Set.Ioc a b + Set.Ioc c d = Set.Ioc (a + c) (b + d)? (And for Sets and Finsets, too...)
Maybe @Yaël Dillies has this somewhere already?

[Kevin Buzzard]

That's not going to be true for Nat, because of the discreteness (x>a and y>c implies x+y can't be a+c+1)

[Michael Stoll]

True. So this would need more assumptions. (But it would work for Icc, for example, I guess.)

[Ruben Van de Velde]

Do we not already have some kind of addition on sets? In locale Pointwise, I think. Adding another meaning for it seems confusing (or is this just a theorem about intervals under this addition?)

[Eric Wieser]

I'm confused by your question; do you mean an HAdd instance?

[Michael Stoll]

OK; I had forgotten about Pointwise.
I was thinking of something like Ioc a b + Ioc b d = Ioc (a+c) (b+d) with pointwise addition on the left. This seems to type-check with open Pointwise, but it looks like the statement (over the reals, say) is not there.

[Eric Wieser]

Ioc a b + Ioc b d = Ioc (a+c) (b+d) already typechecks today, the addition already exists (in scoped Pointwise)

[Michael Stoll]

OK, but the statement is not in Mathlib (at least, exact? does not find it).

[Eric Wieser]

I'm surprised I can't even find the Icc one

[Kevin Buzzard]

I wouldn't be surprised if this was one of those theorems which was false for general additive ordered monoids. For example {0,2,3,4,...} is an additive monoid but [0,2]+[0,2] misses 3.

[Notification Bot]

Qin Yuxuan has marked this topic as resolved.

[Notification Bot]

Qin Yuxuan has marked this topic as unresolved.

[Richard Copley]

[Edit: proved it]

import Mathlib.Data.Set.Intervals.Basic
import Mathlib.Tactic.PushNeg
import Mathlib.Data.Real.Basic

open Pointwise in
example : Set.Icc (1 : ℝ) 0 + Set.Icc (0 : ℝ) 2 ≠ Set.Icc (1 : ℝ) 2 :=
  calc Set.Icc (1 : ℝ) 0 + Set.Icc (0 : ℝ) 2
    _ = ∅ + Set.Icc 0 2 := by simp
    _ = ∅               := Set.empty_add
    _ ≠ Set.Icc 1 2     := by {
    rewrite [Mathlib.Tactic.PushNeg.empty_ne_eq_nonempty, Set.nonempty_Icc]
    exact one_le_two
  }

[Kevin Buzzard]

Yeah that too :-)

[Michael Stoll]

I see. It is a can with a lot of worms...

[Kevin Buzzard]

Probably fine for groups assuming the intervals are nonempty. Groups give you subtraction which saves you from many pathologies.

[Eric Wieser]

I'd expect us to have:

open scoped Pointwise

@[to_additive]
theorem Icc_mul_Icc_subset {α : Type*} [Mul α] [Preorder α]
    [CovariantClass α α HMul.hMul LE.le] [CovariantClass α α (Function.swap HMul.hMul) LE.le] (a b c d : α) :
    Set.Icc a b * Set.Icc c d ⊆ Set.Icc (a * c) (b * d) := by
  rintro x ⟨y, z, ⟨hya, hyb⟩, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_le_mul' hya hzc, mul_le_mul' hyb hzd⟩

[Kevin Buzzard]

Yeah, the easy inclusion is true in huge generality and should surely be there.

[Eric Wieser]

#8368

[Yaël Dillies]

I worked on those lemmas in Lean 3 but I failed to find the correct generality for the reverse inclusion to hold. I am more ideas now though.

[Kevin Buzzard]

The easy way out would be to prove it for ordered groups and also for Nat, and then wait to see if any other use cases actually arise (and I suspect they won't)

[Yaël Dillies]

What's your proof for ordered groups? I have a proof for linear ordered monoids with docs#HasExistsAddOfLe, but it's quite unsatisfying given that this property is clearly closed under products.

[Eric Wieser]

I assume we only care about Icc on products, because Ico is poorly behaved?

[Yaël Dillies]

Yes, at least for now

[Kevin Buzzard]

Oh I was assuming the groups are linearly ordered! So you know strictly more than me.

[Yaël Dillies]

Nono Kevin, knowledge isn't a linear order. That's the whole point. :grinning:

[Eric Wieser]

Eric Wieser said:

#8368

:ping_pong:

[Eric Wieser]

:ping_pong: again; it's a shame to have a Zulip thread about something but then let the PR stagnate

[Michael Stoll]

I started the thread here, but I'm out of my depth regarding this part of Mathlib...