Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Coco: Corecursion with Compositional Heterogeneous Productivity

Jaewoo Kim, Yeonwoo Nam, Chung-Kil Hur

TL;DR

This work addresses the limitations of existing coinductive reasoning in proof assistants by introducing Compositional Heterogeneous Productivity (CHP), a framework that computes productivity for corecursive definitions across heterogeneous domain and codomain types and supports compositional reasoning. CHP bases productivity on type-specific level sets and equality-up-to relations, enabling modular analysis of complex corecursive patterns and guaranteeing the existence of unique fixed points when productivity is sufficiently positive. Building on CHP, the Coco library automates productivity computation and fixed-point generation for a broad class of corecursive definitions in Rocq, while remaining extendable through user-defined CTTs/STTs and combinators; it can still require manual proofs in some cases, highlighting trade-offs with AmiCo. The approach significantly broadens automation and coverage for corecursion while preserving a modular structure, facilitating formal verification and synthesis of infinite data structures and transfinite computations in practical settings. The work lays a foundation for more automated second-order productivity and translation of generating functions to combinator forms, with implications for scalable, compositional corecursive reasoning in proof assistants.

Abstract

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.

Coco: Corecursion with Compositional Heterogeneous Productivity

TL;DR

This work addresses the limitations of existing coinductive reasoning in proof assistants by introducing Compositional Heterogeneous Productivity (CHP), a framework that computes productivity for corecursive definitions across heterogeneous domain and codomain types and supports compositional reasoning. CHP bases productivity on type-specific level sets and equality-up-to relations, enabling modular analysis of complex corecursive patterns and guaranteeing the existence of unique fixed points when productivity is sufficiently positive. Building on CHP, the Coco library automates productivity computation and fixed-point generation for a broad class of corecursive definitions in Rocq, while remaining extendable through user-defined CTTs/STTs and combinators; it can still require manual proofs in some cases, highlighting trade-offs with AmiCo. The approach significantly broadens automation and coverage for corecursion while preserving a modular structure, facilitating formal verification and synthesis of infinite data structures and transfinite computations in practical settings. The work lays a foundation for more automated second-order productivity and translation of generating functions to combinator forms, with implications for scalable, compositional corecursive reasoning in proof assistants.

Abstract

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.

Paper Structure

This paper contains 81 sections, 95 theorems, 107 equations, 26 figures.

Table of Contents

  1. Introduction
  2. AmiCo and Charguéraud's approach
  3. Problem with Rocq
  4. Solutions of AmiCo and Charguéraud's approach
  5. Problem with AmiCo and Charguéraud's approach
  6. Challenges and Our Approach
  7. Outline
  8. Key Ideas
  9. Appropriate level sets
  10. Productivities of constructor and destructors
  11. Analysis via productivity composition
  12. Second Order Productivity and Automation
  13. Implementation Challenges
  14. Coinductive Type
  15. Semantic Polynomial Functor
  16. ...and 66 more sections

Key Result

theorem 1

For a coalgebra $X \in I \!\rightarrow{}\! \mathbf{Type}$ with $\alpha \in X \Rightarrow{} \widehat{\mathcal{E}}(X)$, there uniquely exists $\overline{\alpha}\in X \Rightarrow{} \nu\widehat{\mathcal{E}}$ such that the diagram on the right commutes for all $i$ :

Figures (26)

  • Figure 1: Process of composing productivities for ${F_{\mathtt{s5}}}$
  • Figure 2: Well-definedness condition for $\mathtt{s5}$ (satisfied)
  • Figure 3: Well-definedness condition for $\mathtt{s4}$ (not satisfied)
  • Figure 4: Definition of container
  • Figure 5: Definition of SPF
  • ...and 21 more figures

Theorems & Definitions (115)

  • theorem 1: Final Coalgebra
  • Remark
  • definition 1
  • Remark
  • Remark
  • Remark
  • lemma 1
  • theorem 2
  • Remark
  • Remark
  • ...and 105 more