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.
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.
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.
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')
The so-called respectful arrow is the relational equivalent (or relator) of the arrow type constructor (non-dependent function type constructor). See (Kunčar) for an explanation on how transfer rules are a generalization upon parametricity properties of (Reynolds 1983) (or free theorems of (Wadler 1989)).