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.
LeanSpec.FPL.Message defines the six ICAO flight planning message types — FPL, DLA, CHG, CNL, DEP, and ARR — as Lean types, each selecting the appropriate fields for its purpose. Each message type carries exactly the fields required for its role: the FPL message is the most complete, bearing the full flight plan; the modification and lifecycle messages carry only identification fields plus the data required to effect their specific update. Type class instances on every message type provide flight time estimation and flight identification, enabling the state processing machinery to treat messages uniformly. The module also defines the Message sum type that unifies all six variants into a single type for use in the state.
import LeanSpec.FPL.Flight
open Temporal Core FPL.Field
namespace FPL
Message Type Summary
| Message | Full Name | Purpose | Key Fields |
|---|
FPL | Filed Flight Plan | Initial flight plan submission | F7, F8, F9, F10, F13, F15, F16, F18 |
CHG | Modification | Amend an existing flight plan | F7, F13, F16a, F22 |
CNL | Cancellation | Cancel a filed flight plan | F7, F13, F16a |
DLA | Delay | Report a new estimated departure time | F7, F13, F16a |
DEP | Departure | Confirm actual take-off | F7, F13, F16a |
ARR | Arrival | Confirm actual landing | F7, F13, F16a, F17 |
IsConsistent
Before the individual message types, the module defines the IsConsistent type class. Instances of this class have a isConsistent predicate that tests whether the instance is compatible with a given Flight. Only CHG requires a non-trivial consistency check (since it modifies specific fields of an existing flight), but the class generalises this concept for the Message union type.
class IsConsistent (α : Type) (_ : Flight) where
isConsistent : α → Prop
Filed Flight Plan: FPL
The FPL message communicates the full details of a new flight prior to departure. It carries all the information needed to establish a new flight in the system.
structure FPL where
f7 : Field7
f8 : Field8
f9 : Field9
f10 : Field10
f13 : Field13
f15 : Field15
f16 : Field16
f18 : Option Field18
inv : F8F15Level f8 f15 ∧
F8F15Rule f8 f15 ∧
F9F18Typ f9 f18 ∧
F10F18Sts f10 f18 ∧
F10F18Pbn f10 f18 ∧
F10F18Z f10 f18 ∧
F13F18Dep f13 f18 ∧
F15F18Dle f15 f18 ∧
F16F18Dest f16 f18 ∧
F16F18Altn f16 f18 ∧
F16F18Eet f16 f18 ∧
F16F18Dle f16 f18
deriving DecidableEq
inv field requires simultaneous proof of all twelve cross-field consistency constraints defined in LeanSpec.FPL.Field. These are identical to the corresponding constraints in Flight, minus the Field 17 constraint (which only applies once the flight is completed).
Type Class Instances
FlightTime FPL — The flight time period is derived from the departure point, departure time, destination, and TEET:
instance : FlightTime FPL where
period fpl := adepAdesFlightTime fpl.f13.f13a fpl.f13.f13b fpl.f16.f16a fpl.f16.f16b
IsFlight FPL — The flight identifier is composed from the aircraft identification, departure aerodrome, and computed flight time:
instance : IsFlight FPL where
idOf fpl := ⟨fpl.f7.f7a, fpl.f13.f13a, FlightTime.period fpl⟩
ToFlight FPL — Converts a FPL to a Flight, setting the initial status to filed. All fields map directly from the FPL fields; Field 17 is absent (the flight has not yet arrived):
instance : ToFlight FPL where
toFlight fpl := ⟨.filed, fpl.f7, fpl.f8, fpl.f9, fpl.f10, fpl.f13, fpl.f15, fpl.f16, none, fpl.f18, sorry⟩
Modification: CHG
The CHG message amends one or more fields of an existing filed flight plan. Fields 7, 13, and 16a are used for matching the message against the correct stored flight; Field 22 specifies the actual changes.
structure CHG where
f7 : Field7
f13 : Field13
f16 : Field16a
f22 : Field22
deriving DecidableEq
| Field | Type | Description |
|---|
f7 | Field7 | Aircraft identification (for matching) |
f13 | Field13 | Departure aerodrome and time (for matching) |
f16 | Field16a | Destination aerodrome (for matching) |
f22 | Field22 | Amendment: the new values for all changed fields |
Type Class Instances
instance : FlightTime CHG where
period chg := adepAdesFlightTime chg.f13.f13a chg.f13.f13b chg.f16 none
instance : IsFlight CHG where
idOf chg := ⟨chg.f7.f7a, chg.f13.f13a, FlightTime.period chg⟩
IsConsistent CHG
A CHG message must be consistent with the flight it modifies. Each field in Field22 that is present must satisfy all applicable cross-field consistency predicates. If a field in the CHG is absent, the corresponding field from the existing flight is used in the check. This is implemented via checkOpt, a helper that selects the CHG value when present or falls back to the flight value:
instance (f : Flight) : IsConsistent CHG f where
isConsistent | {f22 := ⟨_,f8,f9,f10,f13,f15,f16,f18,_⟩, ..} =>
checkOpt F8F15Level f8 f15 f.f8 f.f15 ∧
checkOpt F8F15Rule f8 f15 f.f8 f.f15 ∧
checkOpt F9F18Typ f9 f18 f.f9 f.f18 ∧
checkOpt F10F18Sts f10 f18 f.f10 f.f18 ∧
checkOpt F10F18Pbn f10 f18 f.f10 f.f18 ∧
checkOpt F10F18Z f10 f18 f.f10 f.f18 ∧
checkOpt F13F18Dep f13 f18 f.f13 f.f18 ∧
checkOpt F15F18Dle f15 f18 f.f15 f.f18 ∧
checkOpt F16F18Dest f16 f18 f.f16 f.f18 ∧
checkOpt F16F18Eet f16 f18 f.f16 f.f18 ∧
checkOpt F16F18Dle f16 f18 f.f16 f.f18 ∧
checkOpt F16F18Altn f16 f18 f.f16 f.f18
where checkOpt {α β : Type} (p : α → β → Prop) : Option α → Option β → Option α → Option β → Prop
| some chga, some chgb, _, _ => p chga chgb
| some chga, none, _, some fltb => p chga fltb
| none, some chgb, some flta, _ => p flta chgb
| _, _, _, _ => True
checkOpt helper applies constraint p by:
- Using both CHG values if both are present.
- Using the CHG first argument with the flight’s second argument if only the first is changed.
- Using the flight’s first argument with the CHG second argument if only the second is changed.
- Trivially satisfying the constraint if neither related value changed.
Cancellation: CNL
The CNL message cancels a previously filed flight plan. Only identification information is required; no amendments are carried.
structure CNL where
f7 : Field7
f13 : Field13
f16 : Field16a
deriving DecidableEq
| Field | Type | Description |
|---|
f7 | Field7 | Aircraft identification (for matching) |
f13 | Field13 | Departure aerodrome and time (for matching) |
f16 | Field16a | Destination aerodrome (for matching) |
Type Class Instances
instance : FlightTime CNL where
period cnl := adepAdesFlightTime cnl.f13.f13a cnl.f13.f13b cnl.f16 none
instance : IsFlight CNL where
idOf cnl := ⟨cnl.f7.f7a, cnl.f13.f13a, FlightTime.period cnl⟩
Delay: DLA
The DLA message reports a revised estimated departure time. Field 13b in a DLA carries the new estimated off-block time, replacing the original from the FPL. Like CNL, it contains only identification information plus the updated departure time.
structure DLA where
f7 : Field7
f13 : Field13
f16 : Field16a
deriving DecidableEq
| Field | Type | Description |
|---|
f7 | Field7 | Aircraft identification (for matching) |
f13 | Field13 | f13a: departure aerodrome (matching); f13b: new estimated departure time |
f16 | Field16a | Destination aerodrome (for matching) |
Type Class Instances
instance : FlightTime DLA where
period dla := adepAdesFlightTime dla.f13.f13a dla.f13.f13b dla.f16 none
instance : IsFlight DLA where
idOf dla := ⟨dla.f7.f7a, dla.f13.f13a, FlightTime.period dla⟩
Departure: DEP
The DEP message confirms that the aircraft has taken off. Field 13b carries the actual time of departure, which may differ from the EOBT in the FPL.
structure DEP where
f7 : Field7
f13 : Field13
f16 : Field16a
deriving DecidableEq
| Field | Type | Description |
|---|
f7 | Field7 | Aircraft identification (for matching) |
f13 | Field13 | f13a: departure aerodrome (matching); f13b: actual time of departure |
f16 | Field16a | Destination aerodrome (for matching) |
Type Class Instances
instance : FlightTime DEP where
period dep := adepAdesFlightTime dep.f13.f13a dep.f13.f13b dep.f16 none
instance : IsFlight DEP where
idOf dep := ⟨dep.f7.f7a, dep.f13.f13a, FlightTime.period dep⟩
Arrival: ARR
The ARR message confirms the aircraft has landed. It carries Field 17 with the actual arrival aerodrome and time, and imposes the constraint that the actual arrival differs from the planned destination (since a straight-ahead arrival matching the plan needs no ARR to note a diversion).
structure ARR where
f7 : Field7
f13 : Field13
f16 : Field16a
f17 : Field17
inv : F16F17Dest f16 f17
deriving DecidableEq
| Field | Type | Description |
|---|
f7 | Field7 | Aircraft identification (for matching) |
f13 | Field13 | Departure aerodrome and time (for matching) |
f16 | Field16a | Planned destination aerodrome (for matching and flight time) |
f17 | Field17 | Actual arrival aerodrome and time |
F16F17Dest f16 f17 — the planned destination must differ from the actual arrival aerodrome, distinguishing a diversion from an on-plan arrival.
Type Class Instances
FlightTime ARR — The flight time prefers the planned destination for period calculation (to match the period computed from the original FPL), but falls back to the actual arrival if no designator was filed.
instance : FlightTime ARR where
period arr := let dest := -- Use the planned destination if available, otherwise the actual arrival.
arr.f16 ▹ arr.f17.f17a ‖ id
adepAdesFlightTime arr.f13.f13a arr.f13.f13b dest none
IsFlight ARR:
instance : IsFlight ARR where
idOf arr := ⟨arr.f7.f7a, arr.f13.f13a, FlightTime.period arr⟩
Message: The Union Type
All six message types are unified into a single inductive Message type, allowing the state processing machinery to handle any message with a single dispatch.
inductive Message
| fpl (_ : FPL)
| chg (_ : CHG)
| cnl (_ : CNL)
| dla (_ : DLA)
| dep (_ : DEP)
| arr (_ : ARR)
deriving DecidableEq
FlightTime Message
Delegates to the appropriate instance for each constructor:
open FlightTime in
instance : FlightTime Message where
period | .fpl x => period x
| .chg x => period x
| .cnl x => period x
| .dla x => period x
| .dep x => period x
| .arr x => period x
IsFlight Message
Delegates to the appropriate instance:
open IsFlight in
instance : IsFlight Message where
idOf | .fpl x => idOf x
| .chg x => idOf x
| .cnl x => idOf x
| .dla x => idOf x
| .dep x => idOf x
| .arr x => idOf x
IsConsistent Message
Only CHG requires a non-trivial consistency check. All other message types are trivially consistent with any flight.
open IsConsistent in
instance (flt : Flight) : IsConsistent Message flt where
isConsistent | .chg chg => isConsistent flt chg
| _ => True
end FPL
