Sufficiently Complete Partial Orders: Towards Corecursion Without Corecursion in Coq

Presented at the WPTE 2022 workshop (https://wpte2022.github.io), Haïfa, Israel, August 2022, whose proceedings will be published in a journal. Corresponds to preprint https://hal.inria.fr/hal-03689027v4.Coinduction is an important concept in functional programming. To formally prove properties ofcorecursive functions one can try to define them in a proof assistant such as Coq. But there arestrong limitations on the corecursive functions that can be defined. In particular, one cannot freelymix corecursion with recursion. In this paper we introduce the notion of Sufficiently Complete PartialOrder (SCPO) that enables us to transform a program’s coinductive types by means of ”sufficientlycompleting” inductive types, thereby escaping Coq’s builtin limitations. We also show how corecursive functions can be defined on SCPOs without actually using corecursion, by adapting some recentwork where we show how this can be done by means of the unique solution of a fixpoint equation