Time package
Port of the haskell time library to Lean 4 (WIP).
Missing modules
Usage
see time library doc
From Haskell to Lean
Take the function toOrdinalDate, which computes the ISO 8601 ordinal date given a modified Julian day.
In Haskell toOrdinalDate has the type
type Year = Integer
type DayOfYear = Int
toOrdinalDate :: Day -> (Year, DayOfYear)
and computes the year and the day of year.
In Lean toOrdinalDate has the type
inductive DayOfYear where
| common : Time.Icc 1 365 -> DayOfYear
| leap : Time.Icc 1 366 -> DayOfYear
structure OrdinalDate where
year : Int
dayOfYear : DayOfYear
isValid : match dayOfYear with
| .common _ => isLeapYear year = false
| .leap _ => isLeapYear year = true
def toOrdinalDate : Day → OrdinalDate
and computes the year and the day of year and gives a proof that ordinal date is a valid date.
Verification
The date transformations and calculations are verified relative to a intuitive specification of next_date.
It is proved that the following diagrams commute:
| GregorianDate | Transformation | OrdinaleDate | Transformation | Modified Julian Day |
|---|---|---|---|---|
| dt | => dateToOrdinalDate => | odt | => fromOrdinalDate => | mjd |
| ⇓ next_date | proof | ⇓ next_date | proof | ⇓ add 1 |
| dt | <= ordinalDateToDate <= | odt | <= toOrdinalDate <= | mjd |
Build
- update: lake update
- build: lake build
- build docs: lake -R -Kenv=dev update && lake -R -Kenv=dev build Time:docs