LeanSpec.lib.Temporal: DTG, Duration, and Interval Types

LeanSpec.lib.Temporal provides a lightweight model of temporal entities: combined date-and-time values, durations, and intervals. The design draws from ISO 8601 and RFC 3339 but is deliberately simplified — it supplies enough precision to underpin the aviation-related specifications in the tutorial (TMI slot scheduling, FPL active periods, and similar) without attempting to be a production-quality calendar library. All definitions live in the Temporal namespace.

Constants

Fundamental time-conversion constants used throughout the module.

def secondsPerMinute := 60

def minutesPerHour := 60

def secondsPerHour := secondsPerMinute * minutesPerHour

def hoursPerDay := 24

def secondsPerDay := secondsPerHour * hoursPerDay

Constant	Value	Meaning
`secondsPerMinute`	60	Seconds in one minute
`minutesPerHour`	60	Minutes in one hour
`secondsPerHour`	3 600	Seconds in one hour
`hoursPerDay`	24	Hours in one day
`secondsPerDay`	86 400	Seconds in one day

These constants are referenced by Duration.oneDay, Duration.oneHour, and any specification that needs to express time offsets in terms of human-readable units.

DTG (Date/Time Group)

A DTG represents a combined date and time as the number of seconds elapsed since the epoch (year 0 in the Gregorian calendar). Granularity is to the nearest second. The name “Date/Time Group” is borrowed from aviation and military practice where a DTG identifies a precise moment in time.

Structure definition

structure DTG where
  dtg : Nat
deriving Repr, Ord, DecidableEq

The single field dtg : Nat is the raw second count. Repr, Ord, and DecidableEq are derived automatically, giving structural equality, a total order, and a repr display for free.

`OfNat` instance

Natural number literals can be used directly as DTG values — the literal is interpreted as the number of seconds since the epoch:

instance : OfNat DTG n where
  ofNat := ⟨n⟩

Ordering instances

LT — strict less-than, delegating to Nat:

instance : LT DTG where
  lt := fun ⟨d₁⟩ ⟨d₂⟩ ↦ d₁ < d₂

Decidable <:

instance (x y : DTG) : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.dtg < y.dtg))

LE — non-strict less-than-or-equal:

instance : LE DTG where
  le := fun ⟨d₁⟩ ⟨d₂⟩ ↦ d₁ ≤ d₂

Decidable ≤:

instance (x y : DTG) : Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.dtg ≤ y.dtg))

`Min` and `Max` instances

instance : Min DTG where
  min := fun ⟨d₁⟩ ⟨d₂⟩ ↦ ⟨min d₁ d₂⟩

instance : Max DTG where
  max := fun ⟨d₁⟩ ⟨d₂⟩ ↦ ⟨max d₁ d₂⟩

`Add` instance

Two DTG values can be added (useful when a DTG is used as a raw offset):

instance : Add DTG where
  add := fun ⟨d₁⟩ ⟨d₂⟩ ↦ ⟨d₁ + d₂⟩

Duration

A Duration represents an elapsed time expressed as a whole number of seconds. Like DTG, it wraps a Nat and inherits a rich set of typeclass instances.

Structure definition

structure Duration where
  dur : Nat
deriving Repr, Ord, DecidableEq

`OfNat` instance

Natural number literals are interpreted as durations in seconds:

instance : OfNat Duration n where
  ofNat := ⟨n⟩

Ordering instances

LT and decidable <:

instance : LT Duration where
  lt := fun ⟨d₁⟩ ⟨d₂⟩ ↦ d₁ < d₂

instance (x y : Duration) : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.dur < y.dur))

LE and decidable ≤:

instance : LE Duration where
  le := fun ⟨d₁⟩ ⟨d₂⟩ ↦ d₁ ≤ d₂

instance (x y : Duration) : Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.dur ≤ y.dur))

`Min` and `Max` instances

instance : Min Duration where
  min := fun ⟨d₁⟩ ⟨d₂⟩ ↦ ⟨min d₁ d₂⟩

instance : Max Duration where
  max := fun ⟨d₁⟩ ⟨d₂⟩ ↦ ⟨max d₁ d₂⟩

Arithmetic instances

Add — sum of two durations:

instance : Add Duration where
  add := fun ⟨d₁⟩ ⟨d₂⟩ ↦ ⟨d₁ + d₂⟩

Sub — magnitude of the difference (symmetric):

instance : Sub Duration where
  sub := fun ⟨d₁⟩ ⟨d₂⟩ ↦ if d₁ < d₂ then ⟨d₂ - d₁⟩ else ⟨d₁ - d₂⟩

Duration subtraction is commutative: d₁ - d₂ = d₂ - d₁ = max d₁ d₂ - min d₁ d₂. It always returns the absolute difference rather than a signed result.

Named constants

def oneDay : Duration := ⟨secondsPerDay⟩

def oneHour : Duration := ⟨secondsPerHour⟩

Heterogeneous Operations on DTG and Duration

These HAdd, HSub, HMul, and HDiv instances combine DTG and Duration values in the natural ways expected by a time-arithmetic library.

Adding a duration to a DTG

Shifts a point in time forward by a duration:

instance : HAdd DTG Duration DTG where
  hAdd := fun ⟨d₁⟩ ⟨d₂⟩ ↦ ⟨d₁ + d₂⟩

Subtracting a duration from a DTG

Shifts a point in time backward. Natural number subtraction is used, so the result cannot precede the epoch (it saturates at 0):

instance : HSub DTG Duration DTG where
  hSub := fun ⟨d₁⟩ ⟨d₂⟩ ↦ ⟨d₁ - d₂⟩

Duration between two DTGs

Returns the absolute time difference between two points in time:

instance : HSub DTG DTG Duration where
  hSub := fun ⟨d₁⟩ ⟨d₂⟩ ↦ if d₁ < d₂ then ⟨d₂ - d₁⟩ else ⟨d₁ - d₂⟩

Like Duration subtraction, DTG subtraction is symmetric: d₁ - d₂ = d₂ - d₁. It always yields the magnitude of the elapsed time between the two moments.

Scaling a duration

Multiply a duration by a natural number:

instance : HMul Duration Nat Duration where
  hMul := fun ⟨d⟩ n ↦ ⟨d * n⟩

Divide a duration by a natural number (integer division):

instance : HDiv Duration Nat Duration where
  hDiv := fun ⟨d⟩ n ↦ ⟨d / n⟩

Interval

An Interval represents a contiguous span of time bounded by a start DTG (inclusive) and an end DTG (exclusive). The empty interval is the degenerate case where starts = ends.

Structure definition

structure Interval where
  starts : DTG
  ends   : DTG
  inv    : starts ≤ ends
deriving Repr, Ord, DecidableEq

The field inv is a proof that ends is not earlier than starts, making it impossible to construct an ill-formed interval. The Inhabited default is the zero-length interval at the epoch:

instance : Inhabited Interval where
  default := ⟨0, 0, by trivial⟩

The ∅ notation is also available for the empty interval:

instance : EmptyCollection Interval where
  emptyCollection := default

Ordering

Two intervals are ordered by the relation i₁ < i₂ when i₁ ends no later than i₂ starts — that is, i₁ is strictly before i₂ with no overlap:

instance : LT Interval where
  lt i₁ i₂ := i₁.ends ≤ i₂.starts

instance (i₁ i₂ : Interval) : Decidable (i₁ < i₂) :=
  inferInstanceAs (Decidable (i₁.ends ≤ i₂.starts))

`Interval.contains`

Test whether a DTG falls within the interval. The start is inclusive; the end is exclusive:

def contains (i : Interval) (d : DTG) : Bool :=
  i.starts ≤ d ∧ d < i.ends

Membership instance — enables dtg ∈ interval notation:

instance : Membership DTG Interval where
  mem d i := i.contains d

`Interval.overlap`

Test whether two intervals share at least one common point in time:

def overlap (i₁ i₂ : Interval) : Bool :=
  i₁.starts < i₂.ends ∧ i₂.starts < i₁.ends

`Interval.inter`

The intersection of two intervals. If the intervals do not overlap the result is the empty (default) interval:

def inter : Interval → Interval → Interval
  | ⟨s₁, e₁, _⟩, ⟨s₂, e₂, _⟩ =>
      let istart := max s₁ s₂
      let iend := if min e₁ e₂ < istart then istart else min e₁ e₂
      if istart = iend then default else ⟨istart, iend, sorry⟩

Inter instance — enables i₁ ∩ i₂ notation:

instance : Inter Interval := ⟨inter⟩

`Interval.within`

A proposition stating that i₁ is fully contained within i₂:

def within (i₁ i₂ : Interval) : Prop :=
  i₂.starts ≤ i₁.starts ∧ i₁.ends ≤ i₂.ends

HasSubset instance — enables i₁ ⊆ i₂ notation:

instance : HasSubset Interval := ⟨within⟩

Decidable ⊆:

instance (x y : Interval) : Decidable (x ⊆ y) :=
  sorry

`Interval.durationOf`

Compute the length of an interval as a Duration. Because DTG - DTG returns the absolute difference and inv guarantees starts ≤ ends, the result equals ends - starts in seconds:

def durationOf (i : Interval) : Duration :=
  i.ends - i.starts

`Interval.intervalOf`

Construct the interval that begins at a given DTG and lasts for a given Duration:

def intervalOf (dtg : DTG) (dur : Duration) : Interval :=
  ⟨dtg, dtg+dur, sorry⟩

Support Libraries

Flight Planning Modules

LeanSpec.lib.Temporal: DTG, Duration, and Interval Types

Constants

DTG (Date/Time Group)

Structure definition

`OfNat` instance

Ordering instances

`Min` and `Max` instances

`Add` instance

Duration

Structure definition

`OfNat` instance

Ordering instances

`Min` and `Max` instances

Arithmetic instances

Named constants

Heterogeneous Operations on DTG and Duration

Adding a duration to a DTG

Subtracting a duration from a DTG

Duration between two DTGs

Scaling a duration

Interval

Structure definition

Ordering

`Interval.contains`

`Interval.overlap`

`Interval.inter`

`Interval.within`

`Interval.durationOf`

`Interval.intervalOf`

Build docs developers (and LLMs) love

Support Libraries

Flight Planning Modules

Documentation Index

​Constants

​DTG (Date/Time Group)

​Structure definition

​OfNat instance

​Ordering instances

​Min and Max instances

​Add instance

​Duration

​Structure definition

​OfNat instance

​Ordering instances

​Min and Max instances

​Arithmetic instances

​Named constants

​Heterogeneous Operations on DTG and Duration

​Adding a duration to a DTG

​Subtracting a duration from a DTG

​Duration between two DTGs

​Scaling a duration

​Interval

​Structure definition

​Ordering

​Interval.contains

​Interval.overlap

​Interval.inter

​Interval.within

​Interval.durationOf

​Interval.intervalOf

Build docs developers (and LLMs) love

Constants

DTG (Date/Time Group)

Structure definition

`OfNat` instance

Ordering instances

`Min` and `Max` instances

`Add` instance

Duration

Structure definition

`OfNat` instance

Ordering instances

`Min` and `Max` instances

Arithmetic instances

Named constants

Heterogeneous Operations on DTG and Duration

Adding a duration to a DTG

Subtracting a duration from a DTG

Duration between two DTGs

Scaling a duration

Interval

Structure definition

Ordering

`Interval.contains`

`Interval.overlap`

`Interval.inter`

`Interval.within`

`Interval.durationOf`

`Interval.intervalOf`