The Coq mailing list

[François Thiré <franth2 AT gmail.com>]

I have been working on interoperability during my PhD and I would like
to share my insights with you.

Before I start, I would like to say that I was one of the main
contributor to the Logipedia website
(www.logipedia.science/about/about.php). The main goal Of Logipedia is
to provide libraries that could be shared between different proof
systems. As a proof of concept, the project provides a small library
with 300 hundreds arithmetic theorems, the last one being the small
Fermat theorem. This library can be exported to Coq, Matita, Lean, PVS
and OpenTheory (hence HOL-Light, and maybe Isabelle/HOL). However,
this post is not an apology for this project and reflects my own
opinions.

When we talk about interoperability, we first should define what it
means because in the world of proof assistants (or proof systems) this
term is a bit ambiguous.

Empirically, we can observe that a proof assistant is based upon a
logic. This logic can be Set Theory as it is the case for the proof
system Mizar, but most of the time this logic is based upon a type
theory. Many times, using the `principle-as-type` principle, the proof
assistant checks the validity of a proof by checking that a function
is well-typed but this is not always the case. For example, many
systems of the HOL families are based upon a type theory but the
derivation rules of the logic are different from the derivation rules
used to know whether a term is well-typed.

But such details is hidden in a proof assistant behind an interface so
that the user does not really need (in theory) to know what is under
the hood. For most of the proof systems I know, we often have a
separation between the user language, and the internal language of the
proof system. In particular, the user langage has many features which
do not exist in the logic behind the proof system: Type classes,
Implicit parameters, a module system, meta-variables...  Most of the
time, this user langage is split into a vernacular (commands) and a
tactic language.

This remark makes me believe that when we talk about interoperability
we need to be careful. Are we talking about interoperability at the
logic level or at the user level?

For example, in the previous posts of this thread, people used
interoperability to talk about both which is for me confusing. I tend
to believe (but it is only a belief) that these two kind of
interoperability can be addressed separately because we are talking of
different languages.

In my PhD, my work was mainly around the first notion of
interoperability: The one which aims to translate proofs written in
one logic to another.
In particular, I was interested in translations which are shallows so
that at the end, we really a proof in the target logic and not in some
encoding.

In general, shallows translations are not possible (how to translate
in a shallow way the axiom K from Coq to HOL? The logic behind the
latter cannot quantify over proofs). However, I do think that many
proofs and many libraries are interoperable (at the logic level)
between the current proof assistants. This is a reformulation (and
also extension) of a claim made by De Bruijn which is that all the
mathematics developped before the year 1800 could be expressed in
Automath (page 101 of Lambda Calculi with Types).

What I observed, is that the main difficulty comes from
computations. At the logic level, I don't think there are two proofs
assistants which behave the same way. So if you manage to remove
computations from your proofs, it is easier, and often it is easy to
make the proof interoperable with other systems.

It is not that difficult to design automatic and partial translations
which removes computations from proofs. This work for Fermat's little
theorem. This work also for all the HOL-Light libraries because the
logic has no computation.

Of course, it is not the only issue, one of them are axioms such as
mentioned before by Adam Chlipala. I tackled a bit this problem, one
example is when you want to design a shallow translation from
HOL-Light to Coq as it was done by Chantal Keller and Benjamin
Werner. In that case, one needs to remove the axiom that every types
are inhabited because this axiom is inconsistent in Coq.  What I
observed though, is that most of (if not all) the places this axiom is
used, it can be replaced by an axiom or a theorem which is compatible
with Coq (I don't recall all the details in the Keller-Werner paper
about this, this remark comes from my own experimentations).
Moreover, it is also not that difficult to design an automatic and
partial translation which does this.

Other things can be problematic such as the type system. However, my
first take away is to not underestimate how powerful can be an
automatic and partiel translation. Even if we can translate 25% of the
mathematic-components to another proof system, I do think it would be
still a nice achievement! Moreover, a second thing I want to say, is
that these translations can and should be parameterized by the user.

This is where we loose the automatic part. My second take away is that
we do not need a full automatic translation (at the logic level) but a
semi-automatic translation that could be parameterized by the user
(via a configuration file or a nice GUI).  For example, I designed a
tool which "minimizes" (even if it is not correct to say this) the
number of universes needed by a proof. By doing so, the tool may say
that `Nat` do not need to be a `Type`, it could be impredicate and
lives in `Prop` (not always of course, but sometimes). The tool
allows the user to say that `Nat` cannot be a `Prop` for example.

Finally, I would like to mention that probably such transformations
should be done in a "light" logical framework. What I call "light"
here means that proofs from other logics can be embedded in a shallow
way. The problem if the logical framework is not shallow is that
`typing` a real proof coming from another system is way too long.

With "light" logical framework, one advantage is to handle
transformations in a separate way. For example, you can hope that the
problem of universes is common to all the logics which have
universes. Hence, if the "minimization" transformation I mentioned
above should apply the same way independently if the proof comes from
Coq, Matita, Agda, Lean, ... Currently, I know that the tool I
designed works for both Coq and Matita for example (the real magic for
that comes from PTS/CTS).  My final take away is that to make
interoperability work from the logic point of view, a good way is to
design: Modular, semi-automatic, configurable and partial
translations.

Other questions are not answered here, and probably the main one is
about the scalability. It is not because I have experienced
interoperability with a small library of 300 theorems that the
techniques I have developped will work for larger libraries. The
answer to this question is not clear and requires furthers
research. However, my believe is that it can scale. For Fermat's
little theorem the translating time (the part which is automated) from
Matita to HOL takes not more than few minutes and I think this time
should grow linearly with the type checking time of the proof terms.

I have completely eluded the other interoperability question: How to
achieve interoperability so that the proof exported are ready to use?
For example, the Fermat's little theorem in Logipedia is exported in
Coq with 80 axioms to instantiate such as `\forall x, 0 + x = x`. Most
of these axioms come from recursive functions and are trivial to
instantiate. But, also the exported proofs are not linked with the
standard library. Hence the type `Nat` is a parameter as long as `0`
and `S`, but these definitions can be defined with the definition from
the stand library. It took me a couple of hours to make this
instantiation.

In conclusion, Logipedia is not ready at all to provide proofs which
are ready to use... but it can be!

I do not believe, except using Machine Learning techniques that we
will be able to achieve easily interoperability at the user syntax
level: How can you guess that the parameter `plus` in the Logipedia
library should be link with the function `add`? By looking at its
type? It is not enough, `mult` has the same type. Hence you also need
to take into account axioms. But even if you manage to link (the
correct terminlogy is align, or concept alignment), such translation
does not take into account the whole package a proof assistant
provides to help the user to formalize concepts: Type classes,
Implicit Parameters etc...  For example, the Feit-Thompson theorem
probably has a completely different shape at the logic point of a view
than the one the people involved in this project proved.

So, I don't think that we need to look for automatic translations
here, instead, we need an expert user of the system to make this
"concept alignment". I think that interoperability at this level is
the dual of interoperability at the logic level. At the logic level,
the tool was assisted by the user while here, the user should be
assisted by the tool.

However, we cannot expect a user to make this concept alignment
everytime he needs to. My hope, is that concept alignment could be
saved into a file using a DSL. Then, this file could be reused when a
proof is exported by another user. Better, it could be updated or
there might be several "alignement" files depending on what the user
wants to do.

This part is purely prospective and I did not have the time to explore
this path yet.


Finally, I would like to empahize a point made by Adam Chlipala about
social reasons. While I do believe that interoperability may work from
the scientific point of view, I think that social aspects may be the
reason why we will never see interoperability in practice. There are
several reasons I sketch here for which I do not have answers:

1. Who will be the users? Are the users waiting for a package ready to
user or willing to help interoperability?  From my experience, some
people want or need interoperability but are not ready to contribute
or worst, may be very critic, for example because the project is not
exactly the one they expected.

2. While building Logipedia, I had to understand:
 - The logic behind Matita and Coq
 - The logic behind Dedukti (the Logical Framework I used)
 - The logic behind OpenTheory
 - The syntax (and a bit of the logic) of Lean, PVS
 - The implementation of Matita
 - How to instrument Dedukti and therefore knows quite well OCaml
   (Dedukti being implemented in OCaml)

 For the Logipedia project, interoperability is split in three:
 - (import) Translation from the system to the Logical Framework
 - (interoperability) Inner translations inside the Logical Framework
 - (export) Translation from the Logical Framework to the target system

 Who should maintain import and export translations? Currently this
 burden is in the hands of PhD students. Maintaining these
 translations is not easy since it needs to understand the changes
 from the proof systems but also from the Logical Framework. For
 example Coq evolves quite fast since the past few yers and it is not
 always easy to update a correct translation.

3. Assuming that mathematical components can be partially translated
from Coq to another proof system A. Maybe it will be easier to
maintain the library in A everytime the math-comp library is updated
instead of calling again an interoperability tool.

These questions should not be neglected, many interoperability
projects exist and have existed and even if we now understand better
the theory behinds the proof systems that a decade ago, I don't think
it is enough to see a successful story of interoperability between
proof assistants!

P.S.  I tried to be concise, but I realize this mail is actually
really long. I eluded many other questions but I hope this return of
experience can help the discussion.

Le sam. 30 mai 2020 à 13:28, Adam Chlipala <adamc AT csail.mit.edu> a écrit :

I've been watching research papers pop up on the topic since well beyond
just 5 years ago.  It seems entirely plausible at this point that there
are technical and/or social reasons that this intuitive idea just isn't
worth the hassle.  We can at least say this goal has been "obvious" to
the community for a while, so it's not a case of work only beginning on
it when proof assistants reached a certain recent level of adoption.

In a typical open-source ecosystem of libraries, where library users
sometimes feel compelled to contribute improved code to support their
new use cases, it sounds like a mammoth liability to have to hop between
proof assistants for different libraries.  We know how hard it is
already to learn one proof assistant!

Even if a satisfactory translation between proof assistants is
automated, it's likely to bring dependence on axioms that some users of
the target proof assistant object to.  For example, many Coq users are
accustomed to accepting excluded middle, but my understanding is that
many data-type constructions in Isabelle/HOL work via a nonconstructive
choice operator, and I don't think it's standard to assume such an
operator in Coq (it's in the standard library but relatively rarely
used), so that would be a genuine "philosophical" cost of importing
Isabelle/HOL developments.  Conversely, I imagine modeling of nontrivial
Coq dependent typing in HOL would be a nightmare, requiring a whole new
set of skills to use an imported library effectively, even if its
original code doesn't need to be changed.

On 5/29/20 11:36 AM, Abhishek Anand wrote:
> I'd like to understand why such a tool/setup doesn't exist.
> Because of technical difficulties?
> Because such projects won't be cool enough to publish in "top
> conferences" and please the career gods?
> I very vaguely remember hearing about attempts to make such tools,
> about 3-5 years ago. I'd love to hear their experience.