Literate almost everything

parent fb943fef
......@@ -5,6 +5,7 @@ open import Function using (id)
open import Category.Functor using (RawFunctor)
open import Category.Applicative using (RawApplicative; module RawApplicative)
open import Category.Applicative.Indexed using (Morphism; module Morphism)
open Morphism using () renaming (op to opₐ; op-<$> to op-<$>ₐ)
open RawApplicative using (rawFunctor)
open import Category.NaturalT using (NaturalT)
......@@ -12,28 +13,21 @@ open import Category.NaturalT using (NaturalT)
-- the identity functor
%<*IdF>
\AgdaTarget{IdF}
%<*Id>
\AgdaTarget{Id}
\begin{code}
IdF : ∀ {ℓ} → RawFunctor {ℓ} id
IdF = record { _<$>_ = id }
Id : ∀ {ℓ} → RawFunctor {ℓ} id
Id = record { _<$>_ = id }
\end{code}
%</IdF>
%</Id>
-- transforms an applicative functor morphism into a regular natural transformation
%<*app-NaturalT>
\AgdaTarget{app-NaturalT}
\begin{code}
app-NaturalT : ∀ {ℓ} {F′ G′ : Set ℓ → Set ℓ} {F : RawApplicative F′} {G : RawApplicative G′}
app-NaturalT : ∀ {ℓ} {F′ G′ : Set ℓ → Set ℓ} {F : RawApplicative F′} {G : RawApplicative G′}
→ Morphism F G → NaturalT (rawFunctor F) (rawFunctor G)
app-NaturalT ηₐ = record { op = opₐ ηₐ; op-<$> = op-<$>ₐ ηₐ }
where open Morphism using () renaming (op to opₐ; op-<$> to op-<$>ₐ)
\end{code}
%</app-NaturalT>
%<*product-functor>
\begin{code}
\end{code}
%</product-functor>
......@@ -17,7 +17,7 @@ record NaturalT {ℓ} {F′ G′ : Set ℓ → Set ℓ} (F : RawFunctor F′) (G
open module F = RawFunctor F using () renaming (_<$>_ to _<$ᶠ>_)
open module G = RawFunctor G using () renaming (_<$>_ to _<$ᵍ>_)
field op : ∀ {X} → F′ X → G′ X
op-<$> : ∀ {X Y} (f : X → Y) x → op (f <$ᶠ> x) ≡ (f <$ᵍ> (op x))
op-<$> : ∀ {X Y} (f : X → Y) x → op (f <$ᶠ> x) ≡ (f <$ᵍ> (op x)) -- naturality
\end{code}
%</NaturalT>
......@@ -34,6 +34,6 @@ _∘⇓_ {F = F} {_} {H} ε η = record { op = op ε ∘ op η; op-<$> = ∘-<$
open NaturalT using (op; op-<$>)
∘-<$> : ∀ {X Y} (f : X → Y) x → (op ε ∘ op η) (f <$ᶠ> x) ≡ (f <$ʰ> ((op ε ∘ op η) x))
∘-<$> f x rewrite op-<$> η f x = op-<$> ε f (op η x)
∘-<$> f x rewrite op-<$> η f x = op-<$> ε f (op η x) -- naturality of the bigger diagram
\end{code}
%</NaturalT-composition-vertical>
......@@ -6,7 +6,6 @@ open import Data.Nat.Base using (_*_)
open import Data.Fin using (Fin) renaming (zero to Fz)
open import Data.Product using (_×_; _,_)
open import Data.Vec using (Vec; []; _∷_)
open import Algebra using (module CommutativeSemiring)
open import Data.Nat.Properties using () renaming (commutativeSemiring to ℕ-commSemiring)
open import Algebra.Operations (CommutativeSemiring.semiring ℕ-commSemiring) using (_^_)
......
......@@ -133,7 +133,8 @@ data Vec₂ {ℓ₁ ℓ₂} {I₁ I₂ : Set ℓ₁} (C : I₁ → I₂ → Set
%<*head2>
\AgdaTarget{head₂}
\begin{code}
head₂ : ∀ {n ℓ₁ ℓ₂} {I₁ I₂ : Set ℓ₁} {C : I₁ → I₂ → Set ℓ₂} {i : I₁} {j : I₂} {is : Vec I₁ n} {js : Vec I₂ n} → Vec₂ C (i ∷ is) (j ∷ js) → C i j
head₂ : ∀ {n ℓ₁ ℓ₂} {I₁ I₂ : Set ℓ₁} {C : I₁ → I₂ → Set ℓ₂} {i : I₁} {j : I₂} {is : Vec I₁ n} {js : Vec I₂ n}
→ Vec₂ C (i ∷ is) (j ∷ js) → C i j
head₂ (x ∷₂ _) = x
\end{code}
%</head2>
......@@ -142,7 +143,8 @@ head₂ (x ∷₂ _) = x
%<*tail2>
\AgdaTarget{tail₂}
\begin{code}
tail₂ : ∀ {n ℓ₁ ℓ₂} {I₁ I₂ : Set ℓ₁} {C : I₁ → I₂ → Set ℓ₂} {i : I₁} {j : I₂} {is : Vec I₁ n} {js : Vec I₂ n} → Vec₂ C (i ∷ is) (j ∷ js) → Vec₂ C is js
tail₂ : ∀ {n ℓ₁ ℓ₂} {I₁ I₂ : Set ℓ₁} {C : I₁ → I₂ → Set ℓ₂} {i : I₁} {j : I₂} {is : Vec I₁ n} {js : Vec I₂ n}
→ Vec₂ C (i ∷ is) (j ∷ js) → Vec₂ C is js
tail₂ (_ ∷₂ xs) = xs
\end{code}
%</tail2>
......@@ -160,7 +162,8 @@ tail₂ (_ ∷₂ xs) = xs
%<*lookup2>
\AgdaTarget{lookup₂}
\begin{code}
lookup₂ : ∀ {n ℓ₁ ℓ₂} {I₁ I₂ : Set ℓ₁} {C : I₁ → I₂ → Set ℓ₂} {is : Vec I₁ n} {js : Vec I₂ n} (k : Fin n) → Vec₂ C is js → C (lookup k is) (lookup k js)
lookup₂ : ∀ {n ℓ₁ ℓ₂} {I₁ I₂ : Set ℓ₁} {C : I₁ → I₂ → Set ℓ₂} {is : Vec I₁ n} {js : Vec I₂ n} (k : Fin n)
→ Vec₂ C is js → C (lookup k is) (lookup k js)
lookup₂ Fz (x ∷₂ _) = x
lookup₂ (Fs k) (_ ∷₂ xs) = lookup₂ k xs
\end{code}
......@@ -217,7 +220,8 @@ map₂ f (x ∷₂ xs) = f x ∷₂ map₂ f xs
%<*VecI2-to-Vec>
\AgdaTarget{Vec₂⇒Vec}
\begin{code}
Vec₂⇒Vec : ∀ {n ℓ₁ ℓ₂} {I₁ I₂ : Set ℓ₁} {C : I₁ → I₂ → Set ℓ₂} {i : I₁} {j : I₂} → Vec₂ C {n} (replicate i) (replicate j) → Vec (C i j) n
Vec₂⇒Vec : ∀ {n ℓ₁ ℓ₂} {I₁ I₂ : Set ℓ₁} {C : I₁ → I₂ → Set ℓ₂} {i : I₁} {j : I₂}
→ Vec₂ C {n} (replicate i) (replicate j) → Vec (C i j) n
Vec₂⇒Vec []₂ = []
Vec₂⇒Vec (x ∷₂ xs) = x ∷ Vec₂⇒Vec xs
\end{code}
......
\begin{code}
module Data.List.NonEmpty.Properties.Extra where
open import Function using (_∘_)
open import Data.Product using (uncurry′; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
open import Data.List using (List; zipWith; zip; map; []; _∷_; length)
open import Data.List.Properties.Extra using (zipWith-map-zip; unzip-zip-inverse)
open import Data.List.NonEmpty using (List⁺; _∷_) renaming (map to map⁺; length to length⁺)
open import Data.List.NonEmpty.Extra using (zipWith⁺; zip⁺; unzip⁺)
open import Data.Product using (uncurry′; _,_)
open import Data.List.Properties.Extra using (zipWith-map-zip; unzip-zip-inverse)
open import Data.List.NonEmpty.Extra using (zipWith⁺; zip⁺; unzip⁺)
open import Data.Vec.Properties.Extra using (,-injective; suc-injective)
\end{code}
......@@ -27,7 +27,7 @@ zipWith⁺-map⁺-zip⁺ {f = f} {x ∷ _} {y ∷ _} = cong (f x y ∷_) zipWith
\AgdaTarget{unzip⁺-zip⁺-inverse}
\begin{code}
unzip⁺-zip⁺-inverse : ∀ {ℓ₁ ℓ₂} {α : Set ℓ₁} {β : Set ℓ₂} {xs : List⁺ α} {ys : List⁺ β}
→ length⁺ xs ≡ length⁺ ys → unzip⁺ (zip⁺ xs ys) ≡ ( xs , ys )
→ length⁺ xs ≡ length⁺ ys → (unzip⁺ ∘ (uncurry′ zip⁺)) ( xs , ys ) ≡ ( xs , ys )
unzip⁺-zip⁺-inverse {xs = x ∷ xs} {y ∷ ys} p with ,-injective (unzip-zip-inverse {xs = xs} {ys} (suc-injective p))
unzip⁺-zip⁺-inverse {xs = x ∷ xs} {y ∷ ys} p | xs≡ , ys≡ = cong₂ _,_ (cong (x ∷_) xs≡) (cong (y ∷_) ys≡)
\end{code}
......
\begin{code}
module Data.List.Properties.Extra where
open import Function using (_∘_; id)
open import Data.List using (List; []; _∷_; zipWith; map; zip; length)
open import Data.Product using (uncurry′; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂; _≗_)
open import Data.List.Extra using (unzip)
open import Data.Vec.Properties.Extra using (,-injective; suc-injective)
......@@ -26,7 +27,7 @@ zipWith-map-zip {f = f} {x ∷ _} {y ∷ _} = cong (f x y ∷_) zipWith-map-zi
\AgdaTarget{unzip-zip-inverse}
\begin{code}
unzip-zip-inverse : ∀ {ℓ₁ ℓ₂} {α : Set ℓ₁} {β : Set ℓ₂} {xs : List α} {ys : List β}
→ length xs ≡ length ys → unzip (zip xs ys) ≡ ( xs , ys )
→ length xs ≡ length ys → (unzip ∘ (uncurry′ zip)) ( xs , ys ) ≡ ( xs , ys )
unzip-zip-inverse {xs = []} {[]} _ = refl
unzip-zip-inverse {xs = []} {_ ∷ _} ()
unzip-zip-inverse {xs = _ ∷ _} {[]} ()
......
......@@ -3,19 +3,15 @@ module Data.Rvec where
\end{code}
\begin{code}
vec↑⁼ : ∀ {n ℓ₁ ℓ₂} {I : Set ℓ₁} (C : I → I → Set ℓ₂) (d : Decidable {A = I} _≡_) (is js : Vec I n) → Set (ℓ₁ ⊔ ℓ₂)
vec↑⁼ {zero} C d ε ε = Lift ⊤
vec↑⁼ {suc zero} C d (i ◁ ε) (j ◁ ε) = C i j × vec↑⁼ C d ε ε
vec↑⁼ {suc (suc n)} C d (i₀ ◁ i₁ ◁ is) (j₀ ◁ j₁ ◁ js) with d j₀ i₁
vec↑⁼ {suc (suc n)} C d (i₀ ◁ i₁ ◁ is) (j₀ ◁ j₁ ◁ js) | yes p = C i₀ j₀ × C i₁ j₁ × vec↑⁼ C d is js
vec↑⁼ {suc (suc n)} C d (i₀ ◁ i₁ ◁ is) (j₀ ◁ j₁ ◁ js) | no _ = Lift ⊥
\end{code}
\begin{code}
head↑′ : ∀ {n ℓ₁ ℓ₂} {I : Set ℓ₁} {C : I → I → Set ℓ₂} {i j : I} {is js : Vec I n} {d : Decidable {A = I} _≡_}
→ vec↑⁼ C d (i ◁ is) (j ◁ js) → C i j
head↑′ {zero} {is = ε} {js = ε} (x , _) = x
head↑′ {suc n} {is = i ◁ is} {js = j ◁ js} x = {!!}
\end{code}
......@@ -48,6 +48,22 @@ instance
%</Serializable-Unit>
%<*⇓×>
\AgdaTarget{⇓×}
\begin{code}
⇓× : ∀ {i j α β A} ⦃ α̂ : (α ⇕ A) {i} ⦄ ⦃ β̂ : (β ⇕ A) {j} ⦄ → (α × β) → Vec A (i + j)
⇓× {i} = uncurry′ _++_ ∘′ map× (⇓ {i = i}) ⇓
\end{code}
%</⇓×>
%<*⇑×>
\AgdaTarget{⇑×}
\begin{code}
⇑× : ∀ {i j α β A} ⦃ α̂ : (α ⇕ A) {i} ⦄ ⦃ β̂ : (β ⇕ A) {j} ⦄ → Vec A (i + j) → (α × β)
⇑× {i} = map× ⇑ ⇑ ∘′ splitAt′ i
\end{code}
%</⇑×>
\begin{code}
instance
\end{code}
......@@ -55,16 +71,27 @@ instance
\AgdaTarget{⇕×}
\begin{code}
⇕× : ∀ {i j α β A} ⦃ α̂ : (α ⇕ A) {i} ⦄ ⦃ β̂ : (β ⇕ A) {j} ⦄ → (α × β ⇕ A)
⇕× {i} {j} {α} {β} {A} = down ⇓⇑ up
where down : (α × β) → Vec A (i + j)
down = uncurry′ _++_ ∘′ map× (⇓ {i = i}) ⇓
up : Vec A (i + j) → (α × β)
up = map× ⇑ ⇑ ∘′ splitAt′ i
⇕× {i} {j} = (⇓× {i} {j}) ⇓⇑ (⇑× {i} {j})
\end{code}
%</Serializable-Product>
%<*⇓Vec>
\AgdaTarget{⇓Vec}
\begin{code}
⇓Vec : ∀ {n i α A} ⦃ α̂ : (α ⇕ A) {i} ⦄ → Vec α n → Vec A (n * i)
⇓Vec = concat ∘′ map ⇓
\end{code}
%</⇓Vec>
%<*⇑Vec>
\AgdaTarget{⇑Vec}
\begin{code}
⇑Vec : ∀ {n i α A} ⦃ α̂ : (α ⇕ A) {i} ⦄ → Vec A (n * i) → Vec α n
⇑Vec {n} {i} = map ⇑ ∘′ group′ n i
\end{code}
%</⇑Vec>
\begin{code}
instance
\end{code}
......@@ -72,12 +99,7 @@ instance
\AgdaTarget{⇕Vec}
\begin{code}
⇕Vec : ∀ {n i α A} ⦃ α̂ : (α ⇕ A) {i} ⦄ → (Vec α n) ⇕ A
⇕Vec {n} {i} {α} {A} = down ⇓⇑ up
where down : Vec α n → Vec A (n * i)
down = concat ∘′ map ⇓
up : Vec A (n * i) → Vec α n
up = map ⇑ ∘′ group′ n i
⇕Vec {n} {i} = ⇓Vec ⇓⇑ (⇑Vec {n} {i})
\end{code}
%</Serializable-Vec>
......@@ -86,10 +108,26 @@ instance
\AgdaTarget{untagUnpad}
\begin{code}
untagUnpad : ∀ {i j} {A : Set} (l : A) (eq : A → A → Bool) → Vec A (suc (i ⊔ j)) → (Vec A i) ⊎ (Vec A j)
untagUnpad {i} {j} l eq (t ∷ ab) = (if (eq t l) then inj₁ ∘′ unpadFrom₁ j else inj₂ ∘′ unpadFrom₂ i) ab
untagUnpad {i} {j} l eq (t ∷ ab) = (if (eq t l) then (inj₁ ∘′ unpadFrom₁ j) else (inj₂ ∘′ unpadFrom₂ i)) ab
\end{code}
%</untagUnpad>
%<*⇓⊎>
\AgdaTarget{⇓⊎}
\begin{code}
⇓⊎ : ∀ {i j α β A} (l r p : A) ⦃ α̂ : (α ⇕ A) {i} ⦄ ⦃ β̂ : (β ⇕ A) {j} ⦄ → α ⊎ β → Vec A (suc (i ⊔ j))
⇓⊎ {i} {j} l r p = [ (l ∷_) ∘′ (padTo₁ j use p) ∘′ ⇓ {i = i} , (r ∷_) ∘′ (padTo₂ i use p) ∘′ ⇓ ]
\end{code}
%</⇓⊎>
%<*⇑⊎>
\AgdaTarget{⇑⊎}
\begin{code}
⇑⊎ : ∀ {i j α β A} (l : A) (eq : A → A → Bool) ⦃ α̂ : (α ⇕ A) {i} ⦄ ⦃ β̂ : (β ⇕ A) {j} ⦄ → Vec A (suc (i ⊔ j)) → α ⊎ β
⇑⊎ {i} l eq = map⊎ (⇑ {i = i}) ⇑ ∘′ (untagUnpad l eq)
\end{code}
%</⇑⊎>
\begin{code}
instance
\end{code}
......@@ -97,11 +135,6 @@ instance
\AgdaTarget{⇕⊎}
\begin{code}
⇕⊎ : ∀ {i j α β A} (l r p : A) (eq : A → A → Bool) ⦃ α̂ : (α ⇕ A) {i} ⦄ ⦃ β̂ : (β ⇕ A) {j} ⦄ → (α ⊎ β) ⇕ A
⇕⊎ {i} {j} {α} {β} {A} l r p eq = down ⇓⇑ up
where down : α ⊎ β → Vec A (suc (i ⊔ j))
down = [ (l ∷_) ∘′ (padTo₁ j use p) ∘′ ⇓ {i = i} , (r ∷_) ∘′ (padTo₂ i use p) ∘′ ⇓ ]
up : Vec A (suc (i ⊔ j)) → α ⊎ β
up = map⊎ (⇑ {i = i}) ⇑ ∘′ (untagUnpad l eq)
⇕⊎ {i} {j} l r p eq = (⇓⊎ {i} {j} l r p) ⇓⇑ (⇑⊎ {i} l eq)
\end{code}
%</Serializable-Sum>
......@@ -4,41 +4,72 @@ module Data.Stream.DistantReasoning where
open import Data.Nat using (_+_; zero; suc)
open import Data.Nat.Properties.Simple using (+-comm)
open import Data.Product using (_,_; proj₂)
open import Data.Vec using (Vec; _++_; _∷_; drop; splitAt; []; [_])
open import Data.Vec using (Vec; _++_; _∷_; splitAt; []; [_]) renaming (drop to dropᵥ)
open import Data.Vec.Properties using (∷-injective)
open import Data.Stream using (Stream; head; _∷_) renaming (_++_ to _++ₛ_; drop to dropₛ; take to takeₛ)
open import Data.Stream.Properties using (drop-compose)
open import Data.Stream using (Stream; head; _∷_; drop; take) renaming (_++_ to _++ₛ_)
open import Relation.Binary.PropositionalEquality using (_≡_; cong₂; refl)
open import Data.Stream.Properties using (drop-compose)
\end{code}
joinProofs : ∀ {d n m} {α} {xs : Vec α n} {ys : Vec α m} {s : Stream α}
→ takeₛ n (dropₛ d s) ≡ xs → takeₛ m (dropₛ (d + n) s) ≡ ys → takeₛ (n + m) (dropₛ d s) ≡ xs ++ ys
%<*joinProofs>
\AgdaTarget{joinProofs}
\begin{code}
joinProofs : ∀ {d n m α} {xs : Vec α n} {ys : Vec α m} {s : Stream α}
→ take n (drop d s) ≡ xs → take m (drop (d + n) s) ≡ ys → take (n + m) (drop d s) ≡ xs ++ ys
joinProofs {zero} {zero} refl p2 = p2
joinProofs {suc d} {s = _ ∷ _} p1 p2 = joinProofs {d} p1 p2
joinProofs {zero} {suc _} {xs = _ ∷ _} {s = _ ∷ _} p1 p2 with ∷-injective p1
joinProofs {zero} {suc _} {xs = _ ∷ _} {s = _ ∷ _} p1 p2 | x≡ , xs≡ = cong₂ _∷_ x≡ (joinProofs {zero} xs≡ p2)
\end{code}
%</joinProofs>
selectProof⁻' : ∀ {n⁻ n} {α} {xs : Vec α (n⁻ + n)} {s : Stream α} → takeₛ (n⁻ + n) s ≡ xs → takeₛ n (dropₛ n⁻ s) ≡ drop n⁻ xs
selectProof⁻' {zero} p = p
selectProof⁻' {suc n⁻} {n} {xs = x ∷ xs} {_ ∷ _} p with splitAt n⁻ xs | selectProof⁻' {n⁻} {n} (proj₂ (∷-injective p))
selectProof⁻' {suc n⁻} {n} {xs = x ∷ .(ys ++ zs)} {_ ∷ _} p | ys , zs , refl | q = q
%<*selectProof⁻'>
\AgdaTarget{selectProof⁻'}
\begin{code}
selectProof⁻' : ∀ {m n α} {xs : Vec α (m + n)} {s : Stream α} → take (m + n) s ≡ xs → take n (drop m s) ≡ dropᵥ m xs
selectProof⁻' {zero} p = p
selectProof⁻' {suc m} {n} {xs = x ∷ xs} {_ ∷ _} p with splitAt m xs | selectProof⁻' {m} {n} (proj₂ (∷-injective p))
selectProof⁻' {suc m} {n} {xs = x ∷ .(ys ++ zs)} {_ ∷ _} p | ys , zs , refl | q = q
\end{code}
%</selectProof⁻'>
selectProof⁻ : ∀ {d n⁻ n} {α} {xs : Vec α (n⁻ + n)} {s : Stream α} → takeₛ (n⁻ + n) (dropₛ d s) ≡ xs → takeₛ n (dropₛ (d + n⁻) s) ≡ drop n⁻ xs
selectProof⁻ {d} {n⁻} {n} {α} {xs} {s = s} p rewrite +-comm d n⁻ | drop-compose {n⁻} {d} {_} {s} = selectProof⁻' {n⁻} {n} {s = dropₛ d s} p
%<*selectProof⁻>
\AgdaTarget{selectProof⁻}
\begin{code}
selectProof⁻ : ∀ {d m n α} {xs : Vec α (m + n)} {s : Stream α} → take (m + n) (drop d s) ≡ xs → take n (drop (d + m) s) ≡ dropᵥ m xs
selectProof⁻ {d} {m} {n} {_} {xs} {s} p rewrite +-comm d m | drop-compose {m} {d} {_} {s} = selectProof⁻' {m} {n} {s = drop d s} p
\end{code}
%</selectProof⁻>
selectProof⁺ : ∀ {n n⁺} {α} {xs : Vec α n} {ys : Vec α n⁺} {s : Stream α} → takeₛ (n + n⁺) s ≡ xs ++ ys → takeₛ n s ≡ xs
%<*selectProof⁺>
\AgdaTarget{selectProof⁺}
\begin{code}
selectProof⁺ : ∀ {n k α} {xs : Vec α n} {ys : Vec α k} {s : Stream α} → take (n + k) s ≡ xs ++ ys → take n s ≡ xs
selectProof⁺ {zero} {xs = []} p = refl
selectProof⁺ {suc _} {xs = _ ∷ _} {s = _ ∷ _} p with ∷-injective p
selectProof⁺ {suc _} {xs = _ ∷ _} {s = _ ∷ _} p | x≡ , xs≡ = cong₂ _∷_ x≡ (selectProof⁺ xs≡)
\end{code}
%</selectProof⁺>
take-drop-num-cong : ∀ {α t d₁ d₂} {s : Stream α} → d₁ ≡ d₂ → takeₛ t (dropₛ d₁ s) ≡ takeₛ t (dropₛ d₂ s)
%<*take-drop-num-cong>
\AgdaTarget{take-drop-num-cong}
\begin{code}
take-drop-num-cong : ∀ {α t d₁ d₂} {s : Stream α} → d₁ ≡ d₂ → take t (drop d₁ s) ≡ take t (drop d₂ s)
take-drop-num-cong refl = refl
\end{code}
%</take-drop-num-cong>
take-1-head : ∀ {α} {w : α} {s : Stream α} → takeₛ 1 s ≡ [ w ] → head s ≡ w
take-1-head {w = w} {.w ∷ _} refl = refl
%<*take-1-head>
\AgdaTarget{take-1-head}
\begin{code}
take-1-head : ∀ {α} {x : α} {s : Stream α} → take 1 s ≡ [ x ] → head s ≡ x
take-1-head {x = x} {.x ∷ _} refl = refl
\end{code}
%</take-1-head>
\begin{code}
module Data.Stream.Equality.FromPointwiseEquality where
open import Function using (_∘_; flip)
......@@ -5,12 +6,23 @@ open import Coinduction using (♯_; ♭)
open import Data.Nat using (ℕ; suc; zero)
open import Data.Stream using (Stream; lookup; _≈_; _∷_)
open import Relation.Binary.PropositionalEquality using (_≗_)
\end{code}
%<*lookup≗⇒≈>
\AgdaTarget{lookup≗⇒≈}
\begin{code}
lookup≗⇒≈ : ∀ {α} (xs ys : Stream α) → (flip lookup xs ≗ flip lookup ys) → xs ≈ ys
lookup≗⇒≈ (x ∷ xs) (y ∷ ys) p = p 0 ∷ ♯ lookup≗⇒≈ (♭ xs) (♭ ys) (p ∘ suc)
\end{code}
%</lookup≗⇒≈>
%<*≈⇒lookup≗>
\AgdaTarget{≈⇒lookup≗}
\begin{code}
≈⇒lookup≗ : ∀ {α} (xs ys : Stream α) → xs ≈ ys → flip lookup xs ≗ flip lookup ys
≈⇒lookup≗ (_ ∷ _) (_ ∷ _) (x≡y ∷ _) zero = x≡y
≈⇒lookup≗ (_ ∷ xs) (_ ∷ ys) (_ ∷ xs≈ys) (suc n) = ≈⇒lookup≗ (♭ xs) (♭ ys) (♭ xs≈ys) n
\end{code}
%</≈⇒lookup≗>
\begin{code}
module Data.Stream.Equality.FromPrefixEquality where
open import Function using (_∘_)
......@@ -6,32 +7,64 @@ open import Data.Stream using (Stream; take; _≈_; _∷_)
open import Data.Nat using (ℕ; suc; zero)
open import Data.Vec using (Vec; _∷_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
\end{code}
\begin{code}
module _ {n ℓ} {α : Set ℓ} where
private _≡ᵥ_ = _≡_ {A = Vec α (suc n)}
\end{code}
%<*vtail-cong>
\AgdaTarget{vtail-cong}
\begin{code}
vtail-cong : ∀ {x y : α} {xs ys : Vec α n} → (x ∷ xs) ≡ᵥ (y ∷ ys) → xs ≡ ys
vtail-cong refl = refl
\end{code}
%</vtail-cong>
%<*_∷-cong_>
\AgdaTarget{\_∷-cong\_}
\begin{code}
_∷-cong_ : ∀ {x y : α} {xs ys : Vec α n} → x ≡ y → xs ≡ ys → (x ∷ xs) ≡ᵥ (y ∷ ys)
_∷-cong_ refl refl = refl
\end{code}
%</_∷-cong_>
%<*take-tail≡>
\AgdaTarget{take-tail≡}
\begin{code}
take-tail≡ : ∀ {n α x y} (xs ys : ∞ (Stream α)) → take (suc n) (x ∷ xs) ≡ take (suc n) (y ∷ ys) → take n (♭ xs) ≡ take n (♭ ys)
take-tail≡ _ _ p = vtail-cong p
\end{code}
%</take-tail≡>
%<*take-head≡>
\AgdaTarget{take-head≡}
\begin{code}
take-head≡ : ∀ {α x y} (xs ys : ∞ (Stream α)) → (∀ n → take n (x ∷ xs) ≡ take n (y ∷ ys)) → x ≡ y
take-head≡ xs ys p with p 1
take-head≡ xs ys p | refl = refl
take-head≡ _ _ p with p 1
take-head≡ _ _ p | refl = refl
\end{code}
%</take-head≡>
%<*take≗⇒≈>
\AgdaTarget{take≗⇒≈}
\begin{code}
take≗⇒≈ : ∀ {α} (xs ys : Stream α) → (∀ n → take n xs ≡ take n ys) → xs ≈ ys
take≗⇒≈ (x ∷ xs) (y ∷ ys) p = take-head≡ _ _ p ∷ ♯ take≗⇒≈ (♭ xs) (♭ ys) (take-tail≡ xs ys ∘ (p ∘ suc))
take≗⇒≈ (_ ∷ xs) (_ ∷ ys) p = take-head≡ _ _ p ∷ ♯ take≗⇒≈ (♭ xs) (♭ ys) (take-tail≡ xs ys ∘ (p ∘ suc))
\end{code}
%</take≗⇒≈>
%<*≈⇒take≗>
\AgdaTarget{≈⇒take≗}
\begin{code}
≈⇒take≗ : ∀ {α} {xs ys : Stream α} → xs ≈ ys → (∀ n → take n xs ≡ take n ys)
≈⇒take≗ (_ ∷ _) zero = refl
≈⇒take≗ (x≡y ∷ xs≈ys) (suc n) = x≡y ∷-cong (≈⇒take≗ (♭ xs≈ys) n)
\end{code}
%</≈⇒take≗>
......@@ -4,47 +4,95 @@ module Data.Stream.Equality.NAD where
open import Coinduction using (∞; ♭; ♯_)
open import Data.Stream using (Stream; _∷_; _≈_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
\end{code}
\begin{code}
infix 4 _≈ₚ_
\end{code}
%<*_≈ₚ_>
\AgdaTarget{\_≈ₚ\_}
\begin{code}
data _≈ₚ_ {α} : Stream α → Stream α → Set where
_∷ₚ_ : ∀ {xs ys} x → ∞ (♭ xs ≈ₚ ♭ ys) → x ∷ xs ≈ₚ x ∷ ys
transₚ : ∀ {s₁ s₂ s₃} → s₁ ≈ₚ s₂ → s₂ ≈ₚ s₃ → s₁ ≈ₚ s₃
reflₚ : ∀ {s} → s ≈ₚ s
\end{code}
%</_≈ₚ_>
\begin{code}
infix 4 _≈ₕ_
\end{code}
%<*_≈ₕ_>
\AgdaTarget{\_≈ₕ\_}
\begin{code}
data _≈ₕ_ {α} : Stream α → Stream α → Set where
_∷ₕ_ : ∀ {xs ys} x → ♭ xs ≈ₚ ♭ ys → x ∷ xs ≈ₕ x ∷ ys
\end{code}
%</_≈ₕ_>
%<*reflₕ>
\AgdaTarget{reflₕ}
\begin{code}
reflₕ : ∀ {A} {s : Stream A} → s ≈ₕ s
reflₕ {s = x ∷ xs} = x ∷ₕ reflₚ {s = ♭ xs}
\end{code}
%</reflₕ>
%<*transₕ>
\AgdaTarget{transₕ}
\begin{code}
transₕ : ∀ {α} {s₁ s₂ s₃ : Stream α} → s₁ ≈ₕ s₂ → s₂ ≈ₕ s₃ → s₁ ≈ₕ s₃
transₕ {s₁ = x ∷ xs} {s₃ = .x ∷ zs} (.x ∷ₕ s₁≈s₂) (.x ∷ₕ s₂≈s₃) = x ∷ₕ transₚ s₁≈s₂ s₂≈s₃
\end{code}
%</transₕ>
%<*whnf>
\AgdaTarget{whnf}
\begin{code}
whnf : ∀ {α} {s₁ s₂ : Stream α} → s₁ ≈ₚ s₂ → s₁ ≈ₕ s₂
whnf (x ∷ₚ s₁≈ₚs₂) = x ∷ₕ (♭ s₁≈ₚs₂)
whnf (transₚ s₁≈ₚs₂ s₂≈ₚs₃) = transₕ (whnf s₁≈ₚs₂) (whnf s₂≈ₚs₃)
whnf reflₚ = reflₕ
\end{code}
%</whnf>
%<*soundₕ-soundₚ-type>
\AgdaTarget{soundₕ, soundₚ}
\begin{code}
soundₕ : ∀ {α} {s₁ s₂ : Stream α} → s₁ ≈ₕ s₂ → s₁ ≈ s₂
soundₚ : ∀ {α} {s₁ s₂ : Stream α} → s₁ ≈ₚ s₂ → s₁ ≈ s₂
\end{code}
%</soundₕ-soundₚ-type>
%<*soundₕ-soundₚ-def>
\begin{code}
soundₕ (x ∷ₕ s₁≈ₚs₂) = refl ∷ ♯ (soundₚ s₁≈ₚs₂)
soundₚ xs≈ys = soundₕ (whnf xs≈ys)
\end{code}
%</soundₕ-soundₚ-def>
%<*≈-to-≈ₚ>
\AgdaTarget{≈-to-≈ₚ}
\begin{code}
≈-to-≈ₚ : ∀ {α} {s₁ s₂ : Stream α} → s₁ ≈ s₂ → s₁ ≈ₚ s₂
≈-to-≈ₚ {s₁ = x ∷ xs} (refl ∷ xs≈) = x ∷ₚ ♯ ≈-to-≈ₚ (♭ xs≈)
\end{code}
%</≈-to-≈ₚ>
%<*≈ₚ-to-≈>
\AgdaTarget{≈ₚ-to-≈}
\begin{code}
≈ₚ-to-≈ : ∀ {A} {xs ys : Stream A} → xs ≈ₚ ys → xs ≈ ys
≈ₚ-to-≈ = soundₚ
\end{code}
%</≈ₚ-to-≈>
......@@ -4,49 +4,96 @@ module Data.Stream.Equality.WithTrans where
open import Coinduction using (∞; ♭; ♯_)
open import Data.Stream using (Stream; _∷_; _≈_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
\end{code}
\begin{code}
infix 4 _≈ₚ_
\end{code}
\begin{code}
data _≈ₚ_ {α} : Stream α → Stream α → Set where
_∷ₚ_ : ∀ {x y xs ys} → x ≡ y → ∞ (♭ xs ≈ₚ ♭ ys) → x ∷ xs ≈ₚ y ∷ ys
transₚ : ∀ {s₁ s₂ s₃} → s₁ ≈ₚ s₂ → s₂ ≈ₚ s₃ → s₁ ≈ₚ s₃
\end{code}
%<*reflₚ>
\AgdaTarget{reflₚ}
\begin{code}
reflₚ : ∀ {α} {s : Stream α} → s ≈ₚ s
reflₚ {s = x ∷ xs} = refl ∷ₚ ♯ reflₚ
\end{code}
%</reflₚ>
\begin{code}
infix 4 _≈ₕ_
\end{code}
\begin{code}
data _≈ₕ_ {α} : Stream α → Stream α → Set where
_∷ₕ_ : ∀ {x y xs ys} → x ≡ y → ♭ xs ≈ₚ ♭ ys → x ∷ xs ≈ₕ y ∷ ys
\end{code}
%<*reflₕ>
\AgdaTarget{reflₕ}
\begin{code}
reflₕ : ∀ {A} {xs : Stream A} → xs ≈ₕ xs
reflₕ {xs = x ∷ xs} = refl ∷ₕ reflₚ
\end{code}
%</reflₕ>
%<*transₕ>
\AgdaTarget{transₕ}
\begin{code}
transₕ : ∀ {α} {s₁ s₂ s₃ : Stream α} → s₁ ≈ₕ s₂ → s₂ ≈ₕ s₃ → s₁ ≈ₕ s₃
transₕ {s₁ = x ∷ xs} {s₂ = .x ∷ zs} (refl ∷ₕ s₁≈ₚs₂) (refl ∷ₕ s₂≈ₚs₃) = refl ∷ₕ (transₚ s₁≈ₚs₂ s₂≈ₚs₃)
\end{code}
%</transₕ>
%<*whnf>
\AgdaTarget{whnf}