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.

翻译：我们提出AlgCo（代数共归纳法），这是一个实用的框架，用于对常用共归纳类型（如自然数余集、流和有限分支因子的无穷树）进行归纳推理。关键思想是利用域理论中的代数完全偏序概念，通过对其元素"稠密集"上的原始递归来定义共归纳类型上的连续操作，从而通过简单的归纳证明实现代数共归纳类型的便利推理策略。我们在Coq中实现了AlgCo框架，并通过验证埃拉托色尼筛法的流变体、基于形式语言共归纳字典编码的正则表达式库，以及随机比特模型中离散概率分布上共归纳采样过程的期望值语义，展示了其强大功能。