Theorems about Time.dy properties

Main theorems:

• Verify.DayOfYear.dy_eq_dy'
• Verify.DayOfYear.Notation.«termDy'MonthEq%_»
• Verify.DayOfYear.Notation.«termDy'MonthDayEq%_»

def Verify.DayOfYear.Notation.dy'MonthEq.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.dy'MonthEq : Lean.Parser.Category

Equations

• Lean.Parser.Category.dy'MonthEq = { }

def Verify.DayOfYear.Notation.dy'MonthEq_____________ : Lean.ParserDescr

Equations

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

def Verify.DayOfYear.Notation.«termDy'MonthEq%_» : Lean.ParserDescr

Equations

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

def Verify.DayOfYear.Notation.dy'MonthDayEq.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.dy'MonthDayEq : Lean.Parser.Category

Equations

• Lean.Parser.Category.dy'MonthDayEq = { }

def Verify.DayOfYear.Notation.dy'MonthDayEq_________________ : Lean.ParserDescr

Equations

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

def Verify.DayOfYear.Notation.«termDy'MonthDayEq%_» : Lean.ParserDescr

Equations

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

def Verify.DayOfYear.Notation.dy'MonthEq'.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.dy'MonthEq' : Lean.Parser.Category

Equations

• Lean.Parser.Category.dy'MonthEq' = { }

def Verify.DayOfYear.Notation.dy'MonthEq'___________________ : Lean.ParserDescr

Equations

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

def Verify.DayOfYear.Notation.«termDy'MonthEq'%_» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.dy'MonthDayEq' : Lean.Parser.Category

Equations

• Lean.Parser.Category.dy'MonthDayEq' = { }

def Verify.DayOfYear.Notation.dy'MonthDayEq'.quot : Lean.ParserDescr

Equations

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

def Verify.DayOfYear.Notation.dy'MonthDayEq'_________________________ : Lean.ParserDescr

Equations

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

def Verify.DayOfYear.Notation.«termDy'MonthDayEq'%_» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.monthIfLt : Lean.Parser.Category

Equations

• Lean.Parser.Category.monthIfLt = { }

def Verify.DayOfYear.Notation.monthIfLt.quot : Lean.ParserDescr

Equations

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

def Verify.DayOfYear.Notation.monthIfLt_ : Lean.ParserDescr

Equations

• Verify.DayOfYear.Notation.monthIfLt_ = Lean.ParserDescr.node `Verify.DayOfYear.Notation.monthIfLt_ 1022 (Lean.ParserDescr.const `num)

def Verify.DayOfYear.Notation.«termMonthIfLt%_» : Lean.ParserDescr

Equations

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

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 // Verify.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 // Verify.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 // Verify.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 // Verify.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 // Verify.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 // Verify.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.month_11_if_lt {dt : Time.Date} (isLeap : Bool) {ml : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }} (hml : ml = Verify.MonthLength.monthLengths_of_date dt) (h : dt.Day.val < ml.val.snd) (hl : Time.isLeapYear dt.Year = isLeap) : dt.Month.val = 11 → dt.Day.val < 30

theorem Verify.DayOfYear.dy'_month_12_eq (dt : Time.Date) (isleap : Bool) (h : dt.Day.val < 31) (h' : dt.Month.val = 11 → dt.Day.val < 30) (h1 : (if isleap = true then 335 else 334) < Time.dy' isleap dt.Month dt.Day + 1) : 12 = dt.Month.val

theorem Verify.DayOfYear.dy'_month_12_day_eq (dt : Time.Date) (isleap : Bool) (h : dt.Day.val < 31) (h' : dt.Month.val = 11 → dt.Day.val < 30) (h1 : (if isleap = true then 335 else 334) < Time.dy' isleap dt.Month dt.Day + 1) : dt.Day.val + 1 = Time.dy' isleap dt.Month dt.Day - if isleap = true then 334 else 333