Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/paulch42/lean-spec/llms.txt

Use this file to discover all available pages before exploring further.

Air traffic is growing faster than the infrastructure that supports it. Airports, runways, taxiways, and gates are becoming increasingly congested, and the only way to manage the imbalance is to schedule the use of scarce resources more efficiently. This example demonstrates how Lean 4 can formally specify that scheduling process — a departure Traffic Management Initiative (TMI) — encoding the problem constraints directly into the type system using dependent types. The result is a specification where every allocation value is, by construction, a valid solution: no separate validation step, no possibility of an ill-formed allocation slipping through.

​
The Problem

Air Traffic Flow Management (ATFM) is the discipline that assesses future traffic movements and schedules aircraft to make best use of available resources. The application of a set of scheduling rules across resources over a period of time is called a Traffic Management Initiative (TMI). One type is a Ground Delay Program (GDP): hold aircraft on the ground at their departure point so that, after take-off, they can proceed directly to their destination without entering a holding pattern on arrival. An aircraft circling in the air burns significant fuel, increasing both costs and emissions. The particular TMI specified here is a departure program — scheduling aircraft that are all leaving the same airport. Without coordination, aircraft leave their gates according to individual schedules, creating congestion on the taxiways as they queue for take-off. Aircraft sitting idle on the taxiway waste fuel and produce unnecessary emissions. A departure program assigns each aircraft a target take-off time so that the operator knows in advance exactly when to push back from the gate.

​
Constraints

A valid departure program must satisfy the following constraints:
  • Flights: A defined set of flights wish to depart during the program period.
  • Runway compatibility: Each flight may only take off from certain runways — a large aircraft cannot use a short runway.
  • Preferred time: Each flight has a preferred take-off time that the aircraft operator would ideally receive.
  • Departure window: Each flight must take off within a nominated time window — operators have schedules to meet and downstream flight legs to conduct.
  • Available runways: Only certain runways are active during the program; the airport configuration determines which.
  • Runway rates: Each active runway has a maximum departure rate — a minimum gap between successive take-offs — determined by forecast weather, noise restrictions, and other factors.
  • Program period: The TMI runs over a fixed time interval, covering only the period of likely resource competition.

​
Goal

Given these constraints, allocate a runway and a target take-off time to as many flights as possible, minimising the total deviation from each flight’s preferred time.

​
Basic Types

The specification begins by opening the necessary libraries and establishing a namespace. 
import LeanSpec.lib.Temporal
import LeanSpec.lib.Util

open Std Std.Map Temporal

namespace TMI
Three basic identifier types name the key entities. There are rules about how real-world identifiers are formed, but for this specification it is sufficient that they can be distinguished, so each is an abbreviation for String. 
abbrev AirportDesig := String

abbrev FlightId := String

abbrev RunwayDesig := String

​
FlightDeparture

The FlightDeparture structure captures the information about a single flight that is relevant to computing a departure slot. In a wider operational system there is much more information associated with a flight, but here we abstract only the details the scheduling algorithm needs. 
structure FlightDeparture where
  -- The unique identifier of the flight.
  fid       : FlightId
  -- The runways the flight is able to use.
  canUse    : Set RunwayDesig
  -- The operator's preferred take off time for the flight.
  preferred : DTG
  -- The period of time during which the flight can reasonably take off.
  window    : Interval
  -- The flight must be able to use at least one runway.
  inv₁      : canUse ≠ ∅
  -- The preferred take off time must occur within the window.
  inv₂      : preferred ∈ window
deriving DecidableEq
The two invariant fields are where dependent types earn their keep:
  • inv₁ : canUse ≠ ∅ — Although the empty set ∅ has type Set RunwayDesig, no FlightDeparture value can ever have an empty canUse, because constructing such a value would require a proof of ∅ ≠ ∅, which is false. A flight that nominates no runways simply cannot be represented.
  • inv₂ : preferred ∈ window — The preferred take-off time must fall inside the declared departure window. This rules out the degenerate case where a flight nominates a preference that is impossible to achieve even with zero deviation.
Set A is the type of finite sets of elements drawn from A. It is defined in the Util support library, together with the A ⟹ B finite map type used throughout this specification.
Traditionally, structures model data consisting of multiple disparate elements, and validity predicates are defined separately. Dependent types change this: constraints that relate the elements of a type can be placed directly inside the structure. Any candidate value that fails to satisfy an invariant field is excluded at the type level — it is not merely rejected at runtime, it cannot be constructed. In the case of FlightDeparture, both inv₁ and inv₂ are proof obligations that must be discharged when creating an instance, so invalid flights are structurally impossible.

​
Runway Rate and Configuration

The runway rate is the minimum time that must elapse between successive take-offs from the same runway. It is modelled as a Duration. 
abbrev Rate := Duration
Each active runway is mapped to its rate. 
abbrev RunwayRates := RunwayDesig ⟹ Rate
A ⟹ B is the type of finite maps from A to B, defined in the Util library. It supports operations such as .domain, .range, and .find? used throughout this specification.
The TMIConfig structure bundles all the information required to compute a departure TMI: the airport being managed, the time period of the program, the set of flights wishing to depart, and the rates of the participating runways. It also carries two invariants that enforce consistency between the flights and the program configuration. 
structure TMIConfig where
  -- The designator of the airport at which the TMI is run.
  airport : AirportDesig
  -- The period of time over which the TMI runs.
  period  : Interval
  -- The flights that desire to take off within the period of the TMI.
  flights : Set FlightDeparture
  -- The rates of the runways that participate in the TMI.
  rates   : RunwayRates
  -- The take off window of a proposed flight must fall within the TMI period.
  inv₁    : ∀ f ∈ flights, f.window ∩ period ≠ ∅
  -- A flight must be able to take off from one of the participating runways.
  inv₂    : ∀ f ∈ flights, f.canUse ∩ rates.domain ≠ ∅
inv₁ ensures that every flight’s departure window overlaps the TMI period — there is no point including a flight whose window falls entirely outside the program. inv₂ ensures that every flight can use at least one of the runways that are active during the program — a flight that is incompatible with all available runways has no possible allocation.

​
Slot and Flight Allocation

A slot is a pairing of a runway with a target take-off time (TTOT). 
structure Slot where
  -- The runway designator.
  rwy  : RunwayDesig
  -- The target take off time.
  ttot : DTG
deriving DecidableEq
The outcome of running the departure TMI is a FlightAllocation: a map from flight identifiers to slots, together with six invariants that ensure every entry in the map is consistent with the originating TMIConfig. This is where the power of dependent types is most visible — FlightAllocation is parameterised by cfg : TMIConfig, so its invariants can freely reference the configuration data. 
structure FlightAllocation (cfg : TMIConfig) where
  -- The allocation of flight departures to slots.
  gdp  : FlightId ⟹ Slot
  -- Any flight in the GDP must be drawn from the flights in the TMI configuration.
  inv₁ : gdp.domain ⊆ cfg.flights.map (·.fid)
  -- The runway allocated to a flight must be drawn from the runways in the TMI.
  inv₂ : ∀ slot ∈ gdp.range, slot.rwy ∈ cfg.rates.domain
  -- The runway allocated to a flight must be one of the runways it can use.
  inv₃ : ∀ fsl ∈ gdp, ∀ fdep ∈ cfg.flights,
           fsl.key = fdep.fid → fsl.value.rwy ∈ fdep.canUse
  -- The target time allocated to a flight must fall within its window.
  inv₄ : ∀ fsl ∈ gdp, ∀ fdep ∈ cfg.flights,
           fsl.key = fdep.fid → fsl.value.ttot ∈ fdep.window
  -- The target time allocated to a flight must fall within the TMI period.
  inv₅ : ∀ slot ∈ gdp.range, slot.ttot ∈ cfg.period
  -- Two flights allocated the same runway must depart at least the minimum duration apart.
  inv₆ : ∀ fsl₁ ∈ gdp, ∀ fsl₂ ∈ gdp, fsl₁.key ≠ fsl₂.key ∧ fsl₁.value.rwy = fsl₂.value.rwy →
           ∀ fr ∈ cfg.rates, fr.key = fsl₁.value.rwy → fsl₁.value.ttot - fsl₂.value.ttot ≥ fr.value
Each invariant addresses a distinct scheduling constraint:
InvariantConstraint
inv₁Only flights from the TMI configuration can be allocated a slot — no phantom flights.
inv₂Every allocated runway must be one of the runways participating in the TMI.
inv₃The runway allocated to a flight must be one that the flight’s aircraft type can actually use.
inv₄The allocated take-off time must fall within the flight’s declared departure window.
inv₅The allocated take-off time must fall within the overall TMI program period.
inv₆Any two flights on the same runway must be separated by at least that runway’s minimum departure rate.
The sole data field is gdp; inv₁ through inv₆ are all proof fields. For a given cfg : TMIConfig, the type FlightAllocation cfg contains exactly those maps that represent valid solutions to the departure scheduling problem — not valid solutions plus invalid ones that must later be filtered, but only valid solutions.

​
Cost Function

Many allocations satisfy the constraints simultaneously. A cost function selects among them. The cost reflects both flights that received a slot and flights that were omitted:
  • An allocated flight incurs cost proportional to how far its assigned time deviates from its preferred time.
  • An omitted flight incurs a higher cost, modulated by whether its departure window extends beyond the TMI period (giving it a chance to depart later).
The deviation for an allocated flight is the absolute duration between its preferred time and its assigned target take-off time. 
def allocatedDeviation (flight : FlightDeparture) (slot : Slot) : Duration :=
  flight.preferred - slot.ttot
For an omitted flight, if its window lies entirely within the TMI period there is no opportunity to depart outside the program — the operator has a real scheduling problem. If the window extends past the TMI period, the flight can still depart in the overlap region at a lower penalty. 
def omittedDeviation (period window : Interval) : Duration :=
  let d := window.durationOf
  if window ⊆ period then d else d/2
The total cost of an allocation sums the deviation across all flights in the configuration: allocated flights contribute their time deviation, omitted flights contribute their window-based penalty. 
def FlightAllocation.cost (cfg : TMIConfig) (alloc : FlightAllocation cfg) : Duration :=
  let deviation (fdep : FlightDeparture) : Duration :=
        alloc.gdp.find? fdep.fid ▹ omittedDeviation cfg.period fdep.window
                                 ‖ (allocatedDeviation fdep ·)
  cfg.flights.add' deviation 0

​
The Complete Specification

Combining all the components, the departure TMI is the optimal allocation: of all allocations satisfying the configuration, the one (not necessarily unique) whose cost is no greater than any other. 
def DepartureTMI (cfg : TMIConfig) :=
  { opt : FlightAllocation cfg // ∀ alloc : FlightAllocation cfg, opt.cost cfg ≤ alloc.cost cfg }
This is a remarkably concise definition. The subtype { opt : FlightAllocation cfg // P opt } selects the element of FlightAllocation cfg for which P holds — here, the element with minimum cost. Because FlightAllocation cfg already contains only valid allocations, DepartureTMI simply points to the best one, with no need to re-state any of the scheduling constraints.

​
Discussion: Concise vs Verbose Invariants

The six separate invariants of FlightAllocation have some repetition in their quantified variables and preconditions. An equivalent, more compact formulation merges related invariants. 
structure FlightAllocation₁ (cfg : TMIConfig) where
  -- The allocation of flights to slots.
  gdp  : FlightId ⟹ Slot
  -- Any flight in the GDP must be drawn from the TMI configuration.
  inv₁ : gdp.domain ⊆ cfg.flights.map (·.fid)
  -- The runway allocated to a flight must be a participant in the TMI.
  -- The target time allocated to a flight must fall within the TMI period.
  -- The runway allocated to a flight must be one of the runways it can use.
  -- The target time allocated to a flight must fall within its window.
  inv₂ : ∀ fsl ∈ gdp,
           fsl.value.rwy ∈ cfg.rates.domain ∧
           fsl.value.ttot ∈ cfg.period ∧
           ∀ fdep ∈ cfg.flights, fsl.key = fdep.fid →
             fsl.value.rwy ∈ fdep.canUse ∧
             fsl.value.ttot ∈ fdep.window
  -- Two flights allocated the same runway must depart at least the minimum duration apart.
  inv₃ : ∀ fsl₁ ∈ gdp, ∀ fsl₂ ∈ gdp, fsl₁.key ≠ fsl₂.key ∧ fsl₁.value.rwy = fsl₂.value.rwy →
           ∀ fr ∈ cfg.rates, fr.key = fsl₁.value.rwy → fsl₁.value.ttot - fsl₂.value.ttot ≥ fr.value
FlightAllocation₁ reduces six invariants to three by folding the slot-level checks (inv₂, inv₃, inv₄, inv₅ in the original) into a single universal quantification over gdp entries. Both forms capture identical constraints — the choice between them is a matter of readability. The original six-invariant version provides a clearer one-to-one correspondence with the informal problem description, and keeping constraints separate makes it easier to reason about or modify any individual one.

​
Discussion: Non-Dependent vs Dependent Approach

Before adopting dependent types, a natural first attempt defines the allocation as a plain map: 
abbrev FlightAllocation₂ := FlightId ⟹ Slot
This type accepts any map from FlightId to Slot, including maps containing flight identifiers that do not exist in the configuration, or slots referencing runways that are not active. To exclude these, a separate Satisfies predicate must be defined: 
def Satisfies (cfg : TMIConfig) (alloc : FlightAllocation₂) :=
  alloc.domain ⊆ cfg.flights.map (·.fid) ∧
  (∀ slot ∈ alloc.range, slot.rwy ∈ cfg.rates.domain) ∧
  (∀ fsl ∈ alloc, ∀ fdep ∈ cfg.flights,
    fsl.key = fdep.fid → fsl.value.rwy ∈ fdep.canUse) ∧
  (∀ fsl ∈ alloc, ∀ fdep ∈ cfg.flights,
    fsl.key = fdep.fid → fsl.value.ttot ∈ fdep.window) ∧
  (∀ slot ∈ alloc.range, slot.ttot ∈ cfg.period) ∧
  (∀ fsl₁ ∈ alloc, ∀ fsl₂ ∈ alloc, fsl₁.key ≠ fsl₂.key ∧ fsl₁.value.rwy = fsl₂.value.rwy →
     ∀ fr ∈ cfg.rates, fr.key = fsl₁.value.rwy → fsl₁.value.ttot - fsl₂.value.ttot ≥ fr.value)
Notice that, apart from minor syntactic differences, Satisfies states exactly the same constraints as the invariants of FlightAllocation. The information is the same — it has simply moved from inside the type to beside it. The non-dependent approach has two disadvantages. First, the constraints are separated from the data they govern, reducing locality and making the specification harder to read. Second, every function that consumes a FlightAllocation₂ must either carry a Satisfies proof or risk working with an invalid allocation. With the dependent approach, the type system guarantees validity at every use site automatically — if a value of type FlightAllocation cfg exists, it is correct by construction.
Changing the cost function. Small changes to specifications can have major effects. What would happen if the cost function only considered flights that are included in the TMI — that is, omitted flights incur zero cost?
def FlightAllocation.cost₁ (cfg : TMIConfig) (alloc : FlightAllocation cfg) : Duration :=
  let deviation (fdep : FlightDeparture) : Duration :=
        alloc.gdp.find? fdep.fid ▹ 0 ‖ (allocatedDeviation fdep ·)
  cfg.flights.add' deviation 0
What behaviour does this incentivise in the scheduler?Requirements change. A new requirement says a flight must not take off before its preferred time, though it may take off after. Change the specification to enforce this constraint.Boundary case: empty flight set. Say a TMI is run with a configuration in which no flights are specified — flights : Set FlightDeparture is the empty set. Is a solution that meets the specification still possible? What does it look like?Boundary case: empty runway rates. What if rates : RunwayRates is the empty map? Is a solution still possible? Is there any relationship between this boundary case and the empty flights case above?Removing a flight invariant. What is the impact on the specification if the constraint inv₁ : canUse ≠ ∅ on FlightDeparture is removed? Which other invariants become harder to satisfy or easier to vacuously satisfy?Passenger-count cost. An alternative evaluation strategy is to maximise the number of passengers who depart during the TMI rather than minimising time deviation. Modify the specification to implement this approach. (Hint: you will need to add a field to FlightDeparture. Freight operators are on their own.)
end TMI

Build docs developers (and LLMs) love

Get started for freeTalk to us