def Time.monthLengths (isleap : Bool) : List (Nat × Nat)

Month and days of month.

Equations

• Time.monthLengths isleap = [(1, 31), (2, if isleap = true then 29 else 28), (3, 31), (4, 30), (5, 31), (6, 30), (7, 31), (8, 31), (9, 30), (10, 31), (11, 30), (12, 31)]

structure Time.Date : Type

Date in proleptic Gregorian calendar.

• Year : Int
• Month : Time.Icc 1 12
• Day : Time.Icc 1 31
• IsValid : ∃ (m : Nat × Nat), m ∈ Time.monthLengths (Time.isLeapYear self.Year) ∧ m.fst = self.Month.val ∧ self.Day.val ≤ m.snd

theorem Time.Date.ext {x y : Time.Date} (Year : x.Year = y.Year) (Month : x.Month = y.Month) (Day : x.Day = y.Day) : x = y

instance Time.instReprDate : Repr Time.Date

Equations

• Time.instReprDate = { reprPrec := Time.reprDate✝ }

def Time.Notation.date.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.date : Lean.Parser.Category

Date syntactic category

Equations

• Lean.Parser.Category.date = { }

def Time.Notation.«date__-___-__» : Lean.ParserDescr

Date from numeric literals year, month and day

Equations

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

def Time.Notation.«termDate%_» : Lean.ParserDescr

Equations

• Time.Notation.«termDate%_» = Lean.ParserDescr.node `Time.Notation.«termDate%_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "date%") (Lean.ParserDescr.cat `date 0))

instance Time.instBEqDate : BEq Time.Date

Equations

• Time.instBEqDate = { beq := fun (a b : Time.Date) => decide (a.Year = b.Year) && decide (a.Month.val = b.Month.val) && decide (a.Day.val = b.Day.val) }

instance Time.instInhabitedDate : Inhabited Time.Date

Equations

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

def Time.monthLastDayAsDayOfYear (isleap : Bool) : List (Nat × Nat)

Last day of month as day of year, see monthLengths_sum_le_map_pair.

Equations

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

def Time.monthLastDayAsDayOfYear' (isleap : Bool) : List (Nat × Nat × Nat)

First and last day of month as day of year, see monthLengths_sum_le_map_pair'.

Equations

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

@[simp]

theorem Time.monthLastDayAsDayOfYear_length_eq_12 (isleap : Bool) : (Time.monthLastDayAsDayOfYear isleap).length = 12

theorem Time.monthLastDayAsDayOfYear_index_lt {isleap : Bool} (i : Fin (Time.monthLastDayAsDayOfYear isleap).length) : ↑i - 1 < (Time.monthLastDayAsDayOfYear isleap).length

@[simp]

theorem Time.monthLastDayAsDayOfYear'_length_eq_12 (isleap : Bool) : (Time.monthLastDayAsDayOfYear' isleap).length = 12

theorem Time.monthLastDayAsDayOfYear'_index_lt {isleap : Bool} (i : Fin (Time.monthLastDayAsDayOfYear' isleap).length) : ↑i - 1 < (Time.monthLastDayAsDayOfYear' isleap).length

theorem Time.monthLastDayAsDayOfYear_sub_pred_le (isleap : Bool) (i : Fin (Time.monthLastDayAsDayOfYear isleap).length) : ((Time.monthLastDayAsDayOfYear isleap).get i).snd - ((Time.monthLastDayAsDayOfYear isleap).get ⟨↑i - 1, ⋯⟩).snd ≤ 31

theorem Time.monthLastDayAsDayOfYear'_day_1_le (isleap : Bool) (a : Nat × Nat × Nat) : a ∈ Time.monthLastDayAsDayOfYear' isleap → 1 ≤ a.snd.fst

theorem Time.monthLastDayAsDayOfYear'_le_day_1 (isleap : Bool) (a : Nat × Nat × Nat) : a ∈ Time.monthLastDayAsDayOfYear' isleap → a.snd.fst ≤ if isleap = true then 336 else 335

theorem Time.monthLastDayAsDayOfYear'_sub_pred_le (isleap : Bool) (i : Fin (Time.monthLastDayAsDayOfYear' isleap).length) : ((Time.monthLastDayAsDayOfYear' isleap).get i).snd.fst = if ↑i = 0 then 1 else ((Time.monthLastDayAsDayOfYear' isleap).get ⟨↑i - 1, ⋯⟩).snd.snd + 1

theorem Time.monthLastDayAsDayOfYear'_sub_days_le (isleap : Bool) (i : Fin (Time.monthLastDayAsDayOfYear' isleap).length) : ((Time.monthLastDayAsDayOfYear' isleap).get i).snd.snd - ((Time.monthLastDayAsDayOfYear' isleap).get i).snd.fst ≤ 30

theorem Time.Int.le_of_sub_le {a b c d : Nat} (h1 : a ≤ c) (h2 : c - b ≤ d) : a - b ≤ d

theorem Time.monthLastDayAsDayOfYear'_val_in (isLeap : Bool) (yd : Nat) (i : Fin (Time.monthLastDayAsDayOfYear' isLeap).length) (h2 : yd ≤ (Time.monthLastDayAsDayOfYear' isLeap)[i].snd.snd) : 1 ≤ yd - (Time.monthLastDayAsDayOfYear' isLeap)[i].snd.fst + 1 ∧ yd - (Time.monthLastDayAsDayOfYear' isLeap)[i].snd.fst + 1 ≤ 31

theorem Time.monthLastDayAsDayOfYear_val_le {yd : Nat} (isleap : Bool) (i : Fin (Time.monthLastDayAsDayOfYear isleap).length) (val : Nat) (hVal : val = ((Time.monthLastDayAsDayOfYear isleap).get ⟨↑i - 1, ⋯⟩).snd) (h1 : ¬yd ≤ val) (h2 : yd ≤ ((Time.monthLastDayAsDayOfYear isleap).get i).snd) : 1 ≤ yd - val ∧ yd - val ≤ 31

def Time.monthLengths_sum_le (isleap : Bool) (m : Nat) : Nat

Sum of month lengths upto month m

Equations

• Time.monthLengths_sum_le isleap m = List.foldl (fun (acc : Nat) (ml : Nat × Nat) => ml.snd + acc) 0 (List.takeWhile (fun (ml : Nat × Nat) => decide (ml.fst ≤ m)) (Time.monthLengths isleap))

def Time.monthLengths_sum_le_map (isleap : Bool) : List Nat

Equations

• Time.monthLengths_sum_le_map isleap = List.map (fun (x : Nat × Nat) => Time.monthLengths_sum_le isleap x.fst) (Time.monthLengths isleap)

def Time.monthLengths_sum_le_map_pair (isleap : Bool) : List (Nat × Nat)

Equations

• Time.monthLengths_sum_le_map_pair isleap = List.map (fun (ml : Nat × Nat) => (ml.fst, Time.monthLengths_sum_le isleap ml.fst)) (Time.monthLengths isleap)

def Time.monthLengths_sum_le_map_pair' (isleap : Bool) : List (Nat × Nat × Nat)

Equations

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

theorem Time.monthLengths_sum_le_eq_monthLastDayAsDayOfYear (isleap : Bool) : Time.monthLengths_sum_le_map isleap = List.map (fun (x : Nat × Nat) => x.snd) (Time.monthLastDayAsDayOfYear isleap)

def Time.monthLengths' (isleap : Bool) : Nat → Option Nat

Equations

• Time.monthLengths' isleap a = List.lookup a (Time.monthLengths isleap)

def Time.monthLengths_sum (isleap : Bool) : Nat

Equations

• Time.monthLengths_sum isleap = List.foldl (fun (acc : Nat) (m : Nat × Nat) => acc + m.snd) 0 (Time.monthLengths isleap)

theorem Time.monthLengths_sum_eq (isleap : Bool) : (Time.monthLengths_sum isleap == if isleap = true then 366 else 365) = true

theorem Time.monthLengths_length_eq_12 (isleap : Bool) : ((Time.monthLengths isleap).length == 12) = true

theorem Time.monthLengths_length_gt_0 (isleap : Bool) : 0 < (Time.monthLengths isleap).length

theorem Time.monthLengths_month_in (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → 1 ≤ a.fst ∧ a.fst ≤ 12

theorem Time.monthLengths_days_in (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → 1 ≤ a.snd ∧ a.snd ≤ 31

theorem Time.list_foldl_init_add {α : Type u_1} (l : List α) (init v : Nat) (f : α → Nat) : List.foldl (fun (acc : Nat) (v : α) => f v + acc) init l + v = List.foldl (fun (acc : Nat) (v : α) => f v + acc) (init + v) l

def Time.findValidMonthDay_1 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨0, ⋯⟩).snd) : Time.Date

Equations

• Time.findValidMonthDay_1 year isLeap yd h = { Year := year, Month := ⟨1, Time.findValidMonthDay_1.proof_2⟩, Day := ⟨yd.val, ⋯⟩, IsValid := ⋯ }

def Time.findValidMonthDay_2 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[0].snd) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨1, ⋯⟩).snd) : Time.Date

Equations

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

def Time.findValidMonthDay_3 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[1].snd) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨2, ⋯⟩).snd) : Time.Date

Equations

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

def Time.findValidMonthDay_4 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[2].snd) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨3, ⋯⟩).snd) : Time.Date

Equations

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

def Time.findValidMonthDay_5 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[3].snd) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨4, ⋯⟩).snd) : Time.Date

Equations

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

def Time.findValidMonthDay_6 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[4].snd) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨5, ⋯⟩).snd) : Time.Date

Equations

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

def Time.findValidMonthDay_7 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[5].snd) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨6, ⋯⟩).snd) : Time.Date

Equations

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

def Time.findValidMonthDay_8 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[6].snd) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨7, ⋯⟩).snd) : Time.Date

Equations

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

def Time.findValidMonthDay_9 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[7].snd) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨8, ⋯⟩).snd) : Time.Date

Equations

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

def Time.findValidMonthDay_10 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[8].snd) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨9, ⋯⟩).snd) : Time.Date

Equations

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

def Time.findValidMonthDay_11 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[9].snd) (h : yd.val ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨10, ⋯⟩).snd) : Time.Date

Equations

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

def Time.findValidMonthDay_12 (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hn : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[10].snd) (hle : yd.val ≤ if isLeap = true then 366 else 365) : Time.Date

Equations

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

def Time.findValidMonthDay_tail (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hle : yd.val ≤ if isLeap = true then 366 else 365) (h6 : ¬yd.val ≤ (Time.monthLastDayAsDayOfYear isLeap)[5].snd) : Time.Date

Equations

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

def Time.findValidMonthDay (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hle : yd.val ≤ if isLeap = true then 366 else 365) : Time.Date

Equations

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

theorem Time.isLeapYear_false {yd : Time.Icc 1 365} {dt : Time.OrdinalDate} (h : dt.dayOfYear = Time.DayOfYear.common yd) : Time.isLeapYear dt.year = false

theorem Time.isLeapYear_true {yd : Time.Icc 1 366} {dt : Time.OrdinalDate} (h : dt.dayOfYear = Time.DayOfYear.leap yd) : Time.isLeapYear dt.year = true

def Time.ordinalDateToDate (dt : Time.OrdinalDate) : Time.Date

Equations

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

theorem Time.monthLengths_month_le_12 (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → 1 ≤ a.fst ∧ a.fst ≤ 12

theorem Time.monthLengths_days_ge_28 (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → 28 ≤ a.snd

theorem Time.monthLengths_days_le_31 (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → a.snd ≤ 31

def Time.monthLength' (isLeap : Bool) (month' : Fin 12) : Nat

The length of a given month in the Gregorian or Julian calendars.

Equations

• Time.monthLength' isLeap month' = ((Time.monthLengths isLeap).get month').snd

theorem Time.monthLength'_ge_1 (isLeap : Bool) (month' : Fin 12) : 1 ≤ Time.monthLength' isLeap month'

theorem Time.monthLength'_le_31 (isLeap : Bool) (month' : Fin 12) : Time.monthLength' isLeap month' ≤ 31

theorem Time.monthAndDayToDayOfYear_gt_zero_of_month_gt (month day k : Int) (hm : 2 < month) (hk : -2 ≤ k) (hd : 0 < day) : 0 < (367 * month - 362) / 12 + k + day

theorem Time.exists_month_in_monthLastDayAsDayOfYear' (isleap : Bool) (month : Time.Icc 1 12) : ∃ (m : Nat × Nat × Nat), m ∈ Time.monthLastDayAsDayOfYear' isleap ∧ m.fst = month.val

theorem Time.exists_days_in_monthLastDayAsDayOfYear' (isleap : Bool) (month : Time.Icc 1 12) : ∃ (a : Nat), ∃ (b : Nat), (month.val, a, b) ∈ Time.monthLastDayAsDayOfYear' isleap

def Time.memOfMonth (isleap : Bool) (month : Time.Icc 1 12) : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isleap ∧ x.fst = month.val }

Equations

• Time.memOfMonth isleap month = ⟨(List.findExisting (fun (m : Nat × Nat × Nat) => decide (m.fst = month.val)) (Time.monthLastDayAsDayOfYear' isleap) ⋯).val, ⋯⟩

def Time.dy' (isleap : Bool) (month : Time.Icc 1 12) (day : Time.Icc 1 31) : Nat

Get day of year from month and day of month by lookup in monthLastDayAsDayOfYear'.

Equations

• Time.dy' isleap month day = (Time.memOfMonth isleap month).val.snd.fst + day.val - 1

theorem Time.le_dy' (isleap : Bool) (month : Time.Icc 1 12) (day : Time.Icc 1 31) : 1 ≤ Time.dy' isleap month day

theorem Time.dy'_le (isleap : Bool) (month : Time.Icc 1 12) (day : Time.Icc 1 31) : Time.dy' isleap month day ≤ if isleap = true then 366 else 365

def Time.dy (isleap : Bool) (month day : Nat) : Nat

Compute day of year from month (1..12) and day of month (1..31).

Equations

• Time.dy isleap month day = (((367 * ↑month - 362) / 12 + if month ≤ 2 then 0 else if isleap = true then -1 else -2) + ↑day).toNat

def Time.dyOfLastDayOfMonth (isleap : Bool) (month : Nat) : Nat

The day of year of the last day of a month can be computed as the predecessor of the first day of the next month.

Equations

• Time.dyOfLastDayOfMonth isleap month = Time.dy isleap (month + 1) 0

theorem Time.le_dy (isleap : Bool) (month : Time.Icc 1 12) (day : Time.Icc 1 31) : 1 ≤ Time.dy isleap month.val day.val

theorem Time.dy_le (isleap : Bool) (month : Time.Icc 1 12) (day : Time.Icc 1 31) : Time.dy isleap month.val day.val ≤ if isleap = true then 366 else 365

def Time.monthAndDayToDayOfYearClipped' (year : Int) (month day : Nat) (hd1 : 1 ≤ day) (hd2 : day ≤ 31) (hm1 : 1 ≤ month) (hm2 : month ≤ 12) : Time.OrdinalDate

Equations

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

def Time.monthAndDayToDayOfYearClipped (year : Int) (month' : Time.NonemptyIcc 1 12) (day' : Nat) (hd1 : 1 ≤ day') (hd2 : day' ≤ 31) : Time.OrdinalDate

Equations

• Time.monthAndDayToDayOfYearClipped year month' day' hd1 hd2 = Time.monthAndDayToDayOfYearClipped' year month'.icc.val day' hd1 hd2 ⋯ ⋯

theorem Time.days_le_31 (isLeap : Bool) (m : Fin 12) (day : Time.NonemptyIcc 1 (Time.monthLength' isLeap m)) : day.icc.val ≤ 31

def Time.monthAndDayToDayOfYear (year month day : Int) : Time.OrdinalDate

Convert month and day in the Gregorian or Julian calendars to day of year.

Equations

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

def Time.monthAndDayToDayOfYearValid (year month day : Int) : Option Time.OrdinalDate

Convert month and day in the Gregorian or Julian calendars to day of year option.

Equations

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

def Time.dateToOrdinalDate (dt : Time.Date) : Time.OrdinalDate

Equations

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