Automatic and transparent transfer of theorems in the Coq proof assistant


We wish to simplify the life of mathematicians using proof assistants such as Coq.
We also wish to promote large-scale collaboration, first by simplifying sharing.
Reusing theorems proved by others may require a change of representation (the theorem is about a related structure, but this structure is not defined as in one's own development).
Such change of representation should be automatically handled as soon as the required statements are made, relating the two structures.

Tactics provided

Our library provides three tactics to allow such a transfer or change of representation.
The first one is exactm (it stands for "exact modulo"). It is used exactly as exact, that is to give a precise lemma resolving the current goal, but it will handle the change of representation, from the provided lemma, to the actual goal.
The two should look similar in structure and differ only in the types they quantify over and the functions and constants they contain.

The second tactic is transfer. This use of our library was inspired by a similar proof method in the package Transfer of Isabelle. This tactic takes no argument and is guided only by the user declarations relating the two structures. It is less powerful because if many of these declarations are available, it will choose some arbitrarily. However, it can be more convenient to use in some circumstances.

The third tactic is applym (it stands for "apply modulo"). It is used exactly as apply, that is to give a lemma whose conclusion resolves the current goal, but whose hypotheses (if there are some) will need to be proved.
It presently suffers from several limitations due to its use of transfer behind the scene (on the lemma and not on the goal).

So far, we do not handle the context (any variable that was already introduced cannot be transferred). We are planning to add support for the context, to improve the applym tactic and to add some other tactics such as rewritem. We are even planning to generalize the coercion system to allow using the usual set of tactics and automatically inserting theorems of change of representation when they are needed.

Relating two structures

We provide the finest way of declaring relations between structures, not only between isomorphic structures.
We assume that there is a binary logical relation between the elements of the two structures.
If there is a function between the two, then the underlying relation must be used.
We expect declarations on the properties of this relation and its compatibility with the functions and constants of interest.

The respectful arrow

All of these declarations can be made using the respectful arrow ##>, which constructs a new relation between functions from two relations between elements.
Its definition is the following:

f (R ##> S) f' := \(\forall\) x x', x R x' \(\rightarrow\) (f x) S (f' x')