Towards Corecursion Without Corecursion in Coq

EasyChair Preprint 8442, version 2

Abstract

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.

Keyphrases: Coq, coinductive type, corecursive function, fixpoint

@booklet{EasyChair:8442,
  author    = {Vlad Rusu and David Nowak},
  title     = {Towards Corecursion Without Corecursion in Coq},
  howpublished = {EasyChair Preprint 8442},
  year      = {EasyChair, 2022}}