Towards Corecursion Without Corecursion in Coq

Coinduction is an important concept in functional programming. To formally prove properties of corecursive functions one can try to define them in a proof assistant such as Coq. But there are limitations on the functions that can be defined. In particular, corecursive calls must occur directly under a call to a constructor, without any calls to other recursive functions in between. In this paper we show how a partially ordered set endowed with a notion of approximation can be organized as a Complete Partial Order. This makes it possible to define corecursive functions without using Coq's corecursion, as the unique solution of a fixpoint equation, thereby escaping Coq's builtin limitations