diff options
Diffstat (limited to 'src/Codata/Musical')
| -rw-r--r-- | src/Codata/Musical/Cofin.agda | 47 | ||||
| -rw-r--r-- | src/Codata/Musical/Colist.agda | 535 | ||||
| -rw-r--r-- | src/Codata/Musical/Colist/Infinite-merge.agda | 213 | ||||
| -rw-r--r-- | src/Codata/Musical/Conat.agda | 86 | ||||
| -rw-r--r-- | src/Codata/Musical/Costring.agda | 22 | ||||
| -rw-r--r-- | src/Codata/Musical/Covec.agda | 166 | ||||
| -rw-r--r-- | src/Codata/Musical/M.agda | 45 | ||||
| -rw-r--r-- | src/Codata/Musical/M/Indexed.agda | 42 | ||||
| -rw-r--r-- | src/Codata/Musical/Notation.agda | 9 | ||||
| -rw-r--r-- | src/Codata/Musical/Stream.agda | 165 |
10 files changed, 1330 insertions, 0 deletions
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≈) |