------------------------------------------------------------------------
-- A formalisation of some definitions and laws from Section 3 of Ralf
-- Hinze's paper "Streams and Unique Fixed Points"
------------------------------------------------------------------------

module Hinze.Section3 where

open import Stream.Programs
open import Stream.Equality
open import Stream.Pointwise
open import Hinze.Section2-4
open import Hinze.Lemmas

open import Coinduction hiding ()
open import Data.Product
open import Data.Bool
open import Data.Vec hiding (_⋎_)
open import Data.Nat
import Data.Nat.Properties as Nat
import Relation.Binary.PropositionalEquality as P
open import Algebra.Structures
private
  module CS = IsCommutativeSemiring Nat.isCommutativeSemiring

------------------------------------------------------------------------
-- Definitions

pot : Prog Bool
pot = true   (pot  false )

msb : Prog 
msb = 1   (2   _*_  msb  2   _*_  msb)

ones′ : Prog 
ones′ = 1   (ones′  ones′  _+_  1 )

ones : Prog 
ones = 0 ≺♯ ones′

carry : Prog 
carry = 0   (carry  _+_  1   0 )

carry-folded : carry  0   carry  _+_  1 
carry-folded = carry 

2^carry : Prog 
2^carry = 2   _^_  carry

turn-length :   
turn-length zero    = zero
turn-length (suc n) =  + suc 
  where  = turn-length n

turn : (n : )  Vec  (turn-length n)
turn zero    = []
turn (suc n) = turn n ++ [ n ] ++ turn n

tree :   Prog 
tree n = n   (turn n ≺≺ tree (suc n))

frac : Prog 
frac = 0   (frac  nat  _+_  1 )

frac-folded : frac  nat  frac
frac-folded = frac 

god : Prog 
god = (2   _*_  frac)  _+_  1 

------------------------------------------------------------------------
-- Laws and properties

god-lemma : god  2*nat+1  god
god-lemma =
  god
                                          ≡⟨ P.refl 
  (2   _*_  (nat  frac))  _+_  1 
                                          ≊⟨  _+_ ⟩-cong (2   _*_  (nat  frac))
                                                          (2*nat  2   _*_  frac)
                                                          (zip-const-⋎ _*_ 2 nat frac)
                                                          (1 ) (1 ) (1  )  
  (2*nat  2   _*_  frac)  _+_  1 
                                          ≊⟨ zip-⋎-const _+_ 2*nat (2   _*_  frac) 1 
  2*nat+1  god
                                          

carry-god-nat : 2^carry  _*_  god  tailP nat
carry-god-nat =
  2^carry  _*_  god
                                                           ≡⟨ P.refl 
  (2   _^_  (0   carry  _+_  1 ))  _*_  god
                                                           ≊⟨  _*_ ⟩-cong (2   _^_  (0   carry  _+_  1 ))
                                                                           (1   2   _*_  2^carry) lemma
                                                                           god (2*nat+1  god) god-lemma 
  (1   2   _*_  2^carry)  _*_  (2*nat+1  god)
                                                           ≊⟨ ≅-sym (abide-law _*_ (1 ) 2*nat+1
                                                                                   (2   _*_  2^carry) god) 
  1   _*_  2*nat+1  (2   _*_  2^carry)  _*_  god
                                                           ≊⟨ ⋎-cong (1   _*_  2*nat+1) 2*nat+1
                                                                     (pointwise 1  s  1   _*_  s)  s  s)
                                                                                  (proj₁ CS.*-identity) 2*nat+1)
                                                                     ((2   _*_  2^carry)  _*_  god)
                                                                     (2   _*_  (2^carry  _*_  god))
                                                                     (pointwise 3  s t u  (s  _*_  t)  _*_  u)
                                                                                   s t u  s  _*_  (t  _*_  u))
                                                                                  CS.*-assoc (2 ) 2^carry god) 
  2*nat+1  2   _*_  (2^carry  _*_  god)
                                                           ≊⟨ P.refl  coih 
  2*nat+1  2   _*_  tailP nat
                                                           ≊⟨ ≅-sym (tailP-cong nat (2*nat  2*nat+1) nat-lemma₂) 
  tailP nat
                                                           
  where
  coih =  ⋎-cong (2   _*_  (2^carry  _*_  god))
                  (2   _*_  (tailP nat))
                  ( _*_ ⟩-cong (2 ) (2 ) (2  )
                                (2^carry  _*_  god) (tailP nat)
                                carry-god-nat)
                  (tailP 2*nat+1) (tailP 2*nat+1) (tailP 2*nat+1 )

  lemma =
    2^carry
                                                       ≡⟨ P.refl 
    2   _^_  (0   carry  _+_  1 )
                                                       ≊⟨ zip-const-⋎ _^_ 2 (0 ) (carry  _+_  1 ) 
    2   _^_  0   2   _^_  (carry  _+_  1 )
                                                       ≊⟨ ⋎-cong (2   _^_  0 ) (1 )
                                                                 (pointwise 0 (2   _^_  0 ) (1 ) P.refl)
                                                                 (2   _^_  (carry  _+_  1 ))
                                                                 (2   _*_  2^carry)
                                                                 (pointwise 1  s  2   _^_  (s  _+_  1 ))
                                                                               s  2   _*_  (2   _^_  s))
                                                                               x  P.cong (_^_ 2) (CS.+-comm x 1))
                                                                              carry) 
    1   2   _*_  2^carry