Inductive Reasoning for Coinductive Types

TL;DR

This paper introduces AlgCo, a practical framework for inductive reasoning over coinductive types like streams and trees, leveraging domain theory to enable proofs by induction in Coq.

Contribution

It presents a novel approach using algebraic complete partial orders to facilitate inductive reasoning on coinductive types, implemented in Coq.

Findings

Verified a stream-based sieve of Eratosthenes

Developed a coinductive regular expression library

Formalized expected value semantics for coinductive sampling

Abstract

We present AlgCo (Algebraic Coinductives), a practical framework for inductive reasoning over commonly used coinductive types such as conats, streams, and infinitary trees with finite branching factor. The key idea is to exploit the notion of algebraic complete partial order from domain theory to define continuous operations over coinductive types via primitive recursion on ``dense'' collections of their elements, enabling a convenient strategy for reasoning about algebraic coinductives by straightforward proofs by induction. We implement the AlgCo framework in Coq and demonstrate its power by verifying a stream variant of the sieve of Eratosthenes, a regular expression library based on coinductive trie encodings of formal languages, and expected value semantics for coinductive sampling processes over discrete probability distributions in the random bit model.