------------------------------------------------------------------------
-- Instantiation of Contractive for streams
------------------------------------------------------------------------

-- Taken from the paper.

-- The definition of Eq has been changed slightly, as compared to the
-- paper. The paper uses
--   Eq = λ n xs ys → take n xs ≡ take n ys.
-- The reason for the change is that with the definition above
-- coherence does not say anything about the first element in limU s.
-- With the definition in the paper head (s 0), which is the first
-- element in limU s, does not have to be related to head (s n) for
-- any other n, and this makes it impossible to prove isLimitU.
-- (Unless I have missed something.)

module Contractive.Stream {A : Set} where

open import Codata.Musical.Notation
open import Codata.Musical.Stream
open import Contractive
open import Data.Nat
open import Data.Nat.Induction
open import Data.Nat.Properties
import Data.Vec as Vec
open Vec using (_∷_; [])
open import Function
open import Relation.Unary
open import Relation.Binary.PropositionalEquality

<′-isWellFoundedOrder : IsWellFoundedOrder _<′_
<′-isWellFoundedOrder = record
  { trans         = λ {i} {j} {k} i+1≤j j+1≤k  ≤⇒≤′ (begin
                       suc i  ≤⟨ ≤′⇒≤ (≤′-step i+1≤j) 
                       suc j  ≤⟨ ≤′⇒≤ j+1≤k 
                       k      )
  ; isWellFounded = <′-wellFounded
  }
  where open ≤-Reasoning

ofe : OFE
ofe = record
  { Carrier            = 
  ; Domain             = Stream A
  ; _<_                = _<′_
  ; isWellFoundedOrder = <′-isWellFoundedOrder
  ; Eq                 = λ n xs ys  take (suc n) xs  take (suc n) ys
  ; isEquivalence      = λ _  record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }

open OFE ofe

private

  limU : (  Stream A)  Stream A
  limU s = head (s 0)   limU (tail  s  suc)

  η :  {n} {xs : Stream A}  Eq n xs (head xs   tail xs)
  η {xs = x  xs} = refl

  step :  s 
         IsCoherent {U} (lift s) 
         IsCoherent {U} (lift (tail  s  suc))
  step s coh {m} {n} _ _ m<n = begin
    take (suc m) (tail (s (suc m)))      ≡⟨ lem (s (suc m)) 
    Vec.tail (take (2 + m) (s (1 + m)))  ≡⟨ cong Vec.tail $ coh {1 + m} {1 + n} _ _ (s≤′s m<n) 
    Vec.tail (take (2 + m) (s (1 + n)))  ≡⟨ sym $ lem (s (suc n)) 
    take (suc m) (tail (s (suc n)))      
    where
    open ≡-Reasoning

    lem :  {n} (xs : Stream A) 
          take n (tail xs)  Vec.tail (take (1 + n) xs)
    lem (x  xs) = refl

  isLimitU :  s 
             IsCoherent {U} (lift s) 
             IsLimit {U} (lift s) (limU s)
  isLimitU s coh {zero}  _ = begin
    take 1 (s 0)     ≡⟨ η 
    head (s 0)  []  
    where open ≡-Reasoning
  isLimitU s coh {suc n} _ = begin
    take (2 + n) (s (1 + n))                                 ≡⟨ η 
    head (s (1 + n))  take (1 + n) ((tail  s  suc) n)     ≡⟨ cong₂ _∷_ lem₁ (isLimitU (tail  s  suc)
                                                                                         (step s coh) {n} _) 
    head (s 0)        take (1 + n) (limU (tail  s  suc))  
    where
    open ≡-Reasoning

    lem₂ :  {n} (xs ys : Stream A) 
           Eq n xs ys  head xs  head ys
    lem₂ (x  xs) (y  ys) = cong Vec.head

    lem₁ : head (s (1 + n))  head (s 0)
    lem₁ = lem₂ _ _ $ sym $ coh {0} {suc n} _ _ (s≤′s z≤′n)

  lim↓ : A   n  (∀ n'  n' <′ n  Stream A)  Stream A
  lim↓ x zero    s = repeat x
  lim↓ x (suc n) s = s n ≤′-refl

  isLimit↓ :  x n (s : Family ( n)) 
             IsCoherent s  IsLimit s (lim↓ x n s)
  isLimit↓ x zero    s coh ()
  isLimit↓ x (suc n) s coh ≤′-refl       = refl
  isLimit↓ x (suc n) s coh (≤′-step m<n) =
    coh (≤′-step m<n) ≤′-refl m<n

-- The paper implicitly assumes that A is non-empty.

cofe : A  COFE
cofe x = record
  { ofe      = ofe
  ; limU     = limU
  ; isLimitU = isLimitU _
  ; lim↓     = lim↓ x
  ; isLimit↓ = λ n {s}  isLimit↓ x n s
  }