chore: upstream Zero and NeZero

src/Init/Data.lean

@@ -39,3 +39,5 @@ import Init.Data.BEq
 import Init.Data.Subtype
 import Init.Data.ULift
 import Init.Data.PLift
+import Init.Data.Zero
+import Init.Data.NeZero

src/Init/Data/Fin/Basic.lean

@@ -141,8 +141,8 @@ instance : ShiftLeft (Fin n) where
 instance : ShiftRight (Fin n) where
   shiftRight := Fin.shiftRight
 
-instance instOfNat : OfNat (Fin (no_index (n+1))) i where
-  ofNat := Fin.ofNat i
+instance instOfNat {n : Nat} [NeZero n] {i : Nat} : OfNat (Fin (no_index n)) i where
+  ofNat := Fin.ofNat' i (pos_of_neZero _)
 
 instance : Inhabited (Fin (no_index (n+1))) where
   default := 0

src/Init/Data/Nat/Basic.lean

@@ -5,6 +5,8 @@ Authors: Floris van Doorn, Leonardo de Moura
 -/
 prelude
 import Init.SimpLemmas
+import Init.Data.NeZero
+
 set_option linter.missingDocs true -- keep it documented
 universe u
 
@@ -356,6 +358,8 @@ theorem eq_zero_or_pos : ∀ (n : Nat), n = 0 ∨ n > 0
 
 protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_pos n).resolve_left
 
+theorem pos_of_neZero (n : Nat) [NeZero n] : 0 < n := Nat.pos_of_ne_zero (NeZero.ne _)
+
 theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 
 theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
@@ -714,6 +718,8 @@ protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
 
 theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
 
+instance {n : Nat} : NeZero (succ n) := ⟨succ_ne_zero n⟩
+
 /-! # mul + order -/
 
 theorem mul_le_mul_left {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m :=
@@ -784,6 +790,9 @@ theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
   | zero => cases h
   | succ n => simp [Nat.pow_succ]
 
+instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
+  ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pos_pow_of_pos m (pos_of_neZero _))⟩
+
 /-! # min/max -/
 
 /--

src/Init/Data/NeZero.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2021 Eric Rodriguez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Rodriguez
+-/
+prelude
+import Init.Data.Zero
+
+
+/-!
+# `NeZero` typeclass
+
+We create a typeclass `NeZero n` which carries around the fact that `(n : R) ≠ 0`.
+
+## Main declarations
+
+* `NeZero`: `n ≠ 0` as a typeclass.
+-/
+
+
+variable {R : Type _} [Zero R]
+
+/-- A type-class version of `n ≠ 0`.  -/
+class NeZero (n : R) : Prop where
+  /-- The proposition that `n` is not zero. -/
+  out : n ≠ 0
+
+theorem NeZero.ne (n : R) [h : NeZero n] : n ≠ 0 :=
+  h.out
+
+theorem NeZero.ne' (n : R) [h : NeZero n] : 0 ≠ n :=
+  h.out.symm
+
+theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 :=
+  ⟨fun h ↦ h.out, NeZero.mk⟩
+
+@[simp] theorem neZero_zero_iff_false {α : Type _} [Zero α] : NeZero (0 : α) ↔ False :=
+  ⟨fun h ↦ h.ne rfl, fun h ↦ h.elim⟩

src/Init/Data/Zero.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2021 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Mario Carneiro
+-/
+prelude
+import Init.Core
+
+/-!
+Instances converting between `Zero α` and `OfNat α (nat_lit 0)`.
+-/
+
+instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
+  ofNat := ‹Zero α›.1
+
+instance (priority := 200) Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
+  zero := 0

src/Init/Prelude.lean

@@ -1304,6 +1304,11 @@ class HShiftRight (α : Type u) (β : Type v) (γ : outParam (Type w)) where
     this is equivalent to `a / 2 ^ b`. -/
   hShiftRight : α → β → γ
 
+/-- A type with a zero element. -/
+class Zero (α : Type u) where
+  /-- The zero element of the type. -/
+  zero : α
+
 /-- The homogeneous version of `HAdd`: `a + b : α` where `a b : α`. -/
 class Add (α : Type u) where
   /-- `a + b` computes the sum of `a` and `b`. See `HAdd`. -/

src/Lean/ToExpr.lean

@@ -48,7 +48,8 @@ instance : ToExpr (Fin n) where
   toExpr a :=
     let r := mkRawNatLit a.val
     mkApp3 (.const ``OfNat.ofNat [0]) (.app (mkConst ``Fin) (toExpr n)) r
-      (mkApp2 (.const ``Fin.instOfNat []) (mkNatLit (n-1)) r)
+      (mkApp3 (.const ``Fin.instOfNat []) (toExpr n)
+        (.app (.const ``Nat.instNeZeroSucc []) (mkNatLit (n-1))) r)
 
 instance : ToExpr (BitVec n) where
   toTypeExpr := .app (mkConst ``BitVec) (toExpr n)