Towards Corecursion Without Corecursion in Coq

EasyChair Preprint no. 8442, version 1

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: coinductive type, Coq, corecursive function, fixpoint

@Booklet{EasyChair:8442,
  author = {Vlad Rusu and David Nowak},
  title = {Towards Corecursion Without Corecursion in Coq},
  howpublished = {EasyChair Preprint no. 8442},

  year = {EasyChair, 2022}}