Ordered Families of Equivalences (OFE)

In this chapter, we will go into the details of OFEs, non-expansiveness, and contractiveness. We will do this using streams of natural numbers. Streams are not important to the understanding of Iris. However, they form good intuition about the usefulness of OFEs. We will look at streams over natural numbers. These are infinite sequences with head being the first value and tail being the rest of the stream. We define streams as a coinductive type. You should be able to follow this file without extensive knowledge of coinduction.

Coinductive values are allowed to be infinitely deep, meaning we can construct an infinite stream of zeroes as follows:

CoFixpoints allows us to build coinductive values in the same way that Fixpoint allows us to use inductive types recursively. We can get the n'th element of the stream by iterating through the stream until we find the index we are looking for.

We can likewise define a stream from its n'th elements.

We will say that two streams are equivalent when the elements are equal. We can specify this using nth.

Now, for the OFE structure, we introduce the concept of approximate equivalence using the typeclass Dist. This typeclass defines a family of equivalence relations written [x ≡{n}≡ y] where n is the precision. In our case, this will decide how many of the elements of the stream we look at.

These relations should satisfy the following laws:

• dist_equivalence : ∀ n, Equivalence (dist n) As you would expect: The n-equivalences are equivalence relations.
• equiv_dist : ∀ x y, x ≡ y ↔ (∀ n, x ≡{n}≡ y) This states that, as the `precision' of the approximation approaches infinity, the equivalences approach true equivalence.
• dist_lt : ∀ n m x y, x ≡{n}≡ y → m < n → x ≡{m}≡ y This means that reducing the precision can only make more things approximately equivalent.

We can now package this together into an OFE.

We can now ask the question of whether we can build values from a sequence of better and better approximations. To this end, we use the concept of a chain. Here, chains are sequences such that all elements after the n'th element are n-equivalent. An OFE is complete if all chains approach a value. This is also called a COFE for complete OFE. In the case of streams, we can find the completion by considering the n'th number in the n'th stream, as all streams after this point agree on this value after this point.

There are two important classes of functions between OFEs called NonExpansive and Contractive. NonExpansive functions are functions that preserve dist. This is encoded using the setoid library as ∀ n, Proper (dist n ==> dist n) f. Contractive functions furthermore increase the `precision' one step. Encoded as ∀ n, Proper (dist_later n ==> dist n) f. dist_later is defined differently from what you might have seen elsewhere, but it is still equivalent to the usual definition. dist_later n x y := ∀ m, m < n → x ≡{m}≡ y

All Contractive functions are also NonExpansive, but this fact is not registered as an instance to improve type-class instance resolution. It is thus necessary to register this fact for your functions as well.

Furthermore, all NonExpansive functions are also Proper, meaning we only need to prove the strongest of these three properties and then use it for the rest.

We don't have any such nice properties for tail and nth. So we prove that they preserve the equivalence directly.

If we look at tail, we notice that it isn't NonExpansive for the same reason that SCons is contractive. However, it is anti-contractive in that it decreases the `precision' by one step. These functions are rarely used as they aren't NonExpansive and therefore don't behave as well as we would like. However, they can be used when constructing new functions by balancing anti-contractive functions with Contractive functions.

With the setup out of the way, we can now begin defining operations on streams. The first such operation will be appending a list to the front of a stream.

This operation is NonExpansive when we fix the list we wish to prepend. Furthermore, we can prove this without unfolding the definition of dist by using what we have proved thus far.

Now, let's define a stream that simply repeats a list over and over again. Intuitively, we should be able to define it as follows:

However, this correctly fails. Consider the case in which the list is empty. No matter how many times you repeat an empty list, the result remains empty. So we will never end up with an infinite stream. To fix this, we can insert a separator in between the repetitions of the list:

But this still fails with the same error. This is because Coq uses a simple syntactic check to validate co-fixpoint definitions. To satisfy this check, we are forced to syntactically produce at least one element of the stream per recursive call, which is violated by the call to sapp. In practice, this means that we cannot reuse most of our existing operations when writing new recursively defined streams. We instead have to implement it from scratch as follows:

To ensure that this definition is correct, we can show that it still solves the fixpoint equation. To do this, we first need to show that the helper function does what it is supposed to.

This can be non-trivial and requires code duplication, as mentioned previously. COFEs offer a way around these restrictions through guarded-fixpoints. Let us write the function as before, but with the result of a recursive call as the last argument:

We can then notice that this function is contractive with respect to this recursive argument s, as sapp is NonExpansive and SCons is Contractive.

To get a fixpoint for such a function, we need three things:

• The type we wish to produce an element of (stream) must have a COFE structure, which we defined earlier.
• The function we wish to find a fixpoint for must be contractive, which we just proved.
• Finally, the COFE must be inhabited, meaning there is an element of that type. We can use zeroes for this, as the choice of inhabitant doesn't matter.

With all conditions met, we can now define the fixpoint as follows:

And the fixpoint can be unfolded up to equivalence:

Furthermore, any such fixpoint is unique, so we can prove that our two definitions are equivalent.

A common operation one could consider on streams is mapping. This luckily conforms to the rules of co-fixpoints, but we will also define it using guarded recursion.

Notice that our recursive call takes different parameters. So we can't just build this as a fixpoint on streams. Instead, we need to build a fixpoint on stream → stream. However, this is not equipped with a canonical OFE structure. Instead, we need to write stream -d> streamO. Here, d stands for discrete, meaning we don't consider any OFE structure on the domain. As such, we are allowed to change the parameter arbitrarily on recursive calls.

In this way, we can use guarded-fixpoints as an alternative to co-fixpoints. Allowing us to use existing functions in the fixpoint definitions.

Rather than simply restating the fixpoint unfolding lemma directly, we will fully apply the function.

If we now wanted to create a stream of all the powers of 2, we would intuitively want something like this:

However, this again fails the syntactic check, as we are modifying the tail of the stream. To fix this, we could instead define a stream starting with a number n doubling n at every step.

To know that these definitions are equivalent, we must again prove that power2_helper and power2 satisfy respective fixpoint equations.

Now, just like before, we can instead define the function for which we wish to find a fixpoint:

This is again contractive in s because SCons is Contractive and stream_map is NonExpansive.

So we can now get a fixpoint, just as before.

Like before, we know that this fixpoint is unique, so it must be equivalent to the other definition.

iProp also has a COFE structure, but it is not a co-inductive type. This means that even though we can't use CoFixpoint to build propositions recursively, we can use fixpoint. Importantly, all the connectives of the logic are NonExpansive. To then use guarded fixpoints, we need a Contractive function like SCons. And for iProp, this is later ▷ P. We have already run into two connectives defined using the guarded-fixpoint, namely the weakest precondition WP, and invariants inv. This is why we can remove laters from premises when taking a step in the program, as this corresponds to unfolding the fixpoint, thus revealing a later.