#+Title: MathTransfer: Transfer Theorems on Mathematical Structures
#+LaTeX_header: \newcommand[1]{\Cite{#1}}{~\cite{#1}}
* General Presentation of the MathTransfer library
If $A$ and $B$ are two isomorphic mathematical structures, then for
any formula $\varphi_A$ expressed in the language of $A$, the formula
$\varphi_A \to \varphi_B$ is a theorem where $\varphi_B$ is the
formula corresponding to $\varphi_A$ in the language of $B$.
Theorems of the form $\varphi_A \to \varphi_B$ are called transfer
theorems. The use of transfer theorems is a way to formalize
rigorously the mathematical habit of "reasoning modulo isomorphism".
Techniques for automatically proving transfer theorems in proof
assistants have been proposed in Isabelle/HOL\Cite{IsabelleTransfer}
and more recently in Coq\Cite{CoqTransfer} but to our knowledge, no
formal library of mathematical structures and proofs of transfer
theorems has yet been proposed.
An interesting application of transfer is interoperability of proof
systems. Interoperability can be decomposed in two major steps:
1) translating each proof system that we are willing to interoperate
into a common formalism
2) proving transfer theorems in this common formalism to relate the
separately translated developments
As common formalism in the first step, we use the Dedukti logical
framework\Cite{Dedukti} for which translators from a large variety of
proof systems have been developed.
MathTransfer is a library aiming at solving the second step. An
example of the use of the library to achieve interoperability is also
provided in the [[./example][example]] directory.
MathTransfer is written in FoCaLiZe\Cite{focalize}, a language that
eases the definition of mathematical structures and the automation of
proofs and for which a translator to Dedukti exists.
* Installation
** Dependencies
The following tools are required to compile the MathTransfer library:
- FoCaLiZe version 0.9.2
FoCaLiZe features Dedukti export since version 0.9.2
- Dedukti version 2.5
- Sukerujo version 2.5
Sukerujo is an alternative Dedukti parser used by FoCaLiZe
- Zenon Modulo version 0.4.3 Focalide
- Dktactics version 0.2
Dktactics is a tactic language for Dedukti
- Zenon Transfer version 0.4.3
Zenon Transfer is a patched version of Zenon Modulo that does not
perform proof search by itself (unlike Zenon Modulo) but uses
Dktactics to prove transfer theorems.
Moreover, for the interoperability example, the following extra tools
are required to import logical developments from other proof systems:
- Coq version 8.4pl6
Other 8.4 versions of Coq might work as well but Coqine requires Coq
version < 8.5.
- Coqine version 0.4
Coqine is a Coq to Dedukti translator. Previous Coqine versions are
not compatible with Dedukti version >= 2.5.
- OpenTheory version 1.3
OpenTheory is an interoperability format for proof assistants of the
HOL family. The OpenTheory tool is a package manager for files in
this format.
The OpenTheory tool is used to download the OpenTheory standard
library.
- Holide version 0.2.1 Holala
Holide is an OpenTheory to Dedukti translator. The Holala variant
limits the dependencies on non-constructive axioms by taking
implication and universal quantification as primitives.
** Installing dependencies
All dependencies but the OpenTheory tool are written in OCaml and
packaged using Opam.
To install OpenTheory, please refer to http://www.gilith.com/software/opentheory/download.html
If you have Opam installed, you can download and install all
other dependencies by typing
#+BEGIN_SRC bash
$ opam repository add deducteam https://gforge.inria.fr/git/opam-deducteam/opam-deducteam.git
$ opam update
$ opam install math_transfer=0.1
#+END_SRC
** Building the library
To build the library, type the following commands:
#+BEGIN_SRC bash
$ ./configure
$ make
#+END_SRC
* Detailed Content of the MathTransfer library
The MathTransfer library, located in the [[./core][lib]] directory
defines arithmetic and algebraic structures and the morphisms between
such structures but does not contain any interesting properties of
these structures. For example, the structure of natural numbers with
addition is defined in the file [[./lib/arith/naturals.fcl][lib/arith/naturals.fcl]] but it does
not contain proofs for the associativity and commutativity of addition
because these properties are not helpful for proving transfer
theorems. It does however contain the theorem statements and proofs
that these properties can be transferred between isomorphic models of
the natural numbers. They can be imported from any arithmetic library.
*** Logic
The logic used in the MathTransfer library is an higher-order logic
seen as an extension of multi-sorted first-order logic.
*** Natural Number Arithmetic
The directory [[./lib/arith][lib/arith]] contains the definitions of arithmetical
structures, that is mathematical structures about natural numbers.
**** Definitions
The file [[./lib/arith/naturals.fcl][lib/arith/definitions/naturals.fcl]] defines the following species
representing mathematical structures built from natural numbers with
various operations and relations:
- Zenon and Successor
The first building block of the arithmetic library is the =NatDecl=
species in file =naturals.fcl=. This species requires two
functions: =zero= of type =Self= and =succ= of type =Self -> Self=
but does not specify them.
- Unit
=one= is a constant of type =Self= specified as being equal to the
successor of zero.
- Binary notation
The function =bit0= computes the double of a natural number
(=bit0(zero) = zero=, =bit0(succ(n)) = succ(succ(bit0(n)))=). Hence
it corresponds to adding a =0= bit in binary notation.
The function =bit1= adds a =1= bit in binary notation so =bit1(n) =
succ(bit0(n))=.
- Predecessor
The predecessor of =n= is =m= if =n= is =succ(m)= and =zero=
if =n= is =zero=.
- Addition
=plus= is a binary operation over natural numbers defined by the
following axioms:
+ =plus(zero, n) = n=
+ =plus(succ(m), n) = succ(plus(m, n))=
- Multiplication
=times= is a binary operation over natural numbers defined by the
following axioms:
+ =times(zero, n) = zero=
+ =times(succ(m), n) = plus(n, times(m, n))=
- Ordering
=le= is a binary relation over natural numbers defined by the following axiom:
+ =le(m, n) <-> (ex p : Self, plus(m, p) = n)=
- Strict ordering
=lt= is a binary relation over natural numbers defined by the following axiom:
+ =lt(m, n) <-> le(succ(m), n)=
**** Morphisms
The files in the directory [[./lib/arith/morphisms][lib/arith/morphisms]] define isomorphisms
between representations of natural numbers. Three representations of
morphisms are proposed:
- The relational representation, suitable for automatic transfer, is
proposed in file [[./lib/arith/morphisms/natmorph_rel.fcl][lib/arith/morphisms/natmorph_rel.fcl]]. An
isomorphism is there defines as a relation =morph= of type =A ->
Self -> prop= that is assumed
+ functional: it preserves equality
+ injective: it reflects equality (its inverse is functional)
+ surjective
+ total: its inverse is also surjective
Moreover, it preserves and reflects all the operation of the
structure.
- The functional representation, easier to instantiate with functional
proof systems, is proposed in file
[[./lib/arith/morphisms/natmorph.fcl][lib/arith/morphisms/natmorph.fcl]]. An isomorphism is a function
=morph= of type =Self -> B= that preserves =zero= and =succ= . Peano
axioms are assumed in both =Self= and =B=. Injectivity,
surjectivity, and preservation of all arithmetic operations are
proved (using manual Dedukti instantiation of the induction axiom).
- The reversed functional representation is similar but the morphism
is seen as a function of type =A -> Self=.
**** Theorems
The file [[./lib/arith/theorems/natthms.fcl][lib/arith/theorems/natthms.fcl]] extend the hierarchy of
natural number structures by requiring common properties of arithmetic
operations. The statements are taken from OpenTheory standard library.
**** Transfer
The file [[./lib/arith/transfer/nattransfer.fcl][lib/arith/transfer/nattransfer.fcl]] combines the morphism
hierarchy with the theorem hierachy. If the theorems of file
[[./lib/arith/theorems/natthms.fcl][lib/arith/theorems/natthms.fcl]] hold for a collection =A= and if the
current species is isomorphic to =A= then the theorems also hold for
the current species.
These transfer theorems are automatically proved by a Meta Dedukti
tactic defined in the directory [[./lib/arith/transfer/meta][lib/arith/transfer/meta/]]. The calls to
this tactic are produced by Zenon Transfer.
* The Interoperability Example
The directory [[./example][example]] illustrates how the MathTransfer library can be
used for interoperability of proof systems. The chosen systems for
this example are Coq and HOL (more precisely, the OpenTheory proof
format for proof assistants of the HOL family).
The theorem proved using Coq and HOL in combination is a correctness
proof of the Sieve of Eratosthenes. The algorithm and the proof are
written in Coq and the arithmetic results required are imported from
OpenTheory.
** Logic Combination
The directory [[./example/logic][example/logic]] contains the Dedukti combination of the
logics of Coq (defined in file [[./example/logic/Coq.dk][Coq.dk]]) and HOL (defined in file
[[./lib/logic/hol.dk][hol.dk]]). The combination is defined in file [[./example/logic/hol_to_coq.dk][hol_to_coq.dk]], it relies
on a definition of inhabited types in Coq (file [[./example/logic/holtypes.v][holtypes.v]]).
For more details on this logic combination, see
[[https://arxiv.org/pdf/1507.08721.pdf]].
** Extenstion of the hierarchies
To state the lemmas that we need to transfer from HOL to Coq, we first
extend the hierarchies of mathematical structures to axiomatize
divisibility and primality. More precisely, in file [[./example/arith/natural_full.fcl][natural_full.fcl]],
we define the following operations:
- Divisibility
=divides= is a binary relation over natural numbers defined by the following axiom:
+ =divides(m, n) <-> (ex p : Self, times(m, p) = n)=
- Strict Divisibility
=sd= is a binary relation over natural numbers defined by the following axiom:
+ =sd(m, n) <-> (divides(m, n) /\ lt(m, n) /\ lt(succ(zero), m))=
- Primality
=prime= is a predicate over natural numbers defined by the following axiom:
+ =prime(p) <-> lt(succ(zero), p) /\ all d : Self, ~(sd(d, p))=
We then require two properties:
- if =m= divides =n= and 1 < =n=, then =m= is smaller or equal to =n=,
- if =n= is not 1, then =n= has a prime divisor.
We then extend the morphism hierarchy to the new operations and
transfer both theorems.
** Instantiations
In file [[./example/arith/natural_hol.fcl][natural_hol.fcl]], we fully instantiate the hierarchies with the
definitions and proofs of OpenTheory. In file [[./example/arith/natural_coq.fcl][natural_coq.fcl]], we
instantiate the definition hierarchy with the definitions of Coq and
use transfer to instantiate the theorem hierarchy. Finally, both
instantiations are combined in file [[./example/arith/final_coll.fcl][final_coll.fcl]].
** Final Proof
The Coq proof, with the OpenTheory lemmas as hypotheses, is done in
file [[./example/arith/sieve.v][sieve.v]]. The missing bits are added in Dedukti in file [[./example/arith/final.dk][final.dk]].