Commit cc9cac58 by Raphael Cauderlier

parent b5fe2f1b
 ... ... @@ -53,15 +53,17 @@ The following tools are required to compile the MathTransfer library: Sukerujo is an alternative Dedukti parser used by FoCaLiZe - Zenon Modulo version 0.4.3 - Zenon Modulo version 0.4.3 Focalide - Dktactics Dktactics is a tactic language for Dedukti - Dktransfer - Zenon Transfer Dktransfer is a transfer tactic for Dedukti 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: ... ... @@ -133,42 +135,44 @@ the natural numbers. They can be imported from any arithmetic library. The logic used in the MathTransfer library is an higher-order logic seen as an extension of multi-sorted first-order logic. **** TODO detail the description of the logic *** Arithmetic *** Natural Number Arithmetic The directory [[./lib/arith][lib/arith]] contains the definitions of arithmetical structures, that is mathematical structures about natural numbers and integers. structures, that is mathematical structures about natural numbers. **** Natural numbers The file [[./lib/arith/naturals.fcl][lib/arith/naturals.fcl]] defines the following species **** 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: - Peano axioms - 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 Peano axiomatization of natural numbers forms the first building block of the arithmetic library: the =NatDecl= species in file =naturals.fcl=. This species requires two functions: =zero= of type =Self= and =succ= of type =Self -> Self= and three axioms: =zero_succ= expressing that =zero= is the successor of no natural number, =succ_inj= expressing the injectivity of =succ= and =ind= expressing the induction axiom. We see =ind= as a single first-order axiom by representing predicate (and function) application as a binary operation =@=. 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. - Reasoning by case (all numbers are zero or successors) The function =bit1= adds a =1= bit in binary notation so =bit1(n) = succ(bit0(n))=. In FoCaLiZe, first-order statements are easier to use than higher-order ones because the first-order theorem prover Zenon can assist the user in the first case and not in the second case. - Predecessor An inductive argument that does not actually use the induction hypothesis is the same thing than reasoning by case on a natural number and this can be stated as a first-order theorem: any natural number is either zero or the successor of some natural number. The predecessor of =n= is =m= if =n= is =succ(m)= and =zero= if =n= is =zero=. - Addition ... ... @@ -189,69 +193,118 @@ integers. =le= is a binary relation over natural numbers defined by the following axiom: + =le(m, n) <-> (ex p : Self, plus(m, p) = n)= - Subtraction =minus= is a binary operation over natural numbers defined by the following axioms: + =minus(zero, n) = zero= + =minus(succ(n), zero) = succ(n)= + =minus(succ(m), succ(n)) = minus(m, n)= - Strict ordering =lt= is a binary relation over natural numbers defined by the following axiom: + =lt(m, n) <-> le(succ(m), n)= - Divisibility **** Morphisms =divides= is a binary relation over natural numbers defined by the following axiom: + =divides(m, n) <-> (ex p : Self, times(m, p) = n)= The files in the directory [[./lib/arith/morphisms][lib/arith/morphisms]] define isomorphisms between representations of natural numbers. Three representations of morphisms are proposed: - Strict Divisibility - 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 =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))= Moreover, it preserves and reflects all the operation of the structure. - Primality - 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). =prime= is a predicate over natural numbers defined by the following axiom: + =prime(p) <-> lt(succ(zero), p) /\ all d : Self, ~(sd(d, p))= - The reversed functional representation is similar but the morphism is seen as a function of type =A -> Self=. The file **** Theorems **** TODO Integers 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 * TODO Related work 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. ** Automating proofs of transfer theorems ** Logic Combination *** In Isabelle/HOL 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]]). *** In Coq For more details on this logic combination, see [[https://arxiv.org/pdf/1507.08721.pdf]]. *** In Dedukti ** Extenstion of the hierarchies ** TODO Proof reuse 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 Nicolas Magaud =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))= Planning? 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. ** TODO Univalent foundations We then extend the morphism hierarchy to the new operations and transfer both theorems. Ongoing program of founding mathematics on type theory using the univalent axiom. This work does not assume an extra axiom. Can be related to computational content of univalence. ** Instantiations * Future work 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]]. Better distinction between bool and Prop: because of the use of OpenTheory stdlib, we tend to confuse bool and Prop. Decidable operations on natural numbers should be in bool. ** Final Proof Setoids: The development would be a bit more general if it did not depend on equality. This would make the library more compatible with FoCaLiZe stdlib. 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]].
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!