Library coqrel.Transport

The transport tactic

Often, we know that a number of terms are related, and need to transport hypotheses built out the the left-hand sides into ones with similar shapes, but built out of the right-hand sides. For instance, in cirumstances where rauto can establish option_rel R x y, we will want to turn a hypothesis of the form x = Some a into one of the form y = Some b, and remember that R a b. This is the role of the transport tactic.

Transportable hypotheses

The stereotypical example is option_rel, which we can use to transport hypotheses as per the following instances.

A similar approach can be used to transport hypotheses which assert a element of a product type is equal to a specific pair.

For set_rel the situation is slightly more involved, for two reasons. First, a regular eapply set_rel_transport fails to unify the parameter B of Transport against the _ → Prop provied by the instance below. This can be worked around by pre-unifying that specific parameter. Second, because set_rel_transport is potentially applicable to virtually any hypothesis (since there is no strongly distinguishing syntactic format in our target hypotheses), it makes transport_hyps very slow. To address this, we explicitely register hints based on the set_rel_transport tactic, which looks for "keywords" before doing anything, then applies the lemma with the required unification preparation. For example, set_rel_transport is used in the following way in the SimClight library:

    Hint Extern 1 (Transport _ _ _ _ _) =>
      set_rel_transport @assign_loc : typeclass_instances.

Note that it's necessary to use @ because assign_loc is parametrized by typeclasses, and we want to avoid undue specialization at hint registration time.

We defined a few more relation patterns based on set_rel and rel_curry, with a similar strategy.

The situation for impl is similar: since this transport instance can apply to pretty much anything, we need to register it on a case-by-case basis. Here is an example used in the CertiKOS proof for hypotheses of the form writable_block ge b:

    Hint Extern 10 (Transport _ _ _ (writable_block _ _) _) =>
      eapply impl_transport : typeclass_instances.

Often, the target hypotheses declared using the Transport class have existential quantifiers, and need to be broken up to get to the actual relational hypotheses we're interested in. The split_hyp tactic does that. We also use that opportunity to split up prod_rel and rel_incr when appropriate. For prod_rel this is especially useful when rel_curry is involved. Likewise we generally want to split up rel_incr as soon as possible, so that the existentially quantified world therein can be used to instantiate evars that have been spawned from that point on. As a generally useful complement, the split_hyps tactic applies the same process to all hypotheses.

We're now ready to defined the transport tactic, which essentially looks up a Transport instance and applies it the the hypothesis to be transported, using RAuto to solve the relational subgoal. Note that the relation and right-hand side will usually contain existential variables, but the proof search can hopefully proceed by following the structure of the left-hand side. Once the Transport instance has been applied, we use split_hyp on the modified hypothesis as post-processing. Because we have many open-ended evars involved, it is easy for trivial relations such as eq to kick in and sabotage us, overriding the more interesting properties that we actually want to use and preventing any progress from actually being made. In order to attenuate this issue, we require that RAuto yield unconvertible related elements. Another pitfall we want to avoid is illustrated by the option_rel case. When we have a hypothesis of the form H: m = Some a, but no interesting way to relate m to something else, then the search for (option_rel ?R) m ?n can end up using H itself (because option_rel eq is reflexive, hence subrel_eq applies). To prevent such cases we need to make sure that the hypothesis being transported is not used to discharge the relational premise, and so we revert it into the conclusing before we proceed, and use the following lemma to work on a goal of that form directly.

Again we provide a tactic which attempts to transport all hypotheses. Notice that earlier transportations may provide new hypotheses making later transportations possible. Hence it would be hard to provide a much more effective tactic, even though this one may retry failing transportations many times.