Identifying intervals of N with intervals of Z

Stream: Is there code for X?

[Terence Tao]

I recently had need of the following lemma:

import Mathlib

lemma ico_Int_ofNat_eq_Int_ofNat_ico (a b:ℕ) : Set.Ico (Int.ofNat a) (Int.ofNat b) = Int.ofNat '' (Set.Ico a b) := by
  ext x
  simp
  constructor
  . rintro ⟨ ha, hb ⟩
    rcases Int.eq_ofNat_of_zero_le ((Int.zero_le_ofNat a).trans ha) with ⟨ n, rfl ⟩
    norm_cast at ha hb
    use n
  rintro ⟨ n, ⟨ ha, hb⟩, rfl ⟩
  norm_cast

Of course there are also analogues forSet.Icc, Set.Ioc, Set.Ioo, Set.Ioi, Set.Ici (but not Set.Iio, Set.Iic). Is this lemma essentially already in Mathlib? I was unable to locate it with standard searches.

[Ruben Van de Velde]

Is Int.ofNat the common spelling? Have you looked at Nat.cast? (Just guessing)

[Adam Topaz]

I guess one could formulate a general assertion about monotone maps which preserve convexity (injectivity would also be needed for some variants)

[Adam Topaz]

But unfortunately docs#Convex is not the right notion.

[Adam Topaz]

In any case, I'm surprised that we don't have such a lemma already in mathlib, using Nat.cast.

[Yaël Dillies]

Seems that I missed it

[Kevin Buzzard]

@Terence Tao if you try simp on your lemma, it changes Int.ofNat a to ↑a (the notation for Nat.cast a), which is a hint that this is the preferred spelling for mathlib lemmas (Int.ofNat a is not in "simp normal form")

[Terence Tao]

How would one write the lemma using Nat.cast to specifically cast to the integers? Just replace all occurrences of Int.ofNat with Nat.cast (R := ℤ) (or fun n ↦ (n:ℤ))? In any event I was not able to find this lemma in a Nat.cast form either.

[Kevin Buzzard]

If (n : \N) then you can just write (n : \Z) and Lean will cast it.

[Kevin Buzzard]

Yes I agree that the main issue is that the lemma isn't there even in the simp normal form :-)

[Terence Tao]

OK, so Set.Ico (a:ℤ) (b:ℤ) = (fun (n:ℕ) ↦ (n:ℤ)) '' (Set.Ico a b) seems to work as an alternate spelling. (Not sure how to name it now though.)

[Terence Tao]

Adam Topaz said:

I guess one could formulate a general assertion about monotone maps which preserve convexity (injectivity would also be needed for some variants)

I guess the general assertion is that if a map between totally ordered spaces is monotone, injective, and has OrdConnected image, then it maps intervals to intervals; if it is monotone, injective, and has UpperSet image, then it maps right-infinite intervals to right-infinite intervals; and if it is monotone, injective, and has LowerSet image, then it maps left-infinite intervals to left-infinite intervals.

[Terence Tao]

also without the hypotheses on the image (and for partially ordered sets instead of totally ordered sets) one always has a set inclusion instead of equality. (For Set.Icc one can also drop injectivity.)

[Yaël Dillies]

We already have a few lemmas about OrdConnected range. See around docs#CovBy. Treatment is not very thorough yet.

[Terence Tao]

Ah, there is docs#Set.image_subtype_val_Ico etc. which already comes close to this.

[Yaël Dillies]

Set.OrdConnected assumptions really should not be typeclass arguments... :sad:

[Terence Tao]

To get from docs#Set.image_subtype_val_Ico to my original application, one would need that (a) StrictMono maps create an OrderIso between the domain and the image; and (b) intervals are preserved by OrderIso. Presumably (a) is somewhere in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Hom/Basic.html but I can't find (b) yet.

[Terence Tao]

Actually (a) seems to be missing as well. (It's only true for linear orders, which may be one reason why it is missing.)

[Yaël Dillies]

(a) does seem to be missing. (b) is docs#OrderIso.image_Icc

[Terence Tao]

So I guess the minimal thing to do is add (a) to Mathlib? Then everything else can be done in like three lines of existing Mathlib code.

[Terence Tao]

(Well, one needs a proof of Set.OrdConnected (Set.range (fun (n:ℕ) ↦ (n:ℤ))) (and also UpperSet (Set.range (fun (n:ℕ) ↦ (n:ℤ)))), but this isn't too hard. Maybe this could go into Mathlib too?)

[Yury G. Kudryashov]

All of this could go to Mathlib, we just need to find a good place for these lemmas.

[Yury G. Kudryashov]

(possibly, a new file for Nat/Int-specific lemmas)

[Yury G. Kudryashov]

It looks like we don't have Set.range (Nat.cast : Nat → Int) = Ici 0

[Yury G. Kudryashov]

Do you want me to add some of this or you prefer to do it yourself?

[Terence Tao]

I haven't actually done a mathlib PR before, and am unfortunately a bit overwhelmed with other tasks, so if you are willing to do the honours that would be great.

For what it's worth, here is a proof of the last statement you made:

import Mathlib

example : Set.range (Nat.cast : Nat → Int) = Set.Ici 0 := by
  ext a
  simp
  constructor
  . rintro ⟨ n, rfl ⟩
    exact Int.ofNat_nonneg n
  exact CanLift.prf a

[Terence Tao]

Not sure exactly how to even spell the OrderIso statement though. Something like

import Mathlib

def OrderIso.image {α: Type*} {β: Type*} [LinearOrder α] [LinearOrder β] {f: α → β} (hf: StrictMono f)
   : α ≃o Set.range f := sorry

? I'm not very good at actually building isomorphisms.

[Yury G. Kudryashov]

I'll do it.

[Yury G. Kudryashov]

docs#StrictMono.orderIso

[Terence Tao]

Slick proof.

[Yury G. Kudryashov]

I started branch#YK-nat-int-range. I have family duties for the next hour, then I'll complete it before going to bed.

[Terence Tao]

This is what the proof of my original lemma looks like now:

import Mathlib

open Set

@[simp]
theorem Int.range_natCast : Set.range ((↑) : ℕ → ℤ) = Ici 0 :=
  Subset.antisymm (range_subset_iff.2 Int.ofNat_nonneg) CanLift.prf

lemma ico_Int_ofNat_eq_Int_ofNat_ico (a b:ℕ) : Ico (a:ℤ) (b:ℤ) = (fun (n:ℕ) ↦ (n:ℤ)) '' (Ico a b) := by
  let equiv : ℕ ≃o range (Nat.cast : Nat → Int) := StrictMono.orderIso _ Int.coe_nat_strictMono
  change Ico (equiv a:ℤ) (equiv b:ℤ) = (Subtype.val ∘ equiv) '' (Ico a b)
  have : OrdConnected (Set.range (Nat.cast : Nat → Int)) := Int.range_natCast ▸ Set.ordConnected_Ici
  rw [image_comp, OrderIso.image_Ico, image_subtype_val_Ico]

[Yury G. Kudryashov]

I'm going to generalize lemmas about Subtype.val to an OrderEmbedding instead.

[Yury G. Kudryashov]

This is more work but it's better for future applications in the library.

[Yury G. Kudryashov]

#9927 has all the intervals but Ioi and Ici. I'll add them once the kids are sleeping.

[Yury G. Kudryashov]

Done. #9927 and its dependencies.

[Yaël Dillies]

Also note that Data.Nat.Interval exists

[Terence Tao]

There are also the Finset versions, e.g.,

theorem image_cast_int_Icc_finset (a b : ℕ) : Finset.image (↑) (Finset.Icc a b) = Finset.Icc (a : ℤ) b

but I am not sure whether it is worth putting these into Mathlib also as they can be obtained from the set versions easily enough using docs#Finset.coe_inj, docs#Finset.coe_image , and docs#Finset.coe_Icc.

[Eric Wieser]

Those should probably be stated using Finset.map if possible

[Yury G. Kudryashov]

We simplify Filter.map to Filter.image, so simp versions should use Filter.image.

[Yury G. Kudryashov]

I guess, Finset versions are provable by mod_cast <| image_cast_int_Icc a b

[Yury G. Kudryashov]

I'll have a look once Set versions are merged.

[Yury G. Kudryashov]

Yaël Dillies said:

Also note that Data.Nat.Interval exists

It depends on Finsets, and these lemmas don't need Finsets.

[Yaël Dillies]

Yes, but you should coordinate with those lemmas