The power of parameterization in coinductive proof
Coinduction is one of most basic concepts in computer science. It is therefore surprising that commonly-known lattice-theoretic accounts of 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 goal and generalizing 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 parameterized greatest fixed point. The basic idea is to parameterize greatest fixed point of interest over 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 previous accounts suggests its general applicability to improving state of art in interactive coinductive proof.In addition to presenting 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.