chore: update to v4.16.0

README.md

@@ -1,5 +1,5 @@
 # PlainDate.ofDaysSinceUNIXEpoch is a valid date
 
-[Proof](https://github.com/bergmannjg/Std.Time.Lemmas/blob/main/Time/Date/Lemmas.lean#L834) that
+[Proof](https://github.com/bergmannjg/Std.Time.Lemmas/blob/main/Time/Date/Lemmas.lean#L820) that
 [PlainDate.ofDaysSinceUNIXEpoch](https://github.com/leanprover/lean4/blob/v4.15.0-rc1/src/Std/Time/Date/PlainDate.lean#L79) gives a valid
 [PlainDate](https://github.com/leanprover/lean4/blob/v4.15.0-rc1/src/Std/Time/Date/PlainDate.lean#L24).

Time/Data/Int/Lemmas.lean

@@ -51,9 +51,7 @@ protected theorem tdiv_sub_add_eq_div_sub_add {a b c d e : Nat}
       exact Int.ofNat_inj.mp heq
     simp_all
   · contradiction
-  · rename_i heq _
-    rw [heq] at hle
-    contradiction
+  · omega
   · contradiction
 
 protected theorem tdiv_sub_eq_div_sub {a b c d : Nat}
@@ -79,21 +77,10 @@ protected theorem le_div_tdiv_of_nat {a b c : Nat} (h : a ≤ b / c)
   omega
 
 protected theorem neg_ofNat_eq_negSucc {n : Nat} (hlt : 0 < n) : -(n : Int) = -[n - 1+1] := by
-  generalize h : n - 1 = n'
-  have : n'.succ = n := by simp [h]; omega
-  rw [← this]
-  rfl
+  omega
 
-protected theorem sub_eq_add_of_int (n w m' : Nat) (hlt : 0 < w)
-  (heq : -[n +1]  - ↑w = -[m' +1])
+protected theorem sub_eq_add_of_int (n w m' : Nat) (heq : -[n +1]  - ↑w = -[m' +1])
     : n + w = m' := by
-  have h : Int.negSucc n - ↑w = Int.add (Int.negSucc n) (Int.negSucc (w - 1)) := by
-    have := Int.neg_ofNat_eq_negSucc hlt
-    have : Int.negSucc n - ↑w = Int.negSucc n + Int.negSucc (w - 1) := by omega
-    exact this
-  have : Int.negSucc n - ↑w = Int.negSucc (Nat.succ (n + (w - 1))) := h
-  rw [this] at heq
-  have := Int.negSucc_inj.mp heq
   omega
 
 protected theorem sub_tdiv_mul_le (a b : Int) (ha : a < 0) (hb : 1 < b)
@@ -103,16 +90,13 @@ protected theorem sub_tdiv_mul_le (a b : Int) (ha : a < 0) (hb : 1 < b)
     rename_i w h
     simp [tdiv, instHDiv, Nat.instDiv]
     split <;> simp_all
-    · rename_i heq _
-      have : Int.negSucc n - w < 0 := by omega
-      rw [heq] at this
-      contradiction
+    · omega
     · contradiction
     · rename_i m' n' heq' heq
       have : Int.neg (Int.negSucc n) ≤ (↑((m' + 1).div n') * (↑w + 1)) := by
         have : Int.neg (Int.negSucc n) = Nat.succ n := rfl
         rw [this, ← h]
-        have h1 : n + w = m' := Int.sub_eq_add_of_int n w m' (by omega) heq'
+        have h1 : n + w = m' := Int.sub_eq_add_of_int n w m' heq'
         have h2 : n' = w + 1 := by omega
         rw [← h1, h2]
         have := Nat.succ_le_div_mul n w
@@ -127,16 +111,11 @@ protected theorem le_sub_tdiv_mul (a b : Int) (ha : a < 0) (hb : 1 < b)
     rename_i w h
     simp [tdiv, instHDiv, Nat.instDiv]
     split <;> simp_all
-    · rename_i m' n' heq _
-      have : Int.negSucc n - w < 0 := by omega
-      rw [heq] at this
-      contradiction
+    · omega
     · contradiction
     · rename_i m' n' heq' heq
       have : ↑((m' + 1).div n') * (↑w + 1) ≤ Int.neg (Int.negSucc m') := by
-        have : Int.neg (Int.negSucc m') = Nat.succ m' := by
-          unfold Int.neg
-          split <;> simp_all
+        have : Int.neg (Int.negSucc m') = Nat.succ m' := rfl
         rw [this, ← h]
         have : (m' + 1).div n' * n' ≤ m'.succ := by
           rw [Nat.div_mul_eq_sub_mod (m' + 1) n']
@@ -159,11 +138,9 @@ protected theorem mod_zero_of_add_mul_eq_iff (a b c : Int)
     have h1 := Int.dvd_iff_tmod_eq_zero.mpr h
     have h2 := Int.dvd_mul_right c b
     have h3 := Int.dvd_add h1 h2
-    have := Int.dvd_iff_tmod_eq_zero.mp h3
-    exact this)
+    exact Int.dvd_iff_tmod_eq_zero.mp h3)
   (fun h => by
     have h1 := Int.dvd_iff_tmod_eq_zero.mpr h
     have h2 := Int.dvd_mul_right c b
     have h3 := (@Int.dvd_add_left c a (c * b) h2).mp h1
-    have := (@Int.dvd_iff_tmod_eq_zero c a).mp h3
-    exact this)
+    exact (@Int.dvd_iff_tmod_eq_zero c a).mp h3)

Time/Data/Nat/Lemmas.lean

@@ -35,7 +35,7 @@ protected theorem succ_le_div_mul (n w : Nat)
 
   rw [Nat.div_mul_eq_sub_mod n (w + 1)]
   have : n % (w + 1) ≤ w := by
-    have : n % (w + 1) < w + 1 := Nat.mod_lt n (by simp)
+    have : n % (w + 1) < w + 1 := Nat.mod_lt n (zero_lt_succ w)
     exact le_of_lt_succ this
   omega
 
@@ -44,6 +44,5 @@ protected theorem div_mul_lt {a b n : Nat} (hlt : 0 < b) (h : a / b = n)
   simp [(@Nat.le_div_iff_mul_le b n a hlt).mp (Nat.le_of_eq (id (Eq.symm h)))]
   simp [(@Nat.div_lt_iff_lt_mul b a (n+1) hlt).mp (by omega)]
 
-protected theorem div_eq_zero_lt {a b : Nat} (hlt : 0 < b) (hzero : a / b = 0) : a < b := by
-  have := @Nat.div_mul_lt a b 0 hlt
-  simp_all
+protected theorem div_eq_zero_lt {a b : Nat} (hlt : 0 < b) (hzero : a / b = 0) : a < b :=
+  lt_of_div_eq_zero hlt hzero

Time/Date/Lemmas.lean

@@ -21,10 +21,10 @@ open Std.Time Int
 
 /-- monthSizes of year starting at month 1, see `Time.Month.Ordinal`. -/
 def ordinalMonthSizes (leap : Bool) : { val : Array Day.Ordinal // val.size = 12 } :=
-  ⟨#[31, if leap then 29 else 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31], by cases leap <;> decide⟩
+  ⟨#[31, if leap then 29 else 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31], rfl⟩
 
 def toIndex (month : Time.Month.Ordinal) : Fin ((ordinalMonthSizes leap).val.size) :=
-  (month.sub 1).toFin (by decide)
+  (month.sub 1).toFin (Int.le_refl 0)
 
 theorem ordinalMonthSizes_eq_days (leap : Bool)
     : ∀ month : Time.Month.Ordinal,
@@ -271,7 +271,6 @@ theorem yoe_le_of_doe_lt_146096 {doe yoe : Int} (hdoe : 36524 ≤ doe ∧ doe 
         rw [← Int.ofNat_inj.mp hn'] at heq
         have : 0 ≤ Int.ofNat m' - Int.ofNat (m' / 1460) + Int.ofNat (m' / 36524) := hzero
         rwa [heq] at this
-      have := Int.negSucc_lt_zero m''
       omega
     · contradiction
     · contradiction
@@ -480,7 +479,7 @@ theorem doy_le {doe yoe doy : Int} (hdoe : 0 ≤ doe ∧ doe ≤ 146096)
         have hyd := @yoe_of_doe_lt_146096 doe yoe (by omega) heq
         have hm : yoe = (doe - doe / 1460 + doe / 36524) / 365  :=
                    Int.tdiv_sub_add_eq_div_sub_add hyd.left (by simp [Int.tdiv]; omega)
-        have : yoe / 100 = doe / 36524 := by rw [hm, Nat.div_div_eq_div_mul]; omega
+        have : yoe / 100 = doe / 36524 := by omega
         simp only [ofNat_eq_coe, Nat.cast_ofNat_Int] at hdoy
         split
         · omega
@@ -500,8 +499,7 @@ theorem doy_le {doe yoe doy : Int} (hdoe : 0 ≤ doe ∧ doe ≤ 146096)
         have : doe ≤ 146096 := Int.ofNat_le.mp hdoe.right
         omega
   · contradiction
-  · have := hyoe.left
-    contradiction
+  · omega
   · contradiction
 
 theorem mp_of_nat_le {doy mp m : Nat} (hdoy : 0 ≤ ofNat doy ∧ ofNat doy ≤ 365)
@@ -524,7 +522,7 @@ theorem mp_le {doy mp : Int} (hdoy : 0 ≤ doy ∧ doy ≤ 365) (hmp : mp = mont
     match doy, mp with
     | ofNat doy, ofNat mp => exact mp_of_nat_le hdoy (Int.ofNat_inj.mp hmp) (Int.ofNat_inj.mp heq)
   · contradiction
-  · match doy with | ofNat _ => contradiction
+  · omega
   · contradiction
 
 theorem d_le' {d : Int} {doy mp m' m'' n' n'' : Nat}
@@ -569,14 +567,14 @@ theorem d_le {doy mp d : Int} (hdoy : 0 ≤ doy ∧ doy ≤ 365) (hle : 0 ≤ mp
                       (And.intro (Int.ofNat_le.mp hle.left) (Int.ofNat_le.mp hle.right))
                       hd (Int.ofNat_inj.mp hn')
     · contradiction
-    · match doy with | ofNat _ => contradiction
+    · omega
     · contradiction
   · contradiction
   · rename_i heq _
     split at heq
     · contradiction
     · contradiction
-    · match doy with | ofNat _ => contradiction
+    · omega
     · contradiction
   · contradiction
 
@@ -594,7 +592,7 @@ theorem mp_to_month_of_mp_to_month_eq_id (mp : Int ) (hmp : 0 ≤ mp ∧ mp ≤
   omega
 
 protected theorem Array.get_eq_get_of_eq (a : Array α) (n m : Nat) (hn) (hm) (h : n = m)
-    : a[n]'hn = a[m]'hm := getElem_congr h
+    : a[n]'hn = a[m]'hm := getElem_congr rfl h hn
 
 theorem days_eq_days_of_mp_2 (leapOfYear leapOfYearOfEra  : Bool) (mp : Int)
   (hm : 2 = month_from_shifted_month mp) (hmp : 0 ≤ mp ∧ mp ≤ 11)
@@ -606,7 +604,8 @@ theorem days_eq_days_of_mp_2 (leapOfYear leapOfYearOfEra  : Bool) (mp : Int)
   simp [month_from_shifted_month] at hm
   simp
   have h : mp.toNat = 11 := by omega
-  have h1 : 11 < (monthSizes leapOfYearOfEra).val.size := List.isSome_getElem?.mp rfl
+  have h1 : 11 < (monthSizes leapOfYearOfEra).val.size :=
+    (isSome_getElem? (monthSizes leapOfYearOfEra).val 11).mp rfl
   have h2 : mp.toNat < (monthSizes leapOfYearOfEra).val.size := lt_of_eq_of_lt h h1
   rw [Array.get_eq_get_of_eq (monthSizes leapOfYearOfEra).val mp.toNat 11 h2 h1 h]
   have h1 : (monthSizes leapOfYearOfEra).val[11]'h1 = if leapOfYearOfEra then 29 else 28 := rfl
@@ -655,13 +654,7 @@ theorem days_eq_days_of_monthSizes (leapOfYear leapOfYearOfEra : Bool) (month :
         have : mp ≤ 11 := ofNat_le.mp hmp'.right
         have h : mp < 11 := by
           simp [month_from_shifted_month] at hm
-          split at hm
-          · omega
-          · if m = 1
-            then omega
-            else
-              have : ¬ mp ≤ 11 := by omega
-              contradiction
+          omega
         have h := monthSizes_eq_ordinalMonthSizes leapOfYear leapOfYearOfEra ⟨mp, by
           have := (monthSizes leapOfYearOfEra).property
           omega⟩ h
@@ -671,8 +664,7 @@ theorem days_eq_days_of_monthSizes (leapOfYear leapOfYearOfEra : Bool) (month :
         simp
         exact id (Eq.symm h)
       | negSucc _ =>
-        have := hmp'.left
-        contradiction
+        omega
 
 theorem doy_from_month_le (n m day : Nat) (heq : 5 * day + 2 = m) (h : n = m / 153)
     : doy_from_month n ≤ day := by
@@ -721,9 +713,7 @@ theorem month_from_doy_le (n : Nat) (doy : Int) (h : n = month_from_doy doy)
           (doy_from_next_month_le n m' day heq (by omega))
     | negSucc _ => contradiction
   · contradiction
-  · rename_i heq _
-    have : 5 * doy + 2 < 0 := by rw [heq]; exact Int.negSucc_lt_zero _
-    contradiction
+  · omega
   · contradiction
 
 theorem doy_sub_le (mp doy : Int) (leap : Bool) (hmp : mp = month_from_doy doy)
@@ -772,20 +762,18 @@ theorem mod_100_zero_of_add_iff (era : Int) (yoe : Nat)
       exact (Int.mod_zero_of_add_mul_eq_iff (yoe + 1) (era*4) 100).mp h)
     (fun h => by
       have := (Int.mod_zero_of_add_mul_eq_iff (yoe + 1) (era*4) 100).mpr h
-      have h : (yoe + 1) % 100 = 0 := ofNat_eq_zero.mp this
-      exact h)
+      exact ofNat_eq_zero.mp this)
 
 theorem mod_400_zero_of_add_iff (era : Int) (yoe : Nat)
     : (yoe + 1) % 400 = 0 ↔ (yoe + 1 + era * 400).tmod 400 = 0  := by
   rw [Int.mul_comm]
   exact Iff.intro
     (fun h => by
-      have h : ((yoe:Int) + 1).tmod 400 = 0 := by have := ofNat_tmod (yoe+1) 400; simp_all
+      have h : ((yoe:Int) + 1).tmod 400 = 0 := natAbs_eq_zero.mp h
       exact (Int.mod_zero_of_add_mul_eq_iff (yoe + 1) era 400).mp h)
     (fun h => by
       have := (Int.mod_zero_of_add_mul_eq_iff (yoe + 1) era 400).mpr h
-      have h : (yoe + 1) % 400 = 0 := by have := ofNat_tmod (yoe+1) 400; simp_all; omega
-      exact h)
+      exact ofNat_eq_zero.mp this)
 
 /-- Is leap year of year defined by  `era` and `yoe` starting at 0
 -/
@@ -849,8 +837,7 @@ theorem isValid (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal)
     rw [Subtype.ext_iff]
     exact hd
   rw [this]
-  have := doy_sub_le mp doy (isLeapOfYearOfEra yoe.toNat) hmp hmp' (by split at hdoy <;> simp_all)
-  norm_cast
+  exact doy_sub_le mp doy (isLeapOfYearOfEra yoe.toNat) hmp hmp' (by split at hdoy <;> simp_all)
 
 end Verification
 

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e7501e44286e5ae9f2bbf7ed44059f693793ca95",
+   "rev": "fad7e1b793d64ded0af2bfda42f5046a0c12d39d",
    "name": "tryAtEachStep",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "lean-v4.15.0",
+   "inputRev": "lean-v4.16.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "01006c9e86bf9e397c026fef4190478dd1fd897e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "time",

lakefile.lean

@@ -1,9 +1,9 @@
 import Lake
 open System Lake DSL
 
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.15.0"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.16.0"
 
-require tryAtEachStep from git "https://github.com/dwrensha/tryAtEachStep" @ "lean-v4.15.0"
+require tryAtEachStep from git "https://github.com/dwrensha/tryAtEachStep" @ "lean-v4.16.0"
 
 package time {
   lintDriver := "batteries/runLinter"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0