In this file you will discover a classic inductive predicate: acc. Through this example we will learn that induction can be performed over predicates and not only things that you think of as term/data. Some (relatively independent) bonuses explore coinduction and transfinite trees.

Accessibility

Given a binary relation R over an arbitrary type A, the accessible elements of R are those a:A from which there is no infinite chain a R a_1 R a_2 R a_3, etc. The set of accessible elements can also be defined as the least set S such that, for any a:A, if S contains all b such that a R b, then S must also contain a. In Coq, we don't use sets and relations. A type is an A:Type, a binary relation over it is some R:A->A->Prop, and a set is given via a predicate S:A->Prop. The least fixed point definition is directly obtained via the primitive notion of inductive definition.

If x : acc A R a then x must be of the form mk_acc A R a F where F gives, for any b for which there is a proof P of R a b, a subtree F b P : acc A R b. Thus x : acc A R a can be seen as a derivation tree obtained using a single inference rule: (acc b1) (acc b2) ... (acc bN) ...

---

mk_acc acc a where the bI form a complete enumeration of the elements b such that a R b. The rule has an arbitrary arity: it may be infinite, finite, and even zero (in which case the node is a leaf and the derivation is completed). This tree can be infinitely branching, but it cannot have an infinite branch -- this comes from the least fixed point / inductive nature of acc. This aspect will be explored later; for now, let us start with simple examples. We say that a relation is well-founded when all elements of its domain are accessible.

Accessibility for the predecessor relation over natural numbers.

Can you picture the shape of acc trees for that relation ? Prove that 2 is accessible, then generalize to all natural numbers.

When a relation is well-founded, we have H : acc _ R x for any x and we can induct on H. Formally this relies on the induction principle generated by Coq for each inductive definition, called acc_ind for acc. To understand this induction principle, it may be useful to think of H as a derivation tree, as explained above.

In the particular case when we induct over acc nat R_pred _ this yields an induction principle over natural numbers that is essentially the usual one, as illustrated in the next example.

Accessibility over the usual strict order on nat

Let us consider acc on (the converse of) lt. It is a well-founded relation but, unlike pred, its branching is unbounded: given x:nat, there are x-1 natural numbers y such that y<x.

This time, induct over acc nat R_lt x to show that x = x+0. Observe the stronger induction hypothesis that you obtain in this way: do you recognize a familiar scheme of proof by induction ?

Bonus 1: height

We want to express that a tree T : acc A R a has height at most n, i.e. all its branches are of length at most n. For technical reasons (related to the distinction between Type and Prop) we cannot write a predicate height that takes T as a parameter. Instead we define height A R a n that intuitively means that any T : acc A R a has height at most n.

Show that all acc-trees have a height when taking R := R_lt.

Now define some A and R such that wf A R but acc-trees do not have a height: they are transfinite trees.

Bonus 2: coinductives

We shall use least and greatest fixed points to understand inductive and coinductive definitions. Consider the lattice of subsets of some type A, ordered by inclusion. This corresponds to predicates over A, ordered by implication. Consider the following two operators over this lattice, the second one being for A := nat.

Inductive predicates, aka least fixed points

We define two predicates that intuitively correspond to the least fixed points of the previous two operators. To make this connection formal we would have to write mk_LFP : forall x, F LFP x -> LFP x but Coq won't allow this. So we inline F and, in the case of LFP_N, also translate the existential and disjunction connectives of F_N into a simpler form using two constructors; in this way, Coq allows us to work better on LFP_N.

We can now show that we have least pre-fixed points.

Observe finally that our two least fixed points are the extremal predicates of their respective lattices.

Coinductive predicates, aka greatest fixed points

We follow the same approach as before, but using coinductive rather than inductive definitions. Intuitively, we are forming greatest fixed points.

Show that GFP_N is a post-fixed point of F_N.

To show that it is the greatest post-fixed point, we use coinduction rather than induction. In the terminology of the lattice of predicates, we would be proving that the predicate P is less than GFP_N. This would be obtained by showing that P is a post-fixed point of F_N, i.e. showing that, for any x such that if P x, we have F_N P x, which is easy. Coq's coinduction principle is similar, with a difference that comes in part from the fact that F_N is not explicit in the definition of GFP_N. We launch coinduction using cofix HC which introduces an assumption HC : forall x, P x -> GFP_N x and (shockingly) keeps the same goal forall x, P x -> GFP_N x. The assumption HC can only be used after that the goal has been constructor using some constructor of the coinductive type -- this corresponds to introducing the missing F_N step. Improper uses of HC will lead to a failure upon Qed.

Both greatest fixed point examples are the true predicates. Prove it for GFP_id, using coinduction.

Fixed points and complete lattices may be familiar objects, but they do not provide the simplest intuitions for everybody. We outline next a more computational intuition. Induction on some type T (whose parameters are omitted for simplicity) corresponds to the definition of a recursive function of type T -> A, where each recursive call is performed on a (syntactically) strictly decreased argument. In other words, at every new iteration something is consumed. Coinduction on T corresponds to the definition of a recursive computation of type A -> T that produces a possibly infinite object, but in a productive manner: it calls itself recursively only to build subterms of the result, which has first been partially constructed using a constructor of the coinductive type. In other words, at every new iteration something is produced. Overall, this means that any finite prefix of the (possibly infinite) object can be obtained in finite time.

Bonus 3: infinite chains

We define infch as a coinductive predicate. As would be the case for an inductive definition, H : infch A R a is necessarily constructed from one of its constructors; in that case there is a single constructor mk_infch. However, coinductives correspond to greatest fixed points while inductives correspond to least fixed points. For now, this just means that you cannot induct on a coinductive; but you can still use inversion.

You don't need anything new to show that, if there is an infinite chain from some x, then x cannot be accessible.

To prove that for any inaccessible element x, there is an infinite chain starting from x, you need to reason by coinduction, cf. previous bonus. You will need some classical reasoning step: you can choose the axiom that suits you best.

We now define the existence of an infinite chain in a more usual way. Can you show that it is equivalent to the previous coinductive definition? You may need to assume more axioms from classical set theory.