The Power of Parameterization in Coinductive Proof

摘要

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.