From fbd5cf340b276db1e33a581804f5dfc4b7aac8b4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 22 Sep 2023 13:39:05 +0100 Subject: [PATCH 01/15] Addresses issue #2092 --- CHANGELOG.md | 13 +++ README/Data/List/Relation/Unary/Null.agda | 108 ++++++++++++++++++++++ src/Data/List/Relation/Unary/Null.agda | 57 ++++++++++++ src/Data/Nat/Relation/Unary/Null.agda | 54 +++++++++++ src/Relation/Unary/Null.agda | 38 ++++++++ src/Relation/Unary/Refinement.agda | 42 +++++++++ 6 files changed, 312 insertions(+) create mode 100644 README/Data/List/Relation/Unary/Null.agda create mode 100644 src/Data/List/Relation/Unary/Null.agda create mode 100644 src/Data/Nat/Relation/Unary/Null.agda create mode 100644 src/Relation/Unary/Null.agda create mode 100644 src/Relation/Unary/Refinement.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index b1e8ab2fa6..83dbb5f0bb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -985,6 +985,19 @@ Major improvements * A new module `Algebra.Lattice.Bundles.Raw` is also introduced. * `RawLattice` has been moved from `Algebra.Lattice.Bundles` to this new module. +### Generalised the definition of `NonZero` from `Data.Nat.Base` to `NonNull` based on: + +* A new module `Relation.Unary.Refinement` defining a general notion of refinement + of a type wrt a `Bool`-valued predicate. + +* A new module `Relation.Unary.Null` defining being able to test for `null`ity, + based on a `Bool`-valued predicate `null`, using `Refinement`. + +* Instances `Data.{Nat|List}.Relation.Unary.Null` of `Null` for `Nat` and `List`. + +* Example uses in `README.Data.List.Relation.Unary.Null` + + Deprecated modules ------------------ diff --git a/README/Data/List/Relation/Unary/Null.agda b/README/Data/List/Relation/Unary/Null.agda new file mode 100644 index 0000000000..2d8e1805d9 --- /dev/null +++ b/README/Data/List/Relation/Unary/Null.agda @@ -0,0 +1,108 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Illustration of the `NonNull predicate over `List` +------------------------------------------------------------------------ + +module README.Data.List.Relation.Unary.Null where + +open import Data.List.Base using (List; []; _∷_; head) +open import Data.List.Relation.Unary.Null +open import Data.Product.Base using (Σ; _,_; proj₁; proj₂) +open import Level using (Level) +open import Relation.Binary.PropositionalEquality +open import Relation.Unary.Null +open import Relation.Unary.Refinement + +private + variable + + a b : Level + A : Set a + B : Set b + x : A + xs : List A + ys : List B + +------------------------------------------------------------------------ +-- Example deployment: a safe head function + +safe-head : (xs : List A) → .{{NonNull xs}} → A +safe-head (x ∷ _) = x + +------------------------------------------------------------------------ +-- Example deployments: scans + +-- ScanL + +module ScanL (f : A → B → A) where + + scanl : A → List B → List A + scanl e [] = e ∷ [] + scanl e (x ∷ xs) = e ∷ scanl (f e x) xs + + instance scanlNonNull : {e : A} {xs : List B} → NonNull (scanl e xs) + scanlNonNull {xs = []} = _ + scanlNonNull {xs = x ∷ xs} = _ + + scanl⁺ : A → List B → [ List A ]⁺ + scanl⁺ e xs = refine⁺ (scanl e xs) + + +-- ScanR + +module ScanRΣ (f : A → B → B) (e : B) where + +-- design pattern: refinement types via Σ-types + + scanrΣ : List A → Σ (List B) NonNull + scanrΣ [] = e ∷ [] , _ + scanrΣ (x ∷ xs) with ys@(y ∷ _) , _ ← scanrΣ xs = f x y ∷ ys , _ + + scanr : List A → List B + scanr xs = proj₁ (scanrΣ xs) + + instance scanrNonNull : {xs : List A} → NonNull (scanr xs) + scanrNonNull {xs = xs} = proj₂ (scanrΣ xs) + + unfold-scanr-∷ : ∀ xs → + let ys = scanr xs in + let instance _ = scanrNonNull {xs = xs} in + scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys + unfold-scanr-∷ xs with ys@(y ∷ _) , _ ← scanrΣ xs = refl + +module ScanR (f : A → B → B) (e : B) where + +-- design pattern: refinement types via mutual recursion + +-- to simulate the refinement type { xs : List A | NonNull xs } +-- define two functions by mutual recursion: +-- `f` : the bare, 'extracted' underlying function +-- `fNonNull` : the (irrelevant instance) witness to the refinement predicate + +-- but for now, again we seem to have to go via a third function +-- essentially `scanrΣ` but with an irrelevant instance field instead + + scanr⁺ : List A → [ List B ]⁺ + + refine⁻ (scanr⁺ []) = e ∷ [] + refined (scanr⁺ []) = _ + + scanr⁺ (x ∷ xs) with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys + = refine⁺ (f x y ∷ ys) + + scanr : List A → List B + scanr xs = refine⁻ (scanr⁺ xs) + + instance scanrNonNull : {xs : List A} → NonNull (scanr xs) + scanrNonNull {xs = xs} with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = _ + + unfold-scanr-∷ : ∀ xs → + let ys = scanr xs in + let instance _ = scanrNonNull {xs = xs} in + scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys + unfold-scanr-∷ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = refl + + + + diff --git a/src/Data/List/Relation/Unary/Null.agda b/src/Data/List/Relation/Unary/Null.agda new file mode 100644 index 0000000000..335fe769a5 --- /dev/null +++ b/src/Data/List/Relation/Unary/Null.agda @@ -0,0 +1,57 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Null instance for List +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.List.Relation.Unary.Null where + +open import Data.Nat.Base as Nat using (_>_; z-nonNull : length xs > 0 → NonNull xs +>-nonNull {xs = _ ∷ _} _ = _ + +-- Destructors + +≢-nonNull⁻¹ : (xs : List A) → .{{NonNull xs}} → xs ≢ [] +≢-nonNull⁻¹ (_ ∷ _) () + +>-nonNull⁻¹ : (xs : List A) → .{{NonNull xs}} → length xs > 0 +>-nonNull⁻¹ (_ ∷ _) = z_; z-nonZero : n > 0 → NonNull n +>-nonZero z-nonZero⁻¹ : ∀ n → .{{NonNull n}} → n > 0 +>-nonZero⁻¹ (suc n) = z Date: Fri, 22 Sep 2023 13:40:21 +0100 Subject: [PATCH 02/15] fix-whitespace --- README/Data/List/Relation/Unary/Null.agda | 5 +---- src/Data/Nat/Relation/Unary/Null.agda | 2 +- src/Relation/Unary/Null.agda | 2 +- src/Relation/Unary/Refinement.agda | 1 - 4 files changed, 3 insertions(+), 7 deletions(-) diff --git a/README/Data/List/Relation/Unary/Null.agda b/README/Data/List/Relation/Unary/Null.agda index 2d8e1805d9..256360b5d2 100644 --- a/README/Data/List/Relation/Unary/Null.agda +++ b/README/Data/List/Relation/Unary/Null.agda @@ -87,7 +87,7 @@ module ScanR (f : A → B → B) (e : B) where refine⁻ (scanr⁺ []) = e ∷ [] refined (scanr⁺ []) = _ - + scanr⁺ (x ∷ xs) with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = refine⁺ (f x y ∷ ys) @@ -103,6 +103,3 @@ module ScanR (f : A → B → B) (e : B) where scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys unfold-scanr-∷ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = refl - - - diff --git a/src/Data/Nat/Relation/Unary/Null.agda b/src/Data/Nat/Relation/Unary/Null.agda index ad036af658..f51ae501f2 100644 --- a/src/Data/Nat/Relation/Unary/Null.agda +++ b/src/Data/Nat/Relation/Unary/Null.agda @@ -21,7 +21,7 @@ private ------------------------------------------------------------------------ -- Instance -instance +instance nullℕ : Null ℕ nullℕ = record { null = _≡ᵇ 0 } diff --git a/src/Relation/Unary/Null.agda b/src/Relation/Unary/Null.agda index 2769de8967..1fe36d8b73 100644 --- a/src/Relation/Unary/Null.agda +++ b/src/Relation/Unary/Null.agda @@ -35,4 +35,4 @@ NonNull {{nullA}} = T ∘ not-null where open Null nullA [_]⁺ : (A : Set a) → {{nA : Null A}} → Set a [ A ]⁺ {{nullA}} = [ x ∈ A || not-null x ] where open Null nullA - + diff --git a/src/Relation/Unary/Refinement.agda b/src/Relation/Unary/Refinement.agda index daa5635e6b..0a8837d012 100644 --- a/src/Relation/Unary/Refinement.agda +++ b/src/Relation/Unary/Refinement.agda @@ -39,4 +39,3 @@ syntax RefinementSyntax A (λ x → p) = [ x ∈ A || p ] open Refinement public - From 4ef0e1edfa1edfa466c984a7697d009ee492e5d2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 22 Sep 2023 13:56:20 +0100 Subject: [PATCH 03/15] `NonZero` as `NonNull` --- src/Data/Nat/Relation/Unary/Null.agda | 33 ++++++++++++++++++++++----- 1 file changed, 27 insertions(+), 6 deletions(-) diff --git a/src/Data/Nat/Relation/Unary/Null.agda b/src/Data/Nat/Relation/Unary/Null.agda index f51ae501f2..22dba50a93 100644 --- a/src/Data/Nat/Relation/Unary/Null.agda +++ b/src/Data/Nat/Relation/Unary/Null.agda @@ -9,9 +9,10 @@ module Data.Nat.Relation.Unary.Null where open import Data.Nat.Base using (ℕ; zero; suc; _≡ᵇ_; _>_; z-nonZero : n > 0 → NonNull n +>-nonZero : n > 0 → NonZero n >-nonZero z-nonZero⁻¹ : ∀ n → .{{NonNull n}} → n > 0 +>-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0 >-nonZero⁻¹ (suc n) = z Date: Fri, 22 Sep 2023 13:57:53 +0100 Subject: [PATCH 04/15] ... simplified --- src/Data/Nat/Relation/Unary/Null.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/Nat/Relation/Unary/Null.agda b/src/Data/Nat/Relation/Unary/Null.agda index 22dba50a93..ea9bf2c419 100644 --- a/src/Data/Nat/Relation/Unary/Null.agda +++ b/src/Data/Nat/Relation/Unary/Null.agda @@ -9,7 +9,6 @@ module Data.Nat.Relation.Unary.Null where open import Data.Nat.Base using (ℕ; zero; suc; _≡ᵇ_; _>_; z Date: Fri, 22 Sep 2023 14:30:49 +0100 Subject: [PATCH 05/15] refinement (sic): constructor for `cons` --- README/Data/List/Relation/Unary/Null.agda | 9 +++------ src/Data/List/Relation/Unary/Null.agda | 6 ++++++ src/Relation/Unary/Null.agda | 1 - src/Relation/Unary/Refinement.agda | 4 ++-- 4 files changed, 11 insertions(+), 9 deletions(-) diff --git a/README/Data/List/Relation/Unary/Null.agda b/README/Data/List/Relation/Unary/Null.agda index 256360b5d2..d28b492e47 100644 --- a/README/Data/List/Relation/Unary/Null.agda +++ b/README/Data/List/Relation/Unary/Null.agda @@ -85,11 +85,8 @@ module ScanR (f : A → B → B) (e : B) where scanr⁺ : List A → [ List B ]⁺ - refine⁻ (scanr⁺ []) = e ∷ [] - refined (scanr⁺ []) = _ - - scanr⁺ (x ∷ xs) with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys - = refine⁺ (f x y ∷ ys) + scanr⁺ [] = e ∷⁺ [] + scanr⁺ (x ∷ xs) with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = f x y ∷⁺ ys scanr : List A → List B scanr xs = refine⁻ (scanr⁺ xs) @@ -101,5 +98,5 @@ module ScanR (f : A → B → B) (e : B) where let ys = scanr xs in let instance _ = scanrNonNull {xs = xs} in scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys - unfold-scanr-∷ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = refl + unfold-scanr-∷ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = refl diff --git a/src/Data/List/Relation/Unary/Null.agda b/src/Data/List/Relation/Unary/Null.agda index 335fe769a5..9f60ea7b07 100644 --- a/src/Data/List/Relation/Unary/Null.agda +++ b/src/Data/List/Relation/Unary/Null.agda @@ -14,6 +14,7 @@ open import Level open import Relation.Binary.PropositionalEquality using (_≢_; refl) open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Unary.Null +open import Relation.Unary.Refinement private variable @@ -55,3 +56,8 @@ instance >-nonNull⁻¹ : (xs : List A) → .{{NonNull xs}} → length xs > 0 >-nonNull⁻¹ (_ ∷ _) = z Date: Fri, 22 Sep 2023 14:36:06 +0100 Subject: [PATCH 06/15] tidying up `scanr` --- README/Data/List/Relation/Unary/Null.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/README/Data/List/Relation/Unary/Null.agda b/README/Data/List/Relation/Unary/Null.agda index d28b492e47..4fcf5386ee 100644 --- a/README/Data/List/Relation/Unary/Null.agda +++ b/README/Data/List/Relation/Unary/Null.agda @@ -84,8 +84,7 @@ module ScanR (f : A → B → B) (e : B) where -- essentially `scanrΣ` but with an irrelevant instance field instead scanr⁺ : List A → [ List B ]⁺ - - scanr⁺ [] = e ∷⁺ [] + scanr⁺ [] = e ∷⁺ [] scanr⁺ (x ∷ xs) with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = f x y ∷⁺ ys scanr : List A → List B From acb09e0894321f63ff2e5e41365d81691c1c6cc8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 22 Sep 2023 16:25:20 +0100 Subject: [PATCH 07/15] third ways to `scanr` --- README/Data/List/Relation/Unary/Null.agda | 59 ++++++++++++++++++++--- src/Data/List/Relation/Unary/Null.agda | 10 +++- 2 files changed, 60 insertions(+), 9 deletions(-) diff --git a/README/Data/List/Relation/Unary/Null.agda b/README/Data/List/Relation/Unary/Null.agda index 4fcf5386ee..1d5c984ad7 100644 --- a/README/Data/List/Relation/Unary/Null.agda +++ b/README/Data/List/Relation/Unary/Null.agda @@ -8,7 +8,7 @@ module README.Data.List.Relation.Unary.Null where open import Data.List.Base using (List; []; _∷_; head) open import Data.List.Relation.Unary.Null -open import Data.Product.Base using (Σ; _,_; proj₁; proj₂) +open import Data.Product.Base using (Σ; _,_; proj₁; proj₂; ∃₂; _×_) open import Level using (Level) open import Relation.Binary.PropositionalEquality open import Relation.Unary.Null @@ -17,12 +17,11 @@ open import Relation.Unary.Refinement private variable - a b : Level - A : Set a - B : Set b - x : A - xs : List A - ys : List B + a b : Level + A : Set a + B : Set b + x : A + xs zs : List A ------------------------------------------------------------------------ -- Example deployment: a safe head function @@ -30,6 +29,10 @@ private safe-head : (xs : List A) → .{{NonNull xs}} → A safe-head (x ∷ _) = x +safe-head-≡ : (eq : x ∷ xs ≡ zs) → + let instance _ = subst NonNull eq _ in x ≡ safe-head zs +safe-head-≡ refl = refl + ------------------------------------------------------------------------ -- Example deployments: scans @@ -97,5 +100,45 @@ module ScanR (f : A → B → B) (e : B) where let ys = scanr xs in let instance _ = scanrNonNull {xs = xs} in scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys - unfold-scanr-∷ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = refl + unfold-scanr-∷ xs with refine⁺ ys ← scanr⁺ xs in eq with y ∷ _ ← ys = refl + + unfold-scanr-∷≡ : ∀ xs → let ys = scanr xs in + ∃₂ λ y ys′ → ys ≡ y ∷ ys′ × scanr (x ∷ xs) ≡ f x y ∷ ys + unfold-scanr-∷≡ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys + = y , _ , refl , refl + +module ScanR′ (f : A → B → B) (e : B) where + +-- design pattern: refinement types via mutual recursion, using `nonNull-≡` + +-- to simulate the refinement type { xs : List A | NonNull xs } +-- define two functions by mutual recursion: +-- `f` : the bare, 'extracted' underlying function +-- `fNonNull` : the (irrelevant instance) witness to the refinement predicate + +-- but still using a `helper` function + + scanr : List A → List B + instance scanrNonNull : {xs : List A} → NonNull (scanr xs) + + private + helper : (xs : List A) → ∃₂ λ y ys → scanr xs ≡ y ∷ ys + helper xs = nonNull-[ scanr xs ]⁻ {{scanrNonNull {xs = xs}}} + + scanr [] = e ∷ [] + scanr (x ∷ xs) with y , _ ← helper xs = f x y ∷ scanr xs + + scanrNonNull {xs = []} = _ + scanrNonNull {xs = x ∷ xs} with _ ← helper xs = _ + + unfold-scanr-∷ : ∀ xs → + let ys = scanr xs in + let instance _ = scanrNonNull {xs = xs} in + scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys + unfold-scanr-∷ xs with y , _ , eq ← helper xs + = cong (λ y → f _ y ∷ scanr xs) (safe-head-≡ (sym eq)) + + unfold-scanr-∷≡ : ∀ xs → let ys = scanr xs in + ∃₂ λ y ys′ → ys ≡ y ∷ ys′ × scanr (x ∷ xs) ≡ f x y ∷ ys + unfold-scanr-∷≡ xs with y , _ , eq ← helper xs = y , _ , eq , refl diff --git a/src/Data/List/Relation/Unary/Null.agda b/src/Data/List/Relation/Unary/Null.agda index 9f60ea7b07..df14ab4c7e 100644 --- a/src/Data/List/Relation/Unary/Null.agda +++ b/src/Data/List/Relation/Unary/Null.agda @@ -10,8 +10,9 @@ module Data.List.Relation.Unary.Null where open import Data.Nat.Base as Nat using (_>_; z-nonNull⁻¹ : (xs : List A) → .{{NonNull xs}} → length xs > 0 >-nonNull⁻¹ (_ ∷ _) = z Date: Fri, 22 Sep 2023 17:41:46 +0100 Subject: [PATCH 08/15] streamlining --- README/Data/List/Relation/Unary/Null.agda | 24 +++++++++-------------- 1 file changed, 9 insertions(+), 15 deletions(-) diff --git a/README/Data/List/Relation/Unary/Null.agda b/README/Data/List/Relation/Unary/Null.agda index 1d5c984ad7..fb334e12ca 100644 --- a/README/Data/List/Relation/Unary/Null.agda +++ b/README/Data/List/Relation/Unary/Null.agda @@ -68,10 +68,8 @@ module ScanRΣ (f : A → B → B) (e : B) where instance scanrNonNull : {xs : List A} → NonNull (scanr xs) scanrNonNull {xs = xs} = proj₂ (scanrΣ xs) - unfold-scanr-∷ : ∀ xs → - let ys = scanr xs in - let instance _ = scanrNonNull {xs = xs} in - scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys + unfold-scanr-∷ : ∀ xs → let instance _ = scanrNonNull {xs = xs} in + scanr (x ∷ xs) ≡ f x (safe-head (scanr xs)) ∷ scanr xs unfold-scanr-∷ xs with ys@(y ∷ _) , _ ← scanrΣ xs = refl module ScanR (f : A → B → B) (e : B) where @@ -96,20 +94,18 @@ module ScanR (f : A → B → B) (e : B) where instance scanrNonNull : {xs : List A} → NonNull (scanr xs) scanrNonNull {xs = xs} with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = _ - unfold-scanr-∷ : ∀ xs → - let ys = scanr xs in - let instance _ = scanrNonNull {xs = xs} in - scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys - unfold-scanr-∷ xs with refine⁺ ys ← scanr⁺ xs in eq with y ∷ _ ← ys = refl + unfold-scanr-∷ : ∀ xs → let instance _ = scanrNonNull {xs = xs} in + scanr (x ∷ xs) ≡ f x (safe-head (scanr xs)) ∷ scanr xs + unfold-scanr-∷ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = refl unfold-scanr-∷≡ : ∀ xs → let ys = scanr xs in ∃₂ λ y ys′ → ys ≡ y ∷ ys′ × scanr (x ∷ xs) ≡ f x y ∷ ys - unfold-scanr-∷≡ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys + unfold-scanr-∷≡ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = y , _ , refl , refl module ScanR′ (f : A → B → B) (e : B) where --- design pattern: refinement types via mutual recursion, using `nonNull-≡` +-- design pattern: refinement types via mutual recursion, using `nonNull-[_]⁻` -- to simulate the refinement type { xs : List A | NonNull xs } -- define two functions by mutual recursion: @@ -131,10 +127,8 @@ module ScanR′ (f : A → B → B) (e : B) where scanrNonNull {xs = []} = _ scanrNonNull {xs = x ∷ xs} with _ ← helper xs = _ - unfold-scanr-∷ : ∀ xs → - let ys = scanr xs in - let instance _ = scanrNonNull {xs = xs} in - scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys + unfold-scanr-∷ : ∀ xs → let instance _ = scanrNonNull {xs = xs} in + scanr (x ∷ xs) ≡ f x (safe-head (scanr xs)) ∷ (scanr xs) unfold-scanr-∷ xs with y , _ , eq ← helper xs = cong (λ y → f _ y ∷ scanr xs) (safe-head-≡ (sym eq)) From 822b42042b44da2798d9be933e106ac51f2288ed Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 23 Sep 2023 08:57:11 +0100 Subject: [PATCH 09/15] renaming, derived notions --- src/Data/Nat/Relation/Unary/Null.agda | 17 ----------------- src/Relation/Unary/Refinement.agda | 12 ++++++++++-- 2 files changed, 10 insertions(+), 19 deletions(-) diff --git a/src/Data/Nat/Relation/Unary/Null.agda b/src/Data/Nat/Relation/Unary/Null.agda index ea9bf2c419..6606e1f618 100644 --- a/src/Data/Nat/Relation/Unary/Null.agda +++ b/src/Data/Nat/Relation/Unary/Null.agda @@ -55,20 +55,3 @@ instance >-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0 >-nonZero⁻¹ (suc n) = z Date: Sat, 23 Sep 2023 08:58:41 +0100 Subject: [PATCH 10/15] pulled redefinitions out into `README` --- README/Data/Nat/Relation/Unary/Null.agda | 30 ++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 README/Data/Nat/Relation/Unary/Null.agda diff --git a/README/Data/Nat/Relation/Unary/Null.agda b/README/Data/Nat/Relation/Unary/Null.agda new file mode 100644 index 0000000000..814d2a1278 --- /dev/null +++ b/README/Data/Nat/Relation/Unary/Null.agda @@ -0,0 +1,30 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Null instance for ℕ +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module README.Data.Nat.Relation.Unary.Null where + +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Nat.Relation.Unary.Null + +------------------------------------------------------------------------ +-- Specimen reimplementation + +open import Agda.Builtin.Nat + using (div-helper; mod-helper) + +-- Division +-- Note properties of these are in `Nat.DivMod` not `Nat.Properties` + +_/_ : (dividend divisor : ℕ) → .{{NonZero divisor}} → ℕ +m / n@(suc n-1) = div-helper 0 n-1 m n-1 + +-- Remainder/modulus +-- Note properties of these are in `Nat.DivMod` not `Nat.Properties` + +_%_ : (dividend divisor : ℕ) → .{{NonZero divisor}} → ℕ +m % n@(suc n-1) = mod-helper 0 n-1 m n-1 From ced12f8c0f89c0785d57ebfdf4febfc297b634b4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 23 Sep 2023 09:02:00 +0100 Subject: [PATCH 11/15] tidying up `List` instances --- README/Data/List/Relation/Unary/Null.agda | 2 ++ src/Data/List/Relation/Unary/Null.agda | 4 +++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/README/Data/List/Relation/Unary/Null.agda b/README/Data/List/Relation/Unary/Null.agda index fb334e12ca..6caac17f1c 100644 --- a/README/Data/List/Relation/Unary/Null.agda +++ b/README/Data/List/Relation/Unary/Null.agda @@ -72,6 +72,7 @@ module ScanRΣ (f : A → B → B) (e : B) where scanr (x ∷ xs) ≡ f x (safe-head (scanr xs)) ∷ scanr xs unfold-scanr-∷ xs with ys@(y ∷ _) , _ ← scanrΣ xs = refl + module ScanR (f : A → B → B) (e : B) where -- design pattern: refinement types via mutual recursion @@ -103,6 +104,7 @@ module ScanR (f : A → B → B) (e : B) where unfold-scanr-∷≡ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _ ← ys = y , _ , refl , refl + module ScanR′ (f : A → B → B) (e : B) where -- design pattern: refinement types via mutual recursion, using `nonNull-[_]⁻` diff --git a/src/Data/List/Relation/Unary/Null.agda b/src/Data/List/Relation/Unary/Null.agda index df14ab4c7e..c48ec2e4b4 100644 --- a/src/Data/List/Relation/Unary/Null.agda +++ b/src/Data/List/Relation/Unary/Null.agda @@ -58,13 +58,15 @@ instance >-nonNull⁻¹ : (xs : List A) → .{{NonNull xs}} → length xs > 0 >-nonNull⁻¹ (_ ∷ _) = z Date: Sat, 23 Sep 2023 09:02:59 +0100 Subject: [PATCH 12/15] added `Decidable` refinements, plus some derived forms --- src/Relation/Unary/Null.agda | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/src/Relation/Unary/Null.agda b/src/Relation/Unary/Null.agda index f6ca232d62..705b1ce819 100644 --- a/src/Relation/Unary/Null.agda +++ b/src/Relation/Unary/Null.agda @@ -9,9 +9,10 @@ module Relation.Unary.Null where open import Data.Bool.Base using (Bool; not; T) +open import Data.Bool.Properties using (T?) open import Function.Base using (_∘_) open import Level -open import Relation.Unary using (Pred) +open import Relation.Unary using (Pred; Decidable) open import Relation.Unary.Refinement private @@ -28,10 +29,23 @@ record Null (A : Set a) : Set a where null : A → Bool - not-null = not ∘ null + non-null = not ∘ null -NonNull : {{Null A}} → Pred A _ -NonNull {{nullA}} = T ∘ not-null where open Null nullA +------------------------------------------------------------------------ +-- Type constructor + +[_]⁺ : (A : Set a) {{nullA : Null A}} → Set a +[ A ]⁺ {{nullA}} = [ x ∈ A |ᵇ non-null x ] where open Null nullA + +------------------------------------------------------------------------ +-- Derived notions + +module _ {{nullA : Null A}} where + + open Null nullA + + NonNull : Pred A _ + NonNull = T ∘ non-null -[_]⁺ : (A : Set a) → {{nA : Null A}} → Set a -[ A ]⁺ {{nullA}} = [ x ∈ A || not-null x ] where open Null nullA + NonNull? : Decidable NonNull + NonNull? = T? ∘ non-null From d4138cd71a2d0d8e1d3f2aa168ba38f90e99d500 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 23 Sep 2023 09:03:31 +0100 Subject: [PATCH 13/15] fix-whitespace --- src/Data/Vec/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 6752ec1b06..ed8817c66e 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -272,7 +272,7 @@ drop m xs = proj₁ (proj₂ (splitAt m xs)) group : ∀ n k (xs : Vec A (n * k)) → ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss group zero k [] = ([] , refl) -group (suc n) k xs = +group (suc n) k xs = let ys , zs , eq-split = splitAt k xs in let zss , eq-group = group n k zs in (ys ∷ zss) , trans eq-split (cong (ys ++_) eq-group) From 0a7b3b599ebe50d4f70e54471f134352648b605a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 23 Sep 2023 09:16:37 +0100 Subject: [PATCH 14/15] updated `CHANGELOG` --- CHANGELOG.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 83dbb5f0bb..c181ef87b7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -988,14 +988,14 @@ Major improvements ### Generalised the definition of `NonZero` from `Data.Nat.Base` to `NonNull` based on: * A new module `Relation.Unary.Refinement` defining a general notion of refinement - of a type wrt a `Bool`-valued predicate. + of a type wrt a `Bool`-valued/`Decidable` predicate. * A new module `Relation.Unary.Null` defining being able to test for `null`ity, based on a `Bool`-valued predicate `null`, using `Refinement`. * Instances `Data.{Nat|List}.Relation.Unary.Null` of `Null` for `Nat` and `List`. -* Example uses in `README.Data.List.Relation.Unary.Null` +* Example uses in `README.Data.{Nat|List}.Relation.Unary.Null` Deprecated modules From f058a1aa1342eccee0e7d8ea852ee9717cfc86e7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 23 Sep 2023 09:28:03 +0100 Subject: [PATCH 15/15] derived property: `nonZero?` --- README/Data/Nat/Relation/Unary/Null.agda | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/README/Data/Nat/Relation/Unary/Null.agda b/README/Data/Nat/Relation/Unary/Null.agda index 814d2a1278..8beedccab6 100644 --- a/README/Data/Nat/Relation/Unary/Null.agda +++ b/README/Data/Nat/Relation/Unary/Null.agda @@ -10,6 +10,15 @@ module README.Data.Nat.Relation.Unary.Null where open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Nat.Relation.Unary.Null +open import Relation.Unary using (Decidable) +open import Relation.Unary.Null + +------------------------------------------------------------------------ +-- Properties of NonZero +------------------------------------------------------------------------ + +nonZero? : Decidable NonZero +nonZero? = NonNull? ------------------------------------------------------------------------ -- Specimen reimplementation