diff options
author | Sean Whitton <spwhitton@spwhitton.name> | 2018-11-23 17:29:46 -0700 |
---|---|---|
committer | Sean Whitton <spwhitton@spwhitton.name> | 2018-11-23 17:29:46 -0700 |
commit | 5a91775bd7c909bbaf3b3c8ee964136961a5146d (patch) | |
tree | cea89f085c1382f1567ff71a30b6f953708dc6a9 /src/Data/Vec/Any.agda | |
parent | 5d2b156377dce5bdca65b14639306eaed3ac3a92 (diff) | |
parent | a19b25a865b2000bbd3acd909f5951a5407c1eec (diff) |
Merge tag 'upstream/0.17'
Upstream version 0.17
# gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST
# gpg: using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240
# gpg: issuer "spwhitton@spwhitton.name"
# gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate]
# Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4 753F 0F56 D055 3B6D 411B
# Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC 248B 695B 7AE4 BF06 6240
Diffstat (limited to 'src/Data/Vec/Any.agda')
-rw-r--r-- | src/Data/Vec/Any.agda | 79 |
1 files changed, 79 insertions, 0 deletions
diff --git a/src/Data/Vec/Any.agda b/src/Data/Vec/Any.agda new file mode 100644 index 0000000..094bccf --- /dev/null +++ b/src/Data/Vec/Any.agda @@ -0,0 +1,79 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Vectors where at least one element satisfies a given property +------------------------------------------------------------------------ + +module Data.Vec.Any {a} {A : Set a} where + +open import Data.Empty +open import Data.Fin +open import Data.Nat using (zero; suc) +open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) +open import Data.Vec as Vec using (Vec; []; [_]; _∷_) +open import Data.Product as Prod using (∃; _,_) +open import Level using (_⊔_) +open import Relation.Nullary using (¬_; yes; no) +open import Relation.Nullary.Negation using (contradiction) +import Relation.Nullary.Decidable as Dec +open import Relation.Unary + +------------------------------------------------------------------------ +-- Any P xs means that at least one element in xs satisfies P. + +data Any {p} (P : A → Set p) : ∀ {n} → Vec A n → Set (a ⊔ p) where + here : ∀ {n x} {xs : Vec A n} (px : P x) → Any P (x ∷ xs) + there : ∀ {n x} {xs : Vec A n} (pxs : Any P xs) → Any P (x ∷ xs) + +------------------------------------------------------------------------ +-- Operations on Any + +module _ {p} {P : A → Set p} {n x} {xs : Vec A n} where + +-- If the tail does not satisfy the predicate, then the head will. + + head : ¬ Any P xs → Any P (x ∷ xs) → P x + head ¬pxs (here px) = px + head ¬pxs (there pxs) = contradiction pxs ¬pxs + +-- If the head does not satisfy the predicate, then the tail will. + tail : ¬ P x → Any P (x ∷ xs) → Any P xs + tail ¬px (here px) = ⊥-elim (¬px px) + tail ¬px (there pxs) = pxs + +-- Convert back and forth with sum + toSum : Any P (x ∷ xs) → P x ⊎ Any P xs + toSum (here px) = inj₁ px + toSum (there pxs) = inj₂ pxs + + fromSum : P x ⊎ Any P xs → Any P (x ∷ xs) + fromSum = [ here , there ]′ + +map : ∀ {p q} {P : A → Set p} {Q : A → Set q} → + P ⊆ Q → ∀ {n} → Any P {n} ⊆ Any Q {n} +map g (here px) = here (g px) +map g (there pxs) = there (map g pxs) + +index : ∀ {p} {P : A → Set p} {n} {xs : Vec A n} → Any P xs → Fin n +index (here px) = zero +index (there pxs) = suc (index pxs) + +-- If any element satisfies P, then P is satisfied. +satisfied : ∀ {p} {P : A → Set p} {n} {xs : Vec A n} → Any P xs → ∃ P +satisfied (here px) = _ , px +satisfied (there pxs) = satisfied pxs + +------------------------------------------------------------------------ +-- Properties of predicates preserved by Any + +module _ {p} {P : A → Set p} where + + any : Decidable P → ∀ {n} → Decidable (Any P {n}) + any P? [] = no λ() + any P? (x ∷ xs) with P? x + ... | yes px = yes (here px) + ... | no ¬px = Dec.map′ there (tail ¬px) (any P? xs) + + satisfiable : Satisfiable P → ∀ {n} → Satisfiable (Any P {suc n}) + satisfiable (x , p) {zero} = x ∷ [] , here p + satisfiable (x , p) {suc n} = Prod.map (x ∷_) there (satisfiable (x , p)) |