------------------------------------------------------------------------
-- An implementation of the Fibonacci sequence using tail
------------------------------------------------------------------------

module SingletonChunks where

open import Coinduction
open import Data.Bool
open import Data.Nat
open import Data.Stream as S using (Stream; _≈_; _∷_)
open import Data.Vec as V using (Vec; []; _∷_)
import Relation.Binary.PropositionalEquality as P

------------------------------------------------------------------------
-- Stream programs

-- StreamP b A encodes programs generating streams in chunks of size
-- (at least) 1. The first chunk may be empty if b is false.

infixr 5 _∷_

data StreamP : Bool  Set  Set₁ where
  [_]     :  {A} (xs :  (StreamP true A))  StreamP false A
  _∷_     :  {A} (x : A) (xs : StreamP false A)  StreamP true A
  forget  :  {A} (xs : StreamP true A)  StreamP false A
  tail    :  {A} (xs : StreamP true A)  StreamP false A
  zipWith :  {b A B C} (f : A  B  C)
            (xs : StreamP b A) (ys : StreamP b B)  StreamP b C

data StreamW : Bool  Set  Set₁ where
  [_] :  {A} (xs : StreamP true A)  StreamW false A
  _∷_ :  {A} (x : A) (xs : StreamW false A)  StreamW true A

forgetW :  {A}  StreamW true A  StreamW false A
forgetW (x  [ xs ]) = [ x  forget xs ]

tailW :  {A}  StreamW true A  StreamW false A
tailW (x  xs) = xs

zipWithW :  {b A B C}  (A  B  C) 
           StreamW b A  StreamW b B  StreamW b C
zipWithW f [ xs ]   [ ys ]   = [ zipWith f xs ys ]
zipWithW f (x  xs) (y  ys) = f x y  zipWithW f xs ys

whnf :  {b A}  StreamP b A  StreamW b A
whnf [ xs ]            = [  xs ]
whnf (x  xs)          = x  whnf xs
whnf (forget xs)       = forgetW (whnf xs)
whnf (tail xs)         = tailW (whnf xs)
whnf (zipWith f xs ys) = zipWithW f (whnf xs) (whnf ys)

mutual

  ⟦_⟧W :  {A}  StreamW true A  Stream A
   x  [ xs ] ⟧W = x    xs ⟧P

  ⟦_⟧P :  {A}  StreamP true A  Stream A
   xs ⟧P =  whnf xs ⟧W

------------------------------------------------------------------------
-- The Fibonacci sequence

fib : StreamP true 
fib = 0  [  (1  zipWith _+_ (forget fib) (tail fib)) ]

------------------------------------------------------------------------
-- The definition of fib is correct

-- ⟦_⟧ is homomorphic with respect to zipWith/S.zipWith.

zipWith-hom :  {A B C} (_∙_ : A  B  C) xs ys 
               zipWith _∙_ xs ys ⟧P  S.zipWith _∙_  xs ⟧P  ys ⟧P
zipWith-hom _∙_ xs ys with whnf xs | whnf ys
zipWith-hom _∙_ xs ys | x  [ xs′ ] | y  [ ys′ ] =
  P.refl   zipWith-hom _∙_ xs′ ys′

-- forget is the identity on streams.

open import MapIterate as M using (_≈P_; _∷_; _≈⟨_⟩_; _∎)
open import Relation.Binary.PropositionalEquality as P using (_≡_; [_])

forget-lemma :  {A} x (xs : StreamP true A) 
                x  forget xs ⟧P ≈P x    xs ⟧P
forget-lemma x xs with whnf xs | P.inspect whnf xs
... | y  [ ys ] | [ eq ] = x   helper eq
  where
  helper : whnf xs  y  [ ys ] 
            y  forget ys ⟧P ≈P  xs ⟧P
  helper eq rewrite eq = _ ≈⟨ forget-lemma y ys  (y   (_ ))

-- The stream ⟦ fib ⟧P satisfies its intended defining equation.

open import Relation.Binary
module SS {A : Set} = Setoid (S.setoid A)

fib-correct :
   fib ⟧P  0   (1   S.zipWith _+_  fib ⟧P (S.tail  fib ⟧P))
fib-correct =
  P.refl   (P.refl   SS.trans
   (zipWith-hom _+_ (0  forget fib′) fib′)
   (S.zipWith-cong _+_ (SS.trans (M.soundP (forget-lemma 0 fib′))
                                 (P.refl   SS.refl)) SS.refl))
  where fib′ = 1  zipWith _+_ (forget fib) (tail fib)

------------------------------------------------------------------------
-- An equality proof language

infix  4 _≈[_]P_ _≈[_]W_
infix  3 _∎
infixr 2 _≈⟨_⟩_

data _≈[_]P_ : {A : Set}  Stream A  Bool  Stream A  Set₁ where
  [_]     :  {A} {xs ys : Stream A}
            (xs≈ys :  (xs ≈[ true ]P ys))  xs ≈[ false ]P ys
  _∷_     :  {b A} (x : A) {xs ys :  (Stream A)}
            (xs≈ys :  xs ≈[ b ]P  ys)  x  xs ≈[ true ]P x  ys
  forget  :  {A} {xs ys : Stream A}
            (xs≈ys : xs ≈[ true ]P ys)  xs ≈[ false ]P ys
  _≈⟨_⟩_  :  {b A} (xs : Stream A) {ys zs}
            (xs≈ys : xs ≈[ b ]P ys) (ys≈zs : ys ≈[ b ]P zs) 
            xs ≈[ b ]P zs
  _∎      :  {A} (xs : Stream A)  xs ≈[ true ]P xs
  tail    :  {A} {xs ys : Stream A} (xs≈ys : xs ≈[ true ]P ys) 
            S.tail xs ≈[ false ]P S.tail ys
  zipWith :  {b A B C} (f : A  B  C) {xs xs′ ys ys′}
            (xs≈xs′ : xs ≈[ b ]P xs′) (ys≈ys′ : ys ≈[ b ]P ys′) 
            S.zipWith f xs ys ≈[ b ]P S.zipWith f xs′ ys′

-- Completeness.

completeP :  {A : Set} {xs ys : Stream A} 
            xs  ys  xs ≈[ true ]P ys
completeP (P.refl  xs≈ys) = _  [  completeP ( xs≈ys) ]

-- Weak head normal forms.

data _≈[_]W_ {A : Set} : Stream A  Bool  Stream A  Set₁ where
  [_]     : {xs ys : Stream A}
            (xs≈ys : xs ≈[ true ]P ys)  xs ≈[ false ]W ys
  _∷_     :  (x : A) {xs ys}
            (xs≈ys :  xs ≈[ true ]P  ys)  x  xs ≈[ true ]W x  ys

consW≈ :  {A b} (x : A) {xs ys} 
          xs ≈[ b ]W  ys  x  xs ≈[ true ]W x  ys
consW≈ x xs≈ys = x  helper xs≈ys
  where
  helper :  {A b} {xs ys : Stream A} 
           xs ≈[ b ]W ys  xs ≈[ true ]P ys
  helper [ xs≈ys ]   = xs≈ys
  helper (x  xs≈ys) = x  xs≈ys

forgetW≈ :  {A} {xs ys : Stream A} 
           xs ≈[ true ]W ys  xs ≈[ false ]W ys
forgetW≈ (x  xs≈ys) = [ x  forget xs≈ys ]

transW≈ :  {A b} {xs ys zs : Stream A} 
          xs ≈[ b ]W ys  ys ≈[ b ]W zs  xs ≈[ b ]W zs
transW≈ [ xs≈ys ]   [ ys≈zs ]    = [ _ ≈⟨ xs≈ys  ys≈zs ]
transW≈ (x  xs≈ys) (.x  ys≈zs) = x  (_ ≈⟨ xs≈ys  ys≈zs)

reflW≈ :  {A} (xs : Stream A)  xs ≈[ true ]W xs
reflW≈ (x  xs) = x  ( xs )

tailW≈ :  {A} {xs ys : Stream A} 
         xs ≈[ true ]W ys  S.tail xs ≈[ false ]W S.tail ys
tailW≈ (x  xs≈ys) = [ xs≈ys ]

zipWithW≈ :  {A B C b} (_∙_ : A  B  C) {xs₁ ys₁ xs₂ ys₂} 
            xs₁ ≈[ b ]W ys₁  xs₂ ≈[ b ]W ys₂ 
            S.zipWith _∙_ xs₁ xs₂ ≈[ b ]W S.zipWith _∙_ ys₁ ys₂
zipWithW≈ _∙_ [ xs₁≈ys₁ ]    [ xs₂≈ys₂ ]    = [ zipWith _∙_ xs₁≈ys₁ xs₂≈ys₂ ]
zipWithW≈ _∙_ (x₁  xs₁≈ys₁) (x₂  xs₂≈ys₂) =
  (x₁  x₂)  zipWith _∙_ xs₁≈ys₁ xs₂≈ys₂

whnf≈ :  {A : Set} {xs ys : Stream A} {b} 
        xs ≈[ b ]P ys  xs ≈[ b ]W ys
whnf≈ [ xs≈ys ]                 = [  xs≈ys ]
whnf≈ (x  xs≈ys)               = consW≈ x (whnf≈ xs≈ys)
whnf≈ (forget xs≈ys)            = forgetW≈ (whnf≈ xs≈ys)
whnf≈ (xs ≈⟨ xs≈ys  ys≈zs)     = transW≈ (whnf≈ xs≈ys) (whnf≈ ys≈zs)
whnf≈ (xs )                    = reflW≈ xs
whnf≈ (tail xs≈ys)              = tailW≈ (whnf≈ xs≈ys)
whnf≈ (zipWith f xs≈xs′ ys≈ys′) = zipWithW≈ f (whnf≈ xs≈xs′) (whnf≈ ys≈ys′)

-- Soundness.

mutual

  soundW : {A : Set} {xs ys : Stream A}  xs ≈[ true ]W ys  xs  ys
  soundW (x  xs≈ys) = P.refl   soundP xs≈ys

  soundP : {A : Set} {xs ys : Stream A}  xs ≈[ true ]P ys  xs  ys
  soundP xs≈ys = soundW (whnf≈ xs≈ys)

------------------------------------------------------------------------
-- The equation given for fib has a unique solution

fib-rhs : Stream   Stream 
fib-rhs ns = 0   (1   S.zipWith _+_ ns (S.tail ns))

fib-unique :
   ms ns  ms  fib-rhs ms  ns  fib-rhs ns  ms ≈[ true ]P ns
fib-unique ms ns ms≈ ns≈ =
  ms         ≈⟨ completeP ms≈ 
  fib-rhs ms ≈⟨ 0  [  (1  zipWith _+_ (forget (fib-unique ms ns ms≈ ns≈))
                                         (tail (fib-unique ms ns ms≈ ns≈))) ] 
  fib-rhs ns ≈⟨ completeP (SS.sym ns≈) 
  ns