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 : Icc 1 12
• Day : Icc 1 31
• IsValid : ∃ (m : Nat × Nat), m ∈ monthLengths (isLeapYear self.Year) ∧ m.fst = self.Month.val ∧ self.Day.val ≤ m.snd

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

instance Time.instReprDate : Repr 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 : 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.«date-___-___-__» : Lean.ParserDescr

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 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 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.monthLengths_length_eq_12 (isleap : Bool) : (monthLengths isleap).length = 12

@[simp]

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

@[simp]

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

instance Time.instCoeFinLengthProdNatMonthLengthsMonthLastDayAsDayOfYear' {isleap : Bool} : Coe (Fin (monthLengths isleap).length) (Fin (monthLastDayAsDayOfYear' isleap).length)

Equations

• Time.instCoeFinLengthProdNatMonthLengthsMonthLastDayAsDayOfYear' = { coe := fun (x : Fin (Time.monthLengths isleap).length) => Fin.cast ⋯ x }

instance Time.instCoeFinLengthProdNatMonthLastDayAsDayOfYear'MonthLengths {isleap : Bool} : Coe (Fin (monthLastDayAsDayOfYear' isleap).length) (Fin (monthLengths isleap).length)

Equations

• Time.instCoeFinLengthProdNatMonthLastDayAsDayOfYear'MonthLengths = { coe := fun (x : Fin (Time.monthLastDayAsDayOfYear' isleap).length) => Fin.cast ⋯ x }

instance Time.instCoeFinLengthProdNatMonthLastDayAsDayOfYear'MonthLastDayAsDayOfYear {isleap : Bool} : Coe (Fin (monthLastDayAsDayOfYear' isleap).length) (Fin (monthLastDayAsDayOfYear isleap).length)

Equations

• Time.instCoeFinLengthProdNatMonthLastDayAsDayOfYear'MonthLastDayAsDayOfYear = { coe := fun (x : Fin (Time.monthLastDayAsDayOfYear' isleap).length) => Fin.cast ⋯ x }

instance Time.instCoeFinLengthProdNatMonthLastDayAsDayOfYearMonthLastDayAsDayOfYear' {isleap : Bool} : Coe (Fin (monthLastDayAsDayOfYear isleap).length) (Fin (monthLastDayAsDayOfYear' isleap).length)

Equations

• Time.instCoeFinLengthProdNatMonthLastDayAsDayOfYearMonthLastDayAsDayOfYear' = { coe := fun (x : Fin (Time.monthLastDayAsDayOfYear isleap).length) => Fin.cast ⋯ x }

theorem Time.monthLengths_nodup {isleap : Bool} : (monthLengths isleap).Nodup = (true = true)

theorem Time.monthLastDayAsDayOfYear_nodup {isleap : Bool} : (monthLastDayAsDayOfYear isleap).Nodup = (true = true)

theorem Time.monthLastDayAsDayOfYear'_nodup {isleap : Bool} : (monthLastDayAsDayOfYear' isleap).Nodup = (true = true)

theorem Time.monthLastDayAsDayOfYear'_fst_eq_of_le_31 (isleap : Bool) (a : Fin (monthLastDayAsDayOfYear' isleap).length) : (monthLastDayAsDayOfYear' isleap)[a].snd.fst ≤ 31 → (monthLastDayAsDayOfYear' isleap)[a].fst = 1

theorem Time.monthLastDayAsDayOfYear'_snd_eq_of_eq_1 (isleap : Bool) (a : Fin (monthLastDayAsDayOfYear' isleap).length) : (monthLastDayAsDayOfYear' isleap)[a].fst = 1 → (monthLastDayAsDayOfYear' isleap)[a].snd.fst = 1

theorem Time.monthLastDayAsDayOfYear'_month_eq (isleap : Bool) (a : Fin (monthLastDayAsDayOfYear' isleap).length) : (monthLastDayAsDayOfYear' isleap)[a].fst = ↑a + 1

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

theorem Time.monthLastDayAsDayOfYear_snd_eq (isleap : Bool) (i : Fin (monthLastDayAsDayOfYear isleap).length) : ((monthLastDayAsDayOfYear isleap).get i).snd = ((monthLastDayAsDayOfYear' isleap).get (Fin.cast ⋯ i)).snd.snd

theorem Time.monthLastDayAsDayOfYear'_snd_eq (isleap : Bool) (i : Fin (monthLastDayAsDayOfYear' isleap).length) : ((monthLastDayAsDayOfYear' isleap).get i).snd.snd = ((monthLastDayAsDayOfYear isleap).get (Fin.cast ⋯ i)).snd

theorem Time.monthLastDayAsDayOfYear'_fst_eq (isleap : Bool) (i : Fin (monthLastDayAsDayOfYear' isleap).length) : (monthLastDayAsDayOfYear' isleap)[↑i].fst = (monthLengths isleap)[↑i].fst

theorem Time.monthLastDayAsDayOfYear'_fst_lt_snd (isleap : Bool) (i : Fin (monthLastDayAsDayOfYear' isleap).length) : ((monthLastDayAsDayOfYear' isleap).get i).snd.fst < ((monthLastDayAsDayOfYear' isleap).get i).snd.snd

theorem Time.monthLengths_index_eq_of_fst_eq (isleap : Bool) (i i' : Fin (monthLengths isleap).length) : (monthLengths isleap)[↑i].fst = (monthLengths isleap)[↑i'].fst → ↑i = ↑i'

theorem Time.monthLastDayAsDayOfYear'_index_le_of_fst_lt_snd (isleap : Bool) (i i' : Fin (monthLastDayAsDayOfYear' isleap).length) : ((monthLastDayAsDayOfYear' isleap).get i').snd.fst < ((monthLastDayAsDayOfYear' isleap).get i).snd.snd → ↑i' ≤ ↑i

theorem Time.monthLastDayAsDayOfYear'_index_le_of_fst_le_snd (isleap : Bool) (i i' : Fin (monthLastDayAsDayOfYear' isleap).length) : ((monthLastDayAsDayOfYear' isleap).get i').snd.fst ≤ ((monthLastDayAsDayOfYear' isleap).get i).snd.snd → ↑i' ≤ ↑i

theorem Time.monthLastDayAsDayOfYear'_index_le_of_fst_le_snd_incr (isleap : Bool) (i i' : Fin (monthLastDayAsDayOfYear' isleap).length) : ((monthLastDayAsDayOfYear' isleap).get i').snd.fst ≤ ((monthLastDayAsDayOfYear' isleap).get i).snd.snd + 1 → ↑i' ≤ ↑i + 1

theorem Time.monthLastDayAsDayOfYear'_index_le_of_snd_le_snd_incr (isleap : Bool) (i i' : Fin (monthLastDayAsDayOfYear' isleap).length) : ((monthLastDayAsDayOfYear' isleap).get i').snd.snd + 1 ≤ ((monthLastDayAsDayOfYear' isleap).get i).snd.snd → ↑i' + 1 ≤ ↑i

theorem Time.monthLastDayAsDayOfYear'_index_le_of_fst_le_fst (isleap : Bool) (i i' : Fin (monthLastDayAsDayOfYear' isleap).length) : ((monthLastDayAsDayOfYear' isleap).get i').snd.fst ≤ ((monthLastDayAsDayOfYear' isleap).get i).snd.fst + 31 → ↑i' ≤ ↑i + 1

theorem Time.monthLastDayAsDayOfYear'_pred_snd_incr_eq_fst (isleap : Bool) (i : Fin (monthLastDayAsDayOfYear' isleap).length) : ↑i > 0 → ((monthLastDayAsDayOfYear' isleap).get i).snd.fst = ((monthLastDayAsDayOfYear' isleap).get ⟨↑i - 1, ⋯⟩).snd.snd + 1

theorem Time.monthLastDayAsDayOfYear'_pred_snd_lt_fst (isleap : Bool) (i : Fin (monthLastDayAsDayOfYear' isleap).length) : ↑i > 0 → ((monthLastDayAsDayOfYear' isleap).get ⟨↑i - 1, ⋯⟩).snd.snd < ((monthLastDayAsDayOfYear' isleap).get i).snd.fst

theorem Time.monthLastDayAsDayOfYear'_sub_eq (isleap : Bool) (i : Fin (monthLastDayAsDayOfYear' isleap).length) : ((monthLengths isleap).get (Fin.cast ⋯ i)).snd = ((monthLastDayAsDayOfYear' isleap).get i).snd.snd - ((monthLastDayAsDayOfYear' isleap).get i).snd.fst + 1

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

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

theorem Time.monthLastDayAsDayOfYear'_sub_days_le (isleap : Bool) (i : Fin (monthLastDayAsDayOfYear' isleap).length) : ((monthLastDayAsDayOfYear' isleap).get i).snd.snd - ((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 (monthLastDayAsDayOfYear' isLeap).length) (h2 : yd ≤ (monthLastDayAsDayOfYear' isLeap)[i].snd.snd) : 1 ≤ yd - (monthLastDayAsDayOfYear' isLeap)[i].snd.fst + 1 ∧ yd - (monthLastDayAsDayOfYear' isLeap)[i].snd.fst + 1 ≤ 31

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

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

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) : monthLengths_sum_le_map isleap = List.map (fun (x : Nat × Nat) => x.snd) (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) : (monthLengths_sum isleap == if isleap = true then 366 else 365) = true

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

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

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

theorem Time.monthLengths_month_eq (isleap : Bool) (a : Fin (monthLengths isleap).length) : (monthLengths isleap)[a].fst = ↑a + 1

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

theorem Time.monthLengths_eq (isleap : Bool) : (monthLengths isleap).length = (monthLastDayAsDayOfYear isleap).length

theorem Time.month_le_val_exists (isleap : Bool) (i v : Nat) (hle : 1 ≤ i) (hlt : i < (monthLengths isleap).length) (h1 : ((monthLastDayAsDayOfYear isleap).get ⟨i - 1, ⋯⟩).snd < v) (h2 : v ≤ ((monthLastDayAsDayOfYear isleap).get ⟨i, ⋯⟩).snd) : ∃ (m : Nat × Nat), m ∈ monthLengths isleap ∧ m.fst = i + 1 ∧ v - ((monthLastDayAsDayOfYear isleap).get ⟨i - 1, ⋯⟩).snd ≤ m.snd

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 : Icc 1 366) (h : yd.val ≤ ((monthLastDayAsDayOfYear isLeap).get ⟨0, ⋯⟩).snd) : 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_n (year : Int) (isLeap : Bool) (i : Nat) (yd : Icc 1 366) (hl : isLeapYear year = isLeap) (hle : 1 ≤ i) (hlt : i < (monthLengths isLeap).length) (hlt' : i < (monthLastDayAsDayOfYear isLeap).length) (hn : ¬yd.val ≤ ((monthLastDayAsDayOfYear isLeap).get ⟨i - 1, ⋯⟩).snd) (h : yd.val ≤ ((monthLastDayAsDayOfYear isLeap).get ⟨i, hlt'⟩).snd) : Date

Equations

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

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

Equations

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

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

Equations

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

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

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

def Time.ordinalDateToDate (dt : OrdinalDate) : 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 ∈ monthLengths isleap → 1 ≤ a.fst ∧ a.fst ≤ 12

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

theorem Time.monthLengths_days_le_31 (isleap : Bool) (a : Nat × Nat) : a ∈ 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 ≤ monthLength' isLeap month'

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

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

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

def Time.memOfMonth (isleap : Bool) (month : Icc 1 12) : { x : Nat × Nat × Nat // x ∈ 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 : Icc 1 12) (day : 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 : Icc 1 12) (day : Icc 1 31) : 1 ≤ dy' isleap month day

theorem Time.dy'_le (isleap : Bool) (month : Icc 1 12) (day : Icc 1 31) : 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 : Icc 1 12) (day : Icc 1 31) : 1 ≤ dy isleap month.val day.val

theorem Time.dy_le (isleap : Bool) (month : Icc 1 12) (day : Icc 1 31) : 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) : OrdinalDate

Equations

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

def Time.monthAndDayToDayOfYearClipped (year : Int) (month' : NonemptyIcc 1 12) (day' : Nat) (hd1 : 1 ≤ day') (hd2 : day' ≤ 31) : 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 : NonemptyIcc 1 (monthLength' isLeap m)) : day.icc.val ≤ 31

def Time.monthAndDayToDayOfYear (year month day : Int) : 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 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 : Date) : OrdinalDate

Equations

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