Prerequisites

Some instances that would normally cause loops can be used nontheless if we insist that some parameters cannot be existential variables. One way to do this is to use this guard class, similar in spirit to Unconvertible.

Sometimes we may want to introduce an auxiliary variable to help with unification.

Relations

The constructions in Coq.Relations.Relation_Definitions are only concerned with relations within a single type, so that relation A is defined as A → A → Prop. We will need more general relations, and so I define rel A B as A → B → Prop. When we move to a version of Coq with universe polymorphism, we can make this a Polymorphic Definition. In the meantime, we need to use a notation so that universes levels are instantiated at every use site.

Proper elements

I follow Coq.Classes.Morphisms and define morphisms as proper elements of a corresponding logical relation. They can be registered by declaring instances of the Proper typeclass. However, we will build up logical relations from our own set of relators, and use our own tactics to deduce new instances of Proper from the existing ones. To prevent the two systems from interfering with one another, I will use the following nearly identical, but distinct definition of Proper. There is one ugly tweak that we need, compared with the original. Namely, we want the type parameter A to be unified in priority with the type of element m, rather than that of the relation R. That is because by necessity, the relator forall_rel defined below yields an eta-expanded type of the form (fun x ⇒ T x) x. As a consequence, some instances declared using forall_rel become unusable because A takes this peculiar form. To work around this, we flip the order of arguments in our version of Proper, so that A is unified against the type of m, then use notations to fake the original order.

Order on relations

This is our generalization of subrelation. Like the original it constitutes a preorder, and the union and intersection of relations are the corresponding join and meet.

Union of relations

Intersection of relations

The bottom and top relations

Relation equivalence

Relators for function types

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. First, we introduce the core relators necessary to develop the tactics that follow, namely those for function types. In a later section of this file, I provide a more comprehensive library which covers many of the basic inductive type constructors as well. 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.

Non-dependent function types

First, I define relators for non-dependent functions. This generalizes respectful.

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.

Dependent products

Now we consider the dependent case. The definition of forall_rel is somewhat involved, but you can think of relating f and g in the context of a structure-preserving transformation from a quiver (V, E) to the quiver (Type, rel). Like a functor, it has two components: FV maps nodes to types, and FE maps edges to relations. Then, forall_rel FE f g states that given an edge (e : E v1 v2), the images f v1 and g v2 are related by the corresponding relation FE v1 v2 e. We will write forall_rel FE f g as (∀ e : E v1 v2, FE[v1,v2,e]) f g. Notice that this notation binds v1 and v2 as well as e. If that makes no sense, you can think of specific source quivers. So for instance, oftentimes we will want to use (Type, rel) as the source quiver too. This corresponds to parametric polymorphism. The type of Some is ∀ A : Type, A → option A; the corresponding logical relation is ∀ R : rel A1 A2, R ++> option_rel R. Stating that Proper (∀ R : rel A1 A2, R ++> option_rel R) Some means that, given any relation R and elements x1 and x2, if R relates x1 and x2, then option_rel R will relate Some x1 and Some x2. Another example from liblayers is the quiver of our data-indexed simulation relations simrel : layerdata → layerdata → Type. Here the structure-preserving transformations are our simulation relation diagrams, which have types such as lsim : ∀ D1 D2, simrel D1 D2 → rel (layer D1) (layer D2) or psim : ∀ {D1 D2}, simrel D1 D2 → rel (primsem D1) (primsem D2). Then, the monotonicity of a data-indexed function — say, foo: ∀ D : layerdata, layer D → primsem D — can be expressed as Proper (∀ R : simrel D1 D2, siml D1 D2 R ++> simp D1 D2 R) foo. This definition is the same as respectful_hetero.

Dependent pointwise extension

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

Tactics

Resolution process

Now that we have a way to express and register the monotonicity properties of various operators, we want to use them to answer the queries generated by setoid rewriting and the monotonicity tactic. That is, given a relation R with existential holes and a term m, use the registered theorems to prove R m m, instantiating some of the existential holes in R. All things being equal, we will want those instantiations to yield the strongest theorem possible. I use the following procedure, implemented below.

• First, choose an orientation. Since R m m ↔ (flip R) m m, we need to consider both of those goals. Furthermore, we need to normalize flip R so that flip is pushed inward and any occurence of flip (flip Q) is reduced to Q.
• Then, if m is an applied function, we may want to look for a more general Proper theorem. So for instance, assuming that Q x x, we can use a theorem of the form Proper (Q ++> R) f to solve a goal of the form R (f x) (f x).
• Once we've chosen an orientation and a degree of partial application, we can finally look for a corresponding Proper instance.

We may want to add more phases in the future, for instance to generalize the goal using subrel instances. It is most convenient to embed this process into the typeclass resolution mechanism. In particular, nondeterministic choices come in handy. But we don't want these resolution steps to be applied arbitrarily. In order to enforce the sequential aspect, we use the proxy class ProperQuery, which is parametrized by a list of processing phases remaining.

The different processing_phases will peel themselves off the list and generate subgoals to be handled by the next phase. Ultimately the list becomes empty, and we look for a regular instance of Proper.

Flipping Proper goals

Instances of this class can be used to indicate how flip is to be pushed to the inside of given relation operators.

Catch-all, default instance.

Flipping twice. This instance is also used when the first argument is an existential variable, so that the resulting relation is itself as general as possible.

Symmetric relations flip to themselves.

Instances for basic relators.

The proper_orientation phase causes both orientations to be tried.

For proper_orientation_flip above, we only want to use the first instance of FlipsTo found.

Partial applications

In many contexts, we need to show Proper Rg (op a₁ … aₖ … aₙ), but what we acually have is a more general instance of Proper R (op a₁ … aₖ). If R is built up from reflexive relations (or at least, relations for which the corresponding aᵢ is a proper element), then the former can be obtained from the latter. In Coq.Classes.Morphisms, this is handled by partial_application_tactic, which applies Reflexive_partial_app_morphism on a goal of the form Proper R´ (op x) to obtain the new goal Proper (R ==> R´) op, with R an existential variable to be unified against the Proper instances of this form that are eventually found. However, we cannot naively extend this strategy to obtain goals of the form Proper (forall_rel R) op. We would need the many more existential variables V : Type, E : V → V → Type, e : E x x, FV : V → Type, R : ∀ v1 v2, E v1 v2 → rel (FV v1) (FV v2), and what's more we would have to perform the higher-order unification of R´ — likely just some existential variable at this point — against ?R ?v ?v ?e. Maybe this could be achieved by going through another existential variable within the context of a lambda abstraction such that R ≐ (fun v1 v2 e ⇒ ?) (if that is even possible). However the resulting unification process would be rather messy and undebuggable. Instead, we start with whatever instances of Proper (forall_rel R) op we can find, then try to unify R´ against the corresponding mostly-concrete R x x ?e. To this end, we use the following intermediate class.

The processing phase proper_partial_arg is used for proving that a given argument can be applied. It is our version of Morphisms.ProperProxy.

The proper_partial_app processing phase consists in using proper_applies an arbitrary number of times. TODO: we may want to use the Params class to limit the resulting search space to only one possibility instead.

When using proper_partial_app_arg, the unification of the goal against the subterm (B a) is problematic, because usually the type will be an arbitrary expression where a appears freely. Therefore, we first need to put the goal in the right form. The tactic dependent_type_of recovers the type of a term that can be applied, as a function of its first argument.

Using subrel

The processing step proper_subrel causes the search to be extended to subrelations. The order of the ProperQuery and subrel arguments is pretty critical: first, we go on and try to find /any/ instance of Proper for m; then, we check to see if the associated relation is a subrelation of the target one.

Compatibility with setoid rewriting

So far our system is isolated from the similar constructions in Coq.Classes.Morphisms. The convert_proper tactic permits a controlled interaction between them. It converts a Morphisms.Proper goal into a Proper one, replacing legacy relators such as respectful with their more general counterparts defined here. This allows the setoid rewriting mechanism to use the morphisms we define.

We want convert_proper to be used for the initial Proper goal, but we're not really interested in having it applied to the subgoals generated by the original process in Coq.Classes.Morphisms, since we have our own. The following tactic attempts to detect and reject cases where some work has already been done.

The monotonicity of transitive relations is sometimes needed to solve the goals generated by setoid rewriting.

The monotonicity tactic

The purpose of the monotonicity tactic is to automatically select and apply a theorem of the form Proper ?R ?m in order to make progress when the goal is an applied relation. Compared with setoid rewriting, monotonicity is less powerful, but more direct and simple. This means it is easier to debug, and it can seamlessly handle dependent types and heterogenous relations. At the moment, monotonicity does not use any of the preprocessing phases.

Our version of Morphisms.f_equiv.

Our version of Morphisms.solve_proper. Note that we are somewhat parcimonious with introductions because we don't want to cause undue unfoldings. For instance, if we define the relation R1 from R2 as R1 x y := ∀ i, R2 (get i x) (get i y), we may create a situation where applying the monotonicity theorem for get on a goal of the form R2 (get i x) (get i y) produces a subgoal of the form R1 x y, but then an introduction would get us back to where we started. So we limit them to well-defined cases.

Exploiting foo_subrel instances

Although we declared Proper instances for the relation constructors we defined, so far the usefulness of these instances has been limited. But now we can use them in conjunction with our monotonicity tactic to break up subrel goals along the structure of the relations being considered.

Furthermore, the following instance of subrel enables the use of foo_subrel instances for rewriting along within applied relations. So that for instance, a hypothesis H: subrel R1 R2 can be used for rewriting in a goal of the form (R1 × R1´ ++> R) x y.

More relators for basic types

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

Lists

Tests

Partial applications

Setoid rewriting

This test checks that transitive_proper is used as expected.

For your debugging convenience, here are the goals generated by the rewrite above.

Monotonicity tactics

Using foo_subrel instances

FIXME: this should work as well.