Proving Axiom Sane

Stream: general

[Tim Daly]

In \cite[p~7}{Mour15} "Elaboration in Dependent Type Theory", there is an example of a semigroup structure which extends a has_mul structure.
The elaborator figures out this "chain" while defining "mul_assoc".

Axiom has similar separate structures (we call them categories, ... don't ask) that have a similar kind of chaining. Axiom has its own elaborator, although it is just a part of the compiler.

Does Lean provide a command / api to output fully elaborated structures?

[Patrick Massot]

Beware this paper is about Lean 2, not the current version or the next one.

[Tim Daly]

Do you have titles? I'll look them up and put them in the lean.bib file.

[Patrick Massot]

Titles of what?

[Tim Daly]

I assumed that if the elaboration has changed there is a paper that describes the new elaborator.

[Patrick Massot]

I don't think so, but you should ask @Sebastian Ullrich.

[Patrick Massot]

or @Gabriel Ebner

[Sebastian Ullrich]

There isn't

[Tim Daly]

Is there a command / api to show the full elaboration?

[Tim Daly]

Axiom has general type constructs like Group, Ring, Field which exports 'signatures' of functions that must be implemented (e.g. a multiply operator) by any domain (e.g. polynomials need to implement multiply). What Axiom lacks, and I am working to provide, are the 'axioms' that a Ring needs to satisfy and specifications of polynomials (e.g. the multiply operation) that define the operations. To do this I have to re-implement the Axiom compiler for the Axiom language (called Spad, short for Scratchpad).

The new compiler (called Sane) has the dual job of producing Axiom compatible code (common lisp functions) and Lean compatible proofs. I have done a 'first-cut' deep dive into the Lean source code. It seems that the Sane compiler needs to compile to Lean syntax (as well as common lisp). This is basically a 'dual tail' compiler.

Such a compiler would make Axiom's computer algebra functions available in Lean.

There are, of course, 'second level issues', such as proving the Sane compiler lisp output is correct. But, as we all know, "it's kittens all the way down" so it is not a simple job. But it does seem to be a realistic path forward, merging Axiom and Lean.