Decompose finite set of intervals into disjoint intervals

Stream: Is there code for X?

[Iocta]

I'm looking for the statement that for a finite set of intervals, there is a pairwise disjoint finite set of intervals with the same union as the original.

Something like

example {s : Finset (Set ℝ)} (hs : ∀ t ∈ s, ∃ a b, t = Set.Ioc a b) :
    ∃u : Finset (Set ℝ),
      ((↑u : Set (Set ℝ)).PairwiseDisjoint id)
      ∧ (∀ v ∈ u, ∃ c d, v = Set.Ioc c d)
      ∧ (⋃₀ ↑u = ⋃₀ (↑s : Set (Set ℝ))) := by sorry

[Kevin Buzzard]

My former PhD student Ashvni had the exact analogoue of this problem once, but with clopen subsets of a profinite space, and IIRC she solved it by using sets indexed by functions s -> Prop (you intersect the sets for which the function is true and the complements of those for which it's false, and then throw away the set corresponding to the function sending everything to False). Like for you, for her the key thing was that if X and Y were clopen then so was X - Y. This makes me think that probably there is a purely order-theoretic statement at the bottom of this which should be proved first, and both this and Ashvni's results should be deduced as corollaries. @Yaël Dillies any ideas?

[Johan Commelin]

The following sorry is not completely trivial to fill in. But I think it is a step in the direction the generalization that Kevin is looking for.
Also, I'm quite sad about how long the proof of the example is, using foo.

import Mathlib

lemma foo {α : Type*} [BooleanAlgebra α] {P : α → Prop} (s : Finset α) (hs : ∀ a ∈ s, P a)
    (hsup : ∀ a b, P a → P b → ∃ t : Finset α, t.sup id = a ⊔ b ∧ (t : Set α).PairwiseDisjoint id ∧ ∀ x ∈ t, P x)
    (hdiff : ∀ a b, P a → P b → ∃ t : Finset α, t.sup id = a \ b ∧ (t : Set α).PairwiseDisjoint id ∧ ∀ x ∈ t, P x) :
    ∃ t : Finset α, t.sup id = s.sup id ∧ (t : Set α).PairwiseDisjoint id ∧ ∀ x ∈ t, P x := by
  sorry

example {s : Finset (Set ℝ)} (hs : ∀ t ∈ s, ∃ a b, t = Set.Ioc a b) :
    ∃u : Finset (Set ℝ),
      ((↑u : Set (Set ℝ)).PairwiseDisjoint id)
      ∧ (∀ v ∈ u, ∃ c d, v = Set.Ioc c d)
      ∧ (⋃₀ ↑u = ⋃₀ (↑s : Set (Set ℝ))) := by
  have := foo s hs ?sup ?diff
  · obtain ⟨t, ht₁, ht₂, ht₃⟩ := this
    use t, ht₂, ht₃
    simpa only [Finset.sup_id_set_eq_sUnion] using ht₁
  · rintro _ _ ⟨a, b, rfl⟩ ⟨c, d, rfl⟩
    if h : Disjoint (Set.Ioc a b) (Set.Ioc c d) then
      classical
      use {Set.Ioc a b, Set.Ioc c d}
      simp [Set.pairwiseDisjoint_insert]; intro
      simpa using h
    else
      use {Set.Ioc (min a c) (max b d)}
      simp at h
      simp
      ext x
      simp
      constructor
      · rintro ⟨(h1 | h1), (h2 | h2)⟩
        · left; simp [h1, h2]
        · if hxb : x ≤ b then simp [h1, hxb]
          else simp at hxb; right; simp [h2]; linarith
        · if hax : a < x then simp [h2, hax]
          else simp at hax; right; simp [h1]; linarith
        · right; simp [h1, h2]
      · rintro (⟨h1, h2⟩ | ⟨h1, h2⟩) <;> tauto
  · rintro _ _ ⟨a, b, rfl⟩ ⟨c, d, rfl⟩
    if h : Disjoint (Set.Ioc a b) (Set.Ioc c d) then
      use {Set.Ioc a b}
      simp at h
      simp
      ext x
      simp
      intros
      rcases h with (h | h) | (h | h) <;> linarith
    else
      classical
      use {Set.Ioc a c, Set.Ioc d b}
      simp at h
      simp [Set.pairwiseDisjoint_insert]
      constructor
      · ext x
        simp
        constructor
        · rintro (⟨h1, h2⟩ | ⟨h1, h2⟩)
          all_goals
            constructor
            constructor <;> linarith
            intro ; linarith
        · rintro ⟨⟨h1, h2⟩, h3⟩
          if hxc : x ≤ c then simp [h1, hxc]
          else simp at hxc; right; simp [h2]; solve_by_elim
      · intro
        by_contra!
        linarith

[Yaël Dillies]

It's looking like you want to be thinking about the sublattice of Set Real generated by intervals

[Rémy Degenne]

You could prove that intervals are a semiring of sets (docs#MeasureTheory.IsSetSemiring). Then you could use the (poorly named) definition allDiffFinset₀ defined in that other repository to get your finite set of intervals: https://github.com/RemyDegenne/kolmogorov_extension4/blob/master/KolmogorovExtension4/Semiring.lean .

I hope that it's fine for you to copy a bunch of code from that other repository. Sorry that it's not in Mathlib yet. With @Peter Pfaffelhuber we wrote that code some time ago but we did not do a good job of moving stuff to Mathlib. If I remember correctly, Peter also wanted to refactor that file to simplify the construction.

[Peter Pfaffelhuber]

Yes, I am currently working on this refactor (in my evenings). In the same repository @Rémy Degenne mentioned, there is a file Lebesgue.lean which has setSemiring_halfOpenIntervals, which I think shows what you want. (Something seems broken at the moment due to some Mathlib update, sorry.)