Verify date calculations

Main theorems:

• Verify.OrdinalDate.toOrdinalDate_fromOrdinalDate_eq_id
• Verify.OrdinalDate.next_date_eq_add_one
• Verify.OrdinalDate.next_date_eq_mjd_add_one

def Verify.OrdinalDate.next_date (dt : Time.OrdinalDate) : Time.OrdinalDate

Get next_date of dt:

• if dt.dayOfYear is less then days in dt.year then add 1 to dt.dayOfYear,
• else add 1 to dt.Year and set dt.dayOfYear to 1.

Equations

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

def Verify.OrdinalDate.DayOfYear.lt_top (d : Time.DayOfYear) : Bool

Equations

• Verify.OrdinalDate.DayOfYear.lt_top (Time.DayOfYear.common ⟨dy, property⟩) = decide (dy < 365)
• Verify.OrdinalDate.DayOfYear.lt_top (Time.DayOfYear.leap ⟨dy, property⟩) = decide (dy < 366)

def Verify.OrdinalDate.DayOfYear.incr (dt : Time.OrdinalDate) (h : lt_top dt.dayOfYear = true) : Time.OrdinalDate

Equations

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

theorem Verify.OrdinalDate.icc_eq (dt : Time.OrdinalDate) (a : Time.Icc 1 365) (h : dt.dayOfYear = Time.DayOfYear.common a) : ⟨a.val, ⋯⟩ = match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d

theorem Verify.OrdinalDate.icc_eq' (dt : Time.OrdinalDate) (a : Time.Icc 1 366) (h : dt.dayOfYear = Time.DayOfYear.leap a) : a = match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d

theorem Verify.OrdinalDate.val_eq (dt : Time.OrdinalDate) (a : Time.Icc 1 365) (h : dt.dayOfYear = Time.DayOfYear.common a) : a.val = (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val

theorem Verify.OrdinalDate.val_eq' (dt : Time.OrdinalDate) (a : Time.Icc 1 366) (h : dt.dayOfYear = Time.DayOfYear.leap a) : a.val = (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val

theorem Verify.OrdinalDate.mjd_incr_eq_next_date (dt : Time.OrdinalDate) : (Time.fromOrdinalDate (next_date dt)).modifiedJulianDay = (Time.fromOrdinalDate dt).modifiedJulianDay + 1

theorem Verify.OrdinalDate.transform_of_next_date_eq_add_one (dt : Time.OrdinalDate) : Time.toOrdinalDate (Time.fromOrdinalDate (next_date dt)) = Time.OrdinalDate.addDays 1 dt

theorem Verify.OrdinalDate.Int.self_mul_ediv_le {x k : Int} (h : k ≠ 0) : x / k * k ≤ x

theorem Verify.OrdinalDate.Icc.minus_one_add_le {b : Nat} (x : Time.Icc 1 b) : 0 ≤ -1 + ↑x.val

theorem Verify.OrdinalDate.Icc.minus_one_add_lt {a b : Nat} (x : Time.Icc a b) : -1 + ↑x.val < ↑b

theorem Verify.OrdinalDate.assoc' (a b c : Int) : a - c + b = a + (-c + b)

def Verify.OrdinalDate.days_in_100_years_without_year_divisible_by_400 : Nat

Equations

• Verify.OrdinalDate.days_in_100_years_without_year_divisible_by_400 = 76 * 365 + 24 * 366

theorem Verify.OrdinalDate.days_in_100_years_without_year_divisible_by_400_eq : days_in_100_years_without_year_divisible_by_400 = 36524

def Verify.OrdinalDate.days_in_400_years : Nat

Equations

• Verify.OrdinalDate.days_in_400_years = 4 * Verify.OrdinalDate.days_in_100_years_without_year_divisible_by_400 + 1

theorem Verify.OrdinalDate.days_in_400_years_eq : days_in_400_years = 146097

def Verify.OrdinalDate.days_since_1_1_1 (dt : Time.OrdinalDate) (a : Time.Icc 1 366) : Int

Equations

• Verify.OrdinalDate.days_since_1_1_1 dt a = Time.toModifiedJulianDay dt.year a.val - default.modifiedJulianDay

def Verify.OrdinalDate.days_since_1_1_1_mod_146097 (dt : Time.OrdinalDate) (a : Time.Icc 1 366) : Int

Equations

• Verify.OrdinalDate.days_since_1_1_1_mod_146097 dt a = 365 * (dt.year - 1 - (dt.year - 1) / 400 * 400) + (dt.year - 1) / 4 - (dt.year - 1) / 400 * 96 - (dt.year - 1) / 100 - 1 + ↑a.val

def Verify.OrdinalDate.days_since_1_1_1_mod_146097' (dt : Time.OrdinalDate) (a : Time.Icc 1 366) : Int

Equations

• Verify.OrdinalDate.days_since_1_1_1_mod_146097' dt a = Verify.OrdinalDate.days_since_1_1_1 dt a - (dt.year - 1) / 400 * 146097

theorem Verify.OrdinalDate.days_since_1_1_1_mod_146097'_eq (dt : Time.OrdinalDate) (a : Time.Icc 1 366) : days_since_1_1_1_mod_146097 dt a = days_since_1_1_1_mod_146097' dt a

def Verify.OrdinalDate.days_in_years_sub_one (year : Int) : Int

Equations

• Verify.OrdinalDate.days_in_years_sub_one year = 365 * year + year / 4 - year / 100

theorem Verify.OrdinalDate.days_in_400_years_sub_one_eq : days_in_years_sub_one 400 = ↑days_in_400_years - 1

theorem Verify.OrdinalDate.days_in_400_years_sub_one_eq_mul (n : Int) : days_in_years_sub_one (n * 400) = n * 146096

theorem Verify.OrdinalDate.days_in_400_years_sub_one_eq_mod (n : Int) : days_in_years_sub_one (n * 400) % 146096 = 0

theorem Verify.OrdinalDate.days_since_1_1_1_mod_146097_le (dt : Time.OrdinalDate) : 0 ≤ days_since_1_1_1_mod_146097 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d)

theorem Verify.OrdinalDate.days_since_1_1_1_mod_146097_lt (dt : Time.OrdinalDate) : days_since_1_1_1_mod_146097 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d) < 146097

theorem Verify.OrdinalDate.days_since_1_1_1_mul_mod (dt : Time.OrdinalDate) (a : Time.Icc 1 366) : days_since_1_1_1 dt a = (dt.year - 1) / 400 * 146097 + days_since_1_1_1_mod_146097 dt a

theorem Verify.OrdinalDate.days_since_1_1_1_mod_146097_div_eq_zero (dt : Time.OrdinalDate) : days_since_1_1_1_mod_146097 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d) / 146097 = 0

def Verify.OrdinalDate.quadcent (dt : Time.OrdinalDate) : Int

Equations

• Verify.OrdinalDate.quadcent dt = (dt.year - 1) / 400

theorem Verify.OrdinalDate.days_since_1_1_1_div_eq (dt : Time.OrdinalDate) : days_since_1_1_1 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d) / 146097 = quadcent dt

theorem Verify.OrdinalDate.days_since_1_1_1_mod_eq (dt : Time.OrdinalDate) : days_since_1_1_1 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d) % 146097 = days_since_1_1_1_mod_146097 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d)

def Verify.OrdinalDate.cent (dt : Time.OrdinalDate) : Int

Equations

• Verify.OrdinalDate.cent dt = (dt.year - 1 - Verify.OrdinalDate.quadcent dt * 400) / 100

def Verify.OrdinalDate.days_since_1_1_1_mod_146097_mod_36524 (dt : Time.OrdinalDate) (a : Time.Icc 1 366) : Int

Equations

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

theorem Verify.OrdinalDate.days_since_1_1_1_mod_146097_mul_mod (dt : Time.OrdinalDate) (a : Time.Icc 1 366) : days_since_1_1_1_mod_146097 dt a = cent dt * 36524 + days_since_1_1_1_mod_146097_mod_36524 dt a

theorem Verify.OrdinalDate.days_since_1_1_1_mod_146097_mod_36524_le (dt : Time.OrdinalDate) : 0 ≤ days_since_1_1_1_mod_146097_mod_36524 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d)

theorem Verify.OrdinalDate.days_since_1_1_1_mod_146097_mod_36524_lt (dt : Time.OrdinalDate) (h : ¬(dt.year % 400 = 0 ∧ (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val = 366)) : days_since_1_1_1_mod_146097_mod_36524 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d) < 36524

theorem Verify.OrdinalDate.days_since_1_1_1_mod_146097_div_eq (dt : Time.OrdinalDate) (h : ¬(dt.year % 400 = 0 ∧ (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val = 366)) : days_since_1_1_1_mod_146097 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d) / 36524 = cent dt

theorem Verify.OrdinalDate.cent_eq (dt : Time.OrdinalDate) (h : ¬(dt.year % 400 = 0 ∧ (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val = 366)) : cent dt = days_since_1_1_1_mod_146097 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d) / 36524

def Verify.OrdinalDate.dayOfYear_with_day_one (dt : Time.OrdinalDate) : Time.DayOfYear

Equations

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

def Verify.OrdinalDate.dt_with_day_one (dt : Time.OrdinalDate) : Time.OrdinalDate

Equations

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

def Verify.OrdinalDate.quad (dt : Time.OrdinalDate) : Int

Equations

• Verify.OrdinalDate.quad dt = (dt.year - 1 - Verify.OrdinalDate.quadcent dt * 400 - Verify.OrdinalDate.cent dt * 100) / 4

def Verify.OrdinalDate.c (dt : Time.OrdinalDate) : Int

Equations

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

def Verify.OrdinalDate.c_value_factor (dt : Time.OrdinalDate) : Int

Equations

• Verify.OrdinalDate.c_value_factor dt = if ¬dt.year % 4 = 0 then dt.year % 100 / 4 else if ¬dt.year % 100 = 0 then dt.year % 100 / 4 - 1 else 24

theorem Verify.OrdinalDate.c_value_factor_eq (dt dt' : Time.OrdinalDate) (h : dt.year = dt'.year) : c_value_factor dt = c_value_factor dt'

def Verify.OrdinalDate.c_value (dt : Time.OrdinalDate) : Int

Equations

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

theorem Verify.OrdinalDate.year_of_dt_with_day_one_eq (dt : Time.OrdinalDate) : dt.year = (dt_with_day_one dt).year

theorem Verify.OrdinalDate.dayOfYear_of_dt_with_day_one_eq (dt : Time.OrdinalDate) : dayOfYear_with_day_one dt = (dt_with_day_one dt).dayOfYear

theorem Verify.OrdinalDate.dayOfYear_of_dt_with_day_one_val_eq (dt : Time.OrdinalDate) : (match dayOfYear_with_day_one dt with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val = 1

theorem Verify.OrdinalDate.c_value_factor_of_dt_with_day_one_eq (dt : Time.OrdinalDate) : c_value_factor dt = c_value_factor (dt_with_day_one dt)

theorem Verify.OrdinalDate.c_value_of_dt_with_day_one_eq (dt : Time.OrdinalDate) : c_value (dt_with_day_one dt) = (dt.year - 1) % 4 * 365 + c_value_factor dt * 1461

theorem Verify.OrdinalDate.c_value_add_eq (dt : Time.OrdinalDate) : c_value dt = c_value (dt_with_day_one dt) + ↑(match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val - 1

theorem Verify.OrdinalDate.c_eq_c_value (dt : Time.OrdinalDate) : c dt = c_value dt

def Verify.OrdinalDate.c_mod_1461 (dt : Time.OrdinalDate) : Int

Equations

• Verify.OrdinalDate.c_mod_1461 dt = Verify.OrdinalDate.c dt - Verify.OrdinalDate.quad dt * 1461

def Verify.OrdinalDate.d' (dt : Time.OrdinalDate) : Int

Equations

• Verify.OrdinalDate.d' dt = Verify.OrdinalDate.c dt % 1461

theorem Verify.OrdinalDate.d'_lt (dt : Time.OrdinalDate) : d' dt < 1461

theorem Verify.OrdinalDate.c_value_div_eq (dt : Time.OrdinalDate) : c_value dt / 1461 = c_value_factor dt

theorem Verify.OrdinalDate.c_div_eq (dt : Time.OrdinalDate) : c (dt_with_day_one dt) / 1461 = c dt / 1461

theorem Verify.OrdinalDate.c_one_div_eq_quad (dt : Time.OrdinalDate) : c (dt_with_day_one dt) / 1461 = quad dt

theorem Verify.OrdinalDate.c_div_eq_quad (dt : Time.OrdinalDate) : c dt / 1461 = quad dt

theorem Verify.OrdinalDate.year_eq_if_mod_eq_146096 (dt : Time.OrdinalDate) (a : Time.Icc 1 366) (h : days_since_1_1_1_mod_146097 dt a = 146096) : quadcent dt * 400 + 3 * 100 + 24 * 4 + 4 = dt.year

theorem Verify.OrdinalDate.mod_lt_146096_eq (dt : Time.OrdinalDate) (h : days_since_1_1_1_mod_146097 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d) < 146096) : ¬(dt.year % 400 = 0 ∧ (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val = 366)

theorem Verify.OrdinalDate.d'_add_eq (dt : Time.OrdinalDate) : d' dt = (dt.year - 1) % 4 * 365 + ↑(match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val - 1

theorem Verify.OrdinalDate.days_eq_1460_mod_4_eq (dt : Time.OrdinalDate) (hmod : d' dt = 1460) : dt.year % 4 = 0

theorem Verify.OrdinalDate.day_eq_if_days_eq_1460 (dt : Time.OrdinalDate) (hmod : d' dt = 1460) : (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val = 366

theorem Verify.OrdinalDate.year_eq_if_days_eq_1460 (dt : Time.OrdinalDate) (hmod : d' dt = 1460) : quadcent dt * 400 + cent dt * 100 + quad dt * 4 + 4 = dt.year

theorem Verify.OrdinalDate.year_lt_mod_1460_eq (dt : Time.OrdinalDate) (hNot : ¬(dt.year % 400 = 0 ∧ (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val = 366)) : (Time.toModifiedJulianDay dt.year (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val - default.modifiedJulianDay) / 146097 * 400 + (Time.toModifiedJulianDay dt.year (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val - default.modifiedJulianDay) % 146097 / 36524 * 100 + ((Time.toModifiedJulianDay dt.year (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val - default.modifiedJulianDay) % 146097 - (Time.toModifiedJulianDay dt.year (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val - default.modifiedJulianDay) % 146097 / 36524 * 36524) / 1461 * 4 + ((Time.toModifiedJulianDay dt.year (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val - default.modifiedJulianDay) % 146097 - (Time.toModifiedJulianDay dt.year (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val - default.modifiedJulianDay) % 146097 / 36524 * 36524) % 1461 / 365 + 1 = quadcent dt * 400 + cent dt * 100 + quad dt * 4 + d' dt / 365 + 1

theorem Verify.OrdinalDate.d'_eq (dt : Time.OrdinalDate) (h : ¬(dt.year % 400 = 0 ∧ (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val = 366)) : (days_since_1_1_1 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d) % 146097 - days_since_1_1_1 dt (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d) % 146097 / 36524 * 36524) % 1461 = d' dt

theorem Verify.OrdinalDate.d'_lt_1460_eq (dt : Time.OrdinalDate) (hlt : d' dt < 1460) : ¬(dt.year % 4 = 0 ∧ (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val = 366)

theorem Verify.OrdinalDate.d'_lt_1460_lt (dt : Time.OrdinalDate) (hlt : d' dt < 1460) : (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val < 366

theorem Verify.OrdinalDate.d'_lt_1460_eq_year (dt : Time.OrdinalDate) (hlt : d' dt < 1460) : quadcent dt * 400 + cent dt * 100 + quad dt * 4 + d' dt / 365 + 1 = dt.year

theorem Verify.OrdinalDate.d'_lt_1460_eq_day_common {a : Time.Icc 1 365} (dt : Time.OrdinalDate) (h : dt.dayOfYear = Time.DayOfYear.common a) : (d' dt % 365 + 1).toNat = (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val

theorem Verify.OrdinalDate.d'_lt_1460_eq_day_leap {a : Time.Icc 1 366} (dt : Time.OrdinalDate) (h : dt.dayOfYear = Time.DayOfYear.leap a) (hlt : d' dt < 1460) : (d' dt % 365 + 1).toNat = (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d).val

theorem Verify.OrdinalDate.toOrdinalDate_fromOrdinalDate_eq_id (dt : Time.OrdinalDate) : Time.toOrdinalDate (Time.fromOrdinalDate dt) = dt

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

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

theorem Verify.OrdinalDate.next_date_eq_mjd_add_one (dt : Time.OrdinalDate) : next_date dt = Time.toOrdinalDate (Time.Day.addDays 1 (Time.fromOrdinalDate dt))

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