Computer Aided Formal Reasoning (G53CFR, G54CFR)
  Thorsten Altenkirch

  Lecture 15: Coinductive definitions

  In this lecture we look at infinite structures, in particular
  streams which are infinite sequences (similar to lists which are
  finite sequences). We are using Agdas type of delayed computations
  (∞ A) to represent infinite structures. Applying the Curry-Howard
  isomorphism we can also represent infinite proofs. We are using this
  to define bisimilarity, i.e. extensional equality of streams.

module l15 where

open import Coinduction
open import Data.Nat
open import Data.List
open import Relation.Binary.PropositionalEquality

Agda doesn't permit the construction of infinite lists (as in Haskell)
because lists are defined inductively, hence all lists must be
constructable with a finite amount of constructors.

As a consequence Agda rejects the following program:

from : ℕ → List ℕ
from n = n ∷ from (suc n)

{- To represent infinite sequences we define the type of streams using 
   ∞ X which represents "delayed computations of X". Because we are
   not constructing the whole stream now we can represent an infinite
   objects. This is reminiscent of the definition of a function - we
   don't calculate its values yet but only when required. -}

infix 5 _∷_

data Stream (A : Set) : Set where
  _∷_ : A   (Stream A)  Stream A

{- ∞ comes with two basic operations

♯ : A → ∞ A (delay, turn a term into a delayed computation)
♭ : ∞ A → A (forcing a delayed computation to evaluate)

∞ = \infty, ♯ = \sharp, ♭ = \flat

{- We can now define ℕ by delaying the recursive computation of the
   tail of the stream.-}
from :   Stream 
from n = n   (from (suc n))

{- We can access the tails of the stream using: -}
tail :  {A}  Stream A  Stream A
tail (a  as) =  as

{- Or more generally we can obtain a list of the first n elements of a
   stream. -}
taken :  {A}  Stream A    List A
taken (a  as) zero = []
taken (a  as) (suc n) = a  taken ( as) n

{- Try "taken (from 0) 10" -}

{- It is important that a recursive definition computing a stream
   (such as from) is "productive", i.e. whenever we want to access any
   component of the stream we can do this by forcing previously
   delayed computation. -}

{- The following is an example of a non-productive definition which is
   rejected by Agda

bad : Stream ℕ
bad = 0 ∷ (♯ (tail bad))

   While we can compute the head of bad (0) we cannot calculate its tail,
   because it is just defined by itself (bad recursion). 

   Agda recognizes productive definitions, if they are "guarded". I.e. ♯
   guards a recursive call and there are only constructors in between
   ♯ and the recursive call, not arbitrary functions like tail.

   Note that there are cases of productive definitions which are not
   guarded. Agda will reject them and we have to find another way to
   calculate the result. This is similar to recursive definitions
   which are structurally recursive but this is not always recognized
   by Agda.

{- Let's prove a simple theorem about "from".

   First of all we notice that Stream like List is a "functor", i.e. 
   we can "map" a function over a stream:
mapStream : {A B : Set}  (A  B)  Stream A  Stream B
mapStream f (a  as) = f a   (mapStream f ( as))
    "mapStream f as" applies the function f to each of the components
   of as. Note that the definition of mapStream is guarded and that
   each time we force the output (i.e. force the delayed computation 
   "♯ (mapStream f (♭ as)") this will in turn force further
   computation of the input by evaluating "♭ as".
  The theorem we want to prove is that mapping suc to from n is the
   "same" as from (suc n):

  (n : ℕ) → mapStream suc (from n) ≡ from (suc n)

  However, we are unable to prove the theorem in the above form. The
  reason is that Agdas propositional equality (≡) is too
  "intensional". Consider

  "mapStream suc (from zero)"
  this evaluates to something like
  "1 ∷ .l15.♯-2 suc 0 (.l15.♯-0 0)"

  "from (suc zero)"
  this evaluates to something like
  "1 ∷ .l15.♯-0 1"

  While the heads of the streams (1) are clearly definitionally equal
  the tails are different delayed computation. Moreover both
  expressions are closed and hence the only way to prove 

  "mapStream suc (from zero) ≡ from (suc zero)"

  would be by refl but this is only possible if they are
  definitionally equal. 

  Hence we need a different "extensional" equality for streams. 
  This equality should identify two streams which have identical

  The main idea for the definition is to apply the idea of a delayed
  computation into the delayed computation of a stream. Hence we
infix 4 _~_

data _~_ {A} : (xs ys : Stream A)  Set where
  _∷_ :  {x y xs ys}  (x  y)   ( xs ~  ys)  x  xs ~ y  ys

{- The idea is that to prove that two streams are equal we show that
   the heads are equal and provide a delayed computation proving that
   the tails are equal. -}

infix 4 _≈_
  The definition used in the Agda library gets rid of the equality
  proofs by noting that we can just identitfy x and y. It is easy to
  show that both are equivalent.

data _≈_ {A} : (xs ys : Stream A)  Set where
  _∷_ :  x {xs ys} (xs≈ :  ( xs   ys))  x  xs  x  ys

{- For historic reasons the relation _~_ is called "bisimularity"
   because it is conventionally defined via "bisimulation". Our
   definition using Curry-Howard and the idea of a delayed computation
   is an alternative.

{- It is now surprisingly easy to prove the reformulated nthLem: -}

nthLem : (n : )  mapStream suc (from n)  from (suc n)
nthLem n = suc n   nthLem (suc n)

{- We simply observe that the heads of both sides are identical and
   that the tails are an instance of the theorem we are just about to
   prove. Hence we can construct an infinite proof that both streams
   are equal. 

{- We show that ≈ is an equivalence relation using infinite proofs
   again.  -}

refl≈ :  {A}  (as : Stream A)  as  as
refl≈ (a  as) = a   refl≈ ( as)

sym≈ :  {A}  {as bs : Stream A}  as  bs  bs  as
sym≈ (a  as≈bs) = a   sym≈ ( as≈bs)

trans≈ :  {A}  {as bs cs : Stream A}  as  bs  bs  cs  as  cs
trans≈ (a  as≈bs) (.a  bs≈cs) = a   trans≈ ( as≈bs) ( bs≈cs)