Breaking the Loop: Recursive Proofs for Coinductive Predicates in Fibrations

TL;DR

This paper introduces a recursive proof framework for coinductive predicates using fibrations and the later modality, simplifying proof construction and enabling the use of up-to techniques.

Contribution

It develops a novel fibrational recursive proof system for coinductive predicates, incorporating the later modality and up-to techniques, with proven soundness and completeness.

Findings

Recursive proofs are easier to construct and understand.

The framework supports up-to techniques as inference rules.

Proofs are sound and complete within the proposed system.

Abstract

The purpose of this paper is to develop and study recursive proofs of coinductive predicates. Such recursive proofs allow one to discover proof goals in the construction of a proof of a coinductive predicate, while still allowing the use of up-to techniques. This approach lifts the burden to guess invariants, like bisimulation relations, beforehand. Rather, they allow one to start with the sought-after proof goal and develop the proof from there until a point is reached, at which the proof can be closed through a recursion step. Proofs given in this way are both easier to construct and to understand, similarly to proofs given in cyclic proof systems or by appealing parameterised coinduction. In this paper, we develop a framework for recursive proofs of coinductive predicates that are given through fibrational predicate liftings. This framework is built on the so-called later modality, which has made its appearance in type theoretic settings before. In particular, we show the soundness and completeness of recursive proofs, we prove that compatible up-to techniques can be used as inference rules in recursive proofs, and provide some illustrating examples.