Theorems about Time.findValidMonthDay properties

Main theorems:

• Verify.MonthDay.findValidMonthDay_month_eq
• Verify.MonthDay.findValidMonthDay_month_eq_incr

theorem Verify.MonthDay.incr_of_yd_in (yd : Time.Icc 1 366) (isLeap : Bool) (hle : yd.val + 1 ≤ if isLeap = true then 366 else 365) : 1 ≤ yd.val + 1 ∧ yd.val + 1 ≤ 366

theorem Verify.MonthDay.incr_of_day_in_intervall (dt : Time.Date) (ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }) (h : dt.Day.val < ml.val.snd) : 1 ≤ dt.Day.val + 1 ∧ dt.Day.val + 1 ≤ 31

theorem Verify.MonthDay.yd_eq_monthLastDayAsDayOfYear'_val {dt : Time.Date} (isLeap : Bool) (yd : Time.Icc 1 366) {a : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isLeap ∧ x.fst = dt.Month.val }} {ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }} (hml : ml = Verify.MonthLength.monthLengths_of_date dt) (h : dt.Day.val = ml.val.snd) (hmem : ml.val ∈ Time.monthLengths (Time.isLeapYear dt.Year) ∧ ml.val.fst = dt.Month.val ∧ dt.Day.val ≤ ml.val.snd) (heq : a.val.snd.fst + dt.Day.val - 1 = yd.val) (hl : Time.isLeapYear dt.Year = isLeap) : a.val.snd.snd = yd.val

Day of year yd equals (Time.monthLastDayAsDayOfYear' isLeap).val.snd.snd if dt.Day.val = ml.val.snd (if dt.Day is last day of month).

def Lean.Parser.Category.ValidMonthDayMonthEq : Lean.Parser.Category

Equations

• Lean.Parser.Category.ValidMonthDayMonthEq = { }

def Verify.MonthDay.Notation.ValidMonthDayMonthEq.quot : Lean.ParserDescr

Equations

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

def Verify.MonthDay.Notation.ValidMonthDayMonthEq_______________ : Lean.ParserDescr

Equations

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

def Verify.MonthDay.Notation.«termValidMonthDayMonthEq%_» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.ValidMonthDayMonthEq' : Lean.Parser.Category

Equations

• Lean.Parser.Category.ValidMonthDayMonthEq' = { }

def Verify.MonthDay.Notation.ValidMonthDayMonthEq'.quot : Lean.ParserDescr

Equations

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

def Verify.MonthDay.Notation.ValidMonthDayMonthEq'_______________ : Lean.ParserDescr

Equations

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

def Verify.MonthDay.Notation.«termValidMonthDayMonthEq'%_» : Lean.ParserDescr

Equations

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

def Verify.MonthDay.Notation.ValidMonthDayMonthEqIncr'.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.ValidMonthDayMonthEqIncr' : Lean.Parser.Category

Equations

• Lean.Parser.Category.ValidMonthDayMonthEqIncr' = { }

def Verify.MonthDay.Notation.ValidMonthDayMonthEqIncr'_________ : Lean.ParserDescr

Equations

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

def Verify.MonthDay.Notation.«termValidMonthDayMonthEqIncr'%_» : Lean.ParserDescr

Equations

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

def Verify.MonthDay.Notation.ValidMonthDayMonthEqIncr.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.ValidMonthDayMonthEqIncr : Lean.Parser.Category

Equations

• Lean.Parser.Category.ValidMonthDayMonthEqIncr = { }

def Verify.MonthDay.Notation.ValidMonthDayMonthEqIncr___________ : Lean.ParserDescr

Equations

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

def Verify.MonthDay.Notation.«termValidMonthDayMonthEqIncr%_» : Lean.ParserDescr

Equations

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

theorem Verify.MonthDay.incr_of_day_is_valid (dt : Time.Date) (ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }) (h : dt.Day.val < ml.val.snd) : ∃ (m : Nat × Nat), m ∈ Time.monthLengths (Time.isLeapYear dt.Year) ∧ m.fst = dt.Month.val ∧ ⟨dt.Day.val + 1, ⋯⟩.val ≤ m.snd

theorem Verify.MonthDay.incr_of_month_is_valid (dt : Time.Date) (h : dt.Month.val < 12) : ∃ (a : Nat × Nat), a ∈ Time.monthLengths (Time.isLeapYear dt.Year) ∧ a.fst = ⟨dt.Month.val + 1, ⋯⟩.val ∧ ⟨1, ⋯⟩.val ≤ a.snd

theorem Verify.MonthDay.OrdinalDate_of_common_no_leapYear (dt : Time.OrdinalDate) (v : Time.Icc 1 365) (h : dt.dayOfYear = Time.DayOfYear.common v) : Time.isLeapYear dt.year = false

theorem Verify.MonthDay.not_leapYear_eq (year : Int) (h : Time.isLeapYear year = false) (h2 : year % 4 = 0) : ¬(year % 400 = 0 ∨ ¬year % 100 = 0)

theorem Verify.MonthDay.dateToOrdinalDate_year_eq (dt : Time.Date) : (Time.dateToOrdinalDate dt).year = dt.Year

def Verify.MonthDay.date_of_dy' {dt : Time.Date} : Time.OrdinalDate

Equations

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

def Verify.MonthDay.dateToOrdinalDate' (dt : Time.Date) : Time.OrdinalDate

Equations

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

theorem Verify.MonthDay.dateToOrdinalDate'_dateToOrdinalDate_eq {dt : Time.Date} : Verify.MonthDay.dateToOrdinalDate' dt = Time.dateToOrdinalDate dt

theorem Verify.MonthDay.next_date_of_day_lt_top (dt : Time.Date) {ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }} (h : dt.Day.val < ml.val.snd ∨ dt.Month.val < 12) : Verify.OrdinalDate.DayOfYear.lt_top (Verify.MonthDay.dateToOrdinalDate' dt).dayOfYear = true

theorem Verify.MonthDay.next_date_of_day_lt_eq_incr' {dt : Time.Date} {dt' : Time.OrdinalDate} {ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }} (h : dt.Day.val < ml.val.snd ∨ dt.Month.val < 12) (heq : dt' = Time.dateToOrdinalDate dt) : Verify.OrdinalDate.DayOfYear.incr (Verify.MonthDay.dateToOrdinalDate' dt) ⋯ = Verify.OrdinalDate.next_date dt'

theorem Verify.MonthDay.findValidMonthDay_year_eq (year : Int) (isLeap : Bool) (yd : Time.Icc 1 366) (hl : Time.isLeapYear year = isLeap) (hle : yd.val ≤ if isLeap = true then 366 else 365) : (Time.findValidMonthDay year isLeap yd hl hle).Year = year

theorem Verify.MonthDay.findValidMonthDay_1_month_eq {year : Int} {dt : Time.Date} (isLeap : Bool) (yd : Time.Icc 1 366) {ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }} (h : dt.Day.val < ml.val.snd) (heq : Time.dy' isLeap dt.Month dt.Day = yd.val) (hle : yd.val + 1 ≤ if isLeap = true then 366 else 365) (hyd : yd.val + 1 ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨0, ⋯⟩).snd) : (Time.findValidMonthDay_1 year isLeap ⟨yd.val + 1, ⋯⟩ hyd).Month = dt.Month ∧ ⟨dt.Day.val + 1, ⋯⟩ = (Time.findValidMonthDay_1 year isLeap ⟨yd.val + 1, ⋯⟩ hyd).Day

theorem Verify.MonthDay.findValidMonthDay_12_month_eq {dt : Time.Date} (isLeap : Bool) (yd : Time.Icc 1 366) {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' isLeap dt.Month dt.Day = yd.val) (hle : yd.val + 1 ≤ if isLeap = true then 366 else 365) (hl : Time.isLeapYear dt.Year = isLeap) (hne : ¬yd.val + 1 ≤ (Time.monthLastDayAsDayOfYear isLeap)[10].snd) : (Time.findValidMonthDay_12 dt.Year isLeap ⟨yd.val + 1, ⋯⟩ hl hne ⋯).Month = dt.Month ∧ ⟨dt.Day.val + 1, ⋯⟩ = (Time.findValidMonthDay_12 dt.Year isLeap ⟨yd.val + 1, ⋯⟩ hl hne ⋯).Day

theorem Verify.MonthDay.findValidMonthDay_month_eq {dt : Time.Date} (isLeap : Bool) (yd : Time.Icc 1 366) {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' isLeap dt.Month dt.Day = yd.val) (hl : Time.isLeapYear dt.Year = isLeap) (hle : yd.val + 1 ≤ if isLeap = true then 366 else 365) : (Time.findValidMonthDay dt.Year isLeap ⟨yd.val + 1, ⋯⟩ hl hle).Month = dt.Month ∧ ⟨dt.Day.val + 1, ⋯⟩ = (Time.findValidMonthDay dt.Year isLeap ⟨yd.val + 1, ⋯⟩ hl hle).Day

For a day of year yd, if dt.Day is not last day of month, then

• (Time.findValidMonthDay dt.Year (yd + 1)).Month = dt.Month
• (Time.findValidMonthDay dt.Year (yd + 1)).Day = dt.Day + 1

theorem Verify.MonthDay.monthLengths_month_1_eq_31_ne (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → ¬31 = a.snd → ¬a.fst = 1

theorem Verify.MonthDay.monthLengths_month_1_eq_31 (isleap : Bool) (a : { x : Nat × Nat // x ∈ Time.monthLengths isleap }) (h : a.val.fst = 1) : a.val.snd = 31

theorem Verify.MonthDay.findValidMonthDay_1_month_eq_incr {dt : Time.Date} (isLeap : Bool) (yd : Time.Icc 1 366) {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' isLeap dt.Month dt.Day = yd.val) (hl : Time.isLeapYear dt.Year = isLeap) (hyd : yd.val + 1 ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨0, ⋯⟩).snd) : (Time.findValidMonthDay_1 dt.Year isLeap ⟨yd.val + 1, ⋯⟩ hyd).Month = ⟨dt.Month.val + 1, ⋯⟩ ∧ (Time.findValidMonthDay_1 dt.Year isLeap ⟨yd.val + 1, ⋯⟩ hyd).Day = ⟨1, ⋯⟩

theorem Verify.MonthDay.findValidMonthDay_12_month_eq_incr' {dt : Time.Date} (isLeap : Bool) (yd : Time.Icc 1 366) {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' isLeap dt.Month dt.Day = yd.val) (hl : Time.isLeapYear dt.Year = isLeap) (h1 : (if isLeap = true then 335 else 334) ≤ yd.val) (h2 : yd.val ≤ if isLeap = true then 365 else 364) : dt.Month.val = 11 ∧ yd.val = if isLeap = true then 335 else 334

theorem Verify.MonthDay.findValidMonthDay_12_month_eq_incr {dt : Time.Date} (isLeap : Bool) (yd : Time.Icc 1 366) {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' isLeap dt.Month dt.Day = yd.val) (hl : Time.isLeapYear dt.Year = isLeap) (hn : ¬yd.val + 1 ≤ ((Time.monthLastDayAsDayOfYear isLeap).get ⟨10, ⋯⟩).snd) (hle : yd.val + 1 ≤ if isLeap = true then 366 else 365) : (Time.findValidMonthDay_12 dt.Year isLeap ⟨yd.val + 1, ⋯⟩ hl hn ⋯).Month = ⟨dt.Month.val + 1, ⋯⟩ ∧ (Time.findValidMonthDay_12 dt.Year isLeap ⟨yd.val + 1, ⋯⟩ hl hn ⋯).Day = ⟨1, ⋯⟩

theorem Verify.MonthDay.yd_add_one_lt {dt : Time.Date} (isLeap : Bool) (yd : Time.Icc 1 366) (hm : dt.Month.val < 12) (heq : Time.dy' isLeap dt.Month dt.Day = yd.val) (hl : Time.isLeapYear dt.Year = isLeap) (hle : yd.val + 1 ≤ if isLeap = true then 366 else 365) : 1 ≤ yd.val + 1 ∧ yd.val + 1 ≤ 366

theorem Verify.MonthDay.findValidMonthDay_month_eq_incr {dt : Time.Date} (isLeap : Bool) (yd : Time.Icc 1 366) {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' isLeap dt.Month dt.Day = yd.val) (hl : Time.isLeapYear dt.Year = isLeap) (hle : yd.val + 1 ≤ if isLeap = true then 366 else 365) : (Time.findValidMonthDay dt.Year isLeap ⟨yd.val + 1, ⋯⟩ hl hle).Month = ⟨dt.Month.val + 1, ⋯⟩ ∧ (Time.findValidMonthDay dt.Year isLeap ⟨yd.val + 1, ⋯⟩ hl hle).Day = ⟨1, ⋯⟩

For a day of year yd, if dt.Day is equal to last day of month, then

• (Time.findValidMonthDay dt.Year (yd + 1)).Month = dt.Month + 1
• (Time.findValidMonthDay dt.Year (yd + 1)).Day = 1