Proofs by induction on some inductively defined structure, e. g., finitely-branching trees, may appeal to the induction hypothesis at any point in the proof, provided the induction hypothesis is only used for immediate substructures, e. g., the subtrees of the node we are currently considering in the proof. The basic principle of structural induction can be relaxed to course-of-value induction, which allows application of the induction hypothesis also to non-immediate substructures, like any proper subtree of the current tree. If course-of-value induction is not sufficient yet, we can resort to define a well-founded relation on the considered structure and use the induction hypothesis for any substructure which is strictly smaller with regard to the constructed relation. At a closer look, however, this well-founded induction is just structural induction on the derivation of being strictly smaller. This means that in a logical system that allows us to construct inductive predicate and relations, such as, e. g., Martin-Löf Type Theory (Nordström et al. 1990) or the Calculus of Inductive Constructions (Paulin-Mohring 1993), structural induction is complete for any kind of inductive proof.

In all these flavors of induction, validity of induction hypothesis application can be checked easily and locally, independent of its context. In proof assistants, in principle a structural termination checker (Giménez 1995; Abel 2000) sufficesFootnote 1 to check such inductive proofs, which looks at the proof tree, extracts all calls to the induction hypotheses, and checks that they happen only on structurally smaller arguments. In practice, mutual induction is supported as well, based on a simple static call graph analysis (Abel and Altenkirch 2002; Barras 2010; Ben-Amram 2008; Hyvernat 2014).

Dually to structural induction, in a coinductive proof of a proposition defined as the greatest fixed-point of a set of rules, we may appeal to the coinduction hypothesis to fill the premises of the rule we have chosen to prove our goal. For instance, two infinite streams may be defined to be bisimilar if their heads are equal and their tails are bisimilar, coinductively. Our goal might be to show that bisimilarity is reflexive, i. e., any stream is bisimilar to itself. To establish bisimilarity, we use the sole rule with the first subgoal to show that the head of the stream is equal to itself. After this breath-taking enterprise, we are left with the second subgoal to show that the tail of the stream is bisimilar to itself, which we solve by appeal to the coinduction hypothesis. At this point, it is worth noting that not the stream got smaller (the tail of an infinite stream is still infinite), but the coinductive hypothesis is guarded by a rule application. This means that the coinductive proof can unfold into a possibly infinitely deep derivation without getting into a “busy loop”, meaning the proof is productive.

In a similar way as for induction, we seek to relax the criterion for well-formed coinductive proofs, which states that only the immediate subgoals of the final rule application can be filled by the coinductive hypothesis. We can allow several rule applications until we reach the coinductive hypothesis from the root of the derivation. This is dual to course-of-value induction and could be called guarded coinduction.Footnote 2

In contrast to induction, checking the validity of calls to the coinduction hypothesis requires us to look at the context of the calls rather than the call arguments. We have to check that the calls to the coinductive hypotheses happen in a constructor context, i. e., a context of coinductive rule applications only. This lack of locality also leads to a loss of compositionality of proofs by guarded coinduction. For instance, consider a coinductive proof of the bisimilarity of two streams through a bisimilarity chain, i. e., via some intermediate streams and the use of transitivity of bisimilarity. Transitivity is not a constructing rule for bisimilarity,Footnote 3 but an admissible rule proven by coinduction. As transitivity is not a constructor, we cannot use the coinduction hypothesis under transitivity nodes in the proof tree. In practice, often a severe restructuring of a natural informal proof is necessary to make it guarded and please a structural guardedness checker. The resulting proofs may be highly non-compositional and bloated, especially if proofs of previous lemmata have to be inlined and fused into the current proof.

To regain compositionality, we have to relax the contexts of coinductive hypothesis applications to include admissible rules and lemma invocation in general, without jeopardizing productivity. Such contexts need to produce one more rule constructor than they consume, which must be easily verifiable by the productivity checker. Sized types (Hughes et al. 1996; Amadio and Coupet-Grimal 1998; Barthe et al. 2004; Abel 2008; Sacchini 2013) offer the necessary technology. Coinductive types, propositions, and relations are parameterized by an ordinal \(i \le \omega \) which denotes the minimum definedness depth of their derivations. Semantically, this idea is already present in Mendler’s work (Mendler et al. 1986; Mendler 1991), and it is implicit in the principle of ordinal iteration to construct the greatest fixed point of a monotone operator F. We define the approximants \(\nu ^i F\) of the greatest fixed-point \(\nu ^\omega F\) by induction on ordinal i as follows:

For monotone F, we obtain a descending chain \(\nu ^0 F \sqsupseteq \nu ^1 F \sqsupseteq \cdots \sqsupseteq \nu ^\omega F\). The greatest fixed point of F is reached at stage \(\omega \) if F is continuous in the sense that \(\sqcap _{i \in I} F(A_i) \sqsubseteq F(\sqcap _{i \in I} A_i)\). For instance, all strictly positive type transformers correspond to continuous operators (Abel 2003, Theorem 1).

An alternative construction of the greatest fixed-point uses deflationary iteration (Sprenger and Dam 2003; Abel 2012; Abel and Pientka 2013),

which gives a descending chain without the monotonicity of F. However, the same conditions on F are needed to reach the fixed point at stage \(\omega \).

Giving names to the approximants \(\nu ^i F\) of coinductive type \(\nu ^\omega F\), we can express through the type system when a term t, which acts as the context for the coinductive hypothesis, produces one more constructor than it consumes: it needs to have type \(\forall i.\; \nu ^i F \rightarrow \nu ^{i+1} F\) polymorphic in “size” (depth) i. Such a context is called guarding. A weaker, but very common and useful property of a function t is to be guardedness preserving, i. e., having type \(\forall i.\; \nu ^i F \rightarrow \nu ^i F\). For instance, consider bisimilarity on streams, which is defined using relation transformer \(F(X)(x,y) = (\mathsf {head}\,x \equiv \mathsf {head}\,y) \times X\,(\mathsf {tail}\,x)\,(\mathsf {tail}y)\). The symmetry lemma of bisimilarity \(\forall i.\, \nu ^i F (x,y) \rightarrow \nu ^i F (y,x)\) is guardedness preserving: to produce one constructor of the requested bisimilarity derivation, it only needs to inspect the last constructor of the given bisimilarity derivation. Analogously, transitivity of bisimilarity receives type \(\forall i.\; \nu ^i F (x,y) \rightarrow \nu ^i F (y,z) \rightarrow \nu ^i F (x,z)\). Here, to produce the last rule of the output derivations we only need to inspect the last rule of the two input derivations. This typing allows us to freely use transitivity in coinductive proofs without jeopardizing the validity of the coinductive hypothesis.

Tracking guardedness levels in the type systems through “sized” coinductive types gives us compositional coinduction, as we can freely abstract out, for instance, guardedness-preserving contexts without upsetting some structural productivity checker who can only deal with concretely given code.

Recently, guardedness-preserving functions have been rediscovered in the context of Isabelle/HOL as friendly operations (Blanchette et al. 2015). Prototypical implementations of type-based termination with sized types exist for Coq (Sacchini 2015) and Agda. The latter has been subjected to a larger case study: an implementation of normalization by evaluation using the coinductive delay monad (Abel and Chapman 2014). Compositional coinduction with sized types seems to be a promising alternative to parameterized coinduction (Hur et al. 2013) and up-to techniques (Pous and Sangiorgi 2012).