{-# OPTIONS --cubical --no-import-sorts --safe --guardedness #-}
module Cubical.Codata.Stream.Properties where

open import Cubical.Core.Everything

open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Codata.Stream.Base

open Stream

mapS :  {A B}  (A  B)  Stream A  Stream B
tail (mapS f xs) = mapS f (tail xs)

even :  {A}  Stream A  Stream A
tail (even a) = even (tail (tail a))

odd :  {A}  Stream A  Stream A
tail (odd a) = odd (tail (tail a))

merge :  {A}  Stream A  Stream A  Stream A
tail (tail (merge a b)) = merge (tail a) (tail b)

mapS-id :  {A} {xs : Stream A}  mapS  x  x) xs  xs
tail (mapS-id {xs = xs} i) = mapS-id {xs = tail xs} i

Stream-η :  {A} {xs : Stream A}  xs  (head xs , tail xs)
tail (Stream-η {A} {xs} i) = tail xs

elimS :  {A} (P : Stream A  Type₀) (c :  x xs  P (x , xs)) (xs : Stream A)  P xs
elimS P c xs = transp  i  P (Stream-η {xs = xs} (~ i))) i0

odd≡even∘tail :  {A}  (a : Stream A)  odd a  even (tail a)
tail (odd≡even∘tail a i) = odd≡even∘tail (tail (tail a)) i

mergeEvenOdd≡id :  {A}  (a : Stream A)  merge (even a) (odd a)  a
tail (tail (mergeEvenOdd≡id a i)) = mergeEvenOdd≡id (tail (tail a)) i

module Equality≅Bisimulation where

-- Bisimulation
record _≈_ {A : Type₀} (x y : Stream A) : Type₀ where
coinductive
field
≈tail : tail x  tail y

open _≈_

bisim : {A : Type₀}  {x y : Stream A}  x  y  x  y
tail (bisim x≈y i) = bisim (≈tail x≈y) i

misib : {A : Type₀}  {x y : Stream A}  x  y  x  y
≈tail (misib p) = misib  i  tail (p i))

iso1 : {A : Type₀}  {x y : Stream A}  (p : x  y)  bisim (misib p)  p
tail (iso1 p i j) = iso1  i  tail (p i)) i j

iso2 : {A : Type₀}  {x y : Stream A}  (p : x  y)  misib (bisim p)  p
≈tail (iso2 p i) = iso2 (≈tail p) i

path≃bisim : {A : Type₀}  {x y : Stream A}  (x  y)  (x  y)
path≃bisim = isoToEquiv (iso misib bisim iso2 iso1)

path≡bisim : {A : Type₀}  {x y : Stream A}  (x  y)  (x  y)
path≡bisim = ua path≃bisim

-- misib can be implemented by transport as well.
refl≈ : {A : Type₀} {x : Stream A}  x  x
≈tail refl≈ = refl≈

cast :  {A : Type₀} {x y : Stream A} (p : x  y)  x  y
cast {x = x} p = transport  i  x  p i) refl≈

misib-refl :  {A : Type₀} {x : Stream A}  misib {x = x} refl  refl≈
≈tail (misib-refl i) = misib-refl i

misibTransp :  {A : Type₀} {x y : Stream A} (p : x  y)  cast p  misib p
misibTransp p = J  _ p  cast p  misib p) ((transportRefl refl≈)  (sym misib-refl)) p

module Stream≅Nat→ {A : Type₀} where
lookup : Stream A    A
lookup xs zero = head xs
lookup xs (suc n) = lookup (tail xs) n

tabulate : (  A)  Stream A
head (tabulate f) = f zero
tail (tabulate f) = tabulate  n  f (suc n))

lookup∘tabulate :  (x : _  A)  lookup (tabulate x))   x  x)
lookup∘tabulate i f zero = f zero
lookup∘tabulate i f (suc n) = lookup∘tabulate i  n  f (suc n)) n

tabulate∘lookup :  (x : Stream A)  tabulate (lookup x))   x  x)