Verify date calculations

Main theorems:

• Verify.Gregorian.next_date_eq_next_date,
• Verify.Gregorian.next_date_eq_add_one,
• Verify.Gregorian.next_date_eq_mjd_add_one.

def Verify.Gregorian.next_date (dt : Time.Date) : Time.Date

Get next_date of dt:

• if dt.Day is less then days in dt.Month then add 1 to dt.Day,
• else if dt.Month less then 12 then add 1 to dt.Month and set dt.Day to 1,
• else add 1 to dt.Year and set dt.Day and dt.Month to 1.

See UTC Time, Formally Verified.

Equations

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

theorem Verify.Gregorian.zero_of_modified_julian_day_eq : (Time.fromGregorian { Year := 1858, Month := ⟨11, ⋯⟩, Day := ⟨17, ⋯⟩, IsValid := ⋯ } == { modifiedJulianDay := 0 }) = true

the modified julian day of day 1858-11-17 should have value zero.

theorem Verify.Gregorian.default_of_modified_julian_day_eq : (Time.fromGregorian default == default) = true

the default values of Date and Day are january 1 of year 1 and should be equal.

theorem Verify.Gregorian.next_date_of_day_lt_eq' {dt : Time.Date} {dy : Nat} {ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }} (hml : ml = Verify.MonthLength.monthLengths_of_date dt) (h : dt.Day.val < ml.val.snd) (heq : Time.dy' false dt.Month dt.Day = dy) (hl : Time.isLeapYear dt.Year = false) : { Year := dt.Year, Month := dt.Month, Day := ⟨dt.Day.val + 1, ⋯⟩, IsValid := ⋯ } = Time.ordinalDateToDate { year := dt.Year, dayOfYear := Time.DayOfYear.common ⟨dy + 1, ⋯⟩, isValid := ⋯ }

theorem Verify.Gregorian.next_date_of_day_lt_eq'' {dt : Time.Date} {dy : Nat} {ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }} (hml : ml = Verify.MonthLength.monthLengths_of_date dt) (h : dt.Day.val < ml.val.snd) (heq : Time.dy' true dt.Month dt.Day = dy) (hl : Time.isLeapYear dt.Year = true) : { Year := dt.Year, Month := dt.Month, Day := ⟨dt.Day.val + 1, ⋯⟩, IsValid := ⋯ } = Time.ordinalDateToDate { year := dt.Year, dayOfYear := Time.DayOfYear.leap ⟨dy + 1, ⋯⟩, isValid := ⋯ }

theorem Verify.Gregorian.next_date_of_day_lt_eq (dt : Time.Date) (ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }) (hml : ml = Verify.MonthLength.monthLengths_of_date dt) (h : dt.Day.val < ml.val.snd) : { Year := dt.Year, Month := dt.Month, Day := ⟨dt.Day.val + 1, ⋯⟩, IsValid := ⋯ } = Time.ordinalDateToDate (Verify.OrdinalDate.next_date (Time.dateToOrdinalDate dt))

theorem Verify.Gregorian.next_date_of_last_day_of_month_eq' {simp : 1 ≤ 1 ∧ 1 ≤ 31} {dt : Time.Date} {dy : Nat} {ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }} (hml : ml = Verify.MonthLength.monthLengths_of_date dt) (h : dt.Day.val = ml.val.snd) (hm : dt.Month.val < 12) (heq : Time.dy' false dt.Month dt.Day = dy) (hl : Time.isLeapYear dt.Year = false) : { Year := dt.Year, Month := ⟨dt.Month.val + 1, ⋯⟩, Day := ⟨1, simp⟩, IsValid := ⋯ } = Time.ordinalDateToDate { year := dt.Year, dayOfYear := Time.DayOfYear.common ⟨dy + 1, ⋯⟩, isValid := ⋯ }

theorem Verify.Gregorian.next_date_of_last_day_of_month_eq'' {simp : 1 ≤ 1 ∧ 1 ≤ 31} {dt : Time.Date} {dy : Nat} {ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }} (hml : ml = Verify.MonthLength.monthLengths_of_date dt) (h : dt.Day.val = ml.val.snd) (hm : dt.Month.val < 12) (heq : Time.dy' true dt.Month dt.Day = dy) (hl : Time.isLeapYear dt.Year = true) : { Year := dt.Year, Month := ⟨dt.Month.val + 1, ⋯⟩, Day := ⟨1, simp⟩, IsValid := ⋯ } = Time.ordinalDateToDate { year := dt.Year, dayOfYear := Time.DayOfYear.leap ⟨dy + 1, ⋯⟩, isValid := ⋯ }

theorem Verify.Gregorian.next_date_of_last_day_of_month_eq {simp : 1 ≤ 1 ∧ 1 ≤ 31} (dt : Time.Date) (ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }) (hml : ml = Verify.MonthLength.monthLengths_of_date dt) (h : ¬dt.Day.val < ml.val.snd) (hm : dt.Month.val < 12) : { Year := dt.Year, Month := ⟨dt.Month.val + 1, ⋯⟩, Day := ⟨1, simp⟩, IsValid := ⋯ } = Time.ordinalDateToDate (Verify.OrdinalDate.next_date (Time.dateToOrdinalDate dt))

theorem Verify.Gregorian.dy'_of_last_day_of_year (dt : Time.Date) (ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }) (hml : ml = Verify.MonthLength.monthLengths_of_date dt) (h1 : ¬dt.Day.val < ml.val.snd) (h2 : ¬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.Gregorian.next_date_of_last_day_of_year_eq (dt : Time.Date) (ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }) (hml : ml = Verify.MonthLength.monthLengths_of_date dt) (h1 : ¬dt.Day.val < ml.val.snd) (h2 : ¬dt.Month.val < 12) : { Year := dt.Year + 1, Month := ⟨1, ⋯⟩, Day := ⟨1, ⋯⟩, IsValid := ⋯ } = Time.ordinalDateToDate (Verify.OrdinalDate.next_date (Time.dateToOrdinalDate dt))

theorem Verify.Gregorian.next_date_eq_next_date (dt : Time.Date) : Verify.Gregorian.next_date dt = Time.ordinalDateToDate (Verify.OrdinalDate.next_date (Time.dateToOrdinalDate dt))

Verify.Gregorian.next_date transforms to Verify.OrdinalDate.next_date

theorem Verify.Gregorian.next_date_eq_mjd_add_one (dt : Time.Date) : Verify.Gregorian.next_date dt = Time.ordinalDateToDate (Time.toOrdinalDate (Time.Day.addDays 1 (Time.fromOrdinalDate (Time.dateToOrdinalDate dt))))

Verify.Gregorian.next_date transforms to Time.Day.addDays 1.

theorem Verify.Gregorian.next_date_eq_add_one (dt : Time.Date) : Verify.Gregorian.next_date dt = Time.Gregorian.addDays 1 dt

Verify.Gregorian.next_date equals to Time.Gregorian.addDays 1.