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)

tests/lean/1870.lean

@@ -1,12 +1,3 @@
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
-instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
-  zero := 0
-
 class One (α : Type u) where
   one : α
 

tests/lean/1870.lean.expected.out

@@ -1,15 +1,15 @@
-1870.lean:21:2-21:35: error: type mismatch
+1870.lean:12:2-12:35: error: type mismatch
   congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?_)
 has type
   OfNat.ofNat 0 = OfNat.ofNat 0 : Prop
 but is expected to have type
   OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
-1870.lean:25:2-25:16: error: tactic 'apply' failed, failed to unify
+1870.lean:16:2-16:16: error: tactic 'apply' failed, failed to unify
   ?f ?a₁ = ?f ?a₂
 with
   OfNat.ofNat 0 = OfNat.ofNat 1
 ⊢ OfNat.ofNat 0 = OfNat.ofNat 1
-1870.lean:30:2-30:16: error: tactic 'apply' failed, failed to unify
+1870.lean:21:2-21:16: error: tactic 'apply' failed, failed to unify
   ?f ?a₁ = ?f ?a₂
 with
   OfNat.ofNat 0 = OfNat.ofNat 1

tests/lean/2178.lean

@@ -1,5 +1,3 @@
-class Zero (α : Type u) where
-  zero : α
 class AddZeroClass (M : Type u) extends Zero M, Add M
 class AddMonoid (M : Type u) extends AddZeroClass M where
   nsmul : Nat → M → M := fun _ _ => Zero.zero

tests/lean/diamond10.lean

@@ -1,6 +1,3 @@
-class Zero (A : Type u) where zero : A
-instance {A} [Zero A] : OfNat A (nat_lit 0) := ⟨Zero.zero⟩
-
 class AddMonoid (A : Type u) extends Add A, Zero A
 class Semiring (R : Type u) extends AddMonoid R
 class SubNegMonoid (A : Type u) extends AddMonoid A, Neg A

tests/lean/diamond7.lean

@@ -39,12 +39,6 @@ class AddSemigroup (α : Type u) extends Add α where
 class AddCommSemigroup (α : Type u) extends AddSemigroup α where
   add_comm (a b : α) : a + b = b + a
 
-class Zero (α : Type u) where
-  zero : α
-
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := Zero.zero
-
 class AddMonoid (α : Type u) extends AddSemigroup α, Zero α where
   zero_add (a : α) : 0 + a = a
   add_zero (a : α) : a + 0 = a

tests/lean/diamond8.lean

@@ -1,9 +1,6 @@
 class One (M : Type u) where one : M
 instance {M} [One M] : OfNat M (nat_lit 1) := ⟨One.one⟩
 
-class Zero (A : Type u) where zero : A
-instance {A} [Zero A] : OfNat A (nat_lit 0) := ⟨Zero.zero⟩
-
 class Monoid (M : Type u) extends Mul M, One M where
   mul_one (m : M) : m * 1 = m
 

tests/lean/diamond9.lean

@@ -1,6 +1,3 @@
-class Zero (A : Type u) where zero : A
-instance {A} [Zero A] : OfNat A (nat_lit 0) := ⟨Zero.zero⟩
-
 class AddGroup (A : Type u) extends Zero A where
   gsmul : Int → A → A
   gsmul_zero' : ∀ a, gsmul 0 a = 0

tests/lean/isDefEqOffsetBug.lean

@@ -1,11 +1,3 @@
-class Zero (α : Type u) where
-  zero : α
-
-export Zero (zero)
-
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := zero
-
 class AddGroup (α : Type u) extends Add α, Zero α, Neg α where
   addAssoc : {a b c : α} → a + b + c = a + (b + c)
   zeroAdd  : {a : α} → 0 + a = a

tests/lean/isDefEqOffsetBug.lean.expected.out

@@ -1,4 +1,4 @@
-isDefEqOffsetBug.lean:27:2-27:5: error: type mismatch
+isDefEqOffsetBug.lean:19:2-19:5: error: type mismatch
   rfl
 has type
   0 + 0 = 0 + 0 : Prop

tests/lean/run/2265.lean

@@ -1,3 +1,3 @@
-class NeZero (n : Nat) : Prop
-theorem mul_div (m n : Nat) [NeZero n] : (m * n) / n = m := sorry
-example [NeZero n] : (m * n) / n = m := by simp [mul_div m _]
+class NeZero' (n : Nat) : Prop
+theorem mul_div (m n : Nat) [NeZero' n] : (m * n) / n = m := sorry
+example [NeZero' n] : (m * n) / n = m := by simp [mul_div m _]

tests/lean/run/2461.lean

@@ -1,8 +1,5 @@
 section algebra_hierarchy_classes_to_comm_ring
 
-class Zero (α : Type) where
-  zero : α
-
 class One (α : Type) where
   one : α
 

tests/lean/run/326.lean

@@ -1,5 +1,3 @@
-abbrev Zero α := OfNat α (nat_lit 0)
-
 class Monoid (α : Type u) [Zero α] extends Add α where
   zero_add (a : α) : 0 + a = a
   add_zero (a : α) : a + 0 = a

tests/lean/run/3313.lean

@@ -1,6 +1,3 @@
-class Zero (α : Type) where
-  zero : α
-
 class AddCommGroup (α : Type) extends Zero α where
 
 class Ring (α : Type) extends Zero α, AddCommGroup α

tests/lean/run/3807.lean

@@ -93,12 +93,6 @@ section Mathlib.Init.ZeroOne
 
 set_option autoImplicit true
 
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α
 

tests/lean/run/788.lean

@@ -3,3 +3,4 @@ example : (0 : Nat) = Nat.zero := by
 
 example : (0 : Fin 9) = (Fin.ofNat 0) := by
   simp only [OfNat.ofNat]
+  rfl

tests/lean/run/KyleAlg.lean

@@ -21,13 +21,8 @@ export One (one)
 instance [One α] : OfNat α (nat_lit 1) where
     ofNat := one
 
-class Zero (α : Type u) where
-    zero : α
 export Zero (zero)
 
-instance [Zero α] : OfNat α (nat_lit 0) where
-    ofNat := zero
-
 class MulComm (α : Type u) [Mul α] : Prop where
     mulComm : {a b : α} → a * b = b * a
 export MulComm (mulComm)

tests/lean/run/KyleAlgAbbrev.lean

@@ -21,8 +21,6 @@ export One (one)
 instance [One α] : OfNat α (nat_lit 1) where
     ofNat := one
 
-class Zero (α : Type u) where
-    zero : α
 export Zero (zero)
 
 instance [Zero α] : OfNat α (nat_lit 0) where

tests/lean/run/binop_binrel_perf_issue.lean

@@ -26,12 +26,6 @@ section Mathlib.Init.ZeroOne
 
 set_option autoImplicit true
 
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α
 

tests/lean/run/dsimpNatLitIssue.lean

@@ -1,11 +1,5 @@
 variable {R M : Type}
 
-class Zero (α : Type) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 /-- Typeclass for the `⊥` (`\bot`) notation -/
 class Bot (α : Type) where
   /-- The bot (`⊥`, `\bot`) element -/

tests/lean/run/fin_two_pow.lean

@@ -0,0 +1,5 @@
+-- Check that we can write numerals in `Fin (2^n)`
+-- even though `2^n` is not a definitionally a successor,
+-- via the `NeZero (2^n)` instance.
+
+example {n : Nat} : Fin (2^n) := 0

tests/lean/run/linearCategory_perf_issue.lean

@@ -2,12 +2,6 @@ universe u v w v₁ v₂ v₃ u₁ u₂ u₃
 
 section Mathlib.Algebra.Group.ZeroOne
 
-class Zero (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α
 

tests/lean/run/mathlibetaissue.lean

@@ -44,10 +44,6 @@ end Std.Classes.RatCast
 
 section Mathlib.Init.ZeroOne
 
-class Zero.{u} (α : Type u) where
-  zero : α
-instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
 class One (α : Type u) where
   one : α
 instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where

tests/lean/run/matrix.lean

@@ -10,15 +10,6 @@ instance [OfNat α (nat_lit 1)] : One α where
 instance [One α] : OfNat α (nat_lit 1) where
   ofNat := One.one
 
-class Zero (α : Type u) where
-  zero : α
-
-instance [OfNat α (nat_lit 0)] : Zero α where
-  zero := 0
-
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := Zero.zero
-
 /- Simple Matrix -/
 
 def Matrix (m n : Nat) (α : Type u) : Type u :=

tests/lean/run/ofNatNormNum.lean

@@ -6,15 +6,9 @@ export OfNatSound (ofNat_add)
 theorem ex1 {α : Type u} [Add α] [(n : Nat) → OfNat α n] [OfNatSound α] : (10000000 : α) + 10000000 = 20000000 :=
   ofNat_add ..
 
-class Zero (α : Type u) where
-  zero : α
-
 class One (α : Type u) where
   one : α
 
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := Zero.zero
-
 instance [One α] : OfNat α (nat_lit 1) where
   ofNat := One.one
 

tests/lean/run/ofNat_class.lean

@@ -12,4 +12,4 @@ local macro "ofNat_class" Class:ident n:num : command =>
   instance {α} [OfNat α (nat_lit $n)] : $Class α where
     $field:ident := $n)
 
-ofNat_class Zero 0
+ofNat_class Zero' 0