Lean4Less discussion thread

Stream: general

[Rish Vaishnav]

Discussion thread for the Lean4Less announcement

[Violeta Hernández]

Interesting! Is def-eq proof irrelevance the only axiom within scope, or are there plans to expand this project to e.g. proving things without choice or LEM?

[Rish Vaishnav]

It's limited to eliminating definitional equalities, that is, equalities that are checked by the kernel and do not normally require proof. And in the process, it introduces axioms, like the prfIrrel axiom above (which is definitionally true in Lean). It builds the proof in parallel to normal kernel typechecking, and it doesn't do anything more intelligent, like trying to get around using proof irrelevance when it doesn't have to use it. So it's not applicable to translating proofs to evade the use of certain things like the axiom of choice or the excluded middle property. I do have plans to soon extend it to eliminate other defeqs, like struct and function eta for example (there's just a little bit more I need to parameterize first in order to try that out)

[Rish Vaishnav]

I should probably mention that I called the translation "Lean4Less" in the sense of "Lean for a smaller kernel", it's not at all a translation that tries to reduce the size of Lean terms, the translated terms will only get bigger (much bigger, in some cases)

[Max Nowak 🐉]

You mention you were discussing implementing an extTT-to-intTT translation. Has anyone picked up work on that?

[Rish Vaishnav]

I’ve started work on a ground-up kernel rewrite of Lean to allow for user-defined extensional rewrite rules/undirected defeqs, and have a few small examples working. In it, I’ve replaced Lean’s C++ kernel with the Lean4Lean implementation to make modifications easier. I was going more in the direction of having extensionality as a built-in feature of Lean, with an after-the-fact translation to the original theory via Lean4Less that would be isolated to Mathlib CI, for example (as opposed to a real-time translation on the user side). But there’s still a lot more work to be done to make it more efficient and scalable.

Unfortunately I haven’t had much time for it lately between PhD work and other more recent ambitions. I do certainly plan to get back to it eventually however! If anyone wants to try to hack around with it in the meantime, I’d be happy to provide more details.

[Rish Vaishnav]

My Lean4Less paper is now available on HAL! It will also appear in the proceedings of the ICTAC 2025 conference, which I attended last week: here are the slides. Also, there are many more details on the implementation of Lean4Less to come in my PhD thesis, which should be available by February of next year (if everything goes as planned). If you have any questions about the paper, feel free to ask them here (or DM me).

[Bhavik Mehta]

This is really cool! One thing I've dreamed about for a long time is if we could translate Lean terms into a topos (indeed this was part of my motivation for the topos project, but it ended up defining grothendieck toposes and getting used for condensed maths instead!), and the conceptual part which I didn't know how to solve was how to translate Lean's structure defeqs into being explicit rewrites. It looks to me like you've solved that problem?
To be much more concrete, is it now feasible to do the following?
Given a fully polymorphic, constructive definition eg

def myFunc {A B C : Type} : (A × B → C) → A → B → C := fun f a b ↦ f (a, b)

which uses (for now) only the type constructors Prod and non-dependent pi; convert it into a morphism in an arbitrary cartesian closed category? And then, can we automatically derive equalities in the category which correspond to this theorem?

def myFunc {A B C : Type} : (A × B → C) → A → B → C := fun f a b ↦ f (a, b)

def myPi {A B : Type} : A × B → A := fun x ↦ x.1
def myPair {A B : Type} : A → B → A × B := myFunc (fun x ↦ x)

theorem myPi_myPair {A B : Type} {x : A} {y : B} : myPi (myPair x y) = x := rfl

(perhaps this one would be axiomatic, but would be something like https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.html#CategoryTheory.Limits.prod.lift_fst)

Of course eventually this should be extended to more type constructors, I just wanted a small one for the sake of example.

[Johan Commelin]

cc @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒

[Aaron Liu]

I was doing something with this

[Aaron Liu]

https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Constructing.20morphisms.20in.20a.20cartesian.20closed.20category/near/504227246

[Aaron Liu]

I'm also working on a tactic that's complete for equality of parallel morphisms in a free ccc

[Bhavik Mehta]

Right, constructing the morphisms isn't too bad, but converting the proofs is the more interesting part, in particular because we go from a rfl proof to a propositional, non-definitional equality, and it looks like Rish's setup is now able to do this?
Note also that CCC is just the test case, ideally we should be able to interpret in any category with enough structure, so eg convert the natural number game automatically into a topos with NNO, and convert any fully polymorphic constructive proof in mathlib into a topos, and convert any proof in mathlib into a category satisfying ETCS.

[Bhavik Mehta]

Johan Commelin said:

cc 𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒

I remember discussing this exact thing with him back in 2019! How time flies :)

[Rish Vaishnav]

Bhavik Mehta said:

the conceptual part which I didn't know how to solve was how to translate Lean's structure defeqs into being explicit rewrites

Not sure I totally grasped everything, but if your goal is to make Lean's specialized defeqs for structs (struct eta, struct-like reduction, projections) explicit, then that would certainly be within scope, however the translation is not currently set up to do this (though it can already eliminate struct-like reduction). For instance, if you want to make explicit the proof of some theorem X utilizing projection reduction in its typing (like in myPi_myPair), making use of an axiom characterizing the projection reduction:

axiom proj_eq {A B : Type} (a : A) (b : B) : (a, b).1 = a

then that should be feasible for the translation, if you were to generate such axioms for each of the projections of every structure type.

On the other hand, if your objective is rather to make types that are not exactly structs but "similar enough" to structs behave more like structs in terms of the defeqs that are applicable to them, you could feasibly extend Lean4Less to translate from a larger class of defeqs that includes the one that you are targeting. If you replaced the type A × B in the theorem X with some non-struct type T, but are still able to prove the equivalent of proj_eq for T, you could feasibly clue the extended Lean4Less translation in on this fact, telling it to generate a proof of X as if this property was definitional, and achieve a translation identical in structure to the translated proof of the version of X which used A × B, but which uses the new theorem in place of proj_eq.

Is that somewhat along the lines of what you were asking about?

[Bhavik Mehta]

It is, and that's very helpful context, thanks! I'll take a closer look at the paper and implementation

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I replied to the ping in a different thread in order not to hijack this one.

@Rish Vaishnav I am excited about the potential of this to implement Nuprl/Istari-style equality reflection as a custom proof mode! Or Agda-style custom REWRITE rules. I share the caution you express in

The output of ett-to-itt will likely be unacceptably large because it is directly derived from a formalization that makes an only very limited attempt at optimizing the output size

because in SynthLean we have also found term sizes to be an important (and often overlooked) usability consideration. But I think there is hope: IIRC the translation comes with a metatheorem saying that any statement that is definable in ITT and provable in ETT also has an ITT proof. Now when the statement is a proof-irrelevant Prop, we might not care so much about how ugly the translated ITT proof is. There is still a performance consideration, but that seems more surmountable than having users manually wrangle with proof-relevant translation outputs.

EDIT: Oh, just realized that part is talking about a different, hypothetical translation extracted from a formalization. I should actually read the paper :sweat_smile: Comment above still applies, though: performance will always remain a concern.

[Rish Vaishnav]

Yes, indeed there are issues with scaling, some of which may not be entirely avoidable (like the "transport hell" problem). This is part of the reason why I am rather partial to the approach of extending the kernel itself to allow for user-defined defeqs/custom rewrites and eta rules like they have in Andromeda. This obviously would require a larger kernel, so we would have to make sure things remain efficient in the common cases (I think Lean's discrimination trees would be useful for narrowing down possibly applicable user-defined rules, but have yet to look into this further).

And then there's the issue of trust, as larger kernels are more likely to contain bugs that could affect consistency. However, trust could be largely recovered if we can show that the translation is correct, as well as verify the extended kernel w.r.t. the metatheory (see Appendix F and slides 24 - 27).