This files defines (a shallow embedding of) the category of OFEs: Complete ordered families of equivalences. This is a cartesian closed category, and mathematically speaking, the entire development lives in this category. However, we will generally prefer to work with raw Coq functions plus some registered Proper instances for non-expansiveness. This makes writing such functions much easier. It turns out that in many cases, we do not even need non-expansiveness. Unbundled version

Bundled version

When declaring instances of subclasses of OFE (like CMRAs and unital CMRAs) we need Coq to *infer* the canonical OFE instance of a given type and take the mixin out of it. This makes sure we do not use two different OFE instances in different places (see for example the constructors Cmra and Ucmra in the file cmra.v.) In order to infer the OFE instance, we use the definition ofe_mixin_of' which is inspired by the clone trick in ssreflect. It works as follows, when type checking @ofe_mixin_of' A ?Ac id Coq faces a unification problem: ofe_car ?Ac ~ A which will resolve ?Ac to the canonical OFE instance corresponding to A. The definition @ofe_mixin_of' A ?Ac id will then provide the corresponding mixin. Note that type checking of ofe_mixin_of' A id will fail when A does not have a canonical OFE instance. The notation ofe_mixin_of A that we define on top of ofe_mixin_of' A id hides the id and normalizes the mixin to head normal form. The latter is to ensure that we do not end up with redundant canonical projections to the mixin, i.e. them all being of the shape ofe_mixin_of' A id.

Lifting properties from the mixin

Discrete OFEs and discrete OFE elements

OFEs with a completion A (converging) "chain" is a sequence of type A such that from the n-th position onwards, everything is n-equal.

A "bounded chain" up to step index n is similar to a "chain", except that the sequence has length n, i.e., it is only defined for indices strictly less than n.

We define a complete OFE, COFE for short. Roughly speaking, the power of a COFE (over an OFE) is to allow us to compute fixpoints. We want to compute two different kinds of fixpoints: 1. Fixpoints inside of COFEs. For various kinds of recursive definitions inside COFEs (e.g., the Iris weakest precondition or a logical relation with recursive types), we want to compute the fixpoint of a function f : A → A where A is a COFE. We can do so if f is contractive, using a variant of Banach's fixpoint theorem. The construction of this fixpoint is given by fixpoint below. 2. Fixpoints on COFEs. For step-indexed types in Iris (e.g., iProp), we have to solve a recursive domain equation on COFEs. The construction of this fixpoint for natural numbers as the step-index type is given in cofe_solver.v. A COFE extends an OFE A with two additional operations: 1. compl: chain A → A, which takes a chain c of elements from A and maps them to a limit element compl c, 2. lbcompl: ∀ n, SIdx.limit n → bchain A n → A, which takes a bounded chain c of elements from A and maps them to a limit element lbcompl c. The chain is bounded in the sense that its domain ranges from 0 to (but not including) the limit index n. (Later we will define bcompl which completes chains that are bounded by any index, not necessarily a limit index.) We will see the need for the two different limit operations of a COFE below as part of the fixpoint construction. A more detailed explanation can be found in the Iris Reference and the Transfinite Iris Documentation (see https://iris-project.org/pdfs/2021-pldi-transfinite-iris-final-appendix.pdf). These notations Compl and LBCompl are convenient to define instances (e.g., ofe_mor_compl without having to repeat the type. The notation BCompl will be used as the type for bcompl, completing bchain with an arbitrary bound n.

The bounded limit operation is non-expansive: for chains agreeing up to the limit index, the bounded limits agree

General properties of OFEs

ne_proper and ne_proper_2 are not instances to improve efficiency of type class search during setoid rewriting. Local Instances of NonExpansive{,2} are hence accompanied by instances of Proper built using these lemmas.

Contractive functions Defined as a record to avoid eager unfolding.

The tactic f_contractive can be used to prove contractiveness or non-expansiveness of a function f. Inside of the proof of contractiveness/non-expansiveness, if the current goal is g x1 ... xn ≡{i}≡ g y1 ... yn for a contractive function g (that is used inside of the body of f), then the tactic will try to find a suitable Contractive instance for g and apply it. Currently, the tactic only supports one (i.e., n = 1) and two (i.e., n = 2) arguments. As a result of applying the Contractive instance for g, one of the goals will be dist_later i xi yi and the tactic will try to simplify or solve the goal. By simplify we mean that it will turn hypotheses dist_later into dist. The tactic f_contractive is implemented using 1. f_contractive_prepare which looks up a Contractive looks at which function is being applied on both sides of a dist, looks up the Contractive instance (or the equivalent for two arguments) and applies it. 2. dist_later_intro introduces the resulting goals with dist_later n x y.

For the goal dist_later n x y, the tactic dist_later_intro as m Hm introduces a smaller step-index Hm : m < n and tries to lower assumptions in the context to m where possible. The arguments m and Hm can be omitted, in which case a fresh identifier is used.

We combine f_contractive_prepare and dist_later_intro into the f_contractive tactic. For all the goals not solved by dist_later_intro (i.e., the ones that are not dist_later n x y), we try reflexivity. Since reflexivity can be very expensive when unification fails, we use fast_reflexivity.

Limit preserving predicates To perform induction over a fixpoint (fixpoint_ind) and to construct the COFE over a Sigma type (sig_cofe) we need the predicate to be limit preserving: if it holds for every element of a chain, it must hold for the limit.

This is strictly weaker than the _impl variant, but sometimes automation is better at proving Proper for iff than for impl.

We need SIdxFinite because compl_bchain_map does not hold for ≡, only for a bounded ≡{m}≡.

Fixpoint A COFE defines a limit operation lbcompl for all limit indices. When defining a fixpoint operator on COFEs, it is convenient to have a limit operation which can be applied to every index, instead of just the limit indices. We derive such an operation, called bcompl for "bounded completion".

We define the fixpoint of a contractive function f : A → A for an arbitrary step-index type SI. To explain the fixpoint construction in the general case, let us first recall the construction in the finite case. To find the fixpoint of a contractive function f, we start with some dummy element x_0 (an arbitrary inhabitant of A) and iterate f on it such that x_1 := f x_0, x_2 := f x_1, ... (i.e., x_(n + 1) := f x_n). We then find the fixpoint as the completion compl of all of these fixpoint approximations (i.e., x := compl (λ i, x_i)). In the general case with ordinals as step-indices, iterating over all natural numbers is not enough. The way that this is solved is that COFEs provide completion operations lbcompl for all limit ordinals as an additional component of their definition. Then, conceptually, we can first define our approximations as before for all natural numbers (i.e., x_0, x_1, ...) and then we can define x_ω := lbcompl ω (λ n, x_n) to get the limit of all those natural number approximations. Once we have x_ω, we can start our iteration again (i.e., x_(ω + 1) := f (x_ω), ...). We keep repeating this with all ordinals until we have eventually defined x_n for all ordinals n. At that point, we get a fixpoint by using the completion x := compl (λ n, x_n) analogously to the natural number case. There is one small caveat to this construction. In the definition of the fixpoint, it is somewhat inconvenient to distinguish between the cases 0, Sᵢ n, and limit ordinals explicitly. We can get a very clean definition of the fixpoint with a trick: we generalize the operation lbcompl that only works on limit ordinals to work on arbitrary ordinals. This is the operation bcompl defined above.

Getting Coq to agree with the above description of the construction of the fixpoint takes a little work. To apply the completion operations (i.e., compl and bcompl), we need to know that the fixed point approximations (i.e., (x_n for any n) and (x_m for any n < m)) form a "chain". This is not an issue in the case of natural numbers, where we can simply proceed in three steps: 1. We first define all x_n by recursion on n. 2. We prove that they form a chain, and 3. We define x := compl (λ n, x_n) knowing that (λ n, x_n) is a chain. In the general case of ordinals, our life is harder. We want to use recursion on ordinals to define x_n in terms of its predecessors x_m for m < n. However, to define x_n, we need to use the bounded completion operation bcompl, which can only be applied to "bounded chains". Thus, while defining x_n, we need to know that all the previously defined x_m form a chain. In other words, we need a property about the sequence of elements that we have just defined. To that end, we define bfchain, which packages a bounded chain bfchain_car with the property that applying bcompl to bfchain_car gives the fixpoint up to index n. Note that bfchain is a private implementation detail, but Coq does not allow us to make records Local.

We obtain a bounded fixpoint chain for every index n by index recursion. In the recursive case, we construct a new chain up to n by taking, for any m < n, the limit of the m-th chain before applying f to it.

We obtain a final full chain by repeating this construction for every n, using the bounded chains computed before.

This lemma does not work well with rewrite; we usually define a specific unfolding lemma for each fixpoint and then apply fixpoint_unfold in the proof of that unfolding lemma.

Fixpoint of f when f^k is contractive.

Mutual fixpoints