Interval-union semiring

This file defines the semiring of finite unions of pairwise-disjoint intervals over a dense linear order, used for provenance in temporal and numeric-range databases.

An IntervalUnion α is a sorted, non-overlapping list of intervals. Addition is union, multiplication is intersection, and monus is set difference. The natural order is set inclusion.

Main definitions

• IntervalUnion α – a finite union of pairwise-disjoint, sorted intervals
• IntervalUnion.toSet – the corresponding point set
• IntervalUnion.union – union of two interval unions (addition)
• IntervalUnion.inter – intersection of two interval unions (multiplication)
• IntervalUnion.diff – set difference of two interval unions (monus)

Main results

• IntervalUnion.ext_toSet – two interval unions with the same point set are equal (requires DenselyOrdered)
• IntervalUnion.mem_union / mem_inter / mem_diff – membership characterizations
• instance : SemiringWithMonus (IntervalUnion α) – interval unions form an m-semiring for any DenselyOrdered and BoundedOrder linear order
• IntervalUnion.absorptive – the semiring is absorptive (1 + a = 1): the whole space absorbs any interval union under union
• IntervalUnion.mul_sub_left_distributive – a * (b - c) = a * b - a * c, i.e., A ∩ (B \ C) = (A ∩ B) \ (A ∩ C)

Concrete instances

• SemiringWithMonus (IntervalUnion EReal) – interval unions over the extended reals
• SemiringWithMonus (IntervalUnion (WithBot (WithTop ℚ))) – interval unions over the extended rationals

References

• [Widiaatmaja, Djeffal, Dandekar & Senellart, Demonstration of ProvSQL Update Provenance through Temporal Databases][DBLP:conf/pw/WidiaatmajaDDS25]

structure IntervalUnion (α : Type) [LinearOrder α] : Type

A finite union of pairwise-disjoint intervals sorted from left to right. The invariants pairwise_disjoint and pairwise_before ensure the canonical representation.

• intervals : List (Interval α)
• pairwise_disjoint : List.Pairwise Interval.disjoint self.intervals
• pairwise_before : List.Pairwise Interval.before self.intervals

def IntervalUnion.toSet {α : Type} [LinearOrder α] (U : IntervalUnion α) : Set α

The point set of an interval union: the union of the point sets of its intervals.

Equations

• U.toSet = ⋃ I ∈ U.intervals, I.toSet

theorem IntervalUnion.ext_toSet {α : Type} [LinearOrder α] [DenselyOrdered α] (U V : IntervalUnion α) (h : U.toSet = V.toSet) : U = V

theorem IntervalUnion.ext_toSet_iff {α : Type} [LinearOrder α] [DenselyOrdered α] {U V : IntervalUnion α} : U = V ↔ U.toSet = V.toSet

theorem IntervalUnion.ext {α : Type} [LinearOrder α] (U V : IntervalUnion α) (h : U.intervals = V.intervals) : U = V

@[simp]

theorem IntervalUnion.mem {α : Type} [LinearOrder α] (x : α) (U : IntervalUnion α) : x ∈ U.toSet ↔ ∃ I ∈ U.intervals, x ∈ I.toSet

def IntervalUnion.merge {α : Type} [LinearOrder α] (I J : Interval α) (h : ¬(I.before J ∨ J.before I)) : Interval α

Merge two overlapping or adjacent intervals into one.

Equations

• IntervalUnion.merge I J h = { lo := I.lo.minLo J.lo, hi := I.hi.maxHi J.hi, wf := ⋯ }

theorem IntervalUnion.merge_commutative {α : Type} [LinearOrder α] {I J : Interval α} {h : ¬(I.before J ∨ J.before I)} : merge I J h = merge J I ⋯

theorem IntervalUnion.mem_merge' {α : Type} [LinearOrder α] {I J : Interval α} (h : ¬(I.before J ∨ J.before I)) (x : α) : x ∈ I.toSet → x ∈ (merge I J h).toSet

theorem IntervalUnion.mem_merge {α : Type} [LinearOrder α] {I J : Interval α} {h : ¬(I.before J ∨ J.before I)} (x : α) : x ∈ (merge I J h).toSet ↔ x ∈ I.toSet ∨ x ∈ J.toSet

theorem IntervalUnion.merge_preserves_le {α : Type} [LinearOrder α] {I J K : Interval α} (hKI : K ≤ I) (hKJ : K ≤ J) (h : ¬(I.before J ∨ J.before I)) : K ≤ merge I J h

def IntervalUnion.insertMergeList {α : Type} [LinearOrder α] (I : Interval α) : List (Interval α) → List (Interval α)

Insert an interval into a sorted disjoint list, merging with any overlapping or adjacent intervals.

Equations

• One or more equations did not get rendered due to their size.
• IntervalUnion.insertMergeList I [] = [I]

theorem IntervalUnion.mem_insertMergeList {α : Type} [LinearOrder α] (I : Interval α) (L : List (Interval α)) (x : α) : (∃ J ∈ insertMergeList I L, x ∈ J.toSet) ↔ x ∈ I.toSet ∨ ∃ J ∈ L, x ∈ J.toSet

theorem IntervalUnion.insertMergeList_preserves_pairwise_before {α : Type} [LinearOrder α] (I : Interval α) {l : List (Interval α)} : List.Pairwise Interval.before l → List.Pairwise Interval.before (insertMergeList I l)

theorem IntervalUnion.insertMergeList_preserves_disjoint {α : Type} [LinearOrder α] (I : Interval α) {l : List (Interval α)} : List.Pairwise Interval.before l ∧ List.Pairwise Interval.disjoint l → List.Pairwise Interval.disjoint (insertMergeList I l)

def IntervalUnion.insertMerge {α : Type} [LinearOrder α] (I : Interval α) (U : IntervalUnion α) : IntervalUnion α

Equations

• IntervalUnion.insertMerge I U = { intervals := IntervalUnion.insertMergeList I U.intervals, pairwise_disjoint := ⋯, pairwise_before := ⋯ }

theorem IntervalUnion.mem_insertMerge {α : Type} [LinearOrder α] (I : Interval α) (U : IntervalUnion α) (x : α) : x ∈ (insertMerge I U).toSet ↔ x ∈ I.toSet ∨ x ∈ U.toSet

def IntervalUnion.union {α : Type} [LinearOrder α] (U V : IntervalUnion α) : IntervalUnion α

Union of two interval unions (the semiring addition).

Equations

• U.union V = List.foldl (fun (acc : IntervalUnion α) (I : Interval α) => IntervalUnion.insertMerge I acc) U V.intervals

theorem IntervalUnion.mem_union {α : Type} [LinearOrder α] (U V : IntervalUnion α) (x : α) : x ∈ (U.union V).toSet ↔ x ∈ U.toSet ∨ x ∈ V.toSet

def IntervalUnion.inter {α : Type} [LinearOrder α] (U V : IntervalUnion α) : IntervalUnion α

Intersection of two interval unions (the semiring multiplication).

Equations

• One or more equations did not get rendered due to their size.

theorem IntervalUnion.mem_inter {α : Type} [LinearOrder α] (U V : IntervalUnion α) (x : α) : x ∈ (U.inter V).toSet ↔ x ∈ U.toSet ∧ x ∈ V.toSet

def IntervalUnion.diff {α : Type} [LinearOrder α] (U V : IntervalUnion α) : IntervalUnion α

Set difference of two interval unions (the semiring monus).

Equations

• One or more equations did not get rendered due to their size.

theorem IntervalUnion.mem_diff {α : Type} [LinearOrder α] (U V : IntervalUnion α) (x : α) : x ∈ (U.diff V).toSet ↔ x ∈ U.toSet ∧ x ∉ V.toSet

@[implicit_reducible]

instance instZeroIntervalUnion {α : Type} [LinearOrder α] : Zero (IntervalUnion α)

Equations

• instZeroIntervalUnion = { zero := { intervals := [], pairwise_disjoint := ⋯, pairwise_before := ⋯ } }

@[implicit_reducible]

instance instOneIntervalUnionOfBoundedOrder {α : Type} [LinearOrder α] [BoundedOrder α] : One (IntervalUnion α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instAddIntervalUnion {α : Type} [LinearOrder α] : Add (IntervalUnion α)

Equations

• instAddIntervalUnion = { add := fun (U V : IntervalUnion α) => U.union V }

@[implicit_reducible]

instance instMulIntervalUnion {α : Type} [LinearOrder α] : Mul (IntervalUnion α)

Equations

• instMulIntervalUnion = { mul := fun (U V : IntervalUnion α) => U.inter V }

@[implicit_reducible]

instance instSubIntervalUnion {α : Type} [LinearOrder α] : Sub (IntervalUnion α)

Equations

• instSubIntervalUnion = { sub := fun (U V : IntervalUnion α) => U.diff V }

@[implicit_reducible]

instance instAddMonoidIntervalUnionOfDenselyOrdered {α : Type} [LinearOrder α] [DenselyOrdered α] : AddMonoid (IntervalUnion α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instCommSemiringIntervalUnionOfDenselyOrderedOfBoundedOrder {α : Type} [LinearOrder α] [DenselyOrdered α] [BoundedOrder α] : CommSemiring (IntervalUnion α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instSemiringWithMonusIntervalUnionOfDenselyOrderedOfBoundedOrder {α : Type} [LinearOrder α] [DenselyOrdered α] [BoundedOrder α] : SemiringWithMonus (IntervalUnion α)

Interval unions over a dense bounded linear order form a commutative m-semiring, with union as addition, intersection as multiplication, set inclusion as natural order, and set difference as monus.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instCommSemiringWithMonusIntervalUnionOfDenselyOrderedOfBoundedOrder {α : Type} [LinearOrder α] [DenselyOrdered α] [BoundedOrder α] : CommSemiringWithMonus (IntervalUnion α)

Equations

• instCommSemiringWithMonusIntervalUnionOfDenselyOrderedOfBoundedOrder = { toSemiringWithMonus := instSemiringWithMonusIntervalUnionOfDenselyOrderedOfBoundedOrder, mul_comm := ⋯ }

theorem IntervalUnion.absorptive {α : Type} [LinearOrder α] [DenselyOrdered α] [BoundedOrder α] : _root_.absorptive (IntervalUnion α)

The interval-union semiring is absorptive: the multiplicative identity (the whole space) absorbs any element under addition (union).

theorem IntervalUnion.mul_sub_left_distributive {α : Type} [LinearOrder α] [DenselyOrdered α] [BoundedOrder α] : _root_.mul_sub_left_distributive (IntervalUnion α)

Left-distributivity of multiplication (intersection) over monus (set difference): A ∩ (B \ C) = (A ∩ B) \ (A ∩ C).

theorem IntervalUnion.idempotent {α : Type} [LinearOrder α] [DenselyOrdered α] [BoundedOrder α] : _root_.idempotent (IntervalUnion α)

The interval-union semiring is idempotent: a + a = a (derived from absorptivity).

instance instNontrivialIntervalUnionOfBoundedOrder {α : Type} [LinearOrder α] [BoundedOrder α] : Nontrivial (IntervalUnion α)

instance IntervalUnion.instCharPZero {α : Type} [LinearOrder α] [DenselyOrdered α] [BoundedOrder α] : CharP (IntervalUnion α) 0

The interval-union semiring has characteristic 0 in the CharP sense: it is idempotent and nontrivial (the empty list differs from the singleton [⊥,⊤]), so every positive natural-number cast equals 1.

@[implicit_reducible]

noncomputable instance instSemiringWithMonusIntervalUnionEReal : SemiringWithMonus (IntervalUnion EReal)

The interval-union semiring over the extended reals [-∞, +∞].

Equations

• instSemiringWithMonusIntervalUnionEReal = inferInstance

@[implicit_reducible]

noncomputable instance instCommSemiringWithMonusIntervalUnionEReal : CommSemiringWithMonus (IntervalUnion EReal)

Equations

• instCommSemiringWithMonusIntervalUnionEReal = inferInstance

@[implicit_reducible]

instance instSemiringWithMonusIntervalUnionWithBotWithTopRat : SemiringWithMonus (IntervalUnion (WithBot (WithTop ℚ)))

The interval-union semiring over the extended rationals.

Equations

• instSemiringWithMonusIntervalUnionWithBotWithTopRat = inferInstance

@[implicit_reducible]

instance instCommSemiringWithMonusIntervalUnionWithBotWithTopRat : CommSemiringWithMonus (IntervalUnion (WithBot (WithTop ℚ)))

Equations

• instCommSemiringWithMonusIntervalUnionWithBotWithTopRat = inferInstance

Homomorphism from BoolFunc Y to IntervalUnion

For any assignment ν : Y → IntervalUnion β with Y finite, there is an m-semiring homomorphism BoolFunc Y →+* IntervalUnion β sending each variable to its assigned interval union.

Construction. For f ∈ BoolFunc Y, write f in disjunctive normal form over the finite variable set Y: f = ⋁_σ (⋀_i var_i^{σ(i)}), where σ : Y → Bool ranges over assignments with f σ = true and var_i^true = var_i, var_i^false = 1 - var_i. Define evalBF ν f := ∑_σ (if f σ then atomIU ν σ else 0) where atomIU ν σ := ∏_i (if σ i then ν i else 1 - ν i). This is a finite Boolean combination of the ν(i)'s, hence lies in IntervalUnion β.

The correctness rests on the set-theoretic characterisation mem_atomIU_iff_sig: x ∈ (atomIU ν σ).toSet iff σ is the ν-signature of x, where the ν-signature sigOf ν x sends each i to decide (x ∈ ν i). This yields (evalBF ν f).toSet = {x : β | f (sigOf ν x) = true} (evalBF_toSet), from which preservation of 0, 1, +, *, monus, and the variable mapping all follow.

For infinite Y, no such homomorphism exists in general: the set {x | f(τ_x) = true} need not be a finite union of intervals when f depends non-trivially on infinitely many variables. So Fintype Y is essential.

theorem IntervalUnion.homomorphism_from_BoolFunc (β : Type) [LinearOrder β] [DenselyOrdered β] [BoundedOrder β] (Y : Type) [Fintype Y] [DecidableEq Y] (ν : Y → IntervalUnion β) : ∃ (h : SemiringWithMonusHom (BoolFunc Y) (IntervalUnion β)), ∀ (i : Y), (fun (x : BoolFunc Y) => h.toRingHom x) (BoolFunc.var i) = ν i

For any assignment ν : Y → IntervalUnion β with Y finite, there is an m-semiring homomorphism BoolFunc Y →+* IntervalUnion β sending each variable BoolFunc.var i to ν i. The homomorphism is the DNF evaluation evalBF: f ↦ ∑_σ (if f σ then atomIU ν σ else 0).

theorem IntervalUnion.homomorphism_from_BoolFunc_rat (Y : Type) [Fintype Y] [DecidableEq Y] (ν : Y → IntervalUnion (WithBot (WithTop ℚ))) : ∃ (h : SemiringWithMonusHom (BoolFunc Y) (IntervalUnion (WithBot (WithTop ℚ)))), ∀ (i : Y), (fun (x : BoolFunc Y) => h.toRingHom x) (BoolFunc.var i) = ν i

Specialisation of IntervalUnion.homomorphism_from_BoolFunc to the extended rationals.

Home · Documentation · Publications · Contributors · Source · Cite