From 6d495586a1836da3e12efb4fbf9946bd9088ac5f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 28 Nov 2024 16:23:23 +1100 Subject: [PATCH] chore: deprecate Fin.ofNat (replaced by Fin.ofNat', subsequently to be renamed) (#6242) This PR deprecates `Fin.ofNat` in favour of `Fin.ofNat'` (which takes an `[NeZero]` instance, rather than returning an element of `Fin (n+1)`). After leaving the deprecation warning in place for some time, we will then rename `ofNat'` back to `ofNat`. --- src/Init/Data/Fin/Basic.lean | 15 ++++++--------- src/Init/Data/NeZero.lean | 4 ++++ src/Lean/Meta/LitValues.lean | 2 +- src/Std/Time/DateTime/PlainDateTime.lean | 2 +- src/Std/Time/Time/Unit/Nanosecond.lean | 2 +- tests/lean/run/788.lean | 3 +-- tests/lean/run/bigop.lean | 2 +- tests/lean/run/timeAPI.lean | 4 ++-- 8 files changed, 17 insertions(+), 17 deletions(-) diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean index c2ee615b9c..33df16cc40 100644 --- a/src/Init/Data/Fin/Basic.lean +++ b/src/Init/Data/Fin/Basic.lean @@ -36,12 +36,6 @@ def succ : Fin n → Fin (n + 1) variable {n : Nat} -/-- -Returns `a` modulo `n + 1` as a `Fin n.succ`. --/ -protected def ofNat {n : Nat} (a : Nat) : Fin (n + 1) := - ⟨a % (n+1), Nat.mod_lt _ (Nat.zero_lt_succ _)⟩ - /-- Returns `a` modulo `n` as a `Fin n`. @@ -50,9 +44,12 @@ The assumption `NeZero n` ensures that `Fin n` is nonempty. protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n := ⟨a % n, Nat.mod_lt _ (pos_of_neZero n)⟩ --- We intend to deprecate `Fin.ofNat` in favor of `Fin.ofNat'` (and later rename). --- This is waiting on https://github.com/leanprover/lean4/pull/5323 --- attribute [deprecated Fin.ofNat' (since := "2024-09-16")] Fin.ofNat +/-- +Returns `a` modulo `n + 1` as a `Fin n.succ`. +-/ +@[deprecated Fin.ofNat' (since := "2024-11-27")] +protected def ofNat {n : Nat} (a : Nat) : Fin (n + 1) := + ⟨a % (n+1), Nat.mod_lt _ (Nat.zero_lt_succ _)⟩ private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n | 0, h => Nat.mod_lt _ h diff --git a/src/Init/Data/NeZero.lean b/src/Init/Data/NeZero.lean index 1961d0c4d0..6fba725742 100644 --- a/src/Init/Data/NeZero.lean +++ b/src/Init/Data/NeZero.lean @@ -36,3 +36,7 @@ theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 := @[simp] theorem neZero_zero_iff_false {α : Type _} [Zero α] : NeZero (0 : α) ↔ False := ⟨fun _ ↦ NeZero.ne (0 : α) rfl, fun h ↦ h.elim⟩ + +instance {p : Prop} [Decidable p] {n m : Nat} [NeZero n] [NeZero m] : + NeZero (if p then n else m) := by + split <;> infer_instance diff --git a/src/Lean/Meta/LitValues.lean b/src/Lean/Meta/LitValues.lean index 0bc7acd03a..fad889122d 100644 --- a/src/Lean/Meta/LitValues.lean +++ b/src/Lean/Meta/LitValues.lean @@ -68,7 +68,7 @@ def getFinValue? (e : Expr) : MetaM (Option ((n : Nat) × Fin n)) := OptionT.run let n ← getNatValue? (← whnfD type.appArg!) match n with | 0 => failure - | m+1 => return ⟨m+1, Fin.ofNat v⟩ + | m+1 => return ⟨m+1, Fin.ofNat' _ v⟩ /-- Return `some ⟨n, v⟩` if `e` is: diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index ab9ce145fd..7949c9930b 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -106,7 +106,7 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do break remDays := remDays - monLen - let mday : Fin 31 := Fin.ofNat (Int.toNat remDays) + let mday : Fin 31 := Fin.ofNat' _ (Int.toNat remDays) let hmon ← if h₁ : mon.val > 10 diff --git a/src/Std/Time/Time/Unit/Nanosecond.lean b/src/Std/Time/Time/Unit/Nanosecond.lean index 1f092cd4bd..ad32e89895 100644 --- a/src/Std/Time/Time/Unit/Nanosecond.lean +++ b/src/Std/Time/Time/Unit/Nanosecond.lean @@ -22,7 +22,7 @@ def Ordinal := Bounded.LE 0 999999999 deriving Repr, BEq, LE, LT instance : OfNat Ordinal n where - ofNat := Bounded.LE.ofFin (Fin.ofNat n) + ofNat := Bounded.LE.ofFin (Fin.ofNat' _ n) instance : Inhabited Ordinal where default := 0 diff --git a/tests/lean/run/788.lean b/tests/lean/run/788.lean index c8c0e749ec..a727691836 100644 --- a/tests/lean/run/788.lean +++ b/tests/lean/run/788.lean @@ -1,6 +1,5 @@ example : (0 : Nat) = Nat.zero := by simp only [OfNat.ofNat] -example : (0 : Fin 9) = (Fin.ofNat 0) := by +example : (0 : Fin 9) = (Fin.ofNat' _ 0) := by simp only [OfNat.ofNat] - rfl diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean index a317ff915f..60f11a64e4 100644 --- a/tests/lean/run/bigop.lean +++ b/tests/lean/run/bigop.lean @@ -39,7 +39,7 @@ instance : Enumerable (Fin n) where elems := (finElems n).reverse instance : OfNat (Fin (Nat.succ n)) m := - ⟨Fin.ofNat m⟩ + ⟨Fin.ofNat' _ m⟩ -- Declare a new syntax category for "indexing" big operators declare_syntax_cat index diff --git a/tests/lean/run/timeAPI.lean b/tests/lean/run/timeAPI.lean index 881a38bad5..1509c573cf 100644 --- a/tests/lean/run/timeAPI.lean +++ b/tests/lean/run/timeAPI.lean @@ -501,8 +501,8 @@ example := Week.Ordinal.ofInt 1 (by decide) example := Nanosecond.Ordinal.ofFin 1 example := Millisecond.Ordinal.ofFin 1 -example := Second.Ordinal.ofFin (leap := false) (Fin.ofNat 1) -example := Second.Ordinal.ofFin (leap := true) (Fin.ofNat 1) +example := Second.Ordinal.ofFin (leap := false) 37 +example := Second.Ordinal.ofFin (leap := true) 37 example := Minute.Ordinal.ofFin 1 example := Hour.Ordinal.ofFin 1 example := Day.Ordinal.ofFin 1