[ base ] Make Nat's NonZero to be an alias for IsSucc

CHANGELOG_NEXT.md

@@ -240,6 +240,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Added `Data.IORef.atomically` for the chez backend.
 
+* `Data.Nat.NonZero` was made to be an alias for `Data.Nat.IsSucc`.
+  `SIsNonZero` was made to be an alias for `ItIsSucc`, was marked as deprecated,
+  and won't work on LHS anymore.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.

libs/base/Data/Nat.idr

@@ -32,6 +32,9 @@ isSucc : Nat -> Bool
 isSucc Z     = False
 isSucc (S n) = True
 
+||| A definition of non-zero with a better behaviour than `Not (x = Z)`
+||| This is amenable to proof search and `NonZero Z` is more readily
+||| detected as impossible by Idris
 public export
 data IsSucc : (n : Nat) -> Type where
   ItIsSucc : IsSucc (S n)
@@ -45,6 +48,18 @@ isItSucc : (n : Nat) -> Dec (IsSucc n)
 isItSucc Z = No absurd
 isItSucc (S n) = Yes ItIsSucc
 
+||| A hystorical synonym for `IsSucc`
+public export
+0 NonZero : Nat -> Type
+NonZero = IsSucc
+
+-- Remove as soon as 0.8.0 (or greater) is released
+||| Use `ItIsSucc` instead
+public export %inline
+%deprecate
+SIsNonZero : NonZero (S n)
+SIsNonZero = ItIsSucc
+
 public export
 power : Nat -> Nat -> Nat
 power base Z       = S Z
@@ -319,15 +334,6 @@ export
 Injective S where
   injective Refl = Refl
 
-||| A definition of non-zero with a better behaviour than `Not (x = Z)`
-||| This is amenable to proof search and `NonZero Z` is more readily
-||| detected as impossible by Idris
-public export
-data NonZero : Nat -> Type where
-  SIsNonZero : NonZero (S x)
-
-export Uninhabited (NonZero Z) where uninhabited SIsNonZero impossible
-
 export
 SIsNotZ : Not (S x = Z)
 SIsNotZ = absurd
@@ -351,7 +357,7 @@ modNatNZ left (S right) _ = mod' left left right
 
 export partial
 modNat : Nat -> Nat -> Nat
-modNat left (S right) = modNatNZ left (S right) SIsNonZero
+modNat left (S right) = modNatNZ left (S right) ItIsSucc
 
 ||| Auxiliary function:
 ||| div' fuel a b = a `div` (S b)
@@ -372,7 +378,7 @@ divNatNZ left (S right) _ = div' left left right
 
 export partial
 divNat : Nat -> Nat -> Nat
-divNat left (S right) = divNatNZ left (S right) SIsNonZero
+divNat left (S right) = divNatNZ left (S right) ItIsSucc
 
 export
 covering
@@ -383,7 +389,7 @@ divCeilNZ x y p = case (modNatNZ x y p) of
 
 export partial
 divCeil : Nat -> Nat -> Nat
-divCeil x (S y) = divCeilNZ x (S y) SIsNonZero
+divCeil x (S y) = divCeilNZ x (S y) ItIsSucc
 
 
 public export
@@ -411,7 +417,7 @@ covering
 gcd : (a: Nat) -> (b: Nat) -> {auto 0 ok: NotBothZero a b} -> Nat
 gcd a Z     = a
 gcd Z b     = b
-gcd a (S b) = gcd (S b) (modNatNZ a (S b) SIsNonZero)
+gcd a (S b) = gcd (S b) (modNatNZ a (S b) ItIsSucc)
 
 export partial
 lcm : Nat -> Nat -> Nat

libs/contrib/Data/Nat/Factor.idr

@@ -373,8 +373,8 @@ selfIsCommonFactor a = CommonFactorExists a reflexive reflexive
 gcdUnproven' : (m, n : Nat) -> (0 sizeM : SizeAccessible m) -> (0 n_lt_m : LT n m) -> Nat
 gcdUnproven' m Z _ _ = m
 gcdUnproven' m (S n) (Access rec) n_lt_m =
-  let mod_lt_n = boundModNatNZ m (S n) SIsNonZero in
-  gcdUnproven' (S n) (modNatNZ m (S n) SIsNonZero) (rec _ n_lt_m) mod_lt_n
+  let mod_lt_n = boundModNatNZ m (S n) ItIsSucc in
+  gcdUnproven' (S n) (modNatNZ m (S n) ItIsSucc) (rec _ n_lt_m) mod_lt_n
 
 ||| Total definition of the gcd function. Does not return GСD evidence, but is faster.
 gcdUnproven : Nat -> Nat -> Nat
@@ -388,7 +388,7 @@ gcdUnproven'Greatest : {m, n, c : Nat} -> (0 sizeM : SizeAccessible m) -> (0 n_l
   -> Factor c m -> Factor c n -> Factor c (gcdUnproven' m n sizeM n_lt_m)
 gcdUnproven'Greatest {n = Z} _ _ cFactM _ = cFactM
 gcdUnproven'Greatest {n = S n} (Access rec) n_lt_m cFactM cFactN =
-  gcdUnproven'Greatest (rec _ n_lt_m) (boundModNatNZ m (S n) SIsNonZero) cFactN (commonFactorAlsoFactorOfMod cFactM cFactN)
+  gcdUnproven'Greatest (rec _ n_lt_m) (boundModNatNZ m (S n) ItIsSucc) cFactN (commonFactorAlsoFactorOfMod cFactM cFactN)
 
 gcdUnprovenGreatest : (m, n : Nat) -> {auto 0 ok : NotBothZero m n} -> (q : Nat) -> CommonFactor q m n -> Factor q (gcdUnproven m n)
 gcdUnprovenGreatest m n q (CommonFactorExists q qFactM qFactN) with (isLT n m)
@@ -402,7 +402,7 @@ gcdUnprovenGreatest m n q (CommonFactorExists q qFactM qFactN) with (isLT n m)
 
 gcdUnproven'CommonFactor : {m, n : Nat} -> (0 sizeM : SizeAccessible m) -> (0 n_lt_m : LT n m) -> CommonFactor (gcdUnproven' m n sizeM n_lt_m) m n
 gcdUnproven'CommonFactor {n = Z} _ _ = CommonFactorExists _ reflexive (anythingFactorZero m)
-gcdUnproven'CommonFactor {n = S n} (Access rec) n_lt_m with (gcdUnproven'CommonFactor (rec _ n_lt_m) (boundModNatNZ m (S n) SIsNonZero))
+gcdUnproven'CommonFactor {n = S n} (Access rec) n_lt_m with (gcdUnproven'CommonFactor (rec _ n_lt_m) (boundModNatNZ m (S n) ItIsSucc))
   gcdUnproven'CommonFactor (Access rec) n_lt_m | (CommonFactorExists _ factM factN)
     = CommonFactorExists _ (modFactorAlsoFactorOfDivider factM factN) factM
 

libs/contrib/Data/Vect/Properties/Fin.idr

@@ -19,13 +19,13 @@ etaCons (x :: xs) = Refl
 ||| Inhabitants of `Fin n` witness `NonZero n`
 export
 finNonZero : Fin n -> NonZero n
-finNonZero  FZ    = SIsNonZero
-finNonZero (FS i) = SIsNonZero
+finNonZero  FZ    = ItIsSucc
+finNonZero (FS i) = ItIsSucc
 
 ||| Inhabitants of `Fin n` witness runtime-irrelevant vectors of length `n` aren't empty
 export
 finNonEmpty : (0 xs : Vect n a) -> NonZero n -> NonEmpty xs
-finNonEmpty xs SIsNonZero = replace {p = NonEmpty} (etaCons xs) IsNonEmpty
+finNonEmpty xs ItIsSucc = replace {p = NonEmpty} (etaCons xs) IsNonEmpty
 
 ||| Cast an index into a runtime-irrelevant `Vect` into the position
 ||| of the corresponding element

libs/papers/Search/Auto.idr

@@ -150,7 +150,7 @@ namespace RuleName
     where
     display : Nat -> List Char
     display n =
-      let (p, q) = divmodNatNZ n 26 SIsNonZero in
+      let (p, q) = divmodNatNZ n 26 ItIsSucc in
       cast (q + cast 'a') :: if p == 0 then [] else display (assert_smaller n (pred p))