From 8c804eb89e8be6600f26a47a0c82ed44fb63f1db Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 18 Jan 2024 13:39:19 +0000 Subject: [PATCH 1/5] Add `NonNull` on the model of `Data.Nat.NonZero` --- CHANGELOG.md | 13 +++++++++ src/Data/List/Base.agda | 58 ++++++++++++++++++++++++++++++++++++++--- 2 files changed, 68 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5b3079dee4..7285ccfb6e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -37,6 +37,19 @@ Additions to existing modules nonZeroIndex : Fin n → ℕ.NonZero n ``` +* In `Data.List.Base`: + ```agda + record NonNull (xs : List A) : Set + instance nonNull : NonNull (x ∷ xs) + ≢-nonNull : xs ≢ [] → NonNull xs + >-nonNull : length xs > 0 → NonNull xs + ≢-nonNull⁻¹ : .{{NonNull xs}} → xs ≢ [] + nonNull⇒nonZero : .{{NonNull xs}} → ℕ.NonZero (length xs) + >-nonNull⁻¹ : .{{NonNull xs}} → length xs > 0 + nonNull-head : .{{NonNull xs}} → A + nonNull-tail : .{{NonNull xs}} → List A + ``` + * In `Data.List.Relation.Unary.All.Properties`: ```agda All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 16546110b6..cbfcdf6c7b 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -13,10 +13,10 @@ module Data.List.Base where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid) open import Data.Bool.Base as Bool - using (Bool; false; true; not; _∧_; _∨_; if_then_else_) + using (Bool; false; true; not; _∧_; _∨_; if_then_else_; T) open import Data.Fin.Base using (Fin; zero; suc) open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) -open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s; _>_; z-nonNull : length xs > 0 → NonNull xs +>-nonNull {xs = _ ∷ _} _ = _ + +-- Destructors + +≢-nonNull⁻¹ : .{{NonNull xs}} → xs ≢ [] +≢-nonNull⁻¹ {xs = _ ∷ _} () + +nonNull⇒nonZero : (xs : List A) → .{{NonNull xs}} → ℕ.NonZero (length xs) +nonNull⇒nonZero xs@(_ ∷ _) = _ + +>-nonNull⁻¹ : (xs : List A) → .{{NonNull xs}} → length xs > 0 +>-nonNull⁻¹ xs = ℕ.>-nonZero⁻¹ _ where instance _ = nonNull⇒nonZero xs + +-- Specimen uses + +nonNull-head : ∀ xs → .{{NonNull xs}} → A +nonNull-head xs@(y ∷ _) = y + +nonNull-tail : ∀ xs → .{{NonNull xs}} → List A +nonNull-tail xs@(_ ∷ ys) = ys + ------------------------------------------------------------------------ -- DEPRECATED ------------------------------------------------------------------------ From 645a1cd183475f5cbfe1f84444e9273fb27a1640 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 20 Jan 2024 14:29:39 +0000 Subject: [PATCH 2/5] moved content to `Data.List.Relation.Unary.NonNull`; fixed `CHANGELOG` --- CHANGELOG.md | 18 ++----- src/Data/List/Base.agda | 56 ++----------------- src/Data/List/Relation/Unary/NonNull.agda | 66 +++++++++++++++++++++++ 3 files changed, 74 insertions(+), 66 deletions(-) create mode 100644 src/Data/List/Relation/Unary/NonNull.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 7285ccfb6e..8781a6bb82 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,6 +29,11 @@ Deprecated names New modules ----------- +* Non-null lists, on the model of `Data.Nat.Base.NonZero` in: + ```agda + Data.List.Relation.Unary.NonNull + ``` + Additions to existing modules ----------------------------- @@ -37,19 +42,6 @@ Additions to existing modules nonZeroIndex : Fin n → ℕ.NonZero n ``` -* In `Data.List.Base`: - ```agda - record NonNull (xs : List A) : Set - instance nonNull : NonNull (x ∷ xs) - ≢-nonNull : xs ≢ [] → NonNull xs - >-nonNull : length xs > 0 → NonNull xs - ≢-nonNull⁻¹ : .{{NonNull xs}} → xs ≢ [] - nonNull⇒nonZero : .{{NonNull xs}} → ℕ.NonZero (length xs) - >-nonNull⁻¹ : .{{NonNull xs}} → length xs > 0 - nonNull-head : .{{NonNull xs}} → A - nonNull-tail : .{{NonNull xs}} → List A - ``` - * In `Data.List.Relation.Unary.All.Properties`: ```agda All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index cbfcdf6c7b..5d6402db75 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -13,10 +13,10 @@ module Data.List.Base where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid) open import Data.Bool.Base as Bool - using (Bool; false; true; not; _∧_; _∨_; if_then_else_; T) + using (Bool; false; true; not; _∧_; _∨_; if_then_else_) open import Data.Fin.Base using (Fin; zero; suc) open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) -open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s; _>_; z-nonNull : length xs > 0 → NonNull xs ->-nonNull {xs = _ ∷ _} _ = _ - --- Destructors - -≢-nonNull⁻¹ : .{{NonNull xs}} → xs ≢ [] -≢-nonNull⁻¹ {xs = _ ∷ _} () - -nonNull⇒nonZero : (xs : List A) → .{{NonNull xs}} → ℕ.NonZero (length xs) -nonNull⇒nonZero xs@(_ ∷ _) = _ - ->-nonNull⁻¹ : (xs : List A) → .{{NonNull xs}} → length xs > 0 ->-nonNull⁻¹ xs = ℕ.>-nonZero⁻¹ _ where instance _ = nonNull⇒nonZero xs - --- Specimen uses - -nonNull-head : ∀ xs → .{{NonNull xs}} → A -nonNull-head xs@(y ∷ _) = y - -nonNull-tail : ∀ xs → .{{NonNull xs}} → List A -nonNull-tail xs@(_ ∷ ys) = ys ------------------------------------------------------------------------ -- DEPRECATED diff --git a/src/Data/List/Relation/Unary/NonNull.agda b/src/Data/List/Relation/Unary/NonNull.agda new file mode 100644 index 0000000000..2f09650a40 --- /dev/null +++ b/src/Data/List/Relation/Unary/NonNull.agda @@ -0,0 +1,66 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The `NonNull` predicate, on the model of `Data.Nat.Base.NonZero` +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.List.Relation.Unary.NonNull where + +open import Level using (Level) +open import Data.Bool.Base using (not; T) +open import Data.List.Base using (List; []; _∷_; null; length) +open import Data.Nat.Base as ℕ using (ℕ; _>_) +open import Relation.Binary.PropositionalEquality.Core + using (_≢_; refl) +open import Relation.Nullary.Negation.Core using (contradiction) + + +private + variable + a : Level + A : Set a + x : A + xs : List A + +------------------------------------------------------------------------ +-- A predicate saying that a list is not equal to []. + +record NonNull {A : Set a} (xs : List A) : Set a where + field + nonNull : T (not (null xs)) + +-- Instances + +instance + nonNull : NonNull (x ∷ xs) + nonNull = _ + +-- Constructors + +≢-nonNull : xs ≢ [] → NonNull xs +≢-nonNull {xs = []} []≢[] = contradiction refl []≢[] +≢-nonNull {xs = _ ∷ _} xs≢[] = _ + +>-nonNull : length xs > 0 → NonNull xs +>-nonNull {xs = _ ∷ _} _ = _ + +-- Destructors + +≢-nonNull⁻¹ : .{{NonNull xs}} → xs ≢ [] +≢-nonNull⁻¹ {xs = _ ∷ _} () + +nonNull⇒nonZero : (xs : List A) → .{{NonNull xs}} → ℕ.NonZero (length xs) +nonNull⇒nonZero xs@(_ ∷ _) = _ + +>-nonNull⁻¹ : (xs : List A) → .{{NonNull xs}} → length xs > 0 +>-nonNull⁻¹ xs = ℕ.>-nonZero⁻¹ _ where instance _ = nonNull⇒nonZero xs + +-- Specimen uses + +nonNull-head : ∀ xs → .{{NonNull xs}} → A +nonNull-head xs@(y ∷ _) = y + +nonNull-tail : ∀ xs → .{{NonNull xs}} → List A +nonNull-tail xs@(_ ∷ ys) = ys From 5e1bc04017ff59e393dd8f83d07d6e608c3552d6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 20 Jan 2024 14:30:39 +0000 Subject: [PATCH 3/5] removed blank line --- src/Data/List/Base.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 5d6402db75..a90b0a6555 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -547,7 +547,6 @@ module _ (A : Set a) where ; ε = [] } - ------------------------------------------------------------------------ -- DEPRECATED ------------------------------------------------------------------------ From 3ab7fdb1e20f128cd4700f649607a772e9e2506f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 20 Jan 2024 14:31:23 +0000 Subject: [PATCH 4/5] removed blank line --- src/Data/List/Base.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index a90b0a6555..16546110b6 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -29,7 +29,6 @@ import Relation.Binary.Definitions as B open import Relation.Binary.PropositionalEquality.Core using (_≡_) open import Relation.Nullary.Decidable.Core using (T?; does; ¬?) - private variable a b c p ℓ : Level From c1f8e9d9df138bbec51cf0416f8e902683f29f50 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 20 Jan 2024 14:34:52 +0000 Subject: [PATCH 5/5] commentary --- src/Data/List/Relation/Unary/NonNull.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Unary/NonNull.agda b/src/Data/List/Relation/Unary/NonNull.agda index 2f09650a40..a88e8d7084 100644 --- a/src/Data/List/Relation/Unary/NonNull.agda +++ b/src/Data/List/Relation/Unary/NonNull.agda @@ -25,7 +25,7 @@ private xs : List A ------------------------------------------------------------------------ --- A predicate saying that a list is not equal to []. +-- Definition record NonNull {A : Set a} (xs : List A) : Set a where field