Documentation

Time.Verify.Calendar.MonthLength

Theorems about `Time.monthLengths` properties #

def Verify.MonthLength.monthLengthsOfDate (m : Nat × Nat) (dt : Time.Date) :

Relation of Date to Time.monthLengths list.

Equations

Verify.MonthLength.monthLengthsOfDate m dt = (m ∈ Time.monthLengths (Time.isLeapYear dt.Year) ∧ m.fst = dt.Month.val ∧ dt.Day.val ≤ m.snd)

Instances For

def Verify.MonthLength.monthLengths_of_date (dt : Time.Date) :

{ m : Nat × Nat // monthLengthsOfDate m dt }

Build relation of Date to Time.monthLengths.

Equations

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

Instances For

theorem Verify.MonthLength.monthLengths_days_le (isleap : Bool) (a : Nat × Nat) :

a ∈ Time.monthLengths isleap → (if isleap = true then 29 else 28) ≤ a.snd

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_days_sub_lt (isleap : Bool) (a : Nat × Nat × Nat) :

a ∈ Time.monthLastDayAsDayOfYear' isleap → a.snd.fst < a.snd.snd

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_sub_le_31 (isleap : Bool) (a : Nat × Nat × Nat) :

a ∈ Time.monthLastDayAsDayOfYear' isleap → a.snd.snd - a.snd.fst ≤ 31

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_sub_of_monthLengths (isleap : Bool) (a : Nat × Nat × Nat) (b : Nat × Nat) :

a ∈ Time.monthLastDayAsDayOfYear' isleap → b ∈ Time.monthLengths isleap → a.fst = b.fst → a.snd.snd - a.snd.fst + 1 = b.snd

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_snd_fst_lt (isleap : Bool) (a : Nat × Nat × Nat) :

a ∈ Time.monthLastDayAsDayOfYear' isleap → 0 < a.snd.fst

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_month_lt_12_lt (isleap : Bool) (dt : Time.Date) (a : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isleap ∧ x.fst = dt.Month.val }) (h : a.val.fst < 12) :

a.val.snd.fst < if isleap = true then 336 else 335

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_month_1_eq (dt : Time.Date) (isleap : Bool) (a : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isleap ∧ x.fst = dt.Month.val }) (h : a.val.snd.fst ≤ 31) :

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_day_of_month_1_eq (dt : Time.Date) (isleap : Bool) (a : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isleap ∧ x.fst = dt.Month.val }) (h : a.val.fst = 1) :

1 = a.val.snd.fst

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_index_eq_if_fst_eq {isleap : Bool} (i : Fin (Time.monthLastDayAsDayOfYear' isleap).length) (i' : Fin (Time.monthLengths isleap).length) (h : (Time.monthLastDayAsDayOfYear' isleap)[↑i].fst = (Time.monthLengths isleap)[↑i'].fst) :

↑i = ↑i'

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_sub_eq_incr {isleap : Bool} (i : Fin (Time.monthLastDayAsDayOfYear' isleap).length) (dt : Time.Date) (hl : Time.isLeapYear dt.Year = isleap) {ml : { m : Nat × Nat // monthLengthsOfDate m dt }} (hml : ml = monthLengths_of_date dt) (h : dt.Day.val = ml.val.snd) (hmonth : ((Time.monthLastDayAsDayOfYear' isleap).get i).fst = dt.Month.val) :

dt.Day.val = (Time.monthLastDayAsDayOfYear' isleap)[↑i].snd.snd - (Time.monthLastDayAsDayOfYear' isleap)[↑i].snd.fst + 1

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_sub_le {isleap : Bool} (i : Fin (Time.monthLastDayAsDayOfYear' isleap).length) (dt : Time.Date) (hl : Time.isLeapYear dt.Year = isleap) {ml : { m : Nat × Nat // monthLengthsOfDate m dt }} (hml : ml = monthLengths_of_date dt) (h : dt.Day.val < ml.val.snd) (hmonth : ((Time.monthLastDayAsDayOfYear' isleap).get i).fst = dt.Month.val) :

dt.Day.val ≤ (Time.monthLastDayAsDayOfYear' isleap)[i].snd.snd - (Time.monthLastDayAsDayOfYear' isleap)[i].snd.fst

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_index_eq {isleap : Bool} (i i' : Fin (Time.monthLastDayAsDayOfYear' isleap).length) (dt : Time.Date) (hl : Time.isLeapYear dt.Year = isleap) {ml : { m : Nat × Nat // monthLengthsOfDate m dt }} (hml : ml = monthLengths_of_date dt) (h : dt.Day.val < ml.val.snd) (hmonth : ((Time.monthLastDayAsDayOfYear' isleap).get i').fst = dt.Month.val) (h1 : (Time.monthLastDayAsDayOfYear' isleap)[i].snd.fst ≤ (Time.monthLastDayAsDayOfYear' isleap)[i'].snd.fst + dt.Day.val) (h2 : (Time.monthLastDayAsDayOfYear' isleap)[i'].snd.fst + dt.Day.val ≤ (Time.monthLastDayAsDayOfYear' isleap)[i].snd.snd) :

i = i'

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_index_eq_of_last_day_in_month {isleap : Bool} (i i' : Fin (Time.monthLastDayAsDayOfYear' isleap).length) (dt : Time.Date) (hl : Time.isLeapYear dt.Year = isleap) {ml : { m : Nat × Nat // monthLengthsOfDate m dt }} (hml : ml = monthLengths_of_date dt) (h : dt.Day.val = ml.val.snd) (hmonth : ((Time.monthLastDayAsDayOfYear' isleap).get i').fst = dt.Month.val) (h1 : (Time.monthLastDayAsDayOfYear' isleap)[↑i].snd.fst ≤ (Time.monthLastDayAsDayOfYear' isleap)[↑i'].snd.fst + dt.Day.val) (h2 : (Time.monthLastDayAsDayOfYear' isleap)[↑i'].snd.fst + dt.Day.val ≤ (Time.monthLastDayAsDayOfYear' isleap)[↑i].snd.snd) :

↑i - 1 = ↑i'