Proving the equivalence of type and function definitions automatically in Coq

PhD application form

Supervisor: Frédéric Blanqui

Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette

Context: Formal proofs are used in mathematics but also in the industry for certifying the correctness of protocols, software and hardware. Interoperability is a very important feature in computer science and engineering to avoid useless work duplication and allow more safety. Unfortunately, interoperability between proof systems is not well developed. This project aims at improving the interoperability between two important proof systems, HOL-Light which has an extensive library on analysis, and Coq which has an extensive library on algebra.

hol2dk is a tool able to automatically translate definitions and proofs from HOL-Light to Coq. However, to get something readily usable in Coq, it is necessary to align the definitions of HOL-Light with those already defined in Coq. 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, hol2dk 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 for a few common inductive types like natural numbers and lists, and recursive functions like addition and concatenation.

Objective: The goal of this project is to develop tactics in Coq to help prove the equivalence between the way HOL-Light and Coq define inductive types and recursive functions. While inductive type and recursive function definitions are primitive in Coq, this is not the case in HOL-Light, where they are defined as fixpoints of some functionals.

Work plan: The student will start by studying the way inductive types and recursive functions are defined in HOL-Light. Then, through a few examples, they will study how these definitions are translated to Coq, and how they can be proved equivalent to more idiomatic definitions in Coq (using the Coq commands Inductive and Fixpoint). Finally, they will develop tactics in Coq to help automate those equivalence proofs.

References:

• Translating HOL-Light proofs to Coq, Frédéric Blanqui, LPAR, 2024.
• Lambdapi export command, Lambdapi user manual, 2024
• A modular construction of type theories, Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, LMCS 19(1), 2023.
• Creating new tactics, Coq reference manual, 2024.
• Melham, T.F. (1989). Automating Recursive Type Definitions in Higher Order Logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds) Current Trends in Hardware Verification and Automated Theorem Proving. Springer, New York, NY.
• define_type, The HOL Light System REFERENCE, 2023.
• Krauss, A. (2006). Partial Recursive Functions in Higher-Order Logic. In: Furbach, U., Shankar, N. (eds) Automated Reasoning. IJCAR 2006. Lecture Notes in Computer Science(), vol 4130. Springer, Berlin, Heidelberg.
• new_recursive_definition, The HOL Light System REFERENCE, 2023.
• Inductive types and recursive functions, Coq 8.20.0 reference manual, 2024.