diff options
Diffstat (limited to 'src/Codata')
34 files changed, 2712 insertions, 0 deletions
diff --git a/src/Codata/Cofin.agda b/src/Codata/Cofin.agda new file mode 100644 index 0000000..61afc8d --- /dev/null +++ b/src/Codata/Cofin.agda @@ -0,0 +1,65 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- "Finite" sets indexed on coinductive "natural" numbers +------------------------------------------------------------------------ + +module Codata.Cofin where + +open import Size +open import Codata.Thunk +open import Codata.Conat as Conat using (Conat; zero; suc; infinity; _ℕ<_; sℕ≤s; _ℕ≤infinity) +open import Codata.Conat.Bisimilarity as Bisim using (_⊢_≲_ ; s≲s) +open import Data.Nat +open import Data.Fin as Fin hiding (fromℕ; fromℕ≤; toℕ) +open import Function +open import Relation.Binary.PropositionalEquality + +------------------------------------------------------------------------ +-- The type + +-- Note that `Cofin infnity` is /not/ finite. Note also that this is not a +-- coinductive type, but it is indexed on a coinductive type. + +data Cofin : Conat ∞ → Set where + zero : ∀ {n} → Cofin (suc n) + suc : ∀ {n} → Cofin (n .force) → Cofin (suc n) + +suc-injective : ∀ {n} {p q : Cofin (n .force)} → + (Cofin (suc n) ∋ suc p) ≡ suc q → p ≡ q +suc-injective refl = refl + +------------------------------------------------------------------------ +-- Some operations + +fromℕ< : ∀ {n k} → k ℕ< n → Cofin n +fromℕ< {zero} () +fromℕ< {suc n} {zero} (sℕ≤s p) = zero +fromℕ< {suc n} {suc k} (sℕ≤s p) = suc (fromℕ< p) + +fromℕ : ℕ → Cofin infinity +fromℕ k = fromℕ< (suc k ℕ≤infinity) + +toℕ : ∀ {n} → Cofin n → ℕ +toℕ zero = zero +toℕ (suc i) = suc (toℕ i) + +fromFin : ∀ {n} → Fin n → Cofin (Conat.fromℕ n) +fromFin zero = zero +fromFin (suc i) = suc (fromFin i) + +toFin : ∀ n → Cofin (Conat.fromℕ n) → Fin n +toFin zero () +toFin (suc n) zero = zero +toFin (suc n) (suc i) = suc (toFin n i) + +open import Codata.Musical.Notation using (♭; ♯_) +import Codata.Musical.Cofin as M + +fromMusical : ∀ {n} → M.Cofin n → Cofin (Conat.fromMusical n) +fromMusical M.zero = zero +fromMusical (M.suc n) = suc (fromMusical n) + +toMusical : ∀ {n} → Cofin n → M.Cofin (Conat.toMusical n) +toMusical zero = M.zero +toMusical (suc n) = M.suc (toMusical n) diff --git a/src/Codata/Cofin/Literals.agda b/src/Codata/Cofin/Literals.agda new file mode 100644 index 0000000..734f56c --- /dev/null +++ b/src/Codata/Cofin/Literals.agda @@ -0,0 +1,21 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Conat Literals +------------------------------------------------------------------------ + +module Codata.Cofin.Literals where + +open import Data.Nat +open import Agda.Builtin.FromNat +open import Codata.Conat +open import Codata.Conat.Properties +open import Codata.Cofin +open import Relation.Nullary.Decidable + +number : ∀ n → Number (Cofin n) +number n = record + { Constraint = λ k → True (suc k ℕ≤? n) + ; fromNat = λ n {{p}} → fromℕ< (toWitness p) + } + diff --git a/src/Codata/Colist.agda b/src/Codata/Colist.agda new file mode 100644 index 0000000..08f190f --- /dev/null +++ b/src/Codata/Colist.agda @@ -0,0 +1,127 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The Colist type and some operations +------------------------------------------------------------------------ + +module Codata.Colist where + +open import Size +open import Data.Nat.Base +open import Data.Product using (_×_ ; _,_) +open import Data.These using (These; this; that; these) +open import Data.Maybe using (Maybe; nothing; just) +open import Data.List.Base using (List; []; _∷_) +open import Data.List.NonEmpty using (List⁺; _∷_) +open import Data.BoundedVec as BVec using (BoundedVec) +open import Function + +open import Codata.Thunk using (Thunk; force) +open import Codata.Conat as Conat using (Conat ; zero ; suc) +open import Codata.Delay as Delay using (Delay ; now ; later) +open import Codata.Stream using (Stream ; _∷_) + +data Colist {ℓ} (A : Set ℓ) (i : Size) : Set ℓ where + [] : Colist A i + _∷_ : A → Thunk (Colist A) i → Colist A i + +module _ {ℓ} {A : Set ℓ} where + + length : ∀ {i} → Colist A i → Conat i + length [] = zero + length (x ∷ xs) = suc λ where .force → length (xs .force) + + replicate : ∀ {i} → Conat i → A → Colist A i + replicate zero a = [] + replicate (suc n) a = a ∷ λ where .force → replicate (n .force) a + + infixr 5 _++_ _⁺++_ + _++_ : ∀ {i} → Colist A i → Colist A i → Colist A i + [] ++ ys = ys + (x ∷ xs) ++ ys = x ∷ λ where .force → xs .force ++ ys + + lookup : ℕ → Colist A ∞ → Maybe A + lookup n [] = nothing + lookup zero (a ∷ as) = just a + lookup (suc n) (a ∷ as) = lookup n (as .force) + + colookup : ∀ {i} → Conat i → Colist A i → Delay (Maybe A) i + colookup n [] = now nothing + colookup zero (a ∷ as) = now (just a) + colookup (suc n) (a ∷ as) = + later λ where .force → colookup (n .force) (as .force) + + take : ∀ (n : ℕ) → Colist A ∞ → BoundedVec A n + take zero xs = BVec.[] + take n [] = BVec.[] + take (suc n) (x ∷ xs) = x BVec.∷ take n (xs .force) + + cotake : ∀ {i} → Conat i → Stream A i → Colist A i + cotake zero xs = [] + cotake (suc n) (x ∷ xs) = x ∷ λ where .force → cotake (n .force) (xs .force) + + fromList : List A → Colist A ∞ + fromList [] = [] + fromList (x ∷ xs) = x ∷ λ where .force → fromList xs + + _⁺++_ : ∀ {i} → List⁺ A → Thunk (Colist A) i → Colist A i + (x ∷ xs) ⁺++ ys = x ∷ λ where .force → fromList xs ++ ys .force + + fromStream : ∀ {i} → Stream A i → Colist A i + fromStream = cotake Conat.infinity + +module _ {a b} {A : Set a} {B : Set b} where + + map : ∀ {i} (f : A → B) → Colist A i → Colist B i + map f [] = [] + map f (a ∷ as) = f a ∷ λ where .force → map f (as .force) + + unfold : ∀ {i} → (A → Maybe (A × B)) → A → Colist B i + unfold next seed with next seed + ... | nothing = [] + ... | just (seed′ , b) = b ∷ λ where .force → unfold next seed′ + + scanl : ∀ {i} → (B → A → B) → B → Colist A i → Colist B i + scanl c n [] = n ∷ λ where .force → [] + scanl c n (a ∷ as) = n ∷ λ where .force → scanl c (c n a) (as .force) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where + + alignWith : ∀ {i} → (These A B → C) → Colist A i → Colist B i → Colist C i + alignWith f [] bs = map (f ∘′ that) bs + alignWith f as@(_ ∷ _) [] = map (f ∘′ this) as + alignWith f (a ∷ as) (b ∷ bs) = + f (these a b) ∷ λ where .force → alignWith f (as .force) (bs .force) + + zipWith : ∀ {i} → (A → B → C) → Colist A i → Colist B i → Colist C i + zipWith f [] bs = [] + zipWith f as [] = [] + zipWith f (a ∷ as) (b ∷ bs) = + f a b ∷ λ where .force → zipWith f (as .force) (bs .force) + +module _ {a b} {A : Set a} {B : Set b} where + + align : ∀ {i} → Colist A i → Colist B i → Colist (These A B) i + align = alignWith id + + zip : ∀ {i} → Colist A i → Colist B i → Colist (A × B) i + zip = zipWith _,_ + + ap : ∀ {i} → Colist (A → B) i → Colist A i → Colist B i + ap = zipWith _$′_ + +------------------------------------------------------------------------ +-- Legacy + +open import Codata.Musical.Notation using (♭; ♯_) +import Codata.Musical.Colist as M + +module _ {a} {A : Set a} where + + fromMusical : ∀ {i} → M.Colist A → Colist A i + fromMusical M.[] = [] + fromMusical (x M.∷ xs) = x ∷ λ where .force → fromMusical (♭ xs) + + toMusical : Colist A ∞ → M.Colist A + toMusical [] = M.[] + toMusical (x ∷ xs) = x M.∷ ♯ toMusical (xs .force) diff --git a/src/Codata/Colist/Bisimilarity.agda b/src/Codata/Colist/Bisimilarity.agda new file mode 100644 index 0000000..470a671 --- /dev/null +++ b/src/Codata/Colist/Bisimilarity.agda @@ -0,0 +1,59 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bisimilarity for Colists +------------------------------------------------------------------------ + +module Codata.Colist.Bisimilarity where + +open import Level using (_⊔_) +open import Size +open import Codata.Thunk +open import Codata.Colist +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as Eq using (_≡_) + +data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) : + (xs : Colist A ∞) (ys : Colist B ∞) → Set (r ⊔ a ⊔ b) where + [] : Bisim R i [] [] + _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R) i xs ys → Bisim R i (x ∷ xs) (y ∷ ys) + + +module _ {a r} {A : Set a} {R : A → A → Set r} where + + reflexive : Reflexive R → ∀ {i} → Reflexive (Bisim R i) + reflexive refl^R {i} {[]} = [] + reflexive refl^R {i} {r ∷ rs} = refl^R ∷ λ where .force → reflexive refl^R + +module _ {a b} {A : Set a} {B : Set b} + {r} {P : A → B → Set r} {Q : B → A → Set r} where + + symmetric : Sym P Q → ∀ {i} → Sym (Bisim P i) (Bisim Q i) + symmetric sym^PQ [] = [] + symmetric sym^PQ (p ∷ ps) = sym^PQ p ∷ λ where .force → symmetric sym^PQ (ps .force) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} + {r} {P : A → B → Set r} {Q : B → C → Set r} {R : A → C → Set r} where + + transitive : Trans P Q R → ∀ {i} → Trans (Bisim P i) (Bisim Q i) (Bisim R i) + transitive trans^PQR [] [] = [] + transitive trans^PQR (p ∷ ps) (q ∷ qs) = + trans^PQR p q ∷ λ where .force → transitive trans^PQR (ps .force) (qs .force) + +-- Pointwise Equality as a Bisimilarity +------------------------------------------------------------------------ + +module _ {ℓ} {A : Set ℓ} where + + infix 1 _⊢_≈_ + _⊢_≈_ : ∀ i → Colist A ∞ → Colist A ∞ → Set ℓ + _⊢_≈_ = Bisim _≡_ + + refl : ∀ {i} → Reflexive (i ⊢_≈_) + refl = reflexive Eq.refl + + sym : ∀ {i} → Symmetric (i ⊢_≈_) + sym = symmetric Eq.sym + + trans : ∀ {i} → Transitive (i ⊢_≈_) + trans = transitive Eq.trans diff --git a/src/Codata/Colist/Categorical.agda b/src/Codata/Colist/Categorical.agda new file mode 100644 index 0000000..b15283c --- /dev/null +++ b/src/Codata/Colist/Categorical.agda @@ -0,0 +1,21 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A categorical view of Colist +------------------------------------------------------------------------ + +module Codata.Colist.Categorical where + +open import Codata.Conat using (infinity) +open import Codata.Colist +open import Category.Functor +open import Category.Applicative + +functor : ∀ {ℓ i} → RawFunctor {ℓ} (λ A → Colist A i) +functor = record { _<$>_ = map } + +applicative : ∀ {ℓ i} → RawApplicative {ℓ} (λ A → Colist A i) +applicative = record + { pure = replicate infinity + ; _⊛_ = ap + } diff --git a/src/Codata/Colist/Properties.agda b/src/Codata/Colist/Properties.agda new file mode 100644 index 0000000..d96c303 --- /dev/null +++ b/src/Codata/Colist/Properties.agda @@ -0,0 +1,30 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of operations on the Colist type +------------------------------------------------------------------------ + +module Codata.Colist.Properties where + +open import Size +open import Codata.Thunk using (Thunk; force) +open import Codata.Conat +open import Codata.Colist +open import Codata.Colist.Bisimilarity +open import Function +open import Relation.Binary.PropositionalEquality as Eq + +-- Functor laws + +module _ {a} {A : Set a} where + + map-identity : ∀ (as : Colist A ∞) {i} → i ⊢ map id as ≈ as + map-identity [] = [] + map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where + + map-map-fusion : ∀ (f : A → B) (g : B → C) as {i} → i ⊢ map g (map f as) ≈ map (g ∘ f) as + map-map-fusion f g [] = [] + map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force) + diff --git a/src/Codata/Conat.agda b/src/Codata/Conat.agda new file mode 100644 index 0000000..dc72829 --- /dev/null +++ b/src/Codata/Conat.agda @@ -0,0 +1,115 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The Conat type and some operations +------------------------------------------------------------------------ + +module Codata.Conat where + +open import Size +open import Codata.Thunk + +open import Data.Nat.Base using (ℕ ; zero ; suc) +open import Relation.Nullary + +------------------------------------------------------------------------ +-- Definition and first values + +data Conat (i : Size) : Set where + zero : Conat i + suc : Thunk Conat i → Conat i + +infinity : ∀ {i} → Conat i +infinity = suc λ where .force → infinity + +fromℕ : ℕ → Conat ∞ +fromℕ zero = zero +fromℕ (suc n) = suc λ where .force → fromℕ n + +------------------------------------------------------------------------ +-- Arithmetic operations + +pred : ∀ {i} {j : Size< i} → Conat i → Conat j +pred zero = zero +pred (suc n) = n .force + +infixl 6 _∸_ _+_ +infixl 7 _*_ + +_∸_ : Conat ∞ → ℕ → Conat ∞ +m ∸ zero = m +m ∸ suc n = pred m ∸ n + +_ℕ+_ : ℕ → ∀ {i} → Conat i → Conat i +zero ℕ+ n = n +suc m ℕ+ n = suc λ where .force → m ℕ+ n + +_+ℕ_ : ∀ {i} → Conat i → ℕ → Conat i +zero +ℕ n = fromℕ n +suc m +ℕ n = suc λ where .force → (m .force) +ℕ n + +_+_ : ∀ {i} → Conat i → Conat i → Conat i +zero + n = n +suc m + n = suc λ where .force → (m .force) + n + +_*_ : ∀ {i} → Conat i → Conat i → Conat i +m * zero = zero +zero * n = zero +suc m * suc n = suc λ where .force → n .force + (m .force * suc n) + +-- Max and Min + +infixl 6 _⊔_ +infixl 7 _⊓_ + +_⊔_ : ∀ {i} → Conat i → Conat i → Conat i +zero ⊔ n = n +m ⊔ zero = m +suc m ⊔ suc n = suc λ where .force → m .force ⊔ n .force + +_⊓_ : ∀ {i} → Conat i → Conat i → Conat i +zero ⊓ n = zero +m ⊓ zero = zero +suc m ⊓ suc n = suc λ where .force → m .force ⊔ n .force + +------------------------------------------------------------------------ +-- Finiteness + +data Finite : Conat ∞ → Set where + zero : Finite zero + suc : ∀ {n} → Finite (n .force) → Finite (suc n) + +toℕ : ∀ {n} → Finite n → ℕ +toℕ zero = zero +toℕ (suc n) = suc (toℕ n) + +¬Finite∞ : ¬ (Finite infinity) +¬Finite∞ (suc p) = ¬Finite∞ p + +------------------------------------------------------------------------ +-- Order wrt to Nat + +data _ℕ≤_ : ℕ → Conat ∞ → Set where + zℕ≤n : ∀ {n} → zero ℕ≤ n + sℕ≤s : ∀ {k n} → k ℕ≤ n .force → suc k ℕ≤ suc n + +_ℕ<_ : ℕ → Conat ∞ → Set +k ℕ< n = suc k ℕ≤ n + +_ℕ≤infinity : ∀ k → k ℕ≤ infinity +zero ℕ≤infinity = zℕ≤n +suc k ℕ≤infinity = sℕ≤s (k ℕ≤infinity) + +------------------------------------------------------------------------ +-- Legacy + +open import Codata.Musical.Notation using (♭; ♯_) +import Codata.Musical.Conat as M + +fromMusical : ∀ {i} → M.Coℕ → Conat i +fromMusical M.zero = zero +fromMusical (M.suc n) = suc λ where .force → fromMusical (♭ n) + +toMusical : Conat ∞ → M.Coℕ +toMusical zero = M.zero +toMusical (suc n) = M.suc (♯ toMusical (n .force)) diff --git a/src/Codata/Conat/Bisimilarity.agda b/src/Codata/Conat/Bisimilarity.agda new file mode 100644 index 0000000..d3c3cf5 --- /dev/null +++ b/src/Codata/Conat/Bisimilarity.agda @@ -0,0 +1,49 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bisimilarity for Conats +------------------------------------------------------------------------ + +module Codata.Conat.Bisimilarity where + +open import Size +open import Codata.Thunk +open import Codata.Conat +open import Relation.Binary + +infix 1 _⊢_≈_ +data _⊢_≈_ i : (m n : Conat ∞) → Set where + zero : i ⊢ zero ≈ zero + suc : ∀ {m n} → Thunk^R _⊢_≈_ i m n → i ⊢ suc m ≈ suc n + +refl : ∀ {i m} → i ⊢ m ≈ m +refl {m = zero} = zero +refl {m = suc m} = suc λ where .force → refl + +sym : ∀ {i m n} → i ⊢ m ≈ n → i ⊢ n ≈ m +sym zero = zero +sym (suc eq) = suc λ where .force → sym (eq .force) + +trans : ∀ {i m n p} → i ⊢ m ≈ n → i ⊢ n ≈ p → i ⊢ m ≈ p +trans zero zero = zero +trans (suc eq₁) (suc eq₂) = suc λ where .force → trans (eq₁ .force) (eq₂ .force) + +infix 1 _⊢_≲_ +data _⊢_≲_ i : (m n : Conat ∞) → Set where + z≲n : ∀ {n} → i ⊢ zero ≲ n + s≲s : ∀ {m n} → Thunk^R _⊢_≲_ i m n → i ⊢ suc m ≲ suc n + +≈⇒≲ : ∀ {i m n} → i ⊢ m ≈ n → i ⊢ m ≲ n +≈⇒≲ zero = z≲n +≈⇒≲ (suc eq) = s≲s λ where .force → ≈⇒≲ (eq .force) + +≲-refl : ∀ {i m} → i ⊢ m ≲ m +≲-refl = ≈⇒≲ refl + +≲-antisym : ∀ {i m n} → i ⊢ m ≲ n → i ⊢ n ≲ m → i ⊢ m ≈ n +≲-antisym z≲n z≲n = zero +≲-antisym (s≲s le) (s≲s ge) = suc λ where .force → ≲-antisym (le .force) (ge .force) + +≲-trans : ∀ {i m n p} → i ⊢ m ≲ n → i ⊢ n ≲ p → i ⊢ m ≲ p +≲-trans z≲n _ = z≲n +≲-trans (s≲s le₁) (s≲s le₂) = s≲s λ where .force → ≲-trans (le₁ .force) (le₂ .force) diff --git a/src/Codata/Conat/Literals.agda b/src/Codata/Conat/Literals.agda new file mode 100644 index 0000000..de58e5d --- /dev/null +++ b/src/Codata/Conat/Literals.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Conat Literals +------------------------------------------------------------------------ + +module Codata.Conat.Literals where + +open import Agda.Builtin.FromNat +open import Data.Unit +open import Codata.Conat + +number : ∀ {i} → Number (Conat i) +number = record + { Constraint = λ _ → ⊤ + ; fromNat = λ n → fromℕ n + } diff --git a/src/Codata/Conat/Properties.agda b/src/Codata/Conat/Properties.agda new file mode 100644 index 0000000..f1497b1 --- /dev/null +++ b/src/Codata/Conat/Properties.agda @@ -0,0 +1,32 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties for Conats +------------------------------------------------------------------------ + +module Codata.Conat.Properties where + +open import Data.Nat +open import Codata.Thunk +open import Codata.Conat +open import Codata.Conat.Bisimilarity +open import Function +open import Relation.Nullary +open import Relation.Binary + +sℕ≤s⁻¹ : ∀ {m n} → suc m ℕ≤ suc n → m ℕ≤ n .force +sℕ≤s⁻¹ (sℕ≤s p) = p + +_ℕ≤?_ : Decidable _ℕ≤_ +zero ℕ≤? n = yes zℕ≤n +suc m ℕ≤? zero = no (λ ()) +suc m ℕ≤? suc n with m ℕ≤? n .force +... | yes p = yes (sℕ≤s p) +... | no ¬p = no (¬p ∘′ sℕ≤s⁻¹) + +0ℕ+-identity : ∀ {i n} → i ⊢ 0 ℕ+ n ≈ n +0ℕ+-identity = refl + ++ℕ0-identity : ∀ {i n} → i ⊢ n +ℕ 0 ≈ n ++ℕ0-identity {n = zero} = zero ++ℕ0-identity {n = suc n} = suc λ where .force → +ℕ0-identity diff --git a/src/Codata/Covec.agda b/src/Codata/Covec.agda new file mode 100644 index 0000000..6776174 --- /dev/null +++ b/src/Codata/Covec.agda @@ -0,0 +1,103 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The Covec type and some operations +------------------------------------------------------------------------ + +module Codata.Covec where + +open import Size + +open import Codata.Thunk using (Thunk; force) +open import Codata.Conat as Conat hiding (fromMusical; toMusical) +open import Codata.Conat.Bisimilarity +open import Codata.Conat.Properties +open import Codata.Cofin as Cofin using (Cofin; zero; suc) +open import Codata.Colist as Colist using (Colist ; [] ; _∷_) +open import Codata.Stream as Stream using (Stream ; _∷_) +open import Function + +data Covec {ℓ} (A : Set ℓ) (i : Size) : Conat ∞ → Set ℓ where + [] : Covec A i zero + _∷_ : ∀ {n} → A → Thunk (λ i → Covec A i (n .force)) i → Covec A i (suc n) + +module _ {ℓ} {A : Set ℓ} where + + head : ∀ {n i} → Covec A i (suc n) → A + head (x ∷ _) = x + + tail : ∀ {n} → Covec A ∞ (suc n) → Covec A ∞ (n .force) + tail (_ ∷ xs) = xs .force + + lookup : ∀ {n} → Cofin n → Covec A ∞ n → A + lookup zero = head + lookup (suc k) = lookup k ∘′ tail + + replicate : ∀ {i} → (n : Conat ∞) → A → Covec A i n + replicate zero a = [] + replicate (suc n) a = a ∷ λ where .force → replicate (n .force) a + + cotake : ∀ {i} → (n : Conat ∞) → Stream A i → Covec A i n + cotake zero xs = [] + cotake (suc n) (x ∷ xs) = x ∷ λ where .force → cotake (n .force) (xs .force) + + infixr 5 _++_ + _++_ : ∀ {i m n} → Covec A i m → Covec A i n → Covec A i (m + n) + [] ++ ys = ys + (x ∷ xs) ++ ys = x ∷ λ where .force → xs .force ++ ys + + fromColist : ∀ {i} → (xs : Colist A ∞) → Covec A i (Colist.length xs) + fromColist [] = [] + fromColist (x ∷ xs) = x ∷ λ where .force → fromColist (xs .force) + + toColist : ∀ {i n} → Covec A i n → Colist A i + toColist [] = [] + toColist (x ∷ xs) = x ∷ λ where .force → toColist (xs .force) + + fromStream : ∀ {i} → Stream A i → Covec A i infinity + fromStream = cotake infinity + + cast : ∀ {i} {m n} → i ⊢ m ≈ n → Covec A i m → Covec A i n + cast zero [] = [] + cast (suc eq) (a ∷ as) = a ∷ λ where .force → cast (eq .force) (as .force) + +module _ {a b} {A : Set a} {B : Set b} where + + map : ∀ {i n} (f : A → B) → Covec A i n → Covec B i n + map f [] = [] + map f (a ∷ as) = f a ∷ λ where .force → map f (as .force) + + ap : ∀ {i n} → Covec (A → B) i n → Covec A i n → Covec B i n + ap [] [] = [] + ap (f ∷ fs) (a ∷ as) = (f a) ∷ λ where .force → ap (fs .force) (as .force) + + scanl : ∀ {i n} → (B → A → B) → B → Covec A i n → Covec B i (1 ℕ+ n) + scanl c n [] = n ∷ λ where .force → [] + scanl c n (a ∷ as) = n ∷ λ where + .force → cast (suc λ where .force → 0ℕ+-identity) + (scanl c (c n a) (as .force)) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where + + zipWith : ∀ {i n} → (A → B → C) → Covec A i n → Covec B i n → Covec C i n + zipWith f [] [] = [] + zipWith f (a ∷ as) (b ∷ bs) = + f a b ∷ λ where .force → zipWith f (as .force) (bs .force) + + + +------------------------------------------------------------------------ +-- Legacy + +open import Codata.Musical.Notation using (♭; ♯_) +import Codata.Musical.Covec as M + +module _ {a} {A : Set a} where + + fromMusical : ∀ {i n} → M.Covec A n → Covec A i (Conat.fromMusical n) + fromMusical M.[] = [] + fromMusical (x M.∷ xs) = x ∷ λ where .force → fromMusical (♭ xs) + + toMusical : ∀ {n} → Covec A ∞ n → M.Covec A (Conat.toMusical n) + toMusical [] = M.[] + toMusical (x ∷ xs) = x M.∷ ♯ toMusical (xs .force) diff --git a/src/Codata/Covec/Bisimilarity.agda b/src/Codata/Covec/Bisimilarity.agda new file mode 100644 index 0000000..65c49b7 --- /dev/null +++ b/src/Codata/Covec/Bisimilarity.agda @@ -0,0 +1,61 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bisimilarity for Covecs +------------------------------------------------------------------------ + +module Codata.Covec.Bisimilarity where + +open import Level using (_⊔_) +open import Size +open import Codata.Thunk +open import Codata.Conat hiding (_⊔_) +open import Codata.Covec +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as Eq using (_≡_) + +data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) : + ∀ m n (xs : Covec A ∞ m) (ys : Covec B ∞ n) → Set (r ⊔ a ⊔ b) where + [] : Bisim R i zero zero [] [] + _∷_ : ∀ {x y m n xs ys} → R x y → Thunk^R (λ i → Bisim R i (m .force) (n .force)) i xs ys → + Bisim R i (suc m) (suc n) (x ∷ xs) (y ∷ ys) + + +module _ {a r} {A : Set a} {R : A → A → Set r} where + + reflexive : Reflexive R → ∀ {i m} → Reflexive (Bisim R i m m) + reflexive refl^R {i} {m} {[]} = [] + reflexive refl^R {i} {m} {r ∷ rs} = refl^R ∷ λ where .force → reflexive refl^R + +module _ {a b} {A : Set a} {B : Set b} + {r} {P : A → B → Set r} {Q : B → A → Set r} where + + symmetric : Sym P Q → ∀ {i m n} → Sym (Bisim P i m n) (Bisim Q i n m) + symmetric sym^PQ [] = [] + symmetric sym^PQ (p ∷ ps) = sym^PQ p ∷ λ where .force → symmetric sym^PQ (ps .force) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} + {r} {P : A → B → Set r} {Q : B → C → Set r} {R : A → C → Set r} where + + transitive : Trans P Q R → ∀ {i m n p} → Trans (Bisim P i m n) (Bisim Q i n p) (Bisim R i m p) + transitive trans^PQR [] [] = [] + transitive trans^PQR (p ∷ ps) (q ∷ qs) = + trans^PQR p q ∷ λ where .force → transitive trans^PQR (ps .force) (qs .force) + +-- Pointwise Equality as a Bisimilarity +------------------------------------------------------------------------ + +module _ {ℓ} {A : Set ℓ} where + + infix 1 _,_⊢_≈_ + _,_⊢_≈_ : ∀ i m → Covec A ∞ m → Covec A ∞ m → Set ℓ + _,_⊢_≈_ i m = Bisim _≡_ i m m + + refl : ∀ {i m} → Reflexive (i , m ⊢_≈_) + refl = reflexive Eq.refl + + sym : ∀ {i m} → Symmetric (i , m ⊢_≈_) + sym = symmetric Eq.sym + + trans : ∀ {i m} → Transitive (i , m ⊢_≈_) + trans = transitive Eq.trans diff --git a/src/Codata/Covec/Categorical.agda b/src/Codata/Covec/Categorical.agda new file mode 100644 index 0000000..8e99de4 --- /dev/null +++ b/src/Codata/Covec/Categorical.agda @@ -0,0 +1,22 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A categorical view of Covec +------------------------------------------------------------------------ + +module Codata.Covec.Categorical where + +open import Codata.Conat +open import Codata.Covec + +open import Category.Functor +open import Category.Applicative + +functor : ∀ {ℓ i n} → RawFunctor {ℓ} (λ A → Covec A n i) +functor = record { _<$>_ = map } + +applicative : ∀ {ℓ i n} → RawApplicative {ℓ} (λ A → Covec A n i) +applicative = record + { pure = replicate _ + ; _⊛_ = ap + } diff --git a/src/Codata/Covec/Properties.agda b/src/Codata/Covec/Properties.agda new file mode 100644 index 0000000..c86975c --- /dev/null +++ b/src/Codata/Covec/Properties.agda @@ -0,0 +1,30 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of operations on the Covec type +------------------------------------------------------------------------ + +module Codata.Covec.Properties where + +open import Size +open import Codata.Thunk using (Thunk; force) +open import Codata.Conat +open import Codata.Covec +open import Codata.Covec.Bisimilarity +open import Function +open import Relation.Binary.PropositionalEquality as Eq + +-- Functor laws + +module _ {a} {A : Set a} where + + map-identity : ∀ {m} (as : Covec A ∞ m) {i} → i , m ⊢ map id as ≈ as + map-identity [] = [] + map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where + + map-map-fusion : ∀ (f : A → B) (g : B → C) {m} as {i} → i , m ⊢ map g (map f as) ≈ map (g ∘ f) as + map-map-fusion f g [] = [] + map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force) + diff --git a/src/Codata/Delay.agda b/src/Codata/Delay.agda new file mode 100644 index 0000000..fcaf322 --- /dev/null +++ b/src/Codata/Delay.agda @@ -0,0 +1,112 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The Delay type and some operations +------------------------------------------------------------------------ + +module Codata.Delay where + +open import Size +open import Codata.Thunk using (Thunk; force) +open import Codata.Conat using (Conat; zero; suc; Finite) + +open import Data.Empty +open import Relation.Nullary +open import Data.Nat.Base +open import Data.Maybe.Base hiding (map ; fromMaybe ; zipWith ; alignWith ; zip ; align) +open import Data.Product as P hiding (map ; zip) +open import Data.Sum as S hiding (map) +open import Data.These as T using (These; this; that; these) +open import Function + +------------------------------------------------------------------------ +-- Definition + +data Delay {ℓ} (A : Set ℓ) (i : Size) : Set ℓ where + now : A → Delay A i + later : Thunk (Delay A) i → Delay A i + +module _ {ℓ} {A : Set ℓ} where + + length : ∀ {i} → Delay A i → Conat i + length (now _) = zero + length (later d) = suc λ where .force → length (d .force) + + never : ∀ {i} → Delay A i + never = later λ where .force → never + + fromMaybe : Maybe A → Delay A ∞ + fromMaybe = maybe now never + + runFor : ℕ → Delay A ∞ → Maybe A + runFor zero d = nothing + runFor (suc n) (now a) = just a + runFor (suc n) (later d) = runFor n (d .force) + +module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where + + map : (A → B) → ∀ {i} → Delay A i → Delay B i + map f (now a) = now (f a) + map f (later d) = later λ where .force → map f (d .force) + + bind : ∀ {i} → Delay A i → (A → Delay B i) → Delay B i + bind (now a) f = f a + bind (later d) f = later λ where .force → bind (d .force) f + + unfold : (A → A ⊎ B) → A → ∀ {i} → Delay B i + unfold next seed with next seed + ... | inj₁ seed′ = later λ where .force → unfold next seed′ + ... | inj₂ b = now b + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where + + zipWith : (A → B → C) → ∀ {i} → Delay A i → Delay B i → Delay C i + zipWith f (now a) d = map (f a) d + zipWith f d (now b) = map (λ a → f a b) d + zipWith f (later a) (later b) = later λ where .force → zipWith f (a .force) (b .force) + + alignWith : (These A B → C) → ∀ {i} → Delay A i → Delay B i → Delay C i + alignWith f (now a) (now b) = now (f (these a b)) + alignWith f (now a) (later _) = now (f (this a)) + alignWith f (later _) (now b) = now (f (that b)) + alignWith f (later a) (later b) = later λ where + .force → alignWith f (a .force) (b .force) + +module _ {a b} {A : Set a} {B : Set b} where + + zip : ∀ {i} → Delay A i → Delay B i → Delay (A × B) i + zip = zipWith _,_ + + align : ∀ {i} → Delay A i → Delay B i → Delay (These A B) i + align = alignWith id + +------------------------------------------------------------------------ +-- Finite Delays + +module _ {ℓ} {A : Set ℓ} where + + infix 3 _⇓ + data _⇓ : Delay A ∞ → Set ℓ where + now : ∀ a → now a ⇓ + later : ∀ {d} → d .force ⇓ → later d ⇓ + + extract : ∀ {d} → d ⇓ → A + extract (now a) = a + extract (later d) = extract d + + ¬never⇓ : ¬ (never ⇓) + ¬never⇓ (later p) = ¬never⇓ p + + length-⇓ : ∀ {d} → d ⇓ → Finite (length d) + length-⇓ (now a) = zero + length-⇓ (later d⇓) = suc (length-⇓ d⇓) + +module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where + + map-⇓ : ∀ (f : A → B) {d} → d ⇓ → map f d ⇓ + map-⇓ f (now a) = now (f a) + map-⇓ f (later d) = later (map-⇓ f d) + + bind-⇓ : ∀ {m} (m⇓ : m ⇓) {f : A → Delay B ∞} → f (extract m⇓) ⇓ → bind m f ⇓ + bind-⇓ (now a) fa⇓ = fa⇓ + bind-⇓ (later p) fa⇓ = later (bind-⇓ p fa⇓) diff --git a/src/Codata/Delay/Bisimilarity.agda b/src/Codata/Delay/Bisimilarity.agda new file mode 100644 index 0000000..ea4eb85 --- /dev/null +++ b/src/Codata/Delay/Bisimilarity.agda @@ -0,0 +1,58 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bisimilarity for the Delay type +------------------------------------------------------------------------ + +module Codata.Delay.Bisimilarity where + +open import Size +open import Codata.Thunk +open import Codata.Delay +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as Eq using (_≡_) + +data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) i : + (xs : Delay A ∞) (ys : Delay B ∞) → Set r where + now : ∀ {x y} → R x y → Bisim R i (now x) (now y) + later : ∀ {xs ys} → Thunk^R (Bisim R) i xs ys → Bisim R i (later xs) (later ys) + +module _ {a r} {A : Set a} {R : A → A → Set r} where + + reflexive : Reflexive R → ∀ {i} → Reflexive (Bisim R i) + reflexive refl^R {i} {now r} = now refl^R + reflexive refl^R {i} {later rs} = later λ where .force → reflexive refl^R + +module _ {a b} {A : Set a} {B : Set b} + {r} {P : A → B → Set r} {Q : B → A → Set r} where + + symmetric : Sym P Q → ∀ {i} → Sym (Bisim P i) (Bisim Q i) + symmetric sym^PQ (now p) = now (sym^PQ p) + symmetric sym^PQ (later ps) = later λ where .force → symmetric sym^PQ (ps .force) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} + {r} {P : A → B → Set r} {Q : B → C → Set r} {R : A → C → Set r} where + + transitive : Trans P Q R → ∀ {i} → Trans (Bisim P i) (Bisim Q i) (Bisim R i) + transitive trans^PQR (now p) (now q) = now (trans^PQR p q) + transitive trans^PQR (later ps) (later qs) = + later λ where .force → transitive trans^PQR (ps .force) (qs .force) + + +-- Pointwise Equality as a Bisimilarity +------------------------------------------------------------------------ + +module _ {ℓ} {A : Set ℓ} where + + infix 1 _⊢_≈_ + _⊢_≈_ : ∀ i → Delay A ∞ → Delay A ∞ → Set ℓ + _⊢_≈_ = Bisim _≡_ + + refl : ∀ {i} → Reflexive (i ⊢_≈_) + refl = reflexive Eq.refl + + sym : ∀ {i} → Symmetric (i ⊢_≈_) + sym = symmetric Eq.sym + + trans : ∀ {i} → Transitive (i ⊢_≈_) + trans = transitive Eq.trans diff --git a/src/Codata/Delay/Categorical.agda b/src/Codata/Delay/Categorical.agda new file mode 100644 index 0000000..a3d1a84 --- /dev/null +++ b/src/Codata/Delay/Categorical.agda @@ -0,0 +1,61 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A categorical view of Delay +------------------------------------------------------------------------ + +module Codata.Delay.Categorical where + +open import Codata.Delay +open import Function +open import Category.Functor +open import Category.Applicative +open import Category.Monad + +functor : ∀ {i ℓ} → RawFunctor {ℓ} (λ A → Delay A i) +functor = record { _<$>_ = λ f → map f } + +module Sequential where + + applicative : ∀ {i ℓ} → RawApplicative {ℓ} (λ A → Delay A i) + applicative = record + { pure = now + ; _⊛_ = λ df da → bind df (λ f → map f da) + } + + monad : ∀ {i ℓ} → RawMonad {ℓ} (λ A → Delay A i) + monad = record + { return = now + ; _>>=_ = bind + } + + monadZero : ∀ {i ℓ} → RawMonadZero {ℓ} (λ A → Delay A i) + monadZero = record + { monad = monad + ; ∅ = never + } + +module Zippy where + + applicative : ∀ {i ℓ} → RawApplicative {ℓ} (λ A → Delay A i) + applicative = record + { pure = now + ; _⊛_ = zipWith id + } + + -- We do not have `RawApplicativeZero` and `RawApplicativePlus` yet but here is what + -- they would look like + + {- + applicativeZero : ∀ {i ℓ} → RawApplicativeZero {ℓ} (λ A → Delay A i) + applicativeZero = record + { applicative = applicative + ; ∅ = never + } + + applicativePlus : ∀ {i ℓ} → RawApplicativeZero {ℓ} (λ A → Delay A i) + applicativePlus = record + { applicativeZero = applicativeZero + ; _∣_ = alignWith leftMost + } + -} diff --git a/src/Codata/Delay/Properties.agda b/src/Codata/Delay/Properties.agda new file mode 100644 index 0000000..ef1404e --- /dev/null +++ b/src/Codata/Delay/Properties.agda @@ -0,0 +1,48 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of operations on the Delay type +------------------------------------------------------------------------ + +module Codata.Delay.Properties where + +open import Size +import Data.Sum as Sum +open import Codata.Thunk using (Thunk; force) +open import Codata.Conat +open import Codata.Conat.Bisimilarity as Coℕ using (zero ; suc) +open import Codata.Delay +open import Codata.Delay.Bisimilarity +open import Function +open import Relation.Binary.PropositionalEquality as Eq using (_≡_) + +module _ {a} {A : Set a} where + + length-never : ∀ {i} → i Coℕ.⊢ length (never {A = A}) ≈ infinity + length-never = suc λ where .force → length-never + +module _ {a b} {A : Set a} {B : Set b} where + + length-map : ∀ (f : A → B) da {i} → i Coℕ.⊢ length (map f da) ≈ length da + length-map f (now a) = zero + length-map f (later da) = suc λ where .force → length-map f (da .force) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where + + length-zipWith : ∀ (f : A → B → C) da db {i} → + i Coℕ.⊢ length (zipWith f da db) ≈ length da ⊔ length db + length-zipWith f (now a) db = length-map (f a) db + length-zipWith f da@(later _) (now b) = length-map (λ a → f a b) da + length-zipWith f (later da) (later db) = + suc λ where .force → length-zipWith f (da .force) (db .force) + + map-map-fusion : ∀ (f : A → B) (g : B → C) da {i} → + i ⊢ map g (map f da) ≈ map (g ∘′ f) da + map-map-fusion f g (now a) = now Eq.refl + map-map-fusion f g (later da) = later λ where .force → map-map-fusion f g (da .force) + + map-unfold-fusion : ∀ (f : B → C) n (s : A) {i} → + i ⊢ map f (unfold n s) ≈ unfold (Sum.map id f ∘′ n) s + map-unfold-fusion f n s with n s + ... | Sum.inj₁ s′ = later λ where .force → map-unfold-fusion f n s′ + ... | Sum.inj₂ b = now Eq.refl diff --git a/src/Codata/M.agda b/src/Codata/M.agda new file mode 100644 index 0000000..ca80dcf --- /dev/null +++ b/src/Codata/M.agda @@ -0,0 +1,58 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- M-types (the dual of W-types) +------------------------------------------------------------------------ + +module Codata.M where + +open import Size +open import Level +open import Codata.Thunk using (Thunk; force) +open import Data.Product hiding (map) +open import Data.Container.Core +import Data.Container as C + +data M {s p} (C : Container s p) (i : Size) : Set (s ⊔ p) where + inf : ⟦ C ⟧ (Thunk (M C) i) → M C i + +module _ {s p} {C : Container s p} (open Container C) where + + head : ∀ {i} → M C i → Shape + head (inf (x , f)) = x + + tail : (x : M C ∞) → Position (head x) → M C ∞ + tail (inf (x , f)) = λ p → f p .force + +-- map + +module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} + (m : C₁ ⇒ C₂) where + + map : ∀ {i} → M C₁ i → M C₂ i + map (inf t) = inf (⟪ m ⟫ (C.map (λ t → λ where .force → map (t .force)) t)) + +-- unfold + +module _ {s p ℓ} {C : Container s p} (open Container C) + {S : Set ℓ} (alg : S → ⟦ C ⟧ S) where + + unfold : S → ∀ {i} → M C i + unfold seed = let (x , next) = alg seed in + inf (x , λ p → λ where .force → unfold (next p)) + + +------------------------------------------------------------------------ +-- Legacy + +open import Codata.Musical.Notation using (♭; ♯_) +import Codata.Musical.M as M + +module _ {s p} {C : Container s p} where + + fromMusical : ∀ {i} → M.M C → M C i + fromMusical (M.inf t) = inf (C.map rec t) where + rec = λ x → λ where .force → fromMusical (♭ x) + + toMusical : M C ∞ → M.M C + toMusical (inf (s , f)) = M.inf (s , λ p → ♯ toMusical (f p .force)) diff --git a/src/Codata/Musical/Cofin.agda b/src/Codata/Musical/Cofin.agda new file mode 100644 index 0000000..138641c --- /dev/null +++ b/src/Codata/Musical/Cofin.agda @@ -0,0 +1,47 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- "Finite" sets indexed on coinductive "natural" numbers +------------------------------------------------------------------------ + +module Codata.Musical.Cofin where + +open import Codata.Musical.Notation +open import Codata.Musical.Conat as Conat using (Coℕ; suc; ∞ℕ) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Fin using (Fin; zero; suc) +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) +open import Function + +------------------------------------------------------------------------ +-- The type + +-- Note that Cofin ∞ℕ is /not/ finite. Note also that this is not a +-- coinductive type, but it is indexed on a coinductive type. + +data Cofin : Coℕ → Set where + zero : ∀ {n} → Cofin (suc n) + suc : ∀ {n} (i : Cofin (♭ n)) → Cofin (suc n) + +suc-injective : ∀ {m} {p q : Cofin (♭ m)} → (Cofin (suc m) ∋ suc p) ≡ suc q → p ≡ q +suc-injective refl = refl + +------------------------------------------------------------------------ +-- Some operations + +fromℕ : ℕ → Cofin ∞ℕ +fromℕ zero = zero +fromℕ (suc n) = suc (fromℕ n) + +toℕ : ∀ {n} → Cofin n → ℕ +toℕ zero = zero +toℕ (suc i) = suc (toℕ i) + +fromFin : ∀ {n} → Fin n → Cofin (Conat.fromℕ n) +fromFin zero = zero +fromFin (suc i) = suc (fromFin i) + +toFin : ∀ n → Cofin (Conat.fromℕ n) → Fin n +toFin zero () +toFin (suc n) zero = zero +toFin (suc n) (suc i) = suc (toFin n i) diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda new file mode 100644 index 0000000..3824ce3 --- /dev/null +++ b/src/Codata/Musical/Colist.agda @@ -0,0 +1,535 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Coinductive lists +------------------------------------------------------------------------ + +module Codata.Musical.Colist where + +open import Category.Monad +open import Codata.Musical.Notation +open import Codata.Musical.Conat using (Coℕ; zero; suc) +open import Data.Bool.Base using (Bool; true; false) +open import Data.BoundedVec.Inefficient as BVec + using (BoundedVec; []; _∷_) +open import Data.Empty using (⊥) +open import Data.Maybe.Base using (Maybe; nothing; just; Is-just) +open import Data.Nat.Base using (ℕ; zero; suc; _≥′_; ≤′-refl; ≤′-step) +open import Data.Nat.Properties using (s≤′s) +open import Data.List.Base using (List; []; _∷_) +open import Data.List.NonEmpty using (List⁺; _∷_) +open import Data.Product as Prod using (∃; _×_; _,_) +open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′) +open import Function +open import Function.Equality using (_⟨$⟩_) +open import Function.Inverse as Inv using (_↔_; _↔̇_; Inverse; inverse) +open import Level using (_⊔_) +open import Relation.Binary +import Relation.Binary.Construct.FromRel as Ind +open import Relation.Binary.PropositionalEquality as P using (_≡_) +open import Relation.Nullary +open import Relation.Nullary.Negation + +module ¬¬Monad {p} where + open RawMonad (¬¬-Monad {p}) public +open ¬¬Monad -- we don't want the RawMonad content to be opened publicly + +------------------------------------------------------------------------ +-- The type + +infixr 5 _∷_ + +data Colist {a} (A : Set a) : Set a where + [] : Colist A + _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A + +{-# FOREIGN GHC + data AgdaColist a = Nil | Cons a (MAlonzo.RTE.Inf (AgdaColist a)) + type AgdaColist' l a = AgdaColist a + #-} +{-# COMPILE GHC Colist = data AgdaColist' (Nil | Cons) #-} +{-# COMPILE UHC Colist = data __LIST__ (__NIL__ | __CONS__) #-} + +module Colist-injective {a} {A : Set a} where + + ∷-injectiveˡ : ∀ {x y : A} {xs ys} → (Colist A ∋ x ∷ xs) ≡ y ∷ ys → x ≡ y + ∷-injectiveˡ P.refl = P.refl + + ∷-injectiveʳ : ∀ {x y : A} {xs ys} → (Colist A ∋ x ∷ xs) ≡ y ∷ ys → xs ≡ ys + ∷-injectiveʳ P.refl = P.refl + +data Any {a p} {A : Set a} (P : A → Set p) : + Colist A → Set (a ⊔ p) where + here : ∀ {x xs} (px : P x) → Any P (x ∷ xs) + there : ∀ {x xs} (pxs : Any P (♭ xs)) → Any P (x ∷ xs) + +module _ {a p} {A : Set a} {P : A → Set p} where + + here-injective : ∀ {x xs p q} → (Any P (x ∷ xs) ∋ here p) ≡ here q → p ≡ q + here-injective P.refl = P.refl + + there-injective : ∀ {x xs p q} → (Any P (x ∷ xs) ∋ there p) ≡ there q → p ≡ q + there-injective P.refl = P.refl + +data All {a p} {A : Set a} (P : A → Set p) : + Colist A → Set (a ⊔ p) where + [] : All P [] + _∷_ : ∀ {x xs} (px : P x) (pxs : ∞ (All P (♭ xs))) → All P (x ∷ xs) + +module All-injective {a p} {A : Set a} {P : A → Set p} where + + ∷-injectiveˡ : ∀ {x xs} {px qx pxs qxs} → + (All P (x ∷ xs) ∋ px ∷ pxs) ≡ qx ∷ qxs → px ≡ qx + ∷-injectiveˡ P.refl = P.refl + + ∷-injectiveʳ : ∀ {x xs} {px qx pxs qxs} → + (All P (x ∷ xs) ∋ px ∷ pxs) ≡ qx ∷ qxs → pxs ≡ qxs + ∷-injectiveʳ P.refl = P.refl + +------------------------------------------------------------------------ +-- Some operations + +null : ∀ {a} {A : Set a} → Colist A → Bool +null [] = true +null (_ ∷ _) = false + +length : ∀ {a} {A : Set a} → Colist A → Coℕ +length [] = zero +length (x ∷ xs) = suc (♯ length (♭ xs)) + +map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Colist A → Colist B +map f [] = [] +map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs) + +fromList : ∀ {a} {A : Set a} → List A → Colist A +fromList [] = [] +fromList (x ∷ xs) = x ∷ ♯ fromList xs + +take : ∀ {a} {A : Set a} (n : ℕ) → Colist A → BoundedVec A n +take zero xs = [] +take (suc n) [] = [] +take (suc n) (x ∷ xs) = x ∷ take n (♭ xs) + +replicate : ∀ {a} {A : Set a} → Coℕ → A → Colist A +replicate zero x = [] +replicate (suc n) x = x ∷ ♯ replicate (♭ n) x + +lookup : ∀ {a} {A : Set a} → ℕ → Colist A → Maybe A +lookup n [] = nothing +lookup zero (x ∷ xs) = just x +lookup (suc n) (x ∷ xs) = lookup n (♭ xs) + +infixr 5 _++_ + +_++_ : ∀ {a} {A : Set a} → Colist A → Colist A → Colist A +[] ++ ys = ys +(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys) + +-- Interleaves the two colists (until the shorter one, if any, has +-- been exhausted). + +infixr 5 _⋎_ + +_⋎_ : ∀ {a} {A : Set a} → Colist A → Colist A → Colist A +[] ⋎ ys = ys +(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs) + +concat : ∀ {a} {A : Set a} → Colist (List⁺ A) → Colist A +concat [] = [] +concat ((x ∷ []) ∷ xss) = x ∷ ♯ concat (♭ xss) +concat ((x ∷ (y ∷ xs)) ∷ xss) = x ∷ ♯ concat ((y ∷ xs) ∷ xss) + +[_] : ∀ {a} {A : Set a} → A → Colist A +[ x ] = x ∷ ♯ [] + +------------------------------------------------------------------------ +-- Any lemmas + +-- Any lemma for map. + +Any-map : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p} + {f : A → B} {xs} → + Any P (map f xs) ↔ Any (P ∘ f) xs +Any-map {P = P} {f} {xs} = inverse to from from∘to to∘from + where + to : ∀ {xs} → Any P (map f xs) → Any (P ∘ f) xs + to {[]} () + to {x ∷ xs} (here px) = here px + to {x ∷ xs} (there p) = there (to p) + + from : ∀ {xs} → Any (P ∘ f) xs → Any P (map f xs) + from (here px) = here px + from (there p) = there (from p) + + from∘to : ∀ {xs} (p : Any P (map f xs)) → from (to p) ≡ p + from∘to {[]} () + from∘to {x ∷ xs} (here px) = P.refl + from∘to {x ∷ xs} (there p) = P.cong there (from∘to p) + + to∘from : ∀ {xs} (p : Any (P ∘ f) xs) → to (from p) ≡ p + to∘from (here px) = P.refl + to∘from (there p) = P.cong there (to∘from p) + +-- Any lemma for _⋎_. This lemma implies that every member of xs or ys +-- is a member of xs ⋎ ys, and vice versa. + +Any-⋎ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} → + Any P (xs ⋎ ys) ↔ (Any P xs ⊎ Any P ys) +Any-⋎ {P = P} = λ xs → record + { to = P.→-to-⟶ (to xs) + ; from = P.→-to-⟶ (from xs) + ; inverse-of = record + { left-inverse-of = from∘to xs + ; right-inverse-of = to∘from xs + } + } + where + to : ∀ xs {ys} → Any P (xs ⋎ ys) → Any P xs ⊎ Any P ys + to [] p = inj₂ p + to (x ∷ xs) (here px) = inj₁ (here px) + to (x ∷ xs) (there p) = [ inj₂ , inj₁ ∘ there ]′ (to _ p) + + mutual + + from-left : ∀ {xs ys} → Any P xs → Any P (xs ⋎ ys) + from-left (here px) = here px + from-left {ys = ys} (there p) = there (from-right ys p) + + from-right : ∀ xs {ys} → Any P ys → Any P (xs ⋎ ys) + from-right [] p = p + from-right (x ∷ xs) p = there (from-left p) + + from : ∀ xs {ys} → Any P xs ⊎ Any P ys → Any P (xs ⋎ ys) + from xs = Sum.[ from-left , from-right xs ] + + from∘to : ∀ xs {ys} (p : Any P (xs ⋎ ys)) → from xs (to xs p) ≡ p + from∘to [] p = P.refl + from∘to (x ∷ xs) (here px) = P.refl + from∘to (x ∷ xs) {ys = ys} (there p) with to ys p | from∘to ys p + from∘to (x ∷ xs) {ys = ys} (there .(from-left q)) | inj₁ q | P.refl = P.refl + from∘to (x ∷ xs) {ys = ys} (there .(from-right ys q)) | inj₂ q | P.refl = P.refl + + mutual + + to∘from-left : ∀ {xs ys} (p : Any P xs) → + to xs {ys = ys} (from-left p) ≡ inj₁ p + to∘from-left (here px) = P.refl + to∘from-left {ys = ys} (there p) + rewrite to∘from-right ys p = P.refl + + to∘from-right : ∀ xs {ys} (p : Any P ys) → + to xs (from-right xs p) ≡ inj₂ p + to∘from-right [] p = P.refl + to∘from-right (x ∷ xs) {ys = ys} p + rewrite to∘from-left {xs = ys} {ys = ♭ xs} p = P.refl + + to∘from : ∀ xs {ys} (p : Any P xs ⊎ Any P ys) → to xs (from xs p) ≡ p + to∘from xs = Sum.[ to∘from-left , to∘from-right xs ] + +------------------------------------------------------------------------ +-- Equality + +-- xs ≈ ys means that xs and ys are equal. + +infix 4 _≈_ + +data _≈_ {a} {A : Set a} : (xs ys : Colist A) → Set a where + [] : [] ≈ [] + _∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys + +-- The equality relation forms a setoid. + +setoid : ∀ {ℓ} → Set ℓ → Setoid _ _ +setoid A = record + { Carrier = Colist A + ; _≈_ = _≈_ + ; isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + } + where + refl : Reflexive _≈_ + refl {[]} = [] + refl {x ∷ xs} = x ∷ ♯ refl + + sym : Symmetric _≈_ + sym [] = [] + sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈) + + trans : Transitive _≈_ + trans [] [] = [] + trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈) + +module ≈-Reasoning where + import Relation.Binary.EqReasoning as EqR + private + open module R {a} {A : Set a} = EqR (setoid A) public + +-- map preserves equality. + +map-cong : ∀ {a b} {A : Set a} {B : Set b} + (f : A → B) → _≈_ =[ map f ]⇒ _≈_ +map-cong f [] = [] +map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈) + +-- Any respects pointwise implication (for the predicate) and equality +-- (for the colist). + +Any-resp : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} + {xs ys} → (∀ {x} → P x → Q x) → xs ≈ ys → + Any P xs → Any Q ys +Any-resp f (x ∷ xs≈) (here px) = here (f px) +Any-resp f (x ∷ xs≈) (there p) = there (Any-resp f (♭ xs≈) p) + +-- Any maps pointwise isomorphic predicates and equal colists to +-- isomorphic types. + +Any-cong : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} + {xs ys} → P ↔̇ Q → xs ≈ ys → Any P xs ↔ Any Q ys +Any-cong {A = A} {P} {Q} {xs} {ys} P↔Q xs≈ys = record + { to = P.→-to-⟶ (to xs≈ys) + ; from = P.→-to-⟶ (from xs≈ys) + ; inverse-of = record + { left-inverse-of = resp∘resp P↔Q xs≈ys (sym xs≈ys) + ; right-inverse-of = resp∘resp (Inv.sym P↔Q) (sym xs≈ys) xs≈ys + } + } + where + open Setoid (setoid _) using (sym) + + to : ∀ {xs ys} → xs ≈ ys → Any P xs → Any Q ys + to xs≈ys = Any-resp (Inverse.to P↔Q ⟨$⟩_) xs≈ys + + from : ∀ {xs ys} → xs ≈ ys → Any Q ys → Any P xs + from xs≈ys = Any-resp (Inverse.from P↔Q ⟨$⟩_) (sym xs≈ys) + + resp∘resp : ∀ {p q} {P : A → Set p} {Q : A → Set q} {xs ys} + (P↔̇Q : P ↔̇ Q) (xs≈ys : xs ≈ ys) (ys≈xs : ys ≈ xs) + (p : Any P xs) → + Any-resp (Inverse.from P↔̇Q ⟨$⟩_) ys≈xs + (Any-resp (Inverse.to P↔̇Q ⟨$⟩_) xs≈ys p) ≡ p + resp∘resp P↔̇Q (x ∷ xs≈) (.x ∷ ys≈) (here px) = + P.cong here (Inverse.left-inverse-of P↔̇Q px) + resp∘resp P↔̇Q (x ∷ xs≈) (.x ∷ ys≈) (there p) = + P.cong there (resp∘resp P↔̇Q (♭ xs≈) (♭ ys≈) p) + +------------------------------------------------------------------------ +-- Indices + +-- Converts Any proofs to indices into the colist. The index can also +-- be seen as the size of the proof. + +index : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → Any P xs → ℕ +index (here px) = zero +index (there p) = suc (index p) + +-- The position returned by index is guaranteed to be within bounds. + +lookup-index : ∀ {a p} {A : Set a} {P : A → Set p} {xs} (p : Any P xs) → + Is-just (lookup (index p) xs) +lookup-index (here px) = just _ +lookup-index (there p) = lookup-index p + +-- Any-resp preserves the index. + +index-Any-resp : + ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} + {f : ∀ {x} → P x → Q x} {xs ys} + (xs≈ys : xs ≈ ys) (p : Any P xs) → + index (Any-resp f xs≈ys p) ≡ index p +index-Any-resp (x ∷ xs≈) (here px) = P.refl +index-Any-resp (x ∷ xs≈) (there p) = + P.cong suc (index-Any-resp (♭ xs≈) p) + +-- The left-to-right direction of Any-⋎ returns a proof whose size is +-- no larger than that of the input proof. + +index-Any-⋎ : + ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} (p : Any P (xs ⋎ ys)) → + index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎ xs) ⟨$⟩ p) +index-Any-⋎ [] p = ≤′-refl +index-Any-⋎ (x ∷ xs) (here px) = ≤′-refl +index-Any-⋎ (x ∷ xs) {ys = ys} (there p) + with Inverse.to (Any-⋎ ys) ⟨$⟩ p | index-Any-⋎ ys p +... | inj₁ q | q≤p = ≤′-step q≤p +... | inj₂ q | q≤p = s≤′s q≤p + +------------------------------------------------------------------------ +-- Memberships, subsets, prefixes + +-- x ∈ xs means that x is a member of xs. + +infix 4 _∈_ + +_∈_ : ∀ {a} → {A : Set a} → A → Colist A → Set a +x ∈ xs = Any (_≡_ x) xs + +-- xs ⊆ ys means that xs is a subset of ys. + +infix 4 _⊆_ + +_⊆_ : ∀ {a} → {A : Set a} → Colist A → Colist A → Set a +xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys + +-- xs ⊑ ys means that xs is a prefix of ys. + +infix 4 _⊑_ + +data _⊑_ {a} {A : Set a} : Colist A → Colist A → Set a where + [] : ∀ {ys} → [] ⊑ ys + _∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys + +-- Any can be expressed using _∈_ (and vice versa). + +Any-∈ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → + Any P xs ↔ ∃ λ x → x ∈ xs × P x +Any-∈ {P = P} = record + { to = P.→-to-⟶ to + ; from = P.→-to-⟶ (λ { (x , x∈xs , p) → from x∈xs p }) + ; inverse-of = record + { left-inverse-of = from∘to + ; right-inverse-of = λ { (x , x∈xs , p) → to∘from x∈xs p } + } + } + where + to : ∀ {xs} → Any P xs → ∃ λ x → x ∈ xs × P x + to (here p) = _ , here P.refl , p + to (there p) = Prod.map id (Prod.map there id) (to p) + + from : ∀ {x xs} → x ∈ xs → P x → Any P xs + from (here P.refl) p = here p + from (there x∈xs) p = there (from x∈xs p) + + to∘from : ∀ {x xs} (x∈xs : x ∈ xs) (p : P x) → + to (from x∈xs p) ≡ (x , x∈xs , p) + to∘from (here P.refl) p = P.refl + to∘from (there x∈xs) p = + P.cong (Prod.map id (Prod.map there id)) (to∘from x∈xs p) + + from∘to : ∀ {xs} (p : Any P xs) → + let (x , x∈xs , px) = to p in from x∈xs px ≡ p + from∘to (here _) = P.refl + from∘to (there p) = P.cong there (from∘to p) + +-- Prefixes are subsets. + +⊑⇒⊆ : ∀ {a} → {A : Set a} → _⊑_ {A = A} ⇒ _⊆_ +⊑⇒⊆ [] () +⊑⇒⊆ (x ∷ xs⊑ys) (here ≡x) = here ≡x +⊑⇒⊆ (_ ∷ xs⊑ys) (there x∈xs) = there (⊑⇒⊆ (♭ xs⊑ys) x∈xs) + +-- The prefix relation forms a poset. + +⊑-Poset : ∀ {ℓ} → Set ℓ → Poset _ _ _ +⊑-Poset A = record + { Carrier = Colist A + ; _≈_ = _≈_ + ; _≤_ = _⊑_ + ; isPartialOrder = record + { isPreorder = record + { isEquivalence = Setoid.isEquivalence (setoid A) + ; reflexive = reflexive + ; trans = trans + } + ; antisym = antisym + } + } + where + reflexive : _≈_ ⇒ _⊑_ + reflexive [] = [] + reflexive (x ∷ xs≈) = x ∷ ♯ reflexive (♭ xs≈) + + trans : Transitive _⊑_ + trans [] _ = [] + trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈) + + antisym : Antisymmetric _≈_ _⊑_ + antisym [] [] = [] + antisym (x ∷ p₁) (.x ∷ p₂) = x ∷ ♯ antisym (♭ p₁) (♭ p₂) + +module ⊑-Reasoning where + import Relation.Binary.PartialOrderReasoning as POR + private + open module R {a} {A : Set a} = POR (⊑-Poset A) + public renaming (_≤⟨_⟩_ to _⊑⟨_⟩_) + +-- The subset relation forms a preorder. + +⊆-Preorder : ∀ {ℓ} → Set ℓ → Preorder _ _ _ +⊆-Preorder A = Ind.preorder (setoid A) _∈_ + (λ xs≈ys → ⊑⇒⊆ (⊑P.reflexive xs≈ys)) + where module ⊑P = Poset (⊑-Poset A) + +module ⊆-Reasoning where + import Relation.Binary.PreorderReasoning as PreR + private + open module R {a} {A : Set a} = PreR (⊆-Preorder A) + public renaming (_∼⟨_⟩_ to _⊆⟨_⟩_) + + infix 1 _∈⟨_⟩_ + + _∈⟨_⟩_ : ∀ {a} {A : Set a} (x : A) {xs ys} → + x ∈ xs → xs IsRelatedTo ys → x ∈ ys + x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs + +-- take returns a prefix. + +take-⊑ : ∀ {a} {A : Set a} n (xs : Colist A) → + let toColist = fromList {a} ∘ BVec.toList in + toColist (take n xs) ⊑ xs +take-⊑ zero xs = [] +take-⊑ (suc n) [] = [] +take-⊑ (suc n) (x ∷ xs) = x ∷ ♯ take-⊑ n (♭ xs) + +------------------------------------------------------------------------ +-- Finiteness and infiniteness + +-- Finite xs means that xs has finite length. + +data Finite {a} {A : Set a} : Colist A → Set a where + [] : Finite [] + _∷_ : ∀ x {xs} (fin : Finite (♭ xs)) → Finite (x ∷ xs) + +module Finite-injective {a} {A : Set a} where + + ∷-injective : ∀ {x : A} {xs p q} → (Finite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q + ∷-injective P.refl = P.refl + +-- Infinite xs means that xs has infinite length. + +data Infinite {a} {A : Set a} : Colist A → Set a where + _∷_ : ∀ x {xs} (inf : ∞ (Infinite (♭ xs))) → Infinite (x ∷ xs) + +module Infinite-injective {a} {A : Set a} where + + ∷-injective : ∀ {x : A} {xs p q} → (Infinite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q + ∷-injective P.refl = P.refl + +-- Colists which are not finite are infinite. + +not-finite-is-infinite : + ∀ {a} {A : Set a} (xs : Colist A) → ¬ Finite xs → Infinite xs +not-finite-is-infinite [] hyp with hyp [] +... | () +not-finite-is-infinite (x ∷ xs) hyp = + x ∷ ♯ not-finite-is-infinite (♭ xs) (hyp ∘ _∷_ x) + +-- Colists are either finite or infinite (classically). + +finite-or-infinite : + ∀ {a} {A : Set a} (xs : Colist A) → ¬ ¬ (Finite xs ⊎ Infinite xs) +finite-or-infinite xs = helper <$> excluded-middle + where + helper : Dec (Finite xs) → Finite xs ⊎ Infinite xs + helper (yes fin) = inj₁ fin + helper (no ¬fin) = inj₂ $ not-finite-is-infinite xs ¬fin + +-- Colists are not both finite and infinite. + +not-finite-and-infinite : + ∀ {a} {A : Set a} {xs : Colist A} → Finite xs → Infinite xs → ⊥ +not-finite-and-infinite [] () +not-finite-and-infinite (x ∷ fin) (.x ∷ inf) = + not-finite-and-infinite fin (♭ inf) diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda new file mode 100644 index 0000000..a2e1a37 --- /dev/null +++ b/src/Codata/Musical/Colist/Infinite-merge.agda @@ -0,0 +1,213 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Infinite merge operation for coinductive lists +------------------------------------------------------------------------ + +module Codata.Musical.Colist.Infinite-merge where + +open import Codata.Musical.Notation +open import Codata.Musical.Colist as Colist hiding (_⋎_) +open import Data.Nat +open import Data.Nat.Properties +open import Data.Product as Prod +open import Data.Sum +open import Data.Sum.Properties +open import Data.Sum.Relation.Pointwise +open import Function +open import Function.Equality using (_⟨$⟩_) +open import Function.Inverse as Inv using (_↔_; Inverse; inverse) +import Function.Related as Related +open import Function.Related.TypeIsomorphisms +open import Induction.Nat using (<′-wellFounded) +import Induction.WellFounded as WF +open import Relation.Binary.PropositionalEquality as P using (_≡_) + +------------------------------------------------------------------------ +-- Some code that is used to work around Agda's syntactic guardedness +-- checker. + +private + + infixr 5 _∷_ _⋎_ + + data ColistP {a} (A : Set a) : Set a where + [] : ColistP A + _∷_ : A → ∞ (ColistP A) → ColistP A + _⋎_ : ColistP A → ColistP A → ColistP A + + data ColistW {a} (A : Set a) : Set a where + [] : ColistW A + _∷_ : A → ColistP A → ColistW A + + program : ∀ {a} {A : Set a} → Colist A → ColistP A + program [] = [] + program (x ∷ xs) = x ∷ ♯ program (♭ xs) + + mutual + + _⋎W_ : ∀ {a} {A : Set a} → ColistW A → ColistP A → ColistW A + [] ⋎W ys = whnf ys + (x ∷ xs) ⋎W ys = x ∷ (ys ⋎ xs) + + whnf : ∀ {a} {A : Set a} → ColistP A → ColistW A + whnf [] = [] + whnf (x ∷ xs) = x ∷ ♭ xs + whnf (xs ⋎ ys) = whnf xs ⋎W ys + + mutual + + ⟦_⟧P : ∀ {a} {A : Set a} → ColistP A → Colist A + ⟦ xs ⟧P = ⟦ whnf xs ⟧W + + ⟦_⟧W : ∀ {a} {A : Set a} → ColistW A → Colist A + ⟦ [] ⟧W = [] + ⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧P + + mutual + + ⋎-homP : ∀ {a} {A : Set a} (xs : ColistP A) {ys} → + ⟦ xs ⋎ ys ⟧P ≈ ⟦ xs ⟧P Colist.⋎ ⟦ ys ⟧P + ⋎-homP xs = ⋎-homW (whnf xs) _ + + ⋎-homW : ∀ {a} {A : Set a} (xs : ColistW A) ys → + ⟦ xs ⋎W ys ⟧W ≈ ⟦ xs ⟧W Colist.⋎ ⟦ ys ⟧P + ⋎-homW (x ∷ xs) ys = x ∷ ♯ ⋎-homP ys + ⋎-homW [] ys = begin ⟦ ys ⟧P ∎ + where open ≈-Reasoning + + ⟦program⟧P : ∀ {a} {A : Set a} (xs : Colist A) → + ⟦ program xs ⟧P ≈ xs + ⟦program⟧P [] = [] + ⟦program⟧P (x ∷ xs) = x ∷ ♯ ⟦program⟧P (♭ xs) + + Any-⋎P : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} → + Any P ⟦ program xs ⋎ ys ⟧P ↔ (Any P xs ⊎ Any P ⟦ ys ⟧P) + Any-⋎P {P = P} xs {ys} = + Any P ⟦ program xs ⋎ ys ⟧P ↔⟨ Any-cong Inv.id (⋎-homP (program xs)) ⟩ + Any P (⟦ program xs ⟧P Colist.⋎ ⟦ ys ⟧P) ↔⟨ Any-⋎ _ ⟩ + (Any P ⟦ program xs ⟧P ⊎ Any P ⟦ ys ⟧P) ↔⟨ Any-cong Inv.id (⟦program⟧P _) ⊎-cong (_ ∎) ⟩ + (Any P xs ⊎ Any P ⟦ ys ⟧P) ∎ + where open Related.EquationalReasoning + + index-Any-⋎P : + ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} + (p : Any P ⟦ program xs ⋎ ys ⟧P) → + index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎P xs) ⟨$⟩ p) + index-Any-⋎P xs p + with Any-resp id (⋎-homW (whnf (program xs)) _) p + | index-Any-resp {f = id} (⋎-homW (whnf (program xs)) _) p + index-Any-⋎P xs p | q | q≡p + with Inverse.to (Any-⋎ ⟦ program xs ⟧P) ⟨$⟩ q + | index-Any-⋎ ⟦ program xs ⟧P q + index-Any-⋎P xs p | q | q≡p | inj₂ r | r≤q rewrite q≡p = r≤q + index-Any-⋎P xs p | q | q≡p | inj₁ r | r≤q + with Any-resp id (⟦program⟧P xs) r + | index-Any-resp {f = id} (⟦program⟧P xs) r + index-Any-⋎P xs p | q | q≡p | inj₁ r | r≤q | s | s≡r + rewrite s≡r | q≡p = r≤q + +------------------------------------------------------------------------ +-- Infinite variant of _⋎_. + +private + + merge′ : ∀ {a} {A : Set a} → Colist (A × Colist A) → ColistP A + merge′ [] = [] + merge′ ((x , xs) ∷ xss) = x ∷ ♯ (program xs ⋎ merge′ (♭ xss)) + +merge : ∀ {a} {A : Set a} → Colist (A × Colist A) → Colist A +merge xss = ⟦ merge′ xss ⟧P + +------------------------------------------------------------------------ +-- Any lemma for merge. + +module _ {a p} {A : Set a} {P : A → Set p} where + + Any-merge : ∀ xss → Any P (merge xss) ↔ Any (λ { (x , xs) → P x ⊎ Any P xs }) xss + Any-merge xss = inverse (proj₁ ∘ to xss) from (proj₂ ∘ to xss) to∘from + where + open P.≡-Reasoning + + -- The from function. + + Q = λ { (x , xs) → P x ⊎ Any P xs } + + from : ∀ {xss} → Any Q xss → Any P (merge xss) + from (here (inj₁ p)) = here p + from (here (inj₂ p)) = there (Inverse.from (Any-⋎P _) ⟨$⟩ inj₁ p) + from (there {x = _ , xs} p) = there (Inverse.from (Any-⋎P xs) ⟨$⟩ inj₂ (from p)) + + -- The from function is injective. + + from-injective : ∀ {xss} (p₁ p₂ : Any Q xss) → + from p₁ ≡ from p₂ → p₁ ≡ p₂ + from-injective (here (inj₁ p)) (here (inj₁ .p)) P.refl = P.refl + from-injective (here (inj₁ _)) (here (inj₂ _)) () + from-injective (here (inj₂ _)) (here (inj₁ _)) () + from-injective (here (inj₂ p₁)) (here (inj₂ p₂)) eq = + P.cong (here ∘ inj₂) $ + inj₁-injective $ + Inverse.injective (Inv.sym (Any-⋎P _)) {x = inj₁ p₁} {y = inj₁ p₂} $ + there-injective eq + from-injective (here (inj₁ _)) (there _) () + from-injective (here (inj₂ p₁)) (there p₂) eq + with Inverse.injective (Inv.sym (Any-⋎P _)) + {x = inj₁ p₁} {y = inj₂ (from p₂)} + (there-injective eq) + ... | () + from-injective (there _) (here (inj₁ _)) () + from-injective (there p₁) (here (inj₂ p₂)) eq + with Inverse.injective (Inv.sym (Any-⋎P _)) + {x = inj₂ (from p₁)} {y = inj₁ p₂} + (there-injective eq) + ... | () + from-injective (there {x = _ , xs} p₁) (there p₂) eq = + P.cong there $ + from-injective p₁ p₂ $ + inj₂-injective $ + Inverse.injective (Inv.sym (Any-⋎P xs)) + {x = inj₂ (from p₁)} {y = inj₂ (from p₂)} $ + there-injective eq + + -- The to function (defined as a right inverse of from). + + Input = ∃ λ xss → Any P (merge xss) + + Pred : Input → Set _ + Pred (xss , p) = ∃ λ (q : Any Q xss) → from q ≡ p + + to : ∀ xss p → Pred (xss , p) + to = λ xss p → + WF.All.wfRec (WF.Inverse-image.wellFounded size <′-wellFounded) _ + Pred step (xss , p) + where + size : Input → ℕ + size (_ , p) = index p + + step : ∀ p → WF.WfRec (_<′_ on size) Pred p → Pred p + step ([] , ()) rec + step ((x , xs) ∷ xss , here p) rec = here (inj₁ p) , P.refl + step ((x , xs) ∷ xss , there p) rec + with Inverse.to (Any-⋎P xs) ⟨$⟩ p + | Inverse.left-inverse-of (Any-⋎P xs) p + | index-Any-⋎P xs p + ... | inj₁ q | P.refl | _ = here (inj₂ q) , P.refl + ... | inj₂ q | P.refl | q≤p = + Prod.map there + (P.cong (there ∘ _⟨$⟩_ (Inverse.from (Any-⋎P xs)) ∘ inj₂)) + (rec (♭ xss , q) (s≤′s q≤p)) + + to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p))) + +-- Every member of xss is a member of merge xss, and vice versa (with +-- equal multiplicities). + +∈-merge : ∀ {a} {A : Set a} {y : A} xss → + y ∈ merge xss ↔ ∃₂ λ x xs → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs) +∈-merge {y = y} xss = + y ∈ merge xss ↔⟨ Any-merge _ ⟩ + Any (λ { (x , xs) → y ≡ x ⊎ y ∈ xs }) xss ↔⟨ Any-∈ ⟩ + (∃ λ { (x , xs) → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs) }) ↔⟨ Σ-assoc ⟩ + (∃₂ λ x xs → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs)) ∎ + where open Related.EquationalReasoning diff --git a/src/Codata/Musical/Conat.agda b/src/Codata/Musical/Conat.agda new file mode 100644 index 0000000..ced828d --- /dev/null +++ b/src/Codata/Musical/Conat.agda @@ -0,0 +1,86 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Coinductive "natural" numbers +------------------------------------------------------------------------ + +module Codata.Musical.Conat where + +open import Codata.Musical.Notation +open import Data.Nat.Base using (ℕ; zero; suc) +open import Function +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as P using (_≡_) + +------------------------------------------------------------------------ +-- The type + +data Coℕ : Set where + zero : Coℕ + suc : (n : ∞ Coℕ) → Coℕ + +module Coℕ-injective where + + suc-injective : ∀ {m n} → (Coℕ ∋ suc m) ≡ suc n → m ≡ n + suc-injective P.refl = P.refl + +------------------------------------------------------------------------ +-- Some operations + +pred : Coℕ → Coℕ +pred zero = zero +pred (suc n) = ♭ n + +fromℕ : ℕ → Coℕ +fromℕ zero = zero +fromℕ (suc n) = suc (♯ fromℕ n) + +fromℕ-injective : ∀ {m n} → fromℕ m ≡ fromℕ n → m ≡ n +fromℕ-injective {zero} {zero} eq = P.refl +fromℕ-injective {zero} {suc n} () +fromℕ-injective {suc m} {zero} () +fromℕ-injective {suc m} {suc n} eq = P.cong suc (fromℕ-injective (P.cong pred eq)) + +∞ℕ : Coℕ +∞ℕ = suc (♯ ∞ℕ) + +infixl 6 _+_ + +_+_ : Coℕ → Coℕ → Coℕ +zero + n = n +suc m + n = suc (♯ (♭ m + n)) + +------------------------------------------------------------------------ +-- Equality + +data _≈_ : Coℕ → Coℕ → Set where + zero : zero ≈ zero + suc : ∀ {m n} (m≈n : ∞ (♭ m ≈ ♭ n)) → suc m ≈ suc n + +module ≈-injective where + + suc-injective : ∀ {m n p q} → (suc m ≈ suc n ∋ suc p) ≡ suc q → p ≡ q + suc-injective P.refl = P.refl + +setoid : Setoid _ _ +setoid = record + { Carrier = Coℕ + ; _≈_ = _≈_ + ; isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + } + where + refl : Reflexive _≈_ + refl {zero} = zero + refl {suc n} = suc (♯ refl) + + sym : Symmetric _≈_ + sym zero = zero + sym (suc m≈n) = suc (♯ sym (♭ m≈n)) + + trans : Transitive _≈_ + trans zero zero = zero + trans (suc m≈n) (suc n≈k) = suc (♯ trans (♭ m≈n) (♭ n≈k)) diff --git a/src/Codata/Musical/Costring.agda b/src/Codata/Musical/Costring.agda new file mode 100644 index 0000000..30092bf --- /dev/null +++ b/src/Codata/Musical/Costring.agda @@ -0,0 +1,22 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Costrings +------------------------------------------------------------------------ + +module Codata.Musical.Costring where + +open import Codata.Musical.Colist as Colist using (Colist) +open import Data.Char using (Char) +open import Data.String as String using (String) +open import Function using (_∘_) + +-- Possibly infinite strings. + +Costring : Set +Costring = Colist Char + +-- Methods + +toCostring : String → Costring +toCostring = Colist.fromList ∘ String.toList diff --git a/src/Codata/Musical/Covec.agda b/src/Codata/Musical/Covec.agda new file mode 100644 index 0000000..bb9d586 --- /dev/null +++ b/src/Codata/Musical/Covec.agda @@ -0,0 +1,166 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Coinductive vectors +------------------------------------------------------------------------ + +module Codata.Musical.Covec where + +open import Codata.Musical.Notation +open import Codata.Musical.Conat as Coℕ using (Coℕ; zero; suc; _+_) +open import Codata.Musical.Cofin using (Cofin; zero; suc) +open import Codata.Musical.Colist as Colist using (Colist; []; _∷_) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Vec using (Vec; []; _∷_) +open import Data.Product using (_,_) +open import Function using (_∋_) +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as P using (_≡_) + +------------------------------------------------------------------------ +-- The type + +infixr 5 _∷_ +data Covec {a} (A : Set a) : Coℕ → Set a where + [] : Covec A zero + _∷_ : ∀ {n} (x : A) (xs : ∞ (Covec A (♭ n))) → Covec A (suc n) + +module _ {a} {A : Set a} where + + ∷-injectiveˡ : ∀ {a b} {n} {as bs} → (Covec A (suc n) ∋ a ∷ as) ≡ b ∷ bs → a ≡ b + ∷-injectiveˡ P.refl = P.refl + + ∷-injectiveʳ : ∀ {a b} {n} {as bs} → (Covec A (suc n) ∋ a ∷ as) ≡ b ∷ bs → as ≡ bs + ∷-injectiveʳ P.refl = P.refl + +------------------------------------------------------------------------ +-- Some operations + +map : ∀ {a b} {A : Set a} {B : Set b} {n} → (A → B) → Covec A n → Covec B n +map f [] = [] +map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs) + +module _ {a} {A : Set a} where + + fromVec : ∀ {n} → Vec A n → Covec A (Coℕ.fromℕ n) + fromVec [] = [] + fromVec (x ∷ xs) = x ∷ ♯ fromVec xs + + fromColist : (xs : Colist A) → Covec A (Colist.length xs) + fromColist [] = [] + fromColist (x ∷ xs) = x ∷ ♯ fromColist (♭ xs) + + take : ∀ m {n} → Covec A (m + n) → Covec A m + take zero xs = [] + take (suc n) (x ∷ xs) = x ∷ ♯ take (♭ n) (♭ xs) + + drop : ∀ m {n} → Covec A (Coℕ.fromℕ m + n) → Covec A n + drop zero xs = xs + drop (suc n) (x ∷ xs) = drop n (♭ xs) + + replicate : ∀ n → A → Covec A n + replicate zero x = [] + replicate (suc n) x = x ∷ ♯ replicate (♭ n) x + + lookup : ∀ {n} → Cofin n → Covec A n → A + lookup zero (x ∷ xs) = x + lookup (suc n) (x ∷ xs) = lookup n (♭ xs) + + infixr 5 _++_ + + _++_ : ∀ {m n} → Covec A m → Covec A n → Covec A (m + n) + [] ++ ys = ys + (x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys) + + [_] : A → Covec A (suc (♯ zero)) + [ x ] = x ∷ ♯ [] + +------------------------------------------------------------------------ +-- Equality and other relations + +-- xs ≈ ys means that xs and ys are equal. + + infix 4 _≈_ + + data _≈_ : ∀ {n} (xs ys : Covec A n) → Set where + [] : [] ≈ [] + _∷_ : ∀ {n} x {xs ys} + (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → _≈_ {n = suc n} (x ∷ xs) (x ∷ ys) + +-- x ∈ xs means that x is a member of xs. + + infix 4 _∈_ + + data _∈_ : ∀ {n} → A → Covec A n → Set where + here : ∀ {n x } {xs} → _∈_ {n = suc n} x (x ∷ xs) + there : ∀ {n x y} {xs} (x∈xs : x ∈ ♭ xs) → _∈_ {n = suc n} x (y ∷ xs) + +-- xs ⊑ ys means that xs is a prefix of ys. + + infix 4 _⊑_ + + data _⊑_ : ∀ {m n} → Covec A m → Covec A n → Set where + [] : ∀ {n} {ys : Covec A n} → [] ⊑ ys + _∷_ : ∀ {m n} x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → + _⊑_ {m = suc m} {suc n} (x ∷ xs) (x ∷ ys) + +------------------------------------------------------------------------ +-- Some proofs + +setoid : ∀ {a} → Set a → Coℕ → Setoid _ _ +setoid A n = record + { Carrier = Covec A n + ; _≈_ = _≈_ + ; isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + } + where + refl : ∀ {n} → Reflexive (_≈_ {n = n}) + refl {x = []} = [] + refl {x = x ∷ xs} = x ∷ ♯ refl + + sym : ∀ {n} → Symmetric (_≈_ {A = A} {n}) + sym [] = [] + sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈) + + trans : ∀ {n} → Transitive (_≈_ {A = A} {n}) + trans [] [] = [] + trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈) + +poset : ∀ {a} → Set a → Coℕ → Poset _ _ _ +poset A n = record + { Carrier = Covec A n + ; _≈_ = _≈_ + ; _≤_ = _⊑_ + ; isPartialOrder = record + { isPreorder = record + { isEquivalence = Setoid.isEquivalence (setoid A n) + ; reflexive = reflexive + ; trans = trans + } + ; antisym = antisym + } + } + where + reflexive : ∀ {n} → _≈_ {n = n} ⇒ _⊑_ + reflexive [] = [] + reflexive (x ∷ xs≈) = x ∷ ♯ reflexive (♭ xs≈) + + trans : ∀ {n} → Transitive (_⊑_ {n = n}) + trans [] _ = [] + trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈) + + antisym : ∀ {n} → Antisymmetric (_≈_ {n = n}) _⊑_ + antisym [] [] = [] + antisym (x ∷ p₁) (.x ∷ p₂) = x ∷ ♯ antisym (♭ p₁) (♭ p₂) + +map-cong : ∀ {a b} {A : Set a} {B : Set b} {n} (f : A → B) → _≈_ {n = n} =[ map f ]⇒ _≈_ +map-cong f [] = [] +map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈) + +take-⊑ : ∀ {a} {A : Set a} m {n} (xs : Covec A (m + n)) → take m xs ⊑ xs +take-⊑ zero xs = [] +take-⊑ (suc n) (x ∷ xs) = x ∷ ♯ take-⊑ (♭ n) (♭ xs) diff --git a/src/Codata/Musical/M.agda b/src/Codata/Musical/M.agda new file mode 100644 index 0000000..3ae867a --- /dev/null +++ b/src/Codata/Musical/M.agda @@ -0,0 +1,45 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- M-types (the dual of W-types) +------------------------------------------------------------------------ + +module Codata.Musical.M where + +open import Codata.Musical.Notation +open import Level +open import Data.Product hiding (map) +open import Data.Container.Core + +-- The family of M-types. + +data M {s p} (C : Container s p) : Set (s ⊔ p) where + inf : ⟦ C ⟧ (∞ (M C)) → M C + +-- Projections. + +module _ {s p} (C : Container s p) (open Container C) where + + head : M C → Shape + head (inf (x , _)) = x + + tail : (x : M C) → Position (head x) → M C + tail (inf (x , f)) b = ♭ (f b) + +-- map + +module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} + (m : C₁ ⇒ C₂) where + + map : M C₁ → M C₂ + map (inf (x , f)) = inf (shape m x , λ p → ♯ map (♭ (f (position m p)))) + + +-- unfold + +module _ {s p ℓ} {C : Container s p} (open Container C) + {S : Set ℓ} (alg : S → ⟦ C ⟧ S) where + + unfold : S → M C + unfold seed = let (x , f) = alg seed in + inf (x , λ p → ♯ unfold (f p)) diff --git a/src/Codata/Musical/M/Indexed.agda b/src/Codata/Musical/M/Indexed.agda new file mode 100644 index 0000000..3455769 --- /dev/null +++ b/src/Codata/Musical/M/Indexed.agda @@ -0,0 +1,42 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Indexed M-types (the dual of indexed W-types aka Petersson-Synek +-- trees). +------------------------------------------------------------------------ + +module Codata.Musical.M.Indexed where + +open import Level +open import Codata.Musical.Notation +open import Data.Product +open import Data.Container.Indexed.Core +open import Function +open import Relation.Unary + +-- The family of indexed M-types. + +module _ {ℓ c r} {O : Set ℓ} (C : Container O O c r) where + + data M (o : O) : Set (ℓ ⊔ c ⊔ r) where + inf : ⟦ C ⟧ (∞ ∘ M) o → M o + + open Container C + + -- Projections. + + head : M ⊆ Command + head (inf (c , _)) = c + + tail : ∀ {o} (m : M o) (r : Response (head m)) → M (next (head m) r) + tail (inf (_ , k)) r = ♭ (k r) + + force : M ⊆ ⟦ C ⟧ M + force (inf (c , k)) = c , λ r → ♭ (k r) + + -- Coiteration. + + coit : ∀ {ℓ} {X : Pred O ℓ} → X ⊆ ⟦ C ⟧ X → X ⊆ M + coit ψ x = inf (proj₁ cs , λ r → ♯ coit ψ (proj₂ cs r)) + where + cs = ψ x diff --git a/src/Codata/Musical/Notation.agda b/src/Codata/Musical/Notation.agda new file mode 100644 index 0000000..c5d13f3 --- /dev/null +++ b/src/Codata/Musical/Notation.agda @@ -0,0 +1,9 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Basic types related to coinduction +------------------------------------------------------------------------ + +module Codata.Musical.Notation where + +open import Agda.Builtin.Coinduction public diff --git a/src/Codata/Musical/Stream.agda b/src/Codata/Musical/Stream.agda new file mode 100644 index 0000000..de1dc9a --- /dev/null +++ b/src/Codata/Musical/Stream.agda @@ -0,0 +1,165 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Streams +------------------------------------------------------------------------ + +module Codata.Musical.Stream where + +open import Codata.Musical.Notation +open import Codata.Musical.Colist using (Colist; []; _∷_) +open import Data.Vec using (Vec; []; _∷_) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as P using (_≡_) + +------------------------------------------------------------------------ +-- The type + +infixr 5 _∷_ + +data Stream {a} (A : Set a) : Set a where + _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A + +{-# FOREIGN GHC + data AgdaStream a = Cons a (MAlonzo.RTE.Inf (AgdaStream a)) + type AgdaStream' l a = AgdaStream a + #-} +{-# COMPILE GHC Stream = data AgdaStream' (Cons) #-} + +------------------------------------------------------------------------ +-- Some operations + +head : ∀ {a} {A : Set a} → Stream A → A +head (x ∷ xs) = x + +tail : ∀ {a} {A : Set a} → Stream A → Stream A +tail (x ∷ xs) = ♭ xs + +map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Stream A → Stream B +map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs) + +zipWith : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → + (A → B → C) → Stream A → Stream B → Stream C +zipWith _∙_ (x ∷ xs) (y ∷ ys) = (x ∙ y) ∷ ♯ zipWith _∙_ (♭ xs) (♭ ys) + +take : ∀ {a} {A : Set a} n → Stream A → Vec A n +take zero xs = [] +take (suc n) (x ∷ xs) = x ∷ take n (♭ xs) + +drop : ∀ {a} {A : Set a} → ℕ → Stream A → Stream A +drop zero xs = xs +drop (suc n) (x ∷ xs) = drop n (♭ xs) + +repeat : ∀ {a} {A : Set a} → A → Stream A +repeat x = x ∷ ♯ repeat x + +iterate : ∀ {a} {A : Set a} → (A → A) → A → Stream A +iterate f x = x ∷ ♯ iterate f (f x) + +-- Interleaves the two streams. + +infixr 5 _⋎_ + +_⋎_ : ∀ {a} {A : Set a} → Stream A → Stream A → Stream A +(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs) + +mutual + + -- Takes every other element from the stream, starting with the + -- first one. + + evens : ∀ {a} {A : Set a} → Stream A → Stream A + evens (x ∷ xs) = x ∷ ♯ odds (♭ xs) + + -- Takes every other element from the stream, starting with the + -- second one. + + odds : ∀ {a} {A : Set a} → Stream A → Stream A + odds (x ∷ xs) = evens (♭ xs) + +toColist : ∀ {a} {A : Set a} → Stream A → Colist A +toColist (x ∷ xs) = x ∷ ♯ toColist (♭ xs) + +lookup : ∀ {a} {A : Set a} → ℕ → Stream A → A +lookup zero (x ∷ xs) = x +lookup (suc n) (x ∷ xs) = lookup n (♭ xs) + +infixr 5 _++_ + +_++_ : ∀ {a} {A : Set a} → Colist A → Stream A → Stream A +[] ++ ys = ys +(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys) + +------------------------------------------------------------------------ +-- Equality and other relations + +-- xs ≈ ys means that xs and ys are equal. + +infix 4 _≈_ + +data _≈_ {a} {A : Set a} : Stream A → Stream A → Set a where + _∷_ : ∀ {x y xs ys} + (x≡ : x ≡ y) (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ y ∷ ys + +-- x ∈ xs means that x is a member of xs. + +infix 4 _∈_ + +data _∈_ {a} {A : Set a} : A → Stream A → Set a where + here : ∀ {x xs} → x ∈ x ∷ xs + there : ∀ {x y xs} (x∈xs : x ∈ ♭ xs) → x ∈ y ∷ xs + +-- xs ⊑ ys means that xs is a prefix of ys. + +infix 4 _⊑_ + +data _⊑_ {a} {A : Set a} : Colist A → Stream A → Set a where + [] : ∀ {ys} → [] ⊑ ys + _∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys + +------------------------------------------------------------------------ +-- Some proofs + +setoid : ∀ {a} → Set a → Setoid _ _ +setoid A = record + { Carrier = Stream A + ; _≈_ = _≈_ {A = A} + ; isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + } + where + refl : Reflexive _≈_ + refl {_ ∷ _} = P.refl ∷ ♯ refl + + sym : Symmetric _≈_ + sym (x≡ ∷ xs≈) = P.sym x≡ ∷ ♯ sym (♭ xs≈) + + trans : Transitive _≈_ + trans (x≡ ∷ xs≈) (y≡ ∷ ys≈) = P.trans x≡ y≡ ∷ ♯ trans (♭ xs≈) (♭ ys≈) + +head-cong : ∀ {a} {A : Set a} {xs ys : Stream A} → xs ≈ ys → head xs ≡ head ys +head-cong (x≡ ∷ _) = x≡ + +tail-cong : ∀ {a} {A : Set a} {xs ys : Stream A} → xs ≈ ys → tail xs ≈ tail ys +tail-cong (_ ∷ xs≈) = ♭ xs≈ + +map-cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {xs ys} → + xs ≈ ys → map f xs ≈ map f ys +map-cong f (x≡ ∷ xs≈) = P.cong f x≡ ∷ ♯ map-cong f (♭ xs≈) + +zipWith-cong : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} + (_∙_ : A → B → C) {xs xs′ ys ys′} → + xs ≈ xs′ → ys ≈ ys′ → + zipWith _∙_ xs ys ≈ zipWith _∙_ xs′ ys′ +zipWith-cong _∙_ (x≡ ∷ xs≈) (y≡ ∷ ys≈) = + P.cong₂ _∙_ x≡ y≡ ∷ ♯ zipWith-cong _∙_ (♭ xs≈) (♭ ys≈) + +infixr 5 _⋎-cong_ + +_⋎-cong_ : ∀ {a} {A : Set a} {xs xs′ ys ys′ : Stream A} → + xs ≈ xs′ → ys ≈ ys′ → xs ⋎ ys ≈ xs′ ⋎ ys′ +(x ∷ xs≈) ⋎-cong ys≈ = x ∷ ♯ (ys≈ ⋎-cong ♭ xs≈) diff --git a/src/Codata/Stream.agda b/src/Codata/Stream.agda new file mode 100644 index 0000000..306229a --- /dev/null +++ b/src/Codata/Stream.agda @@ -0,0 +1,97 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The Stream type and some operations +------------------------------------------------------------------------ + +module Codata.Stream where + +open import Size +open import Codata.Thunk as Thunk using (Thunk; force) + +open import Data.Nat.Base +open import Data.List.Base using (List; []; _∷_) +open import Data.List.NonEmpty using (List⁺; _∷_) +open import Data.Vec using (Vec; []; _∷_) +open import Data.Product as P hiding (map) + +------------------------------------------------------------------------ +-- Definition + +data Stream {ℓ} (A : Set ℓ) (i : Size) : Set ℓ where + _∷_ : A → Thunk (Stream A) i → Stream A i + +module _ {ℓ} {A : Set ℓ} where + + repeat : ∀ {i} → A → Stream A i + repeat a = a ∷ λ where .force → repeat a + + head : ∀ {i} → Stream A i → A + head (x ∷ xs) = x + + tail : Stream A ∞ → Stream A ∞ + tail (x ∷ xs) = xs .force + + lookup : ℕ → Stream A ∞ → A + lookup zero xs = head xs + lookup (suc k) xs = lookup k (tail xs) + + take : (n : ℕ) → Stream A ∞ → Vec A n + take zero xs = [] + take (suc n) xs = head xs ∷ take n (tail xs) + + infixr 5 _++_ _⁺++_ + _++_ : ∀ {i} → List A → Stream A i → Stream A i + [] ++ ys = ys + (x ∷ xs) ++ ys = x ∷ λ where .force → xs ++ ys + + _⁺++_ : ∀ {i} → List⁺ A → Thunk (Stream A) i → Stream A i + (x ∷ xs) ⁺++ ys = x ∷ λ where .force → xs ++ ys .force + + cycle : ∀ {i} → List⁺ A → Stream A i + cycle xs = xs ⁺++ λ where .force → cycle xs + + concat : ∀ {i} → Stream (List⁺ A) i → Stream A i + concat (xs ∷ xss) = xs ⁺++ λ where .force → concat (xss .force) + +module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where + + map : ∀ {i} → (A → B) → Stream A i → Stream B i + map f (x ∷ xs) = f x ∷ λ where .force → map f (xs .force) + + ap : ∀ {i} → Stream (A → B) i → Stream A i → Stream B i + ap (f ∷ fs) (x ∷ xs) = f x ∷ λ where .force → ap (fs .force) (xs .force) + + unfold : ∀ {i} → (A → A × B) → A → Stream B i + unfold next seed = + let (seed′ , b) = next seed in + b ∷ λ where .force → unfold next seed′ + + scanl : ∀ {i} → (B → A → B) → B → Stream A i → Stream B i + scanl c n (x ∷ xs) = n ∷ λ where .force → scanl c (c n x) (xs .force) + +module _ {ℓ ℓ₁ ℓ₂} {A : Set ℓ} {B : Set ℓ₁} {C : Set ℓ₂} where + + zipWith : ∀ {i} → (A → B → C) → Stream A i → Stream B i → Stream C i + zipWith f (a ∷ as) (b ∷ bs) = f a b ∷ λ where .force → zipWith f (as .force) (bs .force) + +module _ {ℓ} {A : Set ℓ} where + + iterate : ∀ {i} → (A → A) → A → Stream A i + iterate f a = a ∷ λ where .force → map f (iterate f a) + + + +------------------------------------------------------------------------ +-- Legacy + +open import Codata.Musical.Notation using (♭; ♯_) +import Codata.Musical.Stream as M + +module _ {a} {A : Set a} where + + fromMusical : ∀ {i} → M.Stream A → Stream A i + fromMusical (x M.∷ xs) = x ∷ λ where .force → fromMusical (♭ xs) + + toMusical : Stream A ∞ → M.Stream A + toMusical (x ∷ xs) = x M.∷ ♯ toMusical (xs .force) diff --git a/src/Codata/Stream/Bisimilarity.agda b/src/Codata/Stream/Bisimilarity.agda new file mode 100644 index 0000000..998defa --- /dev/null +++ b/src/Codata/Stream/Bisimilarity.agda @@ -0,0 +1,55 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bisimilarity for Streams +------------------------------------------------------------------------ + +module Codata.Stream.Bisimilarity where + +open import Size +open import Codata.Thunk +open import Codata.Stream +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as Eq using (_≡_) + +data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) i : + (xs : Stream A ∞) (ys : Stream B ∞) → Set r where + _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R) i xs ys → + Bisim R i (x ∷ xs) (y ∷ ys) + +module _ {a r} {A : Set a} {R : A → A → Set r} where + + reflexive : Reflexive R → ∀ {i} → Reflexive (Bisim R i) + reflexive refl^R {i} {r ∷ rs} = refl^R ∷ λ where .force → reflexive refl^R + +module _ {a b} {A : Set a} {B : Set b} + {r} {P : A → B → Set r} {Q : B → A → Set r} where + + symmetric : Sym P Q → ∀ {i} → Sym (Bisim P i) (Bisim Q i) + symmetric sym^PQ (p ∷ ps) = sym^PQ p ∷ λ where .force → symmetric sym^PQ (ps .force) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} + {r} {P : A → B → Set r} {Q : B → C → Set r} {R : A → C → Set r} where + + transitive : Trans P Q R → ∀ {i} → Trans (Bisim P i) (Bisim Q i) (Bisim R i) + transitive trans^PQR (p ∷ ps) (q ∷ qs) = + trans^PQR p q ∷ λ where .force → transitive trans^PQR (ps .force) (qs .force) + + +-- Pointwise Equality as a Bisimilarity +------------------------------------------------------------------------ + +module _ {ℓ} {A : Set ℓ} where + + infix 1 _⊢_≈_ + _⊢_≈_ : ∀ i → Stream A ∞ → Stream A ∞ → Set ℓ + _⊢_≈_ = Bisim _≡_ + + refl : ∀ {i} → Reflexive (i ⊢_≈_) + refl = reflexive Eq.refl + + sym : ∀ {i} → Symmetric (i ⊢_≈_) + sym = symmetric Eq.sym + + trans : ∀ {i} → Transitive (i ⊢_≈_) + trans = transitive Eq.trans diff --git a/src/Codata/Stream/Categorical.agda b/src/Codata/Stream/Categorical.agda new file mode 100644 index 0000000..9144274 --- /dev/null +++ b/src/Codata/Stream/Categorical.agda @@ -0,0 +1,29 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A categorical view of Stream +------------------------------------------------------------------------ + +module Codata.Stream.Categorical where + +open import Data.Product using (<_,_>) +open import Codata.Stream +open import Function +open import Category.Functor +open import Category.Applicative +open import Category.Comonad + +functor : ∀ {ℓ i} → RawFunctor {ℓ} (λ A → Stream A i) +functor = record { _<$>_ = λ f → map f } + +applicative : ∀ {ℓ i} → RawApplicative {ℓ} (λ A → Stream A i) +applicative = record + { pure = repeat + ; _⊛_ = ap + } + +comonad : ∀ {ℓ} → RawComonad {ℓ} (λ A → Stream A _) +comonad = record + { extract = head + ; extend = unfold ∘′ < tail ,_> + } diff --git a/src/Codata/Stream/Properties.agda b/src/Codata/Stream/Properties.agda new file mode 100644 index 0000000..09ea262 --- /dev/null +++ b/src/Codata/Stream/Properties.agda @@ -0,0 +1,55 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of operations on the Stream type +------------------------------------------------------------------------ + +module Codata.Stream.Properties where + +open import Size +open import Data.Nat.Base +import Data.Vec as Vec +open import Codata.Thunk using (Thunk; force) +open import Codata.Stream +open import Codata.Stream.Bisimilarity +open import Function +open import Relation.Binary.PropositionalEquality as Eq using (_≡_) + +module _ {a b} {A : Set a} {B : Set b} where + + lookup-repeat-identity : (n : ℕ) (a : A) → lookup n (repeat a) ≡ a + lookup-repeat-identity zero a = Eq.refl + lookup-repeat-identity (suc n) a = lookup-repeat-identity n a + + take-repeat-identity : (n : ℕ) (a : A) → take n (repeat a) ≡ Vec.replicate a + take-repeat-identity zero a = Eq.refl + take-repeat-identity (suc n) a = Eq.cong (a Vec.∷_) (take-repeat-identity n a) + +module _ {a b} {A : Set a} {B : Set b} where + + map-repeat-commute : ∀ (f : A → B) a {i} → i ⊢ map f (repeat a) ≈ repeat (f a) + map-repeat-commute f a = Eq.refl ∷ λ where .force → map-repeat-commute f a + + repeat-ap-identity : ∀ (f : A → B) as {i} → i ⊢ ap (repeat f) as ≈ map f as + repeat-ap-identity f (a ∷ as) = Eq.refl ∷ λ where .force → repeat-ap-identity f (as .force) + + ap-repeat-identity : ∀ (fs : Stream (A → B) ∞) (a : A) {i} → i ⊢ ap fs (repeat a) ≈ map (_$ a) fs + ap-repeat-identity (f ∷ fs) a = Eq.refl ∷ λ where .force → ap-repeat-identity (fs .force) a + + ap-repeat-commute : ∀ (f : A → B) a {i} → i ⊢ ap (repeat f) (repeat a) ≈ repeat (f a) + ap-repeat-commute f a = Eq.refl ∷ λ where .force → ap-repeat-commute f a + + +-- Functor laws + +module _ {a} {A : Set a} where + + map-identity : ∀ (as : Stream A ∞) {i} → i ⊢ map id as ≈ as + map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force) + + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where + + map-map-fusion : ∀ (f : A → B) (g : B → C) as {i} → i ⊢ map g (map f as) ≈ map (g ∘ f) as + map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force) + diff --git a/src/Codata/Thunk.agda b/src/Codata/Thunk.agda new file mode 100644 index 0000000..2a6a255 --- /dev/null +++ b/src/Codata/Thunk.agda @@ -0,0 +1,57 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The Thunk wrappers for sized codata, copredicates and corelations +------------------------------------------------------------------------ + +module Codata.Thunk where + +open import Size +open import Relation.Unary + +------------------------------------------------------------------------ +-- Basic types. + +record Thunk {ℓ} (F : Size → Set ℓ) (i : Size) : Set ℓ where + coinductive + field force : {j : Size< i} → F j +open Thunk public + +Thunk^P : ∀ {f p} {F : Size → Set f} (P : Size → F ∞ → Set p) + (i : Size) (tf : Thunk F ∞) → Set p +Thunk^P P i tf = Thunk (λ i → P i (tf .force)) i + +Thunk^R : ∀ {f g r} {F : Size → Set f} {G : Size → Set g} + (R : Size → F ∞ → G ∞ → Set r) + (i : Size) (tf : Thunk F ∞) (tg : Thunk G ∞) → Set r +Thunk^R R i tf tg = Thunk (λ i → R i (tf .force) (tg .force)) i + +------------------------------------------------------------------------ +-- Basic functions. + +-- Thunk is a functor +module _ {p q} {P : Size → Set p} {Q : Size → Set q} where + + map : ∀[ P ⇒ Q ] → ∀[ Thunk P ⇒ Thunk Q ] + map f p .force = f (p .force) + +-- Thunk is a comonad +module _ {p} {P : Size → Set p} where + + extract : ∀[ Thunk P ] → P ∞ + extract p = p .force + + duplicate : ∀[ Thunk P ⇒ Thunk (Thunk P) ] + duplicate p .force .force = p .force + +module _ {p q} {P : Size → Set p} {Q : Size → Set q} where + + infixl 1 _<*>_ + _<*>_ : ∀[ Thunk (P ⇒ Q) ⇒ Thunk P ⇒ Thunk Q ] + (f <*> p) .force = f .force (p .force) + +-- We can take cofixpoints of functions only making Thunk'd recursive calls +module _ {p} (P : Size → Set p) where + + cofix : ∀[ Thunk P ⇒ P ] → ∀[ P ] + cofix f = f λ where .force → cofix f |