Working on a Translation of Software Foundations to LEAN

Stream: general

[Aniket Mishra (Sati)]

One thing that I really found missing while trying to learn LEAN for the first time was something like Software Foundations. I found Software Foundations amazing since I could read all of it just from my editor (EMACS) and interactively step through the proofs. There are quite a few books for LEAN that have a lean project that is meant to be accompanied with reading of a PDF/markdown page, but I feel like the best way to learn a programming language is to spend time writing programs in it, and a separate markdown book distracts from the experience somewhat.

So, after consulting with Leo, I'm thinking of trying to attempt this translation myself. Of course there will be a differences that would need careful handling. For example, tactics in LEAN feel much more refined than the ones in Rocq (atleast, in the time the book was being written), so it might be worth spending more effort in introducing the tactic language early on/to investigate it in more detail. There might also be some differences caused by universe polymorphism in LEAN (which is not available by default in Rocq) that are also worth looking into but I'm not sure, such quirks will become more apparent during the process of the translation. At the very least, I feel like it requires careful thought and discussion.

I've made a github repo for this, but as of this moment, it contains only an initialised LEAN project.

[Shreyas Srinivas]

You will find that at least the material covered in volume 1 will need substantial revision. I worked through the first few chapters in lean in early 2024

[Shreyas Srinivas]

There are substantial differences in the way we use supposedly analogous tactics between Rocq and Lean

[Shreyas Srinivas]

For example I recall that they use reflexivity quite often and their simpl tactic does not close those goals

[Shreyas Srinivas]

And there is a lot of material dedicated to inversion which is taken care of easily by Lean’s cases tactic

[Shreyas Srinivas]

Further lean has a lot of different ways of peforming induction which might be useful in PL proofs but aren’t described in vol 1. For example functional induction.

[Aniket Mishra (Sati)]

Yeah, that makes sense, in general I've also felt that Rocq primitives are less sophisticated than LEAN (like LEAN's match, with which when working with dependent types, does case elimination which Rocq's match .. with .. end does not). Tactics also mesh much better with other program primitives.

[Shreyas Srinivas]

I wouldn’t say they are better or worse since those are determined by subjective standards. I am just saying that there are substantive differences both in terms of tactic behaviour and proof culture. Further the differences mean that beyond the basic conceptual and pedagogical idea behind volume 1, the whole content and organisation needs some careful rethinking

[Aniket Mishra (Sati)]

Right, I get what you mean. I'll try to take some time to think about this. (Also, I should have been more careful with my wording, I don't think one is objectively better/worse either.)

[Shreyas Srinivas]

You could try writing it in verso using the manual template. It gives a lot of interactivity for free within the compiled book

[Aniket Mishra (Sati)]

Yeah, I took a look at Verso earlier, and I'm not completely sure if it does what I want. As far as I understand, it allows you to write in a DSL in LEAN, which you can get a compiled book/page out of. But for someone looking at the source code, it'd just be confusing, and I want the reader to be able to navigate the book entirely through the source code as easily as possible, if that makes sense. Do correct me if I have a misunderstanding about something.

[Shreyas Srinivas]

There is a tool called subverso that lets you separate the code from the text by allowing you to insert code references into it. I don’t fully understand how it works, but it is worth pinging the experts on this.

[Aniket Mishra (Sati)]

Hmm, Ill try to take a better look into it, but generally I'm deeply hesitant towards using a tool that modifies the language itself, because for someone stepping through the program files, it'd be distracting.

[Shreyas Srinivas]

Depending on what sort of interactivity you seek however verso might be sufficient. Just the generic verso output provides very rich interactivity for the codeblocks

[Shreyas Srinivas]

You can click and check definitions. Look at proof states line by line and so on

[Aniket Mishra (Sati)]

Hmmm

[Quinn]

There's actually a part in hoare logic where inversion is much much easier than without it.

[Quinn]

I still haven't cracked hoare_while in lean!

[Shreyas Srinivas]

Is your code available somewhere so I can try it out?

[Quinn]

i'll DM you! it's a part of a larger product I don't want to post publicly yet