The power of parameterization in coinductive proof
the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013) |
Published by ACM
Coinduction is one of the most basic concepts in computer science.
It is therefore surprising that the commonly-known lattice-theoretic
accounts of the principles underlying coinductive proofs are lacking
in two key respects: they do not support compositional reasoning
(i.e., breaking proofs into separate pieces that can be developed
in isolation), and they do not support incremental reasoning (i.e.,
developing proofs interactively by starting from the goal and generalizing
the coinduction hypothesis repeatedly as necessary).
In this paper, we show how to support coinductive proofs that
are both compositional and incremental, using a dead simple construction
we call the parameterized greatest fixed point. The basic
idea is to parameterize the greatest fixed point of interest over the
accumulated knowledge of “the proof so far”. While this idea has
been proposed before, by Winskel in 1989 and by Moss in 2001,
neither of the previous accounts suggests its general applicability
to improving the state of the art in interactive coinductive proof.
In addition to presenting the lattice-theoretic foundations of parameterized
coinduction, demonstrating its utility on representative
examples, and studying its composition with “up-to” techniques,
we also explore its mechanization in proof assistants like Coq
and Isabelle. Unlike traditional approaches to mechanizing coinduction
(e.g., Coq’s cofix), which employ syntactic “guardedness
checking”, parameterized coinduction offers a semantic account of
guardedness. This leads to faster and more robust proof development,
as we demonstrate using our new Coq library, Paco.