Allen's interval relations

[All83]

The thirteen jointly-exhaustive, pairwise-disjoint relations that can hold between two intervals on a linear order. Originally introduced by James F. Allen for temporal reasoning in AI, this is the canonical relation algebra that Reichenbach, Klein, Pancheva, and Declerck all draw from — every temporal predicate in linglib is a (possibly singleton) subset of these thirteen atomic relations.

Atom	Symbol	Inverse	Defining inequality
precedes	p	precededBy	i.snd < j.fst
meets	m	metBy	i.snd = j.fst
overlaps	o	overlappedBy	i.fst < j.fst < i.snd < j.snd
finishedBy	F	finishes	i.fst < j.fst, i.snd = j.snd
contains	D	during	i.fst < j.fst, j.snd < i.snd
starts	s	startedBy	i.fst = j.fst, i.snd < j.snd
equal	e	equal	i.fst = j.fst, i.snd = j.snd
startedBy	S	starts	i.fst = j.fst, j.snd < i.snd
during	d	contains	j.fst < i.fst, i.snd < j.snd
finishes	f	finishedBy	j.fst < i.fst, i.snd = j.snd
overlappedBy	O	overlaps	j.fst < i.fst < j.snd < i.snd
metBy	M	meets	i.fst = j.snd
precededBy	P	precedes	j.snd < i.fst

For any two intervals on a linear order, at least one atomic relation holds (holds_exists). When both intervals are non-degenerate (fst < snd), exactly one holds (holds_unique). The non-degeneracy hypothesis matches [All83]'s original setup: on point intervals at the same location, meets, metBy, and equal all hold simultaneously, so uniqueness genuinely fails on degenerate inputs. Both proofs use mathlib's order decision procedure for LinearOrder.

The NonemptyInterval relational vocabulary (the containment order ≤, isBefore, finalSubinterval, …) consists of unions of atomic Allen relations — see the Predicate Bridges section.

The Allen algebra also has a 13×13 composition table giving, for each pair (r, s), the set of relations consistent with i r j ∧ j s k. We provide identity laws and the principal compositions used by tense theory; the full table is left as a TODO.

Core.Order.Relation (in Relation.lean) is the point analogue (operating on Time × Time); on point intervals it collapses to {precedes, equal, precededBy} (the only three Allen relations consistent with zero-length intervals).

inductive AllenRelation : Type

The thirteen atomic Allen relations between two intervals on a linear order ([All83]). Naming follows Allen 1983; each atom has an inverse obtained by swapping the two interval arguments — see AllenRelation.inverse.

• precedes : AllenRelation

  i.snd < j.fst — i ends strictly before j starts.

• meets : AllenRelation

  i.snd = j.fst — i's right endpoint is j's left endpoint.

• overlaps : AllenRelation

  i.fst < j.fst < i.snd < j.snd — proper overlap on the right of i.

• finishedBy : AllenRelation

  i.fst < j.fst ∧ i.snd = j.snd — j is a final subinterval of i.

• contains : AllenRelation

  i.fst < j.fst ∧ j.snd < i.snd — j strictly inside i.

• starts : AllenRelation

  i.fst = j.fst ∧ i.snd < j.snd — i is a proper initial subinterval of j.

• equal : AllenRelation

  i.fst = j.fst ∧ i.snd = j.snd — identical intervals.

• startedBy : AllenRelation

  i.fst = j.fst ∧ j.snd < i.snd — j is a proper initial subinterval of i.

• during : AllenRelation

  j.fst < i.fst ∧ i.snd < j.snd — i strictly inside j.

• finishes : AllenRelation

  j.fst < i.fst ∧ i.snd = j.snd — i is a final subinterval of j.

• overlappedBy : AllenRelation

  j.fst < i.fst < j.snd < i.snd — proper overlap on the left of i.

• metBy : AllenRelation

  i.fst = j.snd — i's left endpoint is j's right endpoint.

• precededBy : AllenRelation

  j.snd < i.fst — j ends strictly before i starts.

@[implicit_reducible]

instance instDecidableEqAllenRelation : DecidableEq AllenRelation

Equations

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

def instReprAllenRelation.repr : AllenRelation → ℕ → Std.Format

Equations

• instReprAllenRelation.repr AllenRelation.precedes prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.precedes")).group prec✝
• instReprAllenRelation.repr AllenRelation.meets prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.meets")).group prec✝
• instReprAllenRelation.repr AllenRelation.overlaps prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.overlaps")).group prec✝
• instReprAllenRelation.repr AllenRelation.finishedBy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.finishedBy")).group prec✝
• instReprAllenRelation.repr AllenRelation.contains prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.contains")).group prec✝
• instReprAllenRelation.repr AllenRelation.starts prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.starts")).group prec✝
• instReprAllenRelation.repr AllenRelation.equal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.equal")).group prec✝
• instReprAllenRelation.repr AllenRelation.startedBy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.startedBy")).group prec✝
• instReprAllenRelation.repr AllenRelation.during prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.during")).group prec✝
• instReprAllenRelation.repr AllenRelation.finishes prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.finishes")).group prec✝
• instReprAllenRelation.repr AllenRelation.overlappedBy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.overlappedBy")).group prec✝
• instReprAllenRelation.repr AllenRelation.metBy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.metBy")).group prec✝
• instReprAllenRelation.repr AllenRelation.precededBy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AllenRelation.precededBy")).group prec✝

@[implicit_reducible]

instance instReprAllenRelation : Repr AllenRelation

Equations

• instReprAllenRelation = { reprPrec := instReprAllenRelation.repr }

@[implicit_reducible]

instance instInhabitedAllenRelation : Inhabited AllenRelation

Equations

• instInhabitedAllenRelation = { default := instInhabitedAllenRelation.default }

def AllenRelation.inverse : AllenRelation → AllenRelation

The inverse of an atom: the relation that holds when the two intervals are swapped. equal is the unique self-inverse atom.

Equations

• AllenRelation.precedes.inverse = AllenRelation.precededBy
• AllenRelation.meets.inverse = AllenRelation.metBy
• AllenRelation.overlaps.inverse = AllenRelation.overlappedBy
• AllenRelation.finishedBy.inverse = AllenRelation.finishes
• AllenRelation.contains.inverse = AllenRelation.during
• AllenRelation.starts.inverse = AllenRelation.startedBy
• AllenRelation.equal.inverse = AllenRelation.equal
• AllenRelation.startedBy.inverse = AllenRelation.starts
• AllenRelation.during.inverse = AllenRelation.contains
• AllenRelation.finishes.inverse = AllenRelation.finishedBy
• AllenRelation.overlappedBy.inverse = AllenRelation.overlaps
• AllenRelation.metBy.inverse = AllenRelation.meets
• AllenRelation.precededBy.inverse = AllenRelation.precedes

@[simp]

theorem AllenRelation.inverse_inverse (r : AllenRelation) : r.inverse.inverse = r

theorem AllenRelation.inverse_eq_self_iff (r : AllenRelation) : r.inverse = r ↔ r = equal

equal is the unique self-inverse atom.

def AllenRelation.all : List AllenRelation

The set of all thirteen atoms — useful for stating exhaustiveness.

Equations

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

theorem AllenRelation.all_length : all.length = 13

theorem AllenRelation.mem_all (r : AllenRelation) : r ∈ all

def AllenRelation.holds {Time : Type u_1} [LinearOrder Time] : AllenRelation → NonemptyInterval Time → NonemptyInterval Time → Prop

r.holds i j is true iff atomic Allen relation r is the one that holds between intervals i and j. The defining inequalities follow [All83].

Equations

• AllenRelation.precedes.holds x✝¹ x✝ = (x✝¹.toProd.2 < x✝.toProd.1)
• AllenRelation.meets.holds x✝¹ x✝ = (x✝¹.toProd.2 = x✝.toProd.1)
• AllenRelation.overlaps.holds x✝¹ x✝ = (x✝¹.toProd.1 < x✝.toProd.1 ∧ x✝.toProd.1 < x✝¹.toProd.2 ∧ x✝¹.toProd.2 < x✝.toProd.2)
• AllenRelation.finishedBy.holds x✝¹ x✝ = (x✝¹.toProd.1 < x✝.toProd.1 ∧ x✝¹.toProd.2 = x✝.toProd.2)
• AllenRelation.contains.holds x✝¹ x✝ = (x✝¹.toProd.1 < x✝.toProd.1 ∧ x✝.toProd.2 < x✝¹.toProd.2)
• AllenRelation.starts.holds x✝¹ x✝ = (x✝¹.toProd.1 = x✝.toProd.1 ∧ x✝¹.toProd.2 < x✝.toProd.2)
• AllenRelation.equal.holds x✝¹ x✝ = (x✝¹.toProd.1 = x✝.toProd.1 ∧ x✝¹.toProd.2 = x✝.toProd.2)
• AllenRelation.startedBy.holds x✝¹ x✝ = (x✝¹.toProd.1 = x✝.toProd.1 ∧ x✝.toProd.2 < x✝¹.toProd.2)
• AllenRelation.during.holds x✝¹ x✝ = (x✝.toProd.1 < x✝¹.toProd.1 ∧ x✝¹.toProd.2 < x✝.toProd.2)
• AllenRelation.finishes.holds x✝¹ x✝ = (x✝.toProd.1 < x✝¹.toProd.1 ∧ x✝¹.toProd.2 = x✝.toProd.2)
• AllenRelation.overlappedBy.holds x✝¹ x✝ = (x✝.toProd.1 < x✝¹.toProd.1 ∧ x✝¹.toProd.1 < x✝.toProd.2 ∧ x✝.toProd.2 < x✝¹.toProd.2)
• AllenRelation.metBy.holds x✝¹ x✝ = (x✝¹.toProd.1 = x✝.toProd.2)
• AllenRelation.precededBy.holds x✝¹ x✝ = (x✝.toProd.2 < x✝¹.toProd.1)

theorem AllenRelation.holds_inverse {Time : Type u_1} [LinearOrder Time] (r : AllenRelation) (i j : NonemptyInterval Time) : r.holds i j ↔ r.inverse.holds j i

Holds is symmetric under inversion: r holds of (i, j) iff r⁻¹ holds of (j, i). This is the central algebraic property of the inverse operation.

def AllenRelation.witness {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : { r : AllenRelation // r.holds i j }

Exhaustiveness (constructive witness): every interval pair satisfies at least one atomic Allen relation, computably. The case-split mirrors [All83]'s exhaustive enumeration: trichotomy on i.snd vs j.fst, then i.fst vs j.snd, then refinement on i.fst vs j.fst and i.snd vs j.snd. Used to derive the constructive NonemptyInterval.allenRel projection.

Equations

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

theorem AllenRelation.holds_exists {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : ∃ (r : AllenRelation), r.holds i j

Exhaustiveness (existence half): every interval pair satisfies at least one atomic Allen relation. Existential projection of witness.

Each non-degenerate interval pair (i, j) has a four-tuple signature: the pairwise sgn (lt/eq/gt) of every endpoint of i with every endpoint of j. The thirteen Allen atoms correspond bijectively to thirteen of the 81 possible signature tuples (the other 68 are excluded by i.fst < i.snd and j.fst < j.snd). Factoring uniqueness through this signature reduces the 169-case cross-product cases r₁ <;> cases r₂ (which needs 6× the default heartbeat budget) into two 13-case lemmas.

def AllenRelation.sgn {Time : Type u_1} [LinearOrder Time] (a b : Time) : Ordering

Three-way sign of a vs b on a linear order.

Equations

• AllenRelation.sgn a b = if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt

theorem AllenRelation.sgn_lt {Time : Type u_1} [LinearOrder Time] {a b : Time} (h : a < b) : sgn a b = Ordering.lt

theorem AllenRelation.sgn_eq {Time : Type u_1} [LinearOrder Time] {a b : Time} (h : a = b) : sgn a b = Ordering.eq

theorem AllenRelation.sgn_gt {Time : Type u_1} [LinearOrder Time] {a b : Time} (h : b < a) : sgn a b = Ordering.gt

def AllenRelation.signature {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : Ordering × Ordering × Ordering × Ordering

The 4-tuple signature of an interval pair: pairwise comparisons of (i.fst vs j.fst, i.fst vs j.snd, i.snd vs j.fst, i.snd vs j.snd).

Equations

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

def AllenRelation.expectedSig : AllenRelation → Ordering × Ordering × Ordering × Ordering

The expected signature of each Allen atom — the unique 4-tuple of pairwise endpoint comparisons forced by the atom's defining inequalities together with non-degeneracy of both intervals.

Equations

• AllenRelation.precedes.expectedSig = (Ordering.lt, Ordering.lt, Ordering.lt, Ordering.lt)
• AllenRelation.meets.expectedSig = (Ordering.lt, Ordering.lt, Ordering.eq, Ordering.lt)
• AllenRelation.overlaps.expectedSig = (Ordering.lt, Ordering.lt, Ordering.gt, Ordering.lt)
• AllenRelation.finishedBy.expectedSig = (Ordering.lt, Ordering.lt, Ordering.gt, Ordering.eq)
• AllenRelation.contains.expectedSig = (Ordering.lt, Ordering.lt, Ordering.gt, Ordering.gt)
• AllenRelation.starts.expectedSig = (Ordering.eq, Ordering.lt, Ordering.gt, Ordering.lt)
• AllenRelation.equal.expectedSig = (Ordering.eq, Ordering.lt, Ordering.gt, Ordering.eq)
• AllenRelation.startedBy.expectedSig = (Ordering.eq, Ordering.lt, Ordering.gt, Ordering.gt)
• AllenRelation.during.expectedSig = (Ordering.gt, Ordering.lt, Ordering.gt, Ordering.lt)
• AllenRelation.finishes.expectedSig = (Ordering.gt, Ordering.lt, Ordering.gt, Ordering.eq)
• AllenRelation.overlappedBy.expectedSig = (Ordering.gt, Ordering.lt, Ordering.gt, Ordering.gt)
• AllenRelation.metBy.expectedSig = (Ordering.gt, Ordering.eq, Ordering.gt, Ordering.gt)
• AllenRelation.precededBy.expectedSig = (Ordering.gt, Ordering.gt, Ordering.gt, Ordering.gt)

theorem AllenRelation.expectedSig_injective (r₁ r₂ : AllenRelation) (h : r₁.expectedSig = r₂.expectedSig) : r₁ = r₂

The thirteen expected signatures are pairwise distinct: any two atoms with the same signature are equal. (13-case diagonal + 156 trivial simp contradictions on Ordering constructor mismatch.)

theorem AllenRelation.signature_of_holds {Time : Type u_1} [LinearOrder Time] (r : AllenRelation) (i j : NonemptyInterval Time) (hi : i.toProd.1 < i.toProd.2) (hj : j.toProd.1 < j.toProd.2) (h : r.holds i j) : signature i j = r.expectedSig

If atom r holds of a non-degenerate interval pair, the pair's signature is exactly r.expectedSig. (13 cases, each computing four sgn components via Prod.ext + the appropriate sgn_* lemma + order.)

theorem AllenRelation.holds_unique {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) (hi : i.toProd.1 < i.toProd.2) (hj : j.toProd.1 < j.toProd.2) (r₁ r₂ : AllenRelation) (h₁ : r₁.holds i j) (h₂ : r₂.holds i j) : r₁ = r₂

Uniqueness (pairwise disjointness): on non-degenerate intervals (i.fst < i.snd and j.fst < j.snd), at most one atom holds of a given pair. Combined with holds_exists, this gives the key property of Allen's algebra: the thirteen atoms partition the space of (proper) interval pairs into thirteen exhaustive, pairwise-disjoint cases.

The non-degeneracy hypothesis is essential: at a single time point t, taking i = j = ⟨⟨t, t⟩, le_refl t⟩ makes meets (t = t), metBy (t = t), and equal (t = t ∧ t = t) all hold simultaneously. [All83] sidesteps this by assuming strict intervals throughout.

Proof: factor through the 4-tuple signature. Both r₁ and r₂ force the same signature (signature_of_holds), and distinct atoms have distinct signatures (expectedSig_injective).

Many natural temporal predicates correspond to unions of Allen atoms — "at least one of these atoms holds." We express this uniformly via holdsIn, and name the atom-sets that appear in the NonemptyInterval predicate API. Each existing NonemptyInterval predicate is then a projection from a named atom-set: this exposes the algebraic structure (S₁ ⊆ S₂ ⇒ holdsIn S₁ ⇒ holdsIn S₂) and grounds each predicate in the Allen algebra by construction.

Singleton sets (`precedesSet`, `meetsSet`) recover individual atoms
as predicates; longer sets give the union predicates that linguistic
theory typically works with. The atom sets are first-class data, so
later modules (`Domain`, `RelationOrigin`, …) can manipulate them
uniformly without committing to a specific predicate at the
type level. 

def AllenRelation.holdsIn {Time : Type u_1} [LinearOrder Time] (S : List AllenRelation) (i j : NonemptyInterval Time) : Prop

"holdsIn S i j" iff some atom in the list S is the relation holding between i and j. Singleton lists yield exact-atom predicates; longer lists yield union predicates.

Equations

• AllenRelation.holdsIn S i j = ∃ r ∈ S, r.holds i j

@[simp]

theorem AllenRelation.holdsIn_nil {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : holdsIn [] i j ↔ False

@[simp]

theorem AllenRelation.holdsIn_singleton {Time : Type u_1} [LinearOrder Time] (r : AllenRelation) (i j : NonemptyInterval Time) : holdsIn [r] i j ↔ r.holds i j

theorem AllenRelation.holdsIn_cons {Time : Type u_1} [LinearOrder Time] (r : AllenRelation) (S : List AllenRelation) (i j : NonemptyInterval Time) : holdsIn (r :: S) i j ↔ r.holds i j ∨ holdsIn S i j

theorem AllenRelation.holdsIn_mono {Time : Type u_1} [LinearOrder Time] {S₁ S₂ : List AllenRelation} (h : ∀ r ∈ S₁, r ∈ S₂) (i j : NonemptyInterval Time) : holdsIn S₁ i j → holdsIn S₂ i j

Subset monotonicity: enlarging the atom set weakens the predicate.

def AllenRelation.precedesSet : List AllenRelation

{precedes} — i.e., NonemptyInterval.precedes.

Equations

• AllenRelation.precedesSet = [AllenRelation.precedes]

def AllenRelation.equalSet : List AllenRelation

{equal} — interval coincidence; on point intervals collapses to point equality, the relation behind Reichenbach's R = P etc.

Equations

• AllenRelation.equalSet = [AllenRelation.equal]

def AllenRelation.meetsSet : List AllenRelation

{meets} — i.e., NonemptyInterval.meets.

Equations

• AllenRelation.meetsSet = [AllenRelation.meets]

def AllenRelation.beforeSet : List AllenRelation

{precedes, meets} — i.e., NonemptyInterval.isBefore: strict precedence plus meeting (the conflation i.snd ≤ j.fst represents).

Equations

• AllenRelation.beforeSet = [AllenRelation.precedes, AllenRelation.meets]

def AllenRelation.afterSet : List AllenRelation

{precededBy, metBy} — i.e., NonemptyInterval.isAfter.

Equations

• AllenRelation.afterSet = [AllenRelation.precededBy, AllenRelation.metBy]

def AllenRelation.containmentSet : List AllenRelation

{starts, equal, finishes, during} — i.e., the containment order i ≤ j: every way i can be contained in j.

Equations

• AllenRelation.containmentSet = [AllenRelation.starts, AllenRelation.equal, AllenRelation.finishes, AllenRelation.during]

def AllenRelation.properContainmentSet : List AllenRelation

{starts, finishes, during} — i.e., strict containment i < j: proper containment (excludes equal).

Equations

• AllenRelation.properContainmentSet = [AllenRelation.starts, AllenRelation.finishes, AllenRelation.during]

def AllenRelation.finalContainmentSet : List AllenRelation

{finishes, equal} — i.e., NonemptyInterval.finalSubinterval: contained and sharing the right endpoint.

Equations

• AllenRelation.finalContainmentSet = [AllenRelation.finishes, AllenRelation.equal]

def AllenRelation.reverseContainmentSet : List AllenRelation

{startedBy, equal, finishedBy, contains} — the inverse of containmentSet: every way i can contain j.

Equations

• AllenRelation.reverseContainmentSet = [AllenRelation.startedBy, AllenRelation.equal, AllenRelation.finishedBy, AllenRelation.contains]

def AllenRelation.overlapSet : List AllenRelation

Eleven atoms — every relation except strict precedence in either direction — i.e., NonemptyInterval.overlaps's union characterization.

Equations

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

The NonemptyInterval relational vocabulary equated to projections from named Allen atom-sets via holdsIn. The singleton-atom predicates (precedes, meets) collapse to Iff.rfl; the union predicates require structural-form ↔ disjunction-form translations. These are the only place where the structural definitions in Core/Order/Interval.lean (and mathlib's containment order ≤/<) meet the Allen algebra; downstream modules should depend on the Allen side.

theorem NonemptyInterval.precedes_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : i.precedes j ↔ AllenRelation.holdsIn AllenRelation.precedesSet i j

NonemptyInterval.precedes is exactly the Allen precedes atom.

theorem NonemptyInterval.meets_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : i.meets j ↔ AllenRelation.holdsIn AllenRelation.meetsSet i j

NonemptyInterval.meets is exactly the Allen meets atom.

theorem NonemptyInterval.isBefore_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : i.isBefore j ↔ AllenRelation.holdsIn AllenRelation.beforeSet i j

NonemptyInterval.isBefore (≤) is the union {precedes, meets} — Allen's strict precedes plus meets. This conflation of two atoms into one weakened predicate is exactly the kind of imprecision the Allen algebra removes.

theorem NonemptyInterval.isAfter_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : i.isAfter j ↔ AllenRelation.holdsIn AllenRelation.afterSet i j

NonemptyInterval.isAfter is the inverse of isBefore: {precededBy, metBy}.

theorem NonemptyInterval.le_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : i ≤ j ↔ AllenRelation.holdsIn AllenRelation.containmentSet i j

The containment order i ≤ j is the union {starts, equal, finishes, during} — every way i can be contained in j without sharing the wrong boundary.

theorem NonemptyInterval.finalSubinterval_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : i.finalSubinterval j ↔ AllenRelation.holdsIn AllenRelation.finalContainmentSet i j

NonemptyInterval.finalSubinterval is the union {finishes, equal} — contained in j and sharing j's right endpoint.

theorem NonemptyInterval.lt_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : i < j ↔ AllenRelation.holdsIn AllenRelation.properContainmentSet i j

Strict containment i < j is the union {starts, finishes, during} — containment that excludes the equal case.

@[implicit_reducible]

instance AllenRelation.holds_decidable {Time : Type u_1} [LinearOrder Time] [DecidableEq Time] [DecidableRel fun (x1 x2 : Time) => x1 < x2] (r : AllenRelation) (i j : NonemptyInterval Time) : Decidable (r.holds i j)

holds is decidable on a linear order (provided < and = are).

Equations

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

The full Allen composition table assigns to each pair (r, s) the set of relations consistent with i r j ∧ j s k. The table has 169 entries and is left as a TODO. We provide the identity laws plus the principal transitive closures used by tense theory.

Convention: `holds_*_trans` reads "if r holds of (i, j) and r holds
of (j, k), then r holds of (i, k)" for the relations that are transitive. 

theorem AllenRelation.holds_equal_left {Time : Type u_1} [LinearOrder Time] {i j k : NonemptyInterval Time} (r : AllenRelation) (h₁ : equal.holds i j) (h₂ : r.holds j k) : r.holds i k

equal is a left identity: if i = j and j r k, then i r k.

theorem AllenRelation.holds_equal_right {Time : Type u_1} [LinearOrder Time] {i j k : NonemptyInterval Time} (r : AllenRelation) (h₁ : r.holds i j) (h₂ : equal.holds j k) : r.holds i k

equal is a right identity: if i r j and j = k, then i r k.

theorem AllenRelation.holds_precedes_trans {Time : Type u_1} [LinearOrder Time] {i j k : NonemptyInterval Time} (h₁ : precedes.holds i j) (h₂ : precedes.holds j k) : precedes.holds i k

precedes is transitive: i p j ∧ j p k → i p k. (The composition table entry precedes ∘ precedes is the singleton {precedes}.) The proof chains i.snd < j.fst ≤ j.snd < k.fst via j.fst_le_snd.

theorem AllenRelation.holds_during_trans {Time : Type u_1} [LinearOrder Time] {i j k : NonemptyInterval Time} (h₁ : during.holds i j) (h₂ : during.holds j k) : during.holds i k

The during relation is transitive: i ⊏ j ∧ j ⊏ k → i ⊏ k. (Composition entry during ∘ during = {during}.)

theorem AllenRelation.holds_contains_trans {Time : Type u_1} [LinearOrder Time] {i j k : NonemptyInterval Time} (h₁ : contains.holds i j) (h₂ : contains.holds j k) : contains.holds i k

The contains relation is transitive (mirror of during).

The projection from interval pairs to Allen atoms — the inverse direction of holds. Defined by the constructive AllenRelation.witness, which case-splits on endpoint trichotomies. By holds_unique, on non-degenerate intervals the projection is forced — any atom that holds equals it. Together with holdsIn, this gives a full abstraction-and-projection layer over the algebra.

def NonemptyInterval.allenRel {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : AllenRelation

The Allen atom currently holding between two intervals. Computable; extracted from the constructive AllenRelation.witness. For non-degenerate intervals this is well-defined: allenRel_unique proves every witness equals the projection.

Equations

• i.allenRel j = ↑(AllenRelation.witness i j)

theorem NonemptyInterval.allenRel_holds {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) : (i.allenRel j).holds i j

The projected atom does hold between the intervals.

theorem NonemptyInterval.allenRel_unique {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) (hi : i.toProd.1 < i.toProd.2) (hj : j.toProd.1 < j.toProd.2) {r : AllenRelation} (h : r.holds i j) : r = i.allenRel j

For non-degenerate intervals, the projection is unique: every atom that holds equals allenRel i j. This is the core "well- definedness" theorem for the projection — it justifies treating allenRel i j as the Allen relation between the two intervals.

theorem NonemptyInterval.allenRel_mem_iff_holdsIn {Time : Type u_1} [LinearOrder Time] (i j : NonemptyInterval Time) (hi : i.toProd.1 < i.toProd.2) (hj : j.toProd.1 < j.toProd.2) (S : List AllenRelation) : i.allenRel j ∈ S ↔ AllenRelation.holdsIn S i j

The projection lands in the named atom-set iff the corresponding holdsIn predicate holds. (For non-degenerate intervals; uses uniqueness to convert membership to existence.)