From 01f9ec5647813da654e2a770715bc755386fb646 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Tue, 29 Oct 2024 19:35:36 +0300 Subject: [PATCH] [ base ] Make `Nat`'s `NonZero` to be an alias for `IsSucc` --- CHANGELOG_NEXT.md | 4 +++ libs/base/Data/Nat.idr | 31 +++++++++++++---------- libs/contrib/Data/Nat/Factor.idr | 8 +++--- libs/contrib/Data/Vect/Properties/Fin.idr | 6 ++--- libs/papers/Search/Auto.idr | 2 +- 5 files changed, 30 insertions(+), 21 deletions(-) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 2cb67aff00..8943a5b4e8 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -225,6 +225,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`. diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index 7adb885cad..d633da025c 100644 --- a/libs/base/Data/Nat.idr +++ b/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,17 @@ 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 +public export %inline +%deprecate -- use ItIsSucc instead +SIsNonZero : NonZero (S n) +SIsNonZero = ItIsSucc + public export power : Nat -> Nat -> Nat power base Z = S Z @@ -319,15 +333,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 +356,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 +377,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 +388,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 +416,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 diff --git a/libs/contrib/Data/Nat/Factor.idr b/libs/contrib/Data/Nat/Factor.idr index 86659feab6..faf817387a 100644 --- a/libs/contrib/Data/Nat/Factor.idr +++ b/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 diff --git a/libs/contrib/Data/Vect/Properties/Fin.idr b/libs/contrib/Data/Vect/Properties/Fin.idr index 574ab38f50..938bcfc913 100644 --- a/libs/contrib/Data/Vect/Properties/Fin.idr +++ b/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 diff --git a/libs/papers/Search/Auto.idr b/libs/papers/Search/Auto.idr index 0448cf2771..c36d07f0df 100644 --- a/libs/papers/Search/Auto.idr +++ b/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))