Supervisors: Frédéric Blanqui (LMF) and Patrick Massot (LMO)
Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette
Summary: Proof systems, automated or interactive, have increasing applications in education, industry and research. Although interoperability is a very important property in engineering and computer science to reduce development costs, it is poorly developed within proof systems. This greatly hinders the democratization of those tools and the formalization of advanced mathematical results. One way to improve interoperability is to develop translations between systems. But for translated definitions and theorems to be readily usable, the translated types and functions must be aligned with those already used in the target systems. To this end, it is necessary to prove that a type or a function can be substituted by another one. However, for this to be correct, one needs to show that the two types are indeed isomorphic and that the two functions are indeed equal. This project aims at developing tools to automate this kind of proofs as much as possible.
Scientific objectives and challenges: The goal of this project is to make the existing translations of libraries of mathematical definitions and proofs from one system to the other directly usable by the users of the target systems, by proving the equivalence of the various definitions of the same mathematical notions, and developing proof tactics to automate those proofs as much as possible. For instance, to prove that two types or two mathematical structures are isomorphic (e.g. the type or structure of group or topology), that two constant or function definitions are (point-wise) equal (e.g. the real number pi, the exponential function on real numbers), or that two predicates are equivalent (e.g. the notion of continuity). Equivalence proofs may be non trivial even for simple structures, e.g. the fact that any two models of real numbers (Dedekind-complete ordered fields) are isomorphic.
This is an important task since there are some mathematical results the formalization of which in a given proof assistant took several years to several people (e.g. 4-color theorem, Feit-Thompson theorem, Hales proofs of Kepler conjecture). It is therefore not reasonable to think that such a work can be done again in any other proof assistant. Hence, there are mathematical results that are available in only one system and cannot be reused in other systems because there exist no translation between those two systems. Indeed, translating a definition or a proof from one system to another is a difficult task, that is impossible in some cases if the logic of the target system is weaker than the source system, or if the source system uses axioms that are incompatible with those of the target system. All this slows down the formalization of new more advanced mathematical results.
Context and state of the art: Dedukti is a logical framework in which one can express the deduction rules and proofs of many different proof systems in a modular way. It is based on the lambda-Pi-calculus modulo rewriting, an extension of the lambda-Pi calculus where types are identified modulo user-defined oriented equations.
Lambdapi is a proof assistant on top of Dedukti that can read and write Dedukti files, and export them to the proof assistants Coq and Lean.
There exist various tools that can export the proofs of some given system to Dedukti or Lambdapi. For instance, Hol2dk can export HOL-Light proofs to Dedukti and Lambdapi, Coqine can export Coq proofs to Dedukti, Lean2dk can export Lean proofs to Dedukti, Krajono can export Matita proofs to Dedukti, etc.
By composing these tools, one can translate the definitions and proofs from one system to the other, e.g. Hol2dk+Lambdapi can translate HOL-Light definitions and proofs to Coq and Lean.
However, to get something really usable in the target system, it is necessary to align the definitions of HOL-Light with those already defined in Coq or Lean. For instance, a HOL-Light theorem on HOL-Light natural numbers should be translated to a Coq theorem on Coq natural numbers, and not to a Coq theorem on the representation of HOL-Light natural numbers in Coq. To this end, Lambdapi can replace a HOL-Light symbol by a Coq expression. For instance, the HOL-Light symbol for the type of natural numbers by the Coq symbol for the type of natural numbers, and the HOL-Light symbol for the addition on natural numbers by the Coq symbol for the addition on natural numbers. But, for such a replacement to be valid, one must prove that the Coq expression satisfies the properties defining the HOL-Light symbol. For instance, that the type representing HOL-Light natural numbers in Coq is isomorphic to the Coq type of natural numbers, and that the Coq addition on natural numbers satisfies the property defining the HOL-Light addition on natural numbers. This has already been done by hand in Coq for a few types or type constructors like natural numbers, lists, integers and real numbers, and a few basic functions on them. See coq-hol-light.
Methods, concepts and tools: The goal of this project is to extend this work in various directions:
a) Many types, predicates and functions are defined inductively. However, while inductive type and recursive function definitions are primitive in Coq and Lean, this is not the case in HOL-Light, where they are defined as fixpoints of some monotone functionals. It would therefore be very useful to develop general tactics to prove the equivalence of these two kinds of inductive definitions automatically.
b) The next step is prove the equivalence of algebraic structure definitions of increasing complexity like monoids, groups, rings, sigma-algebras, etc. that are used in advanced mathematical results.
c) The equivalence proofs are currently done in the target systems themselves. This means that, currently, all these equivalence proofs must be done in each system. This is not so surprising as all these proofs are a priori specific to each system. However, it is often the case that, when two proof systems share the same features or constructions, types and functions are defined in the same way. For instance, both Coq and Lean have similar primitive constructions for inductive types and recursive functions. We can therefore wonder whether parts of (if not all) these tactics and equivalence proofs could instead be expressed once and for all in Lambdapi itself so that they get automatically translated to Coq and Lean, together with the other proofs.
Expected results and criteria for evaluation project success: The obtained translated libraries of mathematical definitions and proofs will be made available as Opam packages for Coq, or included in the Mathlib library for Lean.
HOL-Light has a very large library of mathematical theorems, especially in analysis, that are not yet available in other proof assistants. For instance, the Multivariate library of HOL-Light contains more than 20,000 theorems in analysis, topology, measure theory, etc.
To make all these theorems directly usable by Coq and Lean users will boost the formalization of new and more advanced mathematical results.
It will be possible to evaluate the success of the project by counting the number of types and functions that have been proved equivalent, and the number of HOL-Light theorems used in new Coq or Lean developments.
References: