README.org 11.3 KB
Newer Older
Raphael Cauderlier's avatar
Raphael Cauderlier committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
#+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.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
32 33 34
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
35

Raphael Cauderlier's avatar
Raphael Cauderlier committed
36 37 38
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
39

40
* Installation
Raphael Cauderlier's avatar
Raphael Cauderlier committed
41 42 43

** Dependencies

44
The following tools are required to compile the MathTransfer library:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
45

46 47 48 49 50 51 52 53 54 55
- 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

Raphael Cauderlier's avatar
Raphael Cauderlier committed
56
- Zenon Modulo version 0.4.3 Focalide
57

58
- Dktactics version 0.2
Raphael Cauderlier's avatar
Raphael Cauderlier committed
59 60 61

  Dktactics is a tactic language for Dedukti

62
- Zenon Transfer version 0.4.3
Raphael Cauderlier's avatar
Raphael Cauderlier committed
63

Raphael Cauderlier's avatar
Raphael Cauderlier committed
64 65 66
  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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
67 68 69

Moreover, for the interoperability example, the following extra tools
are required to import logical developments from other proof systems:
70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95

- 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.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
96 97 98 99 100 101 102 103 104 105 106 107 108
** 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
109
  $ opam install math_transfer=0.1
Raphael Cauderlier's avatar
Raphael Cauderlier committed
110 111 112 113 114 115 116 117 118 119 120
#+END_SRC

** Building the library

To build the library, type the following commands:

#+BEGIN_SRC bash
  $ ./configure
  $ make
#+END_SRC

121
* Detailed Content of the MathTransfer library
Raphael Cauderlier's avatar
Raphael Cauderlier committed
122

Raphael Cauderlier's avatar
Raphael Cauderlier committed
123
The MathTransfer library, located in the [[./core][lib]] directory
Raphael Cauderlier's avatar
Raphael Cauderlier committed
124 125 126
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
127
addition is defined in the file [[./lib/arith/naturals.fcl][lib/arith/naturals.fcl]] but it does
Raphael Cauderlier's avatar
Raphael Cauderlier committed
128 129
not contain proofs for the associativity and commutativity of addition
because these properties are not helpful for proving transfer
Raphael Cauderlier's avatar
Raphael Cauderlier committed
130 131
theorems. It does however contain the theorem statements and proofs
that these properties can be transferred between isomorphic models of
Raphael Cauderlier's avatar
Raphael Cauderlier committed
132
the natural numbers. They can be imported from any arithmetic library.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
133 134 135 136 137 138

*** Logic

The logic used in the MathTransfer library is an higher-order logic
seen as an extension of multi-sorted first-order logic.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
139
*** Natural Number Arithmetic
Raphael Cauderlier's avatar
Raphael Cauderlier committed
140

Raphael Cauderlier's avatar
Raphael Cauderlier committed
141
The directory [[./lib/arith][lib/arith]] contains the definitions of arithmetical
Raphael Cauderlier's avatar
Raphael Cauderlier committed
142
structures, that is mathematical structures about natural numbers.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
143 144


Raphael Cauderlier's avatar
Raphael Cauderlier committed
145 146 147
**** Definitions

 The file [[./lib/arith/naturals.fcl][lib/arith/definitions/naturals.fcl]] defines the following species
Raphael Cauderlier's avatar
Raphael Cauderlier committed
148 149 150
 representing mathematical structures built from natural numbers with
 various operations and relations:

Raphael Cauderlier's avatar
Raphael Cauderlier committed
151 152 153 154 155 156 157 158 159 160 161 162 163
 - 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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
164

Raphael Cauderlier's avatar
Raphael Cauderlier committed
165 166 167
   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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
168

Raphael Cauderlier's avatar
Raphael Cauderlier committed
169 170
   The function =bit1= adds a =1= bit in binary notation so =bit1(n) =
   succ(bit0(n))=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
171

Raphael Cauderlier's avatar
Raphael Cauderlier committed
172
 - Predecessor
Raphael Cauderlier's avatar
Raphael Cauderlier committed
173

Raphael Cauderlier's avatar
Raphael Cauderlier committed
174 175
   The predecessor of =n= is =m= if =n= is =succ(m)= and =zero=
   if =n= is =zero=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200

 - 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)=

Raphael Cauderlier's avatar
Raphael Cauderlier committed
201
**** Morphisms
Raphael Cauderlier's avatar
Raphael Cauderlier committed
202

Raphael Cauderlier's avatar
Raphael Cauderlier committed
203 204 205
The files in the directory [[./lib/arith/morphisms][lib/arith/morphisms]] define isomorphisms
between representations of natural numbers. Three representations of
morphisms are proposed:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
206

Raphael Cauderlier's avatar
Raphael Cauderlier committed
207 208 209 210 211 212 213 214
- 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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
215

Raphael Cauderlier's avatar
Raphael Cauderlier committed
216 217
  Moreover, it preserves and reflects all the operation of the
  structure.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
218

Raphael Cauderlier's avatar
Raphael Cauderlier committed
219 220 221 222 223 224 225
- 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).
Raphael Cauderlier's avatar
Raphael Cauderlier committed
226

Raphael Cauderlier's avatar
Raphael Cauderlier committed
227 228
- The reversed functional representation is similar but the morphism
  is seen as a function of type =A -> Self=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
229

Raphael Cauderlier's avatar
Raphael Cauderlier committed
230
**** Theorems
Raphael Cauderlier's avatar
Raphael Cauderlier committed
231

Raphael Cauderlier's avatar
Raphael Cauderlier committed
232 233 234
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
235

Raphael Cauderlier's avatar
Raphael Cauderlier committed
236 237 238 239 240 241 242 243 244 245 246
**** 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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
247 248

* The Interoperability Example
Raphael Cauderlier's avatar
Raphael Cauderlier committed
249

Raphael Cauderlier's avatar
Raphael Cauderlier committed
250 251 252 253 254 255 256 257 258
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
259

Raphael Cauderlier's avatar
Raphael Cauderlier committed
260
** Logic Combination
Raphael Cauderlier's avatar
Raphael Cauderlier committed
261

Raphael Cauderlier's avatar
Raphael Cauderlier committed
262 263 264 265
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]]).
Raphael Cauderlier's avatar
Raphael Cauderlier committed
266

Raphael Cauderlier's avatar
Raphael Cauderlier committed
267 268
For more details on this logic combination, see
[[https://arxiv.org/pdf/1507.08721.pdf]].
Raphael Cauderlier's avatar
Raphael Cauderlier committed
269

Raphael Cauderlier's avatar
Raphael Cauderlier committed
270
** Extenstion of the hierarchies
Raphael Cauderlier's avatar
Raphael Cauderlier committed
271

Raphael Cauderlier's avatar
Raphael Cauderlier committed
272 273 274 275 276 277
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
278

Raphael Cauderlier's avatar
Raphael Cauderlier committed
279 280 281 282 283 284 285 286 287 288 289 290
   =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))=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
291

Raphael Cauderlier's avatar
Raphael Cauderlier committed
292 293 294
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
295

Raphael Cauderlier's avatar
Raphael Cauderlier committed
296 297
We then extend the morphism hierarchy to the new operations and
transfer both theorems.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
298

Raphael Cauderlier's avatar
Raphael Cauderlier committed
299
** Instantiations
Raphael Cauderlier's avatar
Raphael Cauderlier committed
300

Raphael Cauderlier's avatar
Raphael Cauderlier committed
301 302 303 304 305
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]].
Raphael Cauderlier's avatar
Raphael Cauderlier committed
306

Raphael Cauderlier's avatar
Raphael Cauderlier committed
307
** Final Proof
Raphael Cauderlier's avatar
Raphael Cauderlier committed
308

Raphael Cauderlier's avatar
Raphael Cauderlier committed
309 310
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]].