chore: deprecate Fin.ofNat (replaced by Fin.ofNat', subsequently to b…

…e 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

@@ -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

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

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:

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

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

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

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

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