Module Sequences

A library of relation operators defining sequences of transitions and useful properties about them.

Zero, one or several transitions: reflexive, transitive closure of R.

One or several transitions: transitive closure of R.

No transitions from a state.

It is easy to characterize the fact that all transition sequences starting from a state a are infinite: it suffices to say that any finite sequence starting from a can always be extended by one more transition.

However, this is not the notion we are trying to characterize: that, starting from a, there exists one infinite sequence of transitions a --> a1 --> a2 --> ... -> aN -> .... Indeed, consider A = nat and R such that R 0 0 and R 0 1. all_seq_inf 0 does not hold, because a sequence 0 -->* 1 cannot be extended. Yet, R admits an infinite sequence, namely 0 --> 0 --> .... Another attempt would be to represent the sequence of states a0 --> a1 --> a2 --> ... -> aN -> ... explicitly, as a function f: nat -> A such that f i is the i-th state ai of the sequence.

This is a correct characterization of the existence of an infinite sequence of reductions. However, it is very inconvenient to work with this definition in Coq's constructive logic: in most use cases, the function f is not computable and therefore cannot be defined in Coq.

To obtain a practical definition of infinite sequences, we use the following coinductive definition of the predicate infseq a.

An inductive predicate such as star a b holds iff there exists a finite derivation of the conclusion star a b that uses the constructors star_refl and star_step a finite number of times. A coinductive predicate is similar, but holds iff there exists a finite OR INFINITE derivation of the conclusion that uses the constructors of the predicate a finite OR INFINITE number of times. In other words, an inductive predicate is a smallest fixpoint: the smallest predicate that satisfies its constructors; a coinductive predicate is a greatest fixpoint: the largest predicate that satisfies its constructors. The infseq predicate above must be defined coinductively. Indeed, if we define it inductively, the predicate would be empty (always false), since there are no base cases! Coq provides some primitive support for constructing infinite derivations of facts such as infseq a. Such constructions are proofs by coinduction. For example, we can prove the following:

This style of proof by coinduction, using the cofix tactic, is effective but can run into limitations of Coq's proof engine (the so-called "guard condition"). However, we can derive more conventional coinduction principles that are often easier to use.

Consider a set X of states A, that is, a predicate X: A -> Prop. Assume that for every a in X, we can make one R transition to a b that is still in X. Then, starting from a in X, we can transition to some a1 in X, then to some a2 still in X, then... It is clear that we are just building an infinite sequence of transitions starting from a. Therefore infseq a should hold. Let's prove this!

An even more useful variant of this coinduction principle considers a set X where for every a in X, we can make one *or several* transitions to reach a b in X.

Here is an example of use of infseq_coinduction_principle: if all finite transition sequences starting at a can be extended, infseq a holds.

Likewise, the function-based characterization infseq_with_function implies infseq.

A transition relation is functional if every state can transition to at most one other state.

Uniqueness of finite transition sequences.

A state cannot both diverge and terminate on an irreducible state.

If there exists an infinite sequence of transitions from a, all sequences of transitions arising from a are infinite.