Add Data.Vec.Relation.Unary.AllPairs (#1257)

Author: umazalakain

CHANGELOG.md

@@ -172,6 +172,20 @@ New modules
   Text.Printf.Generic
   ```
 
+* A predicate for vectors in which every pair of elements is related.
+  ```
+  Data.Vec.Relation.Unary.AllPairs
+  Data.Vec.Relation.Unary.AllPairs.Properties
+  ```
+
+* A predicate for vectors in which every element is unique.
+  ```
+  Data.Vec.Relation.Unary.Unique.Propositional
+  Data.Vec.Relation.Unary.Unique.Propositional.Properties
+  Data.Vec.Relation.Unary.Unique.Setoid
+  Data.Vec.Relation.Unary.Unique.Setoid.Properties
+  ```
+
 Other major changes
 -------------------
 
@@ -455,6 +469,7 @@ Other minor additions
 * Added new proofs to `Data.Vec.Properties`:
   ```agda
   unfold-take : ∀ n {m} x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x ∷ take n xs
+  unfold-drop : ∀ n {m} x (xs : Vec A (n + m)) → drop (suc n) (x ∷ xs) ≡ drop n xs
   lookup-inject≤-take : ∀ m {n} (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
                         lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
   ```
@@ -477,6 +492,15 @@ Other minor additions
   transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n
   ```
 
+* Added new proofs to `Data.Vec.Relation.Unary.All.Properties`:
+  ```agda
+  All-swap : ∀ {xs ys} → All (λ x → All (x ~_) ys) xs → All (λ y → All (_~ y) xs) ys
+  tabulate⁺ : ∀ {f : Fin n → A} → (∀ i → P (f i)) → All P (tabulate f)
+  tabulate⁻ : ∀ {f : Fin n → A} → All P (tabulate f) → (∀ i → P (f i))
+  drop⁺ : ∀ {n} m {xs} → All P {m + n} xs → All P {n} (drop m xs)
+  take⁺ : ∀ {n} m {xs} → All P {m + n} xs → All P {m} (take m xs)
+  ```
+
 Refactorings
 ------------
 

src/Data/Vec/Properties.agda

@@ -76,6 +76,13 @@ unfold-take : ∀ n {m} x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x
 unfold-take n x xs with splitAt n xs
 unfold-take n x .(xs ++ ys) | xs , ys , refl = refl
 
+------------------------------------------------------------------------
+-- drop
+
+unfold-drop : ∀ n {m} x (xs : Vec A (n + m)) → drop (suc n) (x ∷ xs) ≡ drop n xs
+unfold-drop n x xs with splitAt n xs
+unfold-drop n x .(xs ++ ys) | xs , ys , refl = refl
+
 ------------------------------------------------------------------------
 -- lookup
 

src/Data/Vec/Relation/Unary/All/Properties.agda

@@ -8,15 +8,19 @@
 
 module Data.Vec.Relation.Unary.All.Properties where
 
+open import Data.Nat.Base using (zero; suc; _+_)
+open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.Relation.Unary.All as List using ([]; _∷_)
 open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
 open import Data.Vec.Base as Vec
+import Data.Vec.Properties as Vecₚ
 open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
 open import Level using (Level)
 open import Function.Base using (_∘_; id)
 open import Function.Inverse using (_↔_; inverse)
 open import Relation.Unary using (Pred) renaming (_⊆_ to _⋐_)
+open import Relation.Binary as B using (REL)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; cong; cong₂; →-to-⟶)
 
@@ -102,6 +106,51 @@ module _ {m} {P : Pred A p} where
   concat⁻ []         []   = []
   concat⁻ (xs ∷ xss) pxss = ++ˡ⁻ xs pxss ∷ concat⁻ xss (++ʳ⁻ xs pxss)
 
+------------------------------------------------------------------------
+-- swap
+
+module _ {_~_ : REL A B p} where
+
+  All-swap : ∀ {n m xs ys} →
+             All (λ x → All (x ~_) ys) {n} xs →
+             All (λ y → All (_~ y) xs) {m} ys
+  All-swap {ys = []}     _   = []
+  All-swap {ys = y ∷ ys} []  = All.universal (λ _ → []) (y ∷ ys)
+  All-swap {ys = y ∷ ys} ((x~y ∷ x~ys) ∷ pxs) =
+    (x~y ∷ (All.map All.head pxs)) ∷
+    All-swap (x~ys ∷ (All.map All.tail pxs))
+
+
+------------------------------------------------------------------------
+-- tabulate
+
+module _ {P : A → Set p} where
+
+  tabulate⁺ : ∀ {n} {f : Fin n → A} →
+              (∀ i → P (f i)) → All P (tabulate f)
+  tabulate⁺ {zero}  Pf = []
+  tabulate⁺ {suc n} Pf = Pf zero ∷ tabulate⁺ (Pf ∘ suc)
+
+  tabulate⁻ : ∀ {n} {f : Fin n → A} →
+              All P (tabulate f) → (∀ i → P (f i))
+  tabulate⁻ {suc n} (px ∷ _) zero    = px
+  tabulate⁻ {suc n} (_ ∷ pf) (suc i) = tabulate⁻ pf i
+
+------------------------------------------------------------------------
+-- take and drop
+
+module _ {P : A → Set p} where
+
+  drop⁺ : ∀ {n} m {xs} → All P {m + n} xs → All P {n} (drop m xs)
+  drop⁺ zero pxs = pxs
+  drop⁺ (suc m) {x ∷ xs} (px ∷ pxs)
+    rewrite Vecₚ.unfold-drop m x xs = drop⁺ m pxs
+
+  take⁺ : ∀ {n} m {xs} → All P {m + n} xs → All P {m} (take m xs)
+  take⁺ zero pxs = []
+  take⁺ (suc m) {x ∷ xs} (px ∷ pxs)
+    rewrite Vecₚ.unfold-take m x xs = px ∷ take⁺ m pxs
+
 ------------------------------------------------------------------------
 -- toList
 

src/Data/Vec/Relation/Unary/AllPairs.agda

@@ -0,0 +1,82 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Vectors where every pair of elements are related (symmetrically)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Rel)
+
+module Data.Vec.Relation.Unary.AllPairs
+       {a ℓ} {A : Set a} {R : Rel A ℓ} where
+
+open import Data.Vec.Base using (Vec; []; _∷_)
+open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.Product as Prod using (_,_; _×_; uncurry; <_,_>)
+open import Function using (id; _∘_)
+open import Level using (_⊔_)
+open import Relation.Binary as B using (Rel; _⇒_)
+open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
+open import Relation.Nullary using (yes; no)
+import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Product using (_×-dec_)
+
+------------------------------------------------------------------------
+-- Definition
+
+open import Data.Vec.Relation.Unary.AllPairs.Core public
+
+------------------------------------------------------------------------
+-- Operations
+
+head : ∀ {x n} {xs : Vec A n} → AllPairs R (x ∷ xs) → All (R x) xs
+head (px ∷ pxs) = px
+
+tail : ∀ {x n} {xs : Vec A n} → AllPairs R (x ∷ xs) → AllPairs R xs
+tail (px ∷ pxs) = pxs
+
+uncons : ∀ {x n} {xs : Vec A n} → AllPairs R (x ∷ xs) → All (R x) xs × AllPairs R xs
+uncons = < head , tail >
+
+module _ {s} {S : Rel A s} where
+
+  map : ∀ {n} → R ⇒ S → AllPairs R {n} ⊆ AllPairs S {n}
+  map ~₁⇒~₂ [] = []
+  map ~₁⇒~₂ (x~xs ∷ pxs) = All.map ~₁⇒~₂ x~xs ∷ (map ~₁⇒~₂ pxs)
+
+module _ {s t} {S : Rel A s} {T : Rel A t} where
+
+  zipWith : ∀ {n} → R ∩ᵇ S ⇒ T → AllPairs R {n} ∩ᵘ AllPairs S {n} ⊆ AllPairs T {n}
+  zipWith f ([] , [])             = []
+  zipWith f (px ∷ pxs , qx ∷ qxs) = All.map f (All.zip (px , qx)) ∷ zipWith f (pxs , qxs)
+
+  unzipWith : ∀ {n} → T ⇒ R ∩ᵇ S → AllPairs T {n} ⊆ AllPairs R {n} ∩ᵘ AllPairs S {n}
+  unzipWith f []         = [] , []
+  unzipWith f (rx ∷ rxs) = Prod.zip _∷_ _∷_ (All.unzip (All.map f rx)) (unzipWith f rxs)
+
+module _ {s} {S : Rel A s} where
+
+  zip : ∀ {n} → AllPairs R {n} ∩ᵘ AllPairs S {n} ⊆ AllPairs (R ∩ᵇ S) {n}
+  zip = zipWith id
+
+  unzip : ∀ {n} → AllPairs (R ∩ᵇ S) {n} ⊆ AllPairs R {n} ∩ᵘ AllPairs S {n}
+  unzip = unzipWith id
+
+------------------------------------------------------------------------
+-- Properties of predicates preserved by AllPairs
+
+allPairs? : ∀ {n} → B.Decidable R → U.Decidable (AllPairs R {n})
+allPairs? R? []       = yes []
+allPairs? R? (x ∷ xs) =
+  Dec.map′ (uncurry _∷_) uncons (All.all (R? x) xs ×-dec allPairs? R? xs)
+
+irrelevant : ∀ {n} → B.Irrelevant R → U.Irrelevant (AllPairs R {n})
+irrelevant irr []           []           = refl
+irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
+  cong₂ _∷_ (All.irrelevant irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)
+
+satisfiable : U.Satisfiable (AllPairs R)
+satisfiable = [] , []

src/Data/Vec/Relation/Unary/AllPairs/Core.agda

@@ -0,0 +1,34 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Vectors where every pair of elements are related (symmetrically)
+------------------------------------------------------------------------
+
+-- Core modules are not meant to be used directly outside of the
+-- standard library.
+
+-- This module should be removable if and when Agda issue
+-- https://github.com/agda/agda/issues/3210 is fixed
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Rel)
+
+module Data.Vec.Relation.Unary.AllPairs.Core
+  {a ℓ} {A : Set a} (R : Rel A ℓ) where
+
+open import Level
+open import Data.Vec.Base
+open import Data.Vec.Relation.Unary.All
+
+------------------------------------------------------------------------
+-- Definition
+
+-- AllPairs R xs means that every pair of elements (x , y) in xs is a
+-- member of relation R (as long as x comes before y in the vector).
+
+infixr 5 _∷_
+
+data AllPairs : ∀ {n} → Vec A n → Set (a ⊔ ℓ) where
+  []  : AllPairs []
+  _∷_ : ∀ {n x} {xs : Vec A n} → All (R x) xs → AllPairs xs → AllPairs (x ∷ xs)

src/Data/Vec/Relation/Unary/AllPairs/Properties.agda

@@ -0,0 +1,91 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties related to AllPairs
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Vec.Relation.Unary.AllPairs.Properties where
+
+open import Data.Vec
+import Data.Vec.Properties as Vecₚ
+open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
+import Data.Vec.Relation.Unary.All.Properties as Allₚ
+open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
+open import Data.Bool.Base using (true; false)
+open import Data.Fin.Base using (Fin)
+open import Data.Fin.Properties using (suc-injective)
+open import Data.Nat.Base using (zero; suc; _+_)
+open import Function using (_∘_)
+open import Level using (Level)
+open import Relation.Binary using (Rel)
+open import Relation.Binary.PropositionalEquality using (_≢_)
+
+private
+  variable
+    a b c p ℓ : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Introduction (⁺) and elimination (⁻) rules for vector operations
+------------------------------------------------------------------------
+-- map
+
+module _ {R : Rel A ℓ} {f : B → A} where
+
+  map⁺ : ∀ {n xs} → AllPairs (λ x y → R (f x) (f y)) {n} xs →
+         AllPairs R {n} (map f xs)
+  map⁺ []           = []
+  map⁺ (x∉xs ∷ xs!) = Allₚ.map⁺ x∉xs ∷ map⁺ xs!
+
+------------------------------------------------------------------------
+-- ++
+
+module _ {R : Rel A ℓ} where
+
+  ++⁺ : ∀ {n m xs ys} → AllPairs R {n} xs → AllPairs R {m} ys →
+        All (λ x → All (R x) ys) xs → AllPairs R (xs ++ ys)
+  ++⁺ []         Rys _              = Rys
+  ++⁺ (px ∷ Rxs) Rys (Rxys ∷ Rxsys) = Allₚ.++⁺ px Rxys ∷ ++⁺ Rxs Rys Rxsys
+
+------------------------------------------------------------------------
+-- concat
+
+module _ {R : Rel A ℓ} where
+
+  concat⁺ : ∀ {n m xss} → All (AllPairs R {n}) {m} xss →
+            AllPairs (λ xs ys → All (λ x → All (R x) ys) xs) xss →
+            AllPairs R (concat xss)
+  concat⁺ []           []              = []
+  concat⁺ (pxs ∷ pxss) (Rxsxss ∷ Rxss) = ++⁺ pxs (concat⁺ pxss Rxss)
+    (All.map Allₚ.concat⁺ (Allₚ.All-swap Rxsxss))
+
+------------------------------------------------------------------------
+-- take and drop
+
+module _ {R : Rel A ℓ} where
+
+  take⁺ : ∀ {n} m {xs} → AllPairs R {m + n} xs → AllPairs R {m} (take m xs)
+  take⁺ zero pxs = []
+  take⁺ (suc m) {x ∷ xs} (px ∷ pxs)
+    rewrite Vecₚ.unfold-take m x xs = Allₚ.take⁺ m px ∷ take⁺ m pxs
+
+  drop⁺ : ∀ {n} m {xs} → AllPairs R {m + n} xs → AllPairs R {n} (drop m xs)
+  drop⁺ zero pxs = pxs
+  drop⁺ (suc m) {x ∷ xs} (_ ∷ pxs)
+    rewrite Vecₚ.unfold-drop m x xs = drop⁺ m pxs
+
+------------------------------------------------------------------------
+-- tabulate
+
+module _ {R : Rel A ℓ} where
+
+  tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → i ≢ j → R (f i) (f j)) →
+              AllPairs R (tabulate f)
+  tabulate⁺ {zero}  fᵢ~fⱼ = []
+  tabulate⁺ {suc n} fᵢ~fⱼ =
+    Allₚ.tabulate⁺ (λ j → fᵢ~fⱼ λ()) ∷
+    tabulate⁺ (fᵢ~fⱼ ∘ (_∘ suc-injective))

src/Data/Vec/Relation/Unary/Unique/Propositional.agda

@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Vectors made up entirely of unique elements (propositional equality)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Vec.Relation.Unary.Unique.Propositional {a} {A : Set a} where
+
+open import Relation.Binary.PropositionalEquality using (setoid)
+open import Data.Vec.Relation.Unary.Unique.Setoid as SetoidUnique
+
+------------------------------------------------------------------------
+-- Re-export the contents of setoid uniqueness
+
+open SetoidUnique (setoid A) public
+