Add properties of Data.Refinement and refactor module structure

CHANGELOG.md

@@ -114,6 +114,12 @@ New modules
 
 * `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
 
+* Refactored `Data.Refinement` into:
+  ```agda
+  Data.Refinement.Base
+  Data.Refinement.Properties
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -336,6 +342,12 @@ Additions to existing modules
   neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q)
   ```
 
+* New properties re-exported from `Data.Refinement`:
+  ```agda
+  value-injective : value v ≡ value w → v ≡ w
+  _≟_             : DecidableEquality A → DecidableEquality [ x ∈ A ∣ P x ]
+ ```
+
 * New lemma in `Data.Vec.Properties`:
   ```agda
   map-concat : map f (concat xss) ≡ concat (map (map f) xss)

src/Data/Refinement.agda

@@ -8,39 +8,13 @@
 
 module Data.Refinement where
 
-open import Level
-open import Data.Irrelevant as Irrelevant using (Irrelevant)
-open import Function.Base
-open import Relation.Unary using (IUniversal; _⇒_; _⊢_)
-
-private
-  variable
-    a b p q : Level
-    A : Set a
-    B : Set b
-
-record Refinement {a p} (A : Set a) (P : A → Set p) : Set (a ⊔ p) where
-  constructor _,_
-  field value : A
-        proof : Irrelevant (P value)
-infixr 4 _,_
-open Refinement public
-
--- The syntax declaration below is meant to mimick set comprehension.
--- It is attached to Refinement-syntax, to make it easy to import
--- Data.Refinement without the special syntax.
-
-infix 2 Refinement-syntax
-Refinement-syntax = Refinement
-syntax Refinement-syntax A (λ x → P) = [ x ∈ A ∣ P ]
-
-module _ {P : A → Set p} {Q : B → Set q} where
+------------------------------------------------------------------------
+-- Publicly re-export the contents of the base module
 
-  map : (f : A → B) → ∀[ P ⇒ f ⊢ Q ] →
-        [ a ∈ A ∣ P a ] → [ b ∈ B ∣ Q b ]
-  map f prf (a , p) = f a , Irrelevant.map prf p
+open import Data.Refinement.Base public
 
-module _ {P : A → Set p} {Q : A → Set q} where
+------------------------------------------------------------------------
+-- Publicly re-export queries
 
-  refine : ∀[ P ⇒ Q ] → [ a ∈ A ∣ P a ] → [ a ∈ A ∣ Q a ]
-  refine = map id
+open import Data.Refinement.Properties public
+  using (value-injective; _≟_)

src/Data/Refinement/Base.agda

@@ -0,0 +1,54 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Refinement type: a value together with a proof irrelevant witness.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Refinement.Base where
+
+open import Level
+open import Data.Irrelevant as Irrelevant using (Irrelevant)
+open import Function.Base
+open import Relation.Unary using (IUniversal; _⇒_; _⊢_)
+
+private
+  variable
+    a b p q : Level
+    A : Set a
+    B : Set b
+    P : A → Set p
+
+
+------------------------------------------------------------------------
+-- Definition
+
+record Refinement (A : Set a) (P : A → Set p) : Set (a ⊔ p) where
+  constructor _,_
+  field value : A
+        proof : Irrelevant (P value)
+infixr 4 _,_
+open Refinement public
+
+-- The syntax declaration below is meant to mimic set comprehension.
+-- It is attached to Refinement-syntax, to make it easy to import
+-- Data.Refinement without the special syntax.
+
+infix 2 Refinement-syntax
+Refinement-syntax = Refinement
+syntax Refinement-syntax A (λ x → P) = [ x ∈ A ∣ P ]
+
+------------------------------------------------------------------------
+-- Basic operations
+
+module _ {Q : B → Set q} where
+
+  map : (f : A → B) → ∀[ P ⇒ f ⊢ Q ] →
+        [ a ∈ A ∣ P a ] → [ b ∈ B ∣ Q b ]
+  map f prf (a , p) = f a , Irrelevant.map prf p
+
+module _ {Q : A → Set q} where
+
+  refine : ∀[ P ⇒ Q ] → [ a ∈ A ∣ P a ] → [ a ∈ A ∣ Q a ]
+  refine = map id

src/Data/Refinement/Properties.agda

@@ -0,0 +1,35 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of refinement types
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Refinement.Properties where
+
+open import Level
+open import Data.Refinement.Base
+open import Relation.Binary.Definitions using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
+import Relation.Nullary.Decidable.Core as Dec
+
+private
+  variable
+    a p : Level
+    A : Set a
+    P : A → Set p
+    v w : [ x ∈ A ∣ P x ]
+
+
+------------------------------------------------------------------------
+-- Basic properties
+
+value-injective : value v ≡ value w → v ≡ w
+value-injective refl = refl
+
+module _ (eq? : DecidableEquality A) where
+
+  infix 4 _≟_
+  _≟_ : DecidableEquality [ x ∈ A ∣ P x ]
+  v ≟ w = Dec.map′ value-injective (cong value) (eq? (value v) (value w))