Relators

With this infrastructure in place, we can define actual relators that cover the commonly used type constructors. There are two broad categories: those related to function types, and those derived from inductive types. As a convention, we name relators and the associated monotonicity theorems by appending the suffix _rel to the name of original type and those of its constructors. Likewise, we use the suffix _subrel for monotonicity theorems that characterize the variance of corresponding relators with respect to subrel, and the suffix _relim for an associated instance of RElim.

A note about universes

Our use of subrel illustrates the fact that we consider relations over relations, and use relators to build up relations over the types of our relators to characterize their variance. In other words: we relate all kind of higher-order things as a matter of course and make sure our library eats its own dog food. This makes it relatively easy to run into universe inconsistency issues. This note is to explain why those happen, fix the terminology, and formulate best practices to avoid such problems. The critical universe level in Coqrel is the universe U from which the arguments and return type of rel are taken (so that conceptually we will write rel : U → U → U). We will call "small types" the inhabitants of U, and "large types" those taken from a universe strictly larger than U. At the moment, U is implicit, but at some point we may want declare an explicit Universe to aid debugging and enhance clarity. Generally speaking, U is a pretty large universe: for the most part, the world of relational things sits well above the world of the things we want relate, no matter how high-order those are. Even rel A B is still a small type, so that @subrel : ∀ A B : U, rel (rel A B) (rel A B) above didn't cause any issue, although the type of rel itself, namely U → U → U : U+1, is of course a large type. With this in mind, consider the relational operator rel_compose : ∀ A B C, rel A B → rel B C → rel A C. We wish to register a monotonicity property for rel_compose, establishing that composing larger relations yields a larger composite relation. As usual, we express this property by establishing that rel_compose is related to itself by an appropriate relation. However, the type of rel_compose may involve U : U+1 as the type of the arguments A B C, so that the type of rel_compose may itself be forced into sort U+1. Consequently, attempting to define that relation will yield a universe inconsistency as soon as, say, subrel is used as an argument of rel_compose. Fortunately, even if A B C : U, the specialized form rel_compose A B C is still in the small type rel A B → rel B C → rel A C : U. Moreover, there is no relational structure that we want to capture regarding the type parameters A B C, so that we don't lose anything by defining our monotonicity property for the specialized rel_compose A B C, as long as the property itself is generic in the specific values of A B C. This is why, as a general rule, we define the foo_subrel properties of our relators on partially applied versions thereof, and use a foo_subrel_params hint to make sure our monotonicity tactic can resolve them.

Relators for function types

Pointwise extension of a relation

One useful special case is the pointwise extension of a relation on the domain to the function type. This is equivalent to eq ==> R, however with the formulation below we don't have consider two equal elements of the domain.

Note that although the elimination rule could use a single variable and dispense with the equality premise, it actually uses two distinct variables m and n, and a premise in P that m = n. Hence the effect is similar to the elimination rule for the equivalent relation eq ==> R. We do this because in contexts where we have a single term t against which both m and n unify, it is easy and cheap to automatically prove that t = t, but in contexts where we have two disctinct variables and a proof of equality, it is more involved to massage the goal into a form where the single-variable version of the rule could apply.

Dependent pointwise extension

Like we did for non-dependent functions, we can provide a simpler definition for the special case where E is eq.

Dependent products (restricted version)

This is a restricted version of forall_rel with E in Prop, when the codomain relation only depends on the arguments.

Since e : E v1 v2 cannot be unified in Q, the elimination rule adds an E v1 v2 premise to P instead.

TODO: A further specialization could be foralln_rel, which does not even require that v1, v2 be related (let alone care about the proof). In other words, a forallr v1 v2, R which would essentially boil down to forallr v1 v2 : ⊤, R.

Sets (A → Prop)

Sets of type A → Prop can be related using the regular arrow relator, as in R ++> impl. This states that for any two elements related by R, if the first is in the first set, then the second must be in the second set. However, very often we need the following relator instead, which states that for any element of the first set, there exists an element of the second set which is related to it. This is useful for example when defining simulation diagrams.

Inductive types

For inductive types, there is a systematic way of converting their definition into that of the corresponding relator. Where the original inductive definition quantifies over types, the corresponding relator will quantify over pairs of types and relations between them. Then, the constructors of the relator will essentially be Proper instances for the original constructors. In other words, the resulting relation will be the smallest one such that the constructors are order-preserving.

Nullary type constructors

As a proof-of-concept, we start with the most elementary types Empty_set and unit, which can be considered as nullary type constructors related to sum and prod below.

Sum types

The definition of sum_rel could look something like this:

    Inductive sum_rel:
      forall {A1 A2 B1 B2}, rel A1 A2 -> rel B1 B2 -> rel (A1+B1) (A2+B2):=
      | inl_rel: Proper (∀ RA : rel, ∀ RB : rel, RA ++> sum_rel RA RB) (@inl)
      | inr_rel: Proper (∀ RA : rel, ∀ RB : rel, RB ++> sum_rel RA RB) (@inr).

However, to minimize the need for inversions we want to keep as many arguments as possible as parameters of the inductive type.

Since it is not possible to retype the constructors after the fact, we use the _def suffix when defining them, then redeclare a corresponding, full-blown Proper instance.

Pairs

Option types

XXX: This does not fit any of our existing patterns, we should drop it for consistency or introduce a new convention and generalize this kind of lemmas.

Lists

Monotonicity of logical connectives