Computer Aided Formal Reasoning (G53CFR, G54CFR)
  Thorsten Altenkirch

  Lecture 16: More on coinductive definitions

  In this lecture we continue the topic of coinductive
  definitions. We cover the following aspects

  1 We discuss why *co*-inductive definitions can be
    considered as the dual ("mirror image") of inductive definitions. 
  2 We compare our definition of extensional equality for
    streams (_≈_) with the traditional definition as the "largest
  3 We show that Streams over A are "extensionally isomorphic" to
    functions over the natural numbers. This is a general phenomen
    (all coinductive types can be encoded using functions over the
    natural numbers).
  4 We look at an example where we mix inductive and coinductive
    definitions - stream processors as a representation of functions
    over streams.

module l16 where

open import Coinduction
open import Data.Nat hiding (fold)
open import Data.List hiding (unfold)
open import Relation.Binary.PropositionalEquality
open import l15 hiding (tail)

{- 1 Coinductive types as the dual of inductive types. -}

{- For inductive types like lists we can define a "fold"-combinator 
   which is a universal combinator to define recursive functions.
   The type of fold can be derived form the constructors of list 
   and gives rise to a function form lists into another set.

   fold n c replaces each [] by n and each _∷_ by c. This is only
   possible if the list is finite.

fold : {A B : Set}  B  (A  B  B)  List A  B
fold n c [] = n
fold n c (x  xs) = c x (fold n c xs)

{- For coinductive types we start not with the constructors but with
   the destructors - in the case of streams head and tail. -}

head :  {A}  Stream A  A
head (a  as) = a

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

{- Instead of fold we a combinator "unfold" which is universal for
   corecursive definitions. The type of unfold is based on the
   destructors and gives rise to a function from a given set to the
   set of streams.

   unfold h t b produces a stream such that any program which uses
   only h and t on B behaves the same way if we replace h by head and
   t by tail.

unfold : {A B : Set}  (B  A)  (B  B)  B  Stream A
unfold h t b = h b  ( unfold h t (t b))

{- 2 Bisimulations -}

{- A relation R on streams is a bismulation if bisimilar streams have
   the same head and their tails are related by R again. -}

record Bisim {A : Set}(_R_ : Stream A  Stream A  Set) : Set where 
    hd :  {as bs}  as R bs  head as  head bs
    tl :  {as bs}  as R bs  tail as R tail bs

open Bisim

{- We can show that ≈ is a bisimulation -}

bisim≈hd :  {A} {as bs : Stream A}  as  bs  head as  head bs
bisim≈hd (x  xs≈) = refl  

bisim≈tl :  {A} {as bs : Stream A}  as  bs  tail as  tail bs
bisim≈tl (_  xs≈) =  xs≈  

bisim≈ :  {A}  Bisim (_≈_ {A})
bisim≈ = record {hd = bisim≈hd; tl = bisim≈tl}

{- On the other hand any two streams which are related by *any*
   bisimulation (which are bisimilar) are already extensionally

bisim→≈ : {A : Set}(_R_ : Stream A  Stream A  Set)  Bisim _R_  (as bs : Stream A)  as R bs  as  bs
bisim→≈ R bisimR (a  as) (b  bs) asRbs with hd bisimR asRbs 
bisim→≈ R bisimR (.b  as) (b  bs) asRbs | refl = b  ( bisim→≈ R bisimR ( as) ( bs) (tl bisimR asRbs))

{- Hence traditionally ≈ is defined as "the largest bisimulation". -}

{- 3 Streams are extensionally isomorphic to functions over ℕ -}

{- The function nth on streams is not partial (because there is no [])
   hence this gives rise to a function from streams to functions over
   the natural numbers.
nthStream :  {A}  Stream A  (  A)
nthStream (a  as) zero = a
nthStream (a  as) (suc n) = nthStream ( as) n

{- On the other hand given a function over the natural numbers we can
   recursively construct a corresponding stream. 

mkStream :  {A}  (  A)  Stream A
mkStream f = f 0  ( mkStream  n  f (suc n)))

We want to show that nthStream and mkStream are inverses. However, we
have to use extensionally equality on both sides. Hence there is no
hope to be able to prove:

fun→fun : ∀ {A} → (f : ℕ → A) → nthStream (mkStream f) ≡ f
fun→fun f = {!!}

but instead:

fun→fun :  {A}  (f :   A)  (n : )  nthStream (mkStream f) n  f n
fun→fun f zero = refl
fun→fun f (suc n) = fun→fun  n  f (suc n)) n

{- In the other direction we use extensional equality on streams. -}

stream→stream :  {A}  (as : Stream A)  mkStream (nthStream as)  as
stream→stream (a  as) = a  ( stream→stream ( as))

{- What about CoLists? Can they also be represented using functions
   over the natural numbers?-}

{- 4 Stream processors -}

{- Stream processors are a way to represent functions from stremas to
   streams. They are interesting becuase we have to use a mixed
   inductive - coinductive definition. -}

data SP (A B : Set) : Set where
  get : (A  SP A B)  SP A B
  put : B   (SP A B)  SP A B

{- The meaning of a stream processor is a function on streams -}

⟦_⟧_ :  {A B}  SP A B  Stream A  Stream B
 get f  (a  as) =  f a  ( as)
 put b sp   as = b  (   sp  as)

{- we can define the idnetity stream processor -}

id :  {A}  SP A A
id = get  a  put a ( id))

idLem :  {A}  (as : Stream A)   id  as  as
idLem (a  as) = a  ( idLem ( as))

{- and composition on stream processors -}

_>>>_ :  {A B C}  (sp : SP A B)  (sp' : SP B C)  SP A C
get f >>> sp = get  a  f a >>> sp)
put b sp >>> get g =  sp >>> g b
put b sp >>> put c sp' = put c ( put b sp >>>  sp')

>>>Lem :  {A B C}  (sp : SP A B)  (sp' : SP B C)  (as : Stream A) 
         sp >>> sp'  as   sp'  ( sp  as)
>>>Lem (get f) sp (a  as) = >>>Lem (f a) sp ( as)
>>>Lem (put b sp) (get g) as = >>>Lem ( sp) (g b) as
>>>Lem (put b sp) (put c sp') as = c  ( (>>>Lem (put b sp) ( sp') as))