BISIMULATION ON STREAMS

A bisimulation is a relation ~ on stream such that:
  if s1~s2 then (head s1) = (head s2) and (tail s1) ~ (tail s2)

Coinduction Principle:
  Bisimulation implies equality:
  if ~ is a bisimulation and s1 ~ s2, then s1 = s2

> import Streams

In the file Streams.lhs we defined the stream of natural numbers
in two different ways, nat and nat'.
We want to prove that the two streams are equal.

We do it by using the coinduction principle.
Let's define a bisimulation relation:

  s1 ~ s2 if there is a natural number n such that
               s1 = n:(s1+1)  and s2 = unfold id (+1) n

Proof that it is a bisimulation:
Suppose s1 ~ s2, then
  head s1 = head (n:(s1+1)) = n
  head s2 = head (unfold id (+1) n) = id n = n
   therefore (head s1) = (head s2);
  tail s1 = s1+1 = (n:(s1+1))+1
          = (n+1) : (s1+1)+1
          = (n+1) : (tail s1)+1
  tail s2 = tail (unfold id (+1) n)
          = unfold id (+1) (n+1)
    therefore (tail s1) ~ (tail s2)
In conclusion ~ is a bisimulation.
Since nat ~ nat', we have, by the coinduction principle,
  nat = nat'.

Hint:
Very often, as in the example above, the bisimulation that we need
relates generalizations of the definition of the two streams that
we want to equate.
In the example, we generalized the relation by replacing the starting
point 0 with an arbitrary number n.

Exercise:
Make yourself familiar with this proof technique by proving that
fac = fac' and  fib = fib'.

A third way of defining the same stream uses the traditional
recursive form of the Fibonacci function:

> rfib :: Integer -> Integer
> rfib 0 = 0
> rfib 1 = 1
> rfib n = rfib (n-1) + rfib (n-2)

We want to prove that 
  map rfib [0..] = fib
We can do it again by using the coinduction principle.

The relation we are using is:
s1 ~ s2 iff there are two numbers a and b such that
            s1 = a : b : s1 + (tail s1)  and
            s2!!0 = a and s2!!1 = b and s2!!n = s2!!(n-1)+s2!!(n-2) for n>1
           
Verification that ~ is a bisimulation.
Suppose s1 ~ s2  (with parameters a and b)

  head s1 = a = s2!!0 = head s2

  tail s1 = b : s1 + (tail s1)
          = b : (head s1 : tail s1) + (b : s1 + (tail s1))
          = b : (a+b) : tail s1 + s1 + tail s1
          = b : (a+b) : tail s1 + tail (tail s1) 
  (tail s2)!!0 = s2!!1 = b
  (tail s2)!!1 = s2!!2 = s2!!1 + s2!!0 = b + a
  (tail s2)!!n = s2!!(n+1) = s2!!n + s2!!(n-1)
               = (tail s2)!!(n-1) + (tail s2)!!(n-2) if n>1
  Therefore (tail s1)~(tail s2) with parameters b and a+b.    
           
In conclusion ~ is a bisimulation, therefore it implies equality
by the coinduction principle.
We can show that fib ~ map rfib [0..] with parameters 0 and 1:
  fib = 0 : 1 : fib + (tail fib) by definition
  (map rfib [0..])!!0 = rfib 0 = 0
  (map rfib [0..])!!1 = rfib 1 = 1
  (map rfib [0..])!!n = rfib n                  for n>1
                      = rfib (n-1) + rfib (n-2)
                      =  (map rfib [0..])!!(n-1) + (map rfib [0..])!!(n-2)

In conclusion, fib = map rfib [0..] by the coinduction principle.

Exercise.
The definition of rfib is, as is well-known, very inefficient.
On the other hand fib is an efficient way of computing it.
We can give an efficient version of the recursive definition by:

> re2fib :: Integer -> (Integer,Integer)
> re2fib 0 = (0,1)
> re2fib n = let (a,b) = re2fib (n-1) in (b,a+b)

> refib :: [Integer]
> refib = map (fst.re2fib) [0..]

Prove, using the coinduction principle, that refib = fib.

Final exercise. 
Prove that the following streams are equal: al0 = alt1 = alt2.

> power :: [Integer] -> [Integer] -> [Integer]
> power = zipWith (^)

> alt0 :: [Integer]
> alt0 = power (-1) nat

> alt1 :: [Integer]
> alt1 = 1:alt1*(-1)

> alt2 :: [Integer]
> alt2 = fibt ^ 2 - fib * fibtt
> fibt = tail fib
> fibtt = tail fibt