------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors defined by recursion
------------------------------------------------------------------------
-- What is the point of this module? The n-ary products below are
-- intended to be used with a fixed n, in which case the nil constructor
-- can be avoided: pairs are represented as pairs (x , y), not as
-- triples (x , y , unit).
-- Additionally, vectors defined by recursion enjoy η-rules. That is to
-- say that two vectors of known length are definitionally equal
-- whenever their elements are.
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Recursive where
open import Data.Nat.Base as Nat using (ℕ; zero; suc; NonZero; pred)
open import Data.Nat.Properties using (+-comm; *-comm)
open import Data.Empty.Polymorphic using (⊥)
open import Data.Fin.Base as Fin using (Fin; zero; suc)
open import Data.Fin.Properties using (1↔⊤; *↔×)
open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
open import Data.Product.Algebra using (×-cong)
open import Data.Sum.Base as Sum using (_⊎_)
open import Data.Unit.Base using (tt)
open import Data.Unit.Polymorphic.Base using (⊤)
open import Data.Unit.Polymorphic.Properties using (⊤↔⊤*)
open import Data.Vec.Base as Vec using (Vec; _∷_)
open import Function.Base using (_∘′_; _∘_; id; const)
open import Function.Bundles using (_↔_; mk↔ₛ′; mk↔)
open import Function.Properties.Inverse using (↔-isEquivalence; ↔-refl; ↔-sym; ↔-trans)
open import Level using (Level; lift)
open import Relation.Unary using (IUniversal; Universal; _⇒_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Structures using (IsEquivalence)
private
variable
a b c p : Level
A : Set a
B : Set b
C : Set c
------------------------------------------------------------------------
-- Types and patterns
infix 8 _^_
_^_ : Set a → ℕ → Set a
A ^ 0 = ⊤
A ^ 1 = A
A ^ (suc n@(suc _)) = A × A ^ n
pattern [] = lift tt
infix 3 _∈[_]_
_∈[_]_ : {A : Set a} → A → ∀ n → A ^ n → Set a
a ∈[ 0 ] as = ⊥
a ∈[ 1 ] a′ = a ≡ a′
a ∈[ suc n@(suc _) ] a′ , as = a ≡ a′ ⊎ a ∈[ n ] as
------------------------------------------------------------------------
-- Basic operations
cons : ∀ n → A → A ^ n → A ^ suc n
cons 0 a _ = a
cons (suc n) a as = a , as
uncons : ∀ n → A ^ suc n → A × A ^ n
uncons 0 a = a , lift tt
uncons (suc n) (a , as) = a , as
head : ∀ n → A ^ suc n → A
head n as = proj₁ (uncons n as)
tail : ∀ n → A ^ suc n → A ^ n
tail n as = proj₂ (uncons n as)
fromVec : ∀[ Vec A ⇒ (A ^_) ]
fromVec = Vec.foldr (_ ^_) (cons _) _
toVec : Π[ (A ^_) ⇒ Vec A ]
toVec 0 as = Vec.[]
toVec (suc n) as = head n as ∷ toVec n (tail n as)
lookup : ∀ {n} → A ^ n → Fin n → A
lookup as (zero {n}) = head n as
lookup as (suc {n} k) = lookup (tail n as) k
replicate : ∀ n → A → A ^ n
replicate n a = fromVec (Vec.replicate n a)
tabulate : ∀ n → (Fin n → A) → A ^ n
tabulate n f = fromVec (Vec.tabulate f)
append : ∀ m n → A ^ m → A ^ n → A ^ (m Nat.+ n)
append 0 n xs ys = ys
append 1 n x ys = cons n x ys
append (suc m@(suc _)) n (x , xs) ys = x , append m n xs ys
splitAt : ∀ m n → A ^ (m Nat.+ n) → A ^ m × A ^ n
splitAt 0 n xs = [] , xs
splitAt (suc m) n xs =
let (ys , zs) = splitAt m n (tail (m Nat.+ n) xs) in
cons m (head (m Nat.+ n) xs) ys , zs
------------------------------------------------------------------------
-- Manipulating N-ary products
map : (A → B) → ∀ n → A ^ n → B ^ n
map f 0 as = lift tt
map f 1 a = f a
map f (suc n@(suc _)) (a , as) = f a , map f n as
ap : ∀ n → (A → B) ^ n → A ^ n → B ^ n
ap 0 fs ts = []
ap 1 f t = f t
ap (suc n@(suc _)) (f , fs) (t , ts) = f t , ap n fs ts
module _ {P : ℕ → Set p} where
foldr : P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (suc (suc n))) →
∀ n → A ^ n → P n
foldr p0 p1 p2+ 0 as = p0
foldr p0 p1 p2+ 1 a = p1 a
foldr p0 p1 p2+ (suc n′@(suc n)) (a , as) = p2+ n a (foldr p0 p1 p2+ n′ as)
foldl : (P : ℕ → Set p) →
P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (suc (suc n))) →
∀ n → A ^ n → P n
foldl P p0 p1 p2+ 0 as = p0
foldl P p0 p1 p2+ 1 a = p1 a
foldl P p0 p1 p2+ (suc n@(suc _)) (a , as) = let p1′ = p1 a in
foldl (P ∘′ suc) p1′ (λ a → p2+ 0 a p1′) (p2+ ∘ suc) n as
reverse : ∀ n → A ^ n → A ^ n
reverse = foldl (_ ^_) [] id (λ n → _,_)
zipWith : (A → B → C) → ∀ n → A ^ n → B ^ n → C ^ n
zipWith f 0 as bs = []
zipWith f 1 a b = f a b
zipWith f ((suc n@(suc _))) (a , as) (b , bs) = f a b , zipWith f n as bs
unzipWith : (A → B × C) → ∀ n → A ^ n → B ^ n × C ^ n
unzipWith f 0 as = [] , []
unzipWith f 1 a = f a
unzipWith f (suc n@(suc _)) (a , as) = Product.zip _,_ _,_ (f a) (unzipWith f n as)
zip : ∀ n → A ^ n → B ^ n → (A × B) ^ n
zip = zipWith _,_
unzip : ∀ n → (A × B) ^ n → A ^ n × B ^ n
unzip = unzipWith id
lift↔ : ∀ n → A ↔ B → A ^ n ↔ B ^ n
lift↔ 0 A↔B = mk↔ₛ′ _ _ (const refl) (const refl)
lift↔ 1 A↔B = A↔B
lift↔ (suc n@(suc _)) A↔B = ×-cong A↔B (lift↔ n A↔B)
Fin[m^n]↔Fin[m]^n : ∀ m n → Fin (m Nat.^ n) ↔ Fin m ^ n
Fin[m^n]↔Fin[m]^n m 0 = ↔-trans 1↔⊤ (↔-sym ⊤↔⊤*)
Fin[m^n]↔Fin[m]^n m 1 = subst (λ x → Fin x ↔ Fin m)
(trans (sym (+-comm m zero)) (*-comm 1 m)) ↔-refl
Fin[m^n]↔Fin[m]^n m (suc (suc n)) = ↔-trans (*↔× {m = m}) (×-cong ↔-refl (Fin[m^n]↔Fin[m]^n _ _))
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4