------------------------------------------------------------------------
-- Some examples
------------------------------------------------------------------------

module Contractive.Examples where

open import Coinduction
open import Data.Nat
open import Data.Nat.Properties
open import Data.Stream
import Data.Vec as Vec
open Vec using (_∷_; [])
open import Function
open import Contractive
import Contractive.Stream as S
open import StreamProg using (Ord; lt; eq; gt; merge)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open COFE (S.cofe )

fibF : ContractiveFun (S.cofe )
fibF = record
  { F             = F
  ; isContractive = isCon _ _ _
  }
  where
  F = λ xs →  ∷ ♯ ( ∷ ♯ zipWith _+_ xs (tail xs))

  lemma₁ : ∀ _∙_ (xs ys : Stream ℕ) n →
           take n (zipWith _∙_ xs ys) ≡
           Vec.zipWith _∙_ (take n xs) (take n ys)
  lemma₁ _∙_ _        _        zero    = refl
  lemma₁ _∙_ (x ∷ xs) (y ∷ ys) (suc n) =
    cong (_∷_ (x ∙ y)) (lemma₁ _∙_ (♭ xs) (♭ ys) n)

  lemma₂ : ∀ (xs ys : Stream ℕ) n →
           Eq n xs ys → take n xs ≡ take n ys
  lemma₂ _        _         zero    _   = refl
  lemma₂ (x ∷ xs) ( y ∷ ys) (suc n) hyp
    with cong Vec.head hyp | take n (♭ xs) | lemma₂ (♭ xs) (♭ ys) n (cong Vec.tail hyp)
  lemma₂ (x ∷ xs) (.x ∷ ys) (suc n) hyp | refl | .(take n (♭ ys)) | refl = refl

  isCon : ∀ (xs ys : Stream ℕ) n →
          (∀ {m} → m <′ n → Eq m xs ys) →
          Eq n (F xs) (F ys)
  isCon _        _        zero    _   = refl
  isCon (x ∷ xs) (y ∷ ys) (suc n) hyp = cong (λ zs →  ∷  ∷ zs) (begin
    take n (zipWith _+_ (x ∷ xs) (♭ xs))               ≡⟨ lemma₁ _+_ (x ∷ xs) (♭ xs) n ⟩
    Vec.zipWith _+_ (take n (x ∷ xs)) (take n (♭ xs))  ≡⟨ cong₂ (Vec.zipWith _+_)
                                                                (lemma₂ _ _ n (hyp ≤′-refl))
                                                                (cong Vec.tail (hyp ≤′-refl)) ⟩
    Vec.zipWith _+_ (take n (y ∷ ys)) (take n (♭ ys))  ≡⟨ sym $ lemma₁ _+_ (y ∷ ys) (♭ ys) n ⟩
    take n (zipWith _+_ (y ∷ ys) (♭ ys))               ∎)

fib : Stream ℕ
fib = ContractiveFun.fixpoint fibF

-- Note that I could not be bothered to finish the following
-- definition.

hammingF : ContractiveFun (S.cofe )
hammingF = record
  { F             = F
  ; isContractive = isCon _ _ _
  }
  where
  toOrd : ∀ {m n} → Ordering m n → Ord
  toOrd (less _ _)    = lt
  toOrd (equal _)     = eq
  toOrd (greater _ _) = gt

  cmp : ℕ → ℕ → Ord
  cmp m n = toOrd (compare m n)

  F = λ (xs : _) →  ∷ ♯ merge cmp (map (_*_ ) xs) (map (_*_ ) xs)

  postulate
    lemma : ∀ n → cmp ( * suc n) ( * suc n) ≡ lt

  isCon : ∀ (xs ys : Stream ℕ) n →
          (∀ {m} → m <′ n → Eq m xs ys) →
          Eq n (F xs) (F ys)
  isCon _        _         zero    _   = refl
  isCon (x ∷ xs) (y  ∷ ys) (suc n) hyp with cong Vec.head (hyp (s≤′s z≤′n))
  isCon ( ∷ xs) (. ∷ ys) (suc n) hyp | refl =
    cong (λ zs →  ∷  ∷ zs) (begin
      take n (merge cmp (map (_*_ ) (♭ xs)) (map (_*_ ) (♭ xs)))  ≡⟨ iCantBeBothered ⟩
      take n (merge cmp (map (_*_ ) (♭ ys)) (map (_*_ ) (♭ ys)))  ∎)
    where postulate iCantBeBothered : _
  isCon (suc x ∷ xs) (.(suc x) ∷ ys) (suc n) hyp | refl
    with cmp ( * suc x) ( * suc x) | lemma x
  isCon (suc x ∷ xs) (.(suc x) ∷ ys) (suc n) hyp | refl | .lt | refl =
    cong (λ zs →  ∷  * suc x ∷ zs) (begin
      take n (merge cmp (map (_*_ ) (♭ xs))
                        (map (_*_ ) (suc x ∷ xs)))  ≡⟨ iCantBeBothered ⟩
      take n (merge cmp (map (_*_ ) (♭ ys))
                        (map (_*_ ) (suc x ∷ ys)))  ∎)
    where postulate iCantBeBothered : _

hamming : Stream ℕ
hamming = ContractiveFun.fixpoint hammingF