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 it many cases, we do not even need non-expansiveness. The tactic si_solver solves goals that are solely concerned with step-indices and their relations (i.e., 0, S n, n < m, and n ≤ m). Currently, this tactic is just an alias for lia. However, in the future, Iris will generalize over the type of step-indices, and this tactic will be able to solve step-indexing goals also in this generalized setting. The tactic can be used as part of eauto by using the hint database si_solver.

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

General properties

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.

We define dist_later_fin, an equivalent (see dist_later_fin_iff) version of dist_later that uses a match on the step-index instead of the quantification over smaller step-indicies. The definition of dist_later_fin matches how dist_later used to be defined (i.e., with a match on the step-index), so dist_later_fin simplifies adapting existing Iris developments that used to rely on the reduction behavior of dist_later. The "fin" indicates that when, in the future, the step-index is abstracted away, this equivalence will only hold for finite step-indices (as in, ordinals without "limit" steps such as natural numbers).

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. For backwards compatibility, we also define the tactic f_contractive_fin that works with an earlier definition of dist_later now called dist_later_fin. The new version of f_contractive is future proof with respect to generalizing the type of step-indices, while the old tactic relies crucially on the step-indices being nat and the reduction behavior of dist_later. The tactic f_contractive_fin simplifies backwards compatibility of existing Iris developments (e.g., RustBelt), that define custom notions of dist and dist_later but should be avoided if possible. The tactics f_contractive and f_contractive_fin are 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 and dist_later_fin_intro which introduces the resulting goals with dist_later n x y/dist_later_fin n x y. The tactic dist_later_intro works with the normal definition of dist_later and is future compatible with generalizing the step-index beyond natural numbers. The tactic dist_later_fin_intro is a special case which only works for natural numbers as step-indicies. It changes dist_later to dist_later_fin, which only makes sense on natural numbers. We keep dist_later_fin_intro around for backwards compatibility.

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.

For the goal dist_later n x y, the tactic dist_later_fin_intro changes the goal to dist_later_fin and takes care of the case where n=0, such that we are only left with the case where n = S n' for some n'. Changing dist_later to dist_later_fin enables reduction and thus works better with custom versions of dist as used e.g. by LambdaRust.

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

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

Fixpoint

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

Non-expansive function space

Identity and composition and constant function

Unit type

Empty type

Product type

Below we make prod_dist type class opaque, so we first lift all instances