Relational vocabulary for nonempty intervals

[All83] [KR93] [Kle94] [Pan03] [Sag86] [Smi97]

Extends mathlib's NonemptyInterval with the relational algebra linguistic semantics consumes: overlap, precedence, meets, plus the nuclear cluster needed by aspectual semantics (final subinterval, initial overlap, isAfter/isBefore). Consumed as the time axis by tense, aspect, and event semantics, and as the timing tier by autosegmental phonology ([Sag86]).

Containment, the subinterval order, and point intervals are mathlib's own API: t ∈ i (mem_def), i₁ ≤ i₂ (le_def), i₁ < i₂ (strict containment, see lt_def), pure t.

Generalized intervals with open/closed boundaries ([Rou26]) live with their consuming study in Studies/Rouillard2026.lean.

Relational vocabulary

def NonemptyInterval.overlaps {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : Prop

Intervals overlap: neither lies strictly beyond the other.

Equations

• i₁.overlaps i₂ = (i₁.toProd.1 ≤ i₂.toProd.2 ∧ i₂.toProd.1 ≤ i₁.toProd.2)

def NonemptyInterval.meets {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : Prop

i₁ meets i₂ (i₁ ends exactly when i₂ starts).

Equations

• i₁.meets i₂ = (i₁.toProd.2 = i₂.toProd.1)

def NonemptyInterval.IsPoint {α : Type u_1} [LE α] (i : NonemptyInterval α) : Prop

An interval is a point iff its endpoints coincide. The atomic case in the time dimension — used by Bennett-Partee 1972 strict subinterval property and Zhao 2025 ATOM-DIST_t at the atomic granularity.

Equations

• i.IsPoint = (i.toProd.1 = i.toProd.2)

def NonemptyInterval.isAfter {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : Prop

i₁ is entirely after i₂ (i₁ starts at or after i₂ finishes).

Equations

• i₁.isAfter i₂ = (i₂.toProd.2 ≤ i₁.toProd.1)

def NonemptyInterval.isBefore {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : Prop

i₁ is entirely before i₂.

Equations

• i₁.isBefore i₂ = (i₁.toProd.2 ≤ i₂.toProd.1)

def NonemptyInterval.finalSubinterval {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : Prop

Final subinterval: i₁ ⊆ i₂ and they share the same right endpoint. [Pan03]: PTS(i', i) iff i is a final subinterval of i'.

Equations

• i₁.finalSubinterval i₂ = (i₁ ≤ i₂ ∧ i₁.toProd.2 = i₂.toProd.2)

theorem NonemptyInterval.isAfter_iff_isBefore {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : i₁.isAfter i₂ ↔ i₂.isBefore i₁

@[implicit_reducible]

instance NonemptyInterval.instDecidableOverlaps {α : Type u_1} [LE α] [DecidableLE α] {i₁ i₂ : NonemptyInterval α} : Decidable (i₁.overlaps i₂)

Equations

• NonemptyInterval.instDecidableOverlaps = id inferInstance

@[implicit_reducible]

instance NonemptyInterval.instDecidableMeets {α : Type u_1} [LE α] [DecidableEq α] {i₁ i₂ : NonemptyInterval α} : Decidable (i₁.meets i₂)

Equations

• NonemptyInterval.instDecidableMeets = id inferInstance

@[implicit_reducible]

instance NonemptyInterval.instDecidableIsPoint {α : Type u_1} [LE α] [DecidableEq α] {i : NonemptyInterval α} : Decidable i.IsPoint

Equations

• NonemptyInterval.instDecidableIsPoint = id inferInstance

@[implicit_reducible]

instance NonemptyInterval.instDecidableIsAfter {α : Type u_1} [LE α] [DecidableLE α] {i₁ i₂ : NonemptyInterval α} : Decidable (i₁.isAfter i₂)

Equations

• NonemptyInterval.instDecidableIsAfter = id inferInstance

@[implicit_reducible]

instance NonemptyInterval.instDecidableIsBefore {α : Type u_1} [LE α] [DecidableLE α] {i₁ i₂ : NonemptyInterval α} : Decidable (i₁.isBefore i₂)

Equations

• NonemptyInterval.instDecidableIsBefore = id inferInstance

@[implicit_reducible]

instance NonemptyInterval.instDecidableFinalSubinterval {α : Type u_1} [LE α] [DecidableLE α] [DecidableEq α] {i₁ i₂ : NonemptyInterval α} : Decidable (i₁.finalSubinterval i₂)

Equations

• NonemptyInterval.instDecidableFinalSubinterval = id inferInstance

theorem NonemptyInterval.le_of_finalSubinterval {α : Type u_1} [LE α] {i₁ i₂ : NonemptyInterval α} (h : i₁.finalSubinterval i₂) : i₁ ≤ i₂

Final subintervals are subintervals.

@[simp]

theorem NonemptyInterval.overlaps_refl {α : Type u_1} [LE α] (i : NonemptyInterval α) : i.overlaps i

Overlap is reflexive: every interval overlaps itself.

theorem NonemptyInterval.overlaps_symm {α : Type u_1} [LE α] {i₁ i₂ : NonemptyInterval α} (h : i₁.overlaps i₂) : i₂.overlaps i₁

Overlap is symmetric.

theorem NonemptyInterval.overlaps_comm {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : i₁.overlaps i₂ ↔ i₂.overlaps i₁

Overlap is symmetric (iff version).

@[implicit_reducible]

instance NonemptyInterval.instDecidableMemOfDecidableLE_linglib {α : Type u_1} [Preorder α] {a : α} {s : NonemptyInterval α} [DecidableLE α] : Decidable (a ∈ s)

Membership in a nonempty interval is decidable when ≤ is.

Equations

• NonemptyInterval.instDecidableMemOfDecidableLE_linglib = decidable_of_iff' (s.toProd.1 ≤ a ∧ a ≤ s.toProd.2) ⋯

@[implicit_reducible]

instance NonemptyInterval.instDecidableLtOfDecidableLE_linglib {α : Type u_1} [Preorder α] {s t : NonemptyInterval α} [DecidableLE α] : Decidable (s < t)

Strict containment is decidable when ≤ is.

Equations

• NonemptyInterval.instDecidableLtOfDecidableLE_linglib = decidable_of_iff' (s ≤ t ∧ ¬t ≤ s) ⋯

def NonemptyInterval.precedes {α : Type u_1} [Preorder α] (i₁ i₂ : NonemptyInterval α) : Prop

i₁ precedes i₂ (no overlap, i₁ entirely before i₂).

Equations

• i₁.precedes i₂ = (i₁.toProd.2 < i₂.toProd.1)

def NonemptyInterval.initialOverlap {α : Type u_1} [Preorder α] (i₁ i₂ : NonemptyInterval α) : Prop

Initial overlap (∂): i₁ and i₂ overlap, and the start of i₂ is in i₁. [Pan03]: i ∂τ(e) — the beginning of the eventuality is included in the reference interval but the end may not be. [Smi97]: the neutral viewpoint uses the same interval relation.

Equations

• i₁.initialOverlap i₂ = (i₁.overlaps i₂ ∧ i₂.toProd.1 ∈ i₁)

@[implicit_reducible]

instance NonemptyInterval.instDecidableInitialOverlapOfDecidableLE {α : Type u_1} [Preorder α] [DecidableLE α] {i₁ i₂ : NonemptyInterval α} : Decidable (i₁.initialOverlap i₂)

Equations

• NonemptyInterval.instDecidableInitialOverlapOfDecidableLE = id inferInstance

@[implicit_reducible]

instance NonemptyInterval.instDecidablePrecedesOfDecidableLE {α : Type u_1} [Preorder α] [DecidableLE α] {i₁ i₂ : NonemptyInterval α} : Decidable (i₁.precedes i₂)

Equations

• NonemptyInterval.instDecidablePrecedesOfDecidableLE = id (decidable_of_iff' (i₁.toProd.2 ≤ i₂.toProd.1 ∧ ¬i₂.toProd.1 ≤ i₁.toProd.2) ⋯)

theorem NonemptyInterval.finalSubinterval_refl {α : Type u_1} [Preorder α] (i : NonemptyInterval α) : i.finalSubinterval i

Every interval is a final subinterval of itself.

theorem NonemptyInterval.overlaps_of_le {α : Type u_1} [Preorder α] {i₁ i₂ : NonemptyInterval α} (h : i₁ ≤ i₂) : i₁.overlaps i₂

Subintervals overlap their containing intervals.

theorem NonemptyInterval.precedes_irrefl {α : Type u_1} [Preorder α] (i : NonemptyInterval α) : ¬i.precedes i

Precedence is irreflexive: no interval precedes itself.

theorem NonemptyInterval.precedes_asymm {α : Type u_1} [Preorder α] {i₁ i₂ : NonemptyInterval α} (h : i₁.precedes i₂) : ¬i₂.precedes i₁

Precedence is asymmetric.

theorem NonemptyInterval.precedes_trans {α : Type u_1} [Preorder α] {i₁ i₂ i₃ : NonemptyInterval α} (h₁₂ : i₁.precedes i₂) (h₂₃ : i₂.precedes i₃) : i₁.precedes i₃

Precedence is transitive.

theorem NonemptyInterval.precedes_not_overlaps {α : Type u_1} [Preorder α] {i₁ i₂ : NonemptyInterval α} (h : i₁.precedes i₂) : ¬i₁.overlaps i₂

Precedence and overlap are mutually exclusive.

theorem NonemptyInterval.lt_def {α : Type u_1} [LinearOrder α] {i₁ i₂ : NonemptyInterval α} : i₁ < i₂ ↔ i₁ ≤ i₂ ∧ (i₂.toProd.1 < i₁.toProd.1 ∨ i₁.toProd.2 < i₂.toProd.2)

Strict containment unfolded to endpoints: i₁ < i₂ iff i₁ ≤ i₂ with at least one strictly interior endpoint. The shape the IMPF semantics consumes (reference time PROPERLY inside event runtime).

theorem NonemptyInterval.overlaps_not_transitive : ¬∀ (i₁ i₂ i₃ : NonemptyInterval ℤ), i₁.overlaps i₂ → i₂.overlaps i₃ → i₁.overlaps i₃

Overlap is NOT transitive: [0,1] overlaps [1,2] and [1,2] overlaps [2,3], but [0,1] does not overlap [2,3].

This is the cornerstone property that distinguishes overlap from simultaneity (identity) and makes the No-Crossing Constraint derivable from temporal precedence alone ([Sag86] §5.2.3, fn. 6).

Boundary type (open/closed endpoints)

inductive NonemptyInterval.BoundaryType : Type

Whether an interval's boundary is included (closed) or excluded (open). [Rou26] §2.2.4: the distinction between closed and open times is central to deriving the polarity sensitivity of G-TIAs. Event runtimes are closed; PTSs are open intervals.

Consumed by GInterval (in Studies/Rouillard2026.lean).

• closed : BoundaryType
• open_ : BoundaryType

@[implicit_reducible]

instance NonemptyInterval.instDecidableEqBoundaryType : DecidableEq BoundaryType

Equations

• NonemptyInterval.instDecidableEqBoundaryType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NonemptyInterval.instReprBoundaryType : Repr BoundaryType

Equations

• NonemptyInterval.instReprBoundaryType = { reprPrec := NonemptyInterval.instReprBoundaryType.repr }

def NonemptyInterval.instReprBoundaryType.repr : BoundaryType → ℕ → Std.Format

Equations

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