We describe two representations for real numbers, signed
digit streams and Cauchy sequences. We give coinductive proofs for the
correctness of functions converting between these two representations to
show the adequacy of signed digit stream representation. We also show
a coinductive proof for the correctness of a corecursive program for the
average function with regard to the signed digit stream representation.
We implemented this proof in the interactive proof
system Minlog. Thus,
reliable, corecursive functions for real computation can be guaranteed,
which is very helpful in formal software development for real numbers.