Subsidiary Recursion in Coq

Aaron Stump, Alex Hubers, Christopher Jenkins, and Benjamin Delaware

abstract

This paper describes a functor-generic derivation in Coq of subsidiary recursion. With this recursion scheme, inner recursions may be initiated within outer ones, in such a way that outer recursive calls may be made on results from inner ones. The derivation utilizes a novel (necessarily weakened) form of positive-recursive types in Coq, dubbed retractive-positive recursive types. A corresponding form of induction is also supported. The method is demonstrated through several examples.