Contemporary proof assistants impose restrictive syntactic guardedness conditions that reject many valid corecursive definitions. Existing approaches to overcome these restrictions present a fundamental trade-off between coverage and automation. We present Compositional Heterogeneous Productivity (CHP), a theoretical framework that unifies high automation with extensive coverage for corecursive definitions. CHP introduces heterogeneous productivity applicable to functions with diverse domain and codomain types, including non-coinductive types. Its key innovation is compositionality: the productivity of composite functions is systematically computed from their components, enabling modular reasoning about complex corecursive patterns. Building on CHP, we develop Coco, a corecursion library for Rocq that provides extensive automation for productivity computation and fixed-point generation.

翻译：当代证明辅助工具施加了严格的语法守卫条件，导致许多有效的共递归定义被拒绝。现有克服这些限制的方法在覆盖范围与自动化程度之间存在根本性权衡。本文提出组合异质生产力理论框架，将高度自动化与广泛的共递归定义覆盖范围相统一。该框架引入适用于具有不同定义域和值域类型（包括非共归纳类型）函数的异质生产力概念。其核心创新在于组合性：复合函数的生产力可通过其组成部分系统计算，从而实现对复杂共递归模式的模块化推理。基于此框架，我们开发了面向Rocq的共递归库Coco，为生产力计算和不动点生成提供了全面的自动化支持。