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!