Theorems about Time.dy properties

Main theorems:

• Verify.DayOfYear.dy_eq_dy'
• Verify.DayOfYear.dy'_month_n_and_day_eq
• Verify.DayOfYear.dy'_month_n_and_day_eq_incr

def Verify.DayOfYear.dyOfLastDayOfMonth_map (isleap : Bool) : List Nat

Get day of year of last day of all months by Time.dy

Equations

• Verify.DayOfYear.dyOfLastDayOfMonth_map isleap = List.map (fun (m : Nat) => Time.dyOfLastDayOfMonth isleap m) (List.range' 1 12)

def Verify.DayOfYear.dy_map (isleap : Bool) : List Nat

Compute Time.dy for all days in a year

Equations

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

def Verify.DayOfYear.dy'_map (isleap : Bool) : List Nat

Equations

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

theorem Verify.DayOfYear.monthFirstDayAsDayOfYear_eq_dy (isleap : Bool) (a : Nat × Nat × Nat) : a ∈ Time.monthLastDayAsDayOfYear' isleap → a.snd.fst = Time.dy isleap a.fst 1

Get first day of month as day of year by lookup in monthLastDayAsDayOfYear is equal to compute by Time.dy

theorem Verify.DayOfYear.monthLastDayAsDayOfYear_eq_dy (isleap : Bool) (a : Nat × Nat × Nat) : a ∈ Time.monthLastDayAsDayOfYear' isleap → a.snd.snd = Time.dyOfLastDayOfMonth isleap a.fst

Get last day of month as day of year by lookup in monthLastDayAsDayOfYear is equal to compute by Time.dy

theorem Verify.DayOfYear.dy_eq_incr (isleap : Bool) (m : Time.Icc 1 12) (d : Time.Icc 1 31) : Time.dy isleap m.val d.val = Time.dy isleap m.val 1 + d.val - 1

theorem Verify.DayOfYear.dy_eq_dy' (isleap : Bool) (m : Time.Icc 1 12) (d : Time.Icc 1 31) : Time.dy isleap m.val d.val = Time.dy' isleap m d

theorem Verify.DayOfYear.lt_dy'_lt (isleap : Bool) (month : Time.Icc 1 12) (day1 day2 : Time.Icc 1 31) (hlt : day1.val < day2.val) : Time.dy' isleap month day1 < Time.dy' isleap month day2

theorem Verify.DayOfYear.dy'_hlt {dt : Time.Date} {ml : { m : Nat × Nat // MonthLength.monthLengthsOfDate m dt }} (h : dt.Day.val < ml.val.snd) : Time.dy' (Time.isLeapYear dt.Year) dt.Month dt.Day < Time.dy' (Time.isLeapYear dt.Year) dt.Month ⟨ml.val.snd, ⋯⟩

theorem Verify.DayOfYear.dy'_hle {dt : Time.Date} (ml : { m : Nat × Nat // MonthLength.monthLengthsOfDate m dt }) : Time.dy' (Time.isLeapYear dt.Year) dt.Month ⟨ml.val.snd, ⋯⟩ ≤ if Time.isLeapYear dt.Year = true then 366 else 365

theorem Verify.DayOfYear.dy'_hlt' {dt : Time.Date} {ml : { m : Nat × Nat // MonthLength.monthLengthsOfDate m dt }} (h : dt.Day.val < ml.val.snd) : Time.dy' (Time.isLeapYear dt.Year) dt.Month dt.Day < if Time.isLeapYear dt.Year = true then 366 else 365

theorem Verify.DayOfYear.dy'_add_one_hle {dt : Time.Date} {ml : { m : Nat × Nat // MonthLength.monthLengthsOfDate m dt }} (h : dt.Day.val < ml.val.snd) : Time.dy' (Time.isLeapYear dt.Year) dt.Month dt.Day + 1 ≤ if Time.isLeapYear dt.Year = true then 366 else 365

theorem Verify.DayOfYear.dy'_lt_of_month_lt {dt : Time.Date} (h : dt.Month.val < 12) : Time.dy' (Time.isLeapYear dt.Year) dt.Month dt.Day < if Time.isLeapYear dt.Year = true then 366 else 365

theorem Verify.DayOfYear.dy_lt_of_month_lt {dt : Time.Date} (h : dt.Month.val < 12) : match (Time.dateToOrdinalDate dt).dayOfYear with | Time.DayOfYear.common dy => dy.val < 365 | Time.DayOfYear.leap dy => dy.val < 366

theorem Verify.DayOfYear.dy_lt_of_day_lt {dt : Time.Date} {ml : { m : Nat × Nat // MonthLength.monthLengthsOfDate m dt }} (h : dt.Day.val < ml.val.snd) : match (Time.dateToOrdinalDate dt).dayOfYear with | Time.DayOfYear.common dy => dy.val < 365 | Time.DayOfYear.leap dy => dy.val < 366

theorem Verify.DayOfYear.dy_lt_of_day_or_month_lt {dt : Time.Date} {ml : { m : Nat × Nat // MonthLength.monthLengthsOfDate m dt }} (h : dt.Day.val < ml.val.snd ∨ dt.Month.val < 12) : match (Time.dateToOrdinalDate dt).dayOfYear with | Time.DayOfYear.common dy => dy.val < 365 | Time.DayOfYear.leap dy => dy.val < 366

theorem Verify.DayOfYear.dy'_month_1_eq (dt : Time.Date) (isleap : Bool) (h : Time.dy' isleap dt.Month dt.Day ≤ 30) : 1 = dt.Month.val

theorem Verify.DayOfYear.dy'_month_1_day_eq (dt : Time.Date) (isleap : Bool) (h : Time.dy' isleap dt.Month dt.Day ≤ 30) : Time.dy' isleap dt.Month dt.Day = dt.Day.val

theorem Verify.DayOfYear.dy'_day_n_eq (isleap : Bool) (i : Fin (Time.monthLastDayAsDayOfYear' isleap).length) (hle : 1 ≤ ↑i) (a : Nat × Nat × Nat) (h : (Time.monthLastDayAsDayOfYear' isleap)[↑i] = a) : (Time.monthLastDayAsDayOfYear' isleap)[↑i - 1].snd.snd + 1 = a.snd.fst

theorem Verify.DayOfYear.dy'_day_n_eq_incr (isleap : Bool) (dt : Time.Date) (i i' : Fin (Time.monthLastDayAsDayOfYear' isleap).length) (hi : ↑i - 1 = ↑i') (a : Nat × Nat × Nat) (h1 : (Time.monthLastDayAsDayOfYear' isleap)[↑i'] = a) (h2 : dt.Day.val = (Time.monthLastDayAsDayOfYear' isleap)[↑i'].snd.snd - (Time.monthLastDayAsDayOfYear' isleap)[↑i'].snd.fst + 1) : a.snd.fst + dt.Day.val - ((Time.monthLastDayAsDayOfYear isleap).get ⟨↑i - 1, ⋯⟩).snd = 1

theorem Verify.DayOfYear.dy'_month_n_and_day_eq (dt : Time.Date) (isleap : Bool) (i : Fin (Time.monthLastDayAsDayOfYear isleap).length) (hle : 1 ≤ ↑i) (hl : Time.isLeapYear dt.Year = isleap) {ml : { m : Nat × Nat // MonthLength.monthLengthsOfDate m dt }} (hml : ml = MonthLength.monthLengths_of_date dt) (h : dt.Day.val < ml.val.snd) (h1 : ((Time.monthLastDayAsDayOfYear isleap).get ⟨↑i - 1, ⋯⟩).snd < Time.dy' isleap dt.Month dt.Day + 1) (h2 : Time.dy' isleap dt.Month dt.Day + 1 ≤ ((Time.monthLastDayAsDayOfYear isleap).get i).snd) : ↑i + 1 = dt.Month.val ∧ dt.Day.val + 1 = Time.dy' isleap dt.Month dt.Day + 1 - ((Time.monthLastDayAsDayOfYear isleap).get ⟨↑i - 1, ⋯⟩).snd

theorem Verify.DayOfYear.dy'_month_n_and_day_eq_incr (dt : Time.Date) (isleap : Bool) (i : Fin (Time.monthLastDayAsDayOfYear isleap).length) (hle : 1 ≤ ↑i) (hl : Time.isLeapYear dt.Year = isleap) {ml : { m : Nat × Nat // MonthLength.monthLengthsOfDate m dt }} (hml : ml = MonthLength.monthLengths_of_date dt) (h : dt.Day.val = ml.val.snd) (h1 : ((Time.monthLastDayAsDayOfYear isleap).get ⟨↑i - 1, ⋯⟩).snd < Time.dy' isleap dt.Month dt.Day + 1) (h2 : Time.dy' isleap dt.Month dt.Day + 1 ≤ ((Time.monthLastDayAsDayOfYear isleap).get i).snd) : ↑i = dt.Month.val ∧ Time.dy' isleap dt.Month dt.Day + 1 - ((Time.monthLastDayAsDayOfYear isleap).get ⟨↑i - 1, ⋯⟩).snd = 1