Raphael Cauderlier committed Mar 21, 2017 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 committed Apr 09, 2017 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 committed Mar 21, 2017 35   Raphael Cauderlier committed Apr 09, 2017 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 committed Mar 21, 2017 39   Raphael Cauderlier committed Mar 26, 2017 40 * Installation  Raphael Cauderlier committed Mar 26, 2017 41 42 43  ** Dependencies  Raphael Cauderlier committed Mar 26, 2017 44 The following tools are required to compile the MathTransfer library:  Raphael Cauderlier committed Mar 21, 2017 45   Raphael Cauderlier committed Mar 26, 2017 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 committed Apr 15, 2017 56 - Zenon Modulo version 0.4.3 Focalide  Raphael Cauderlier committed Mar 26, 2017 57   Raphael Cauderlier committed Apr 15, 2017 58 - Dktactics version 0.2  Raphael Cauderlier committed Apr 09, 2017 59 60 61  Dktactics is a tactic language for Dedukti  Raphael Cauderlier committed Apr 15, 2017 62 - Zenon Transfer version 0.4.3  Raphael Cauderlier committed Apr 09, 2017 63   Raphael Cauderlier committed Apr 15, 2017 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 committed Apr 09, 2017 67 68 69  Moreover, for the interoperability example, the following extra tools are required to import logical developments from other proof systems:  Raphael Cauderlier committed Mar 26, 2017 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 committed Mar 26, 2017 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  Raphael Cauderlier committed Apr 15, 2017 109  $opam install math_transfer=0.1  Raphael Cauderlier committed Mar 26, 2017 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  Raphael Cauderlier committed Mar 26, 2017 121 * Detailed Content of the MathTransfer library  Raphael Cauderlier committed Mar 21, 2017 122   Raphael Cauderlier committed Apr 09, 2017 123 The MathTransfer library, located in the [[./core][lib]] directory  Raphael Cauderlier committed Mar 21, 2017 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 committed Apr 09, 2017 127 addition is defined in the file [[./lib/arith/naturals.fcl][lib/arith/naturals.fcl]] but it does  Raphael Cauderlier committed Mar 21, 2017 128 129 not contain proofs for the associativity and commutativity of addition because these properties are not helpful for proving transfer  Raphael Cauderlier committed Apr 02, 2017 130 131 theorems. It does however contain the theorem statements and proofs that these properties can be transferred between isomorphic models of  Raphael Cauderlier committed Apr 09, 2017 132 the natural numbers. They can be imported from any arithmetic library.  Raphael Cauderlier committed Mar 21, 2017 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 committed Apr 15, 2017 139 *** Natural Number Arithmetic  Raphael Cauderlier committed Mar 21, 2017 140   Raphael Cauderlier committed Apr 09, 2017 141 The directory [[./lib/arith][lib/arith]] contains the definitions of arithmetical  Raphael Cauderlier committed Apr 15, 2017 142 structures, that is mathematical structures about natural numbers.  Raphael Cauderlier committed Mar 21, 2017 143 144   Raphael Cauderlier committed Apr 15, 2017 145 146 147 **** Definitions The file [[./lib/arith/naturals.fcl][lib/arith/definitions/naturals.fcl]] defines the following species  Raphael Cauderlier committed Mar 21, 2017 148 149 150  representing mathematical structures built from natural numbers with various operations and relations:  Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 164   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 168   Raphael Cauderlier committed Apr 15, 2017 169 170  The function =bit1= adds a =1= bit in binary notation so =bit1(n) = succ(bit0(n))=.  Raphael Cauderlier committed Mar 21, 2017 171   Raphael Cauderlier committed Apr 15, 2017 172  - Predecessor  Raphael Cauderlier committed Mar 21, 2017 173   Raphael Cauderlier committed Apr 15, 2017 174 175  The predecessor of =n= is =m= if =n= is =succ(m)= and =zero= if =n= is =zero=.  Raphael Cauderlier committed Mar 21, 2017 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 committed Apr 15, 2017 201 **** Morphisms  Raphael Cauderlier committed Mar 21, 2017 202   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 206   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 215   Raphael Cauderlier committed Apr 15, 2017 216 217  Moreover, it preserves and reflects all the operation of the structure.  Raphael Cauderlier committed Mar 21, 2017 218   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 226   Raphael Cauderlier committed Apr 15, 2017 227 228 - The reversed functional representation is similar but the morphism is seen as a function of type =A -> Self=.  Raphael Cauderlier committed Mar 21, 2017 229   Raphael Cauderlier committed Apr 15, 2017 230 **** Theorems  Raphael Cauderlier committed Apr 02, 2017 231   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 235   Raphael Cauderlier committed Apr 15, 2017 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 committed Apr 09, 2017 247 248  * The Interoperability Example  Raphael Cauderlier committed Mar 21, 2017 249   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 259   Raphael Cauderlier committed Apr 15, 2017 260 ** Logic Combination  Raphael Cauderlier committed Mar 21, 2017 261   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 266   Raphael Cauderlier committed Apr 15, 2017 267 268 For more details on this logic combination, see [[https://arxiv.org/pdf/1507.08721.pdf]].  Raphael Cauderlier committed Mar 21, 2017 269   Raphael Cauderlier committed Apr 15, 2017 270 ** Extenstion of the hierarchies  Raphael Cauderlier committed Mar 21, 2017 271   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 278   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 291   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 295   Raphael Cauderlier committed Apr 15, 2017 296 297 We then extend the morphism hierarchy to the new operations and transfer both theorems.  Raphael Cauderlier committed Mar 21, 2017 298   Raphael Cauderlier committed Apr 15, 2017 299 ** Instantiations  Raphael Cauderlier committed Mar 21, 2017 300   Raphael Cauderlier committed Apr 15, 2017 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 committed Mar 21, 2017 306   Raphael Cauderlier committed Apr 15, 2017 307 ** Final Proof  Raphael Cauderlier committed Mar 21, 2017 308   Raphael Cauderlier committed Apr 15, 2017 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]].