Coinduction

Proof Methods for Corecursive Programs
(Jeremy Gibbons and Graham Hutton)

5. Coinduction

A bisimulation

- A relation R on lists

xs R ys if xs = ys = \bot
or xs = ys = []
or \exists v,vs,ws. xs=v:vs and ys=v:ws and vs R ws

The two lists xs and ys are related by a bisimulation. They are
either both undefined, both empty, or both non-empty with heads
that are equal and tails that are themselves releated by the
bisumulation.

xs ~ ys if \exists R. R is a bisimulation and xs R ys

xs and ys are related by such a bisimulation.

Coinduction

- xs = ys iff xs ~ ys

The proof is present in the paper.

A Proof Principle

The problem of proving map f (iterate f x) = iterate f (f x) is
equal to the problem of finding a bisimulation that relates the two
lists.

For example, R = { (map f (iterate f x), iterate f (f x)) f, x of
appropriate types }.

To verify R is a bisimulation is to prove the equality!