Zulip Chat Archive

Stream: general

Topic: metatheory libraries/frameworks


Brendan Zabarauskas (May 17 2018 at 04:42):

Hello, I was wondering if anybody was working on libraries/frameworks for making defining metatheory stuff in Lean easier. I'm thinking like LN for Coq: http://www.chargueraud.org/softs/ln/ - Context is that I'd like to prove some properties about my language Pikelet. See this issue: https://github.com/brendanzab/pikelet/issues/39

Sean Leather (May 17 2018 at 06:09):

Hi @Brendan Zabarauskas!

I'm currently working on a Lean proof of part of the Coq locally nameless library predecessor to the one you've linked to. I've forked that library for my own reference. The reason I'm using the predecessor is because it had the Core ML typing formalization example, which seems to have been lost. (Also, are you familiar with Metalib, a successor to that library?)

My own work is currently strictly focused on what I need to get working for my research. However, I have certainly thought about making it useful more generally. As it is, I try to push into mathlib small improvements/additions that have helped me as I go. I think that the better mathlib gets — and it is well-maintained! — the less one needs another library.

All that said, it will probably be a lot of work to formalize what you need in Lean. There's a lot of existing knowledge, including libraries/frameworks, of how to do it in Coq. But I do find Lean easier to use, faster to compile, and more enjoyable. If you do plan on trying it out, you may want to take at look at my work. It's still in progress, but I'll do my best to answer questions or help out.

Brendan Zabarauskas (May 17 2018 at 06:12):

Oh cool, glad to know work is being done! I'll check out your stuff.

I definitely find the ergonomics of Lean much more pleasant than Coq, but the ecosystem is still lacking. In the future I will definitely start needing some kind of separation logic, but earlier on I can probably get by without (need to tackle the higher level metatheory before then).

Brendan Zabarauskas (May 17 2018 at 06:15):

What in particular is interesting to look at in mathlib? I saw it before but didn't make the connection that it might have interesting things for metatheory in it.

Sean Leather (May 17 2018 at 06:16):

Mathlib has a lot of basic theories and data structures. It's really like a standard library for Lean.

Brendan Zabarauskas (May 17 2018 at 06:17):

Oh that's good to know. I'm guessing folks like it because it can move faster than the builtin libs?

Sean Leather (May 17 2018 at 06:17):

In particular data.finset is very useful for my work. But the wealth of list-related proofs (data.list) also make it easy to work with lists.

Sean Leather (May 17 2018 at 06:18):

Oh that's good to know. I'm guessing folks like it because it can move faster than the builtin libs?

Yeah... Currently, the developers of Lean are working on the next version. They're not too keen on other changes right now. But mathlib, on the other hand, has had a lot of changes and is constantly growing.

Brendan Zabarauskas (May 17 2018 at 06:19):

Are you using a locally nameless representation in tts? Also would be handy to get a quick description of what tts is. Is the README opaque by design? :P

Sean Leather (May 17 2018 at 06:19):

Mathlib used to be the standard library before it was extracted from the Lean core.

Sean Leather (May 17 2018 at 06:19):

Not by design, just by fact of me focusing on proofs and less on evangelism. :wink:

Sean Leather (May 17 2018 at 06:20):

It's based on a let-polymorphic lambda-calculus.

Sean Leather (May 17 2018 at 06:20):

Core ML is another term for it.

Sean Leather (May 17 2018 at 06:20):

exp has the expression language.

Brendan Zabarauskas (May 17 2018 at 06:20):

Ah, right! Still, can be handy for folks like me searching for Lean examples on Github. I did a survey a few weeks ago, but had a hard time finding examples that I could learn off. Your work would have been super handy! <3

Sean Leather (May 17 2018 at 06:21):

Sorry. I've just been too busy to make it usable for others to read. I still have a lot to do.

Sean Leather (May 17 2018 at 06:22):

When I'm closer to writing about it, the documentation will be a paper and/or thesis, I hope.

Sean Leather (May 17 2018 at 06:23):

But, just FYI, every core.lean file has the definitions. Every other .lean file (except default.lean) has proofs.

Brendan Zabarauskas (May 17 2018 at 06:24):

Yeah, perfectly understandable that it's a WIP. I'm cool if it's messy - don't let me looking put any pressure on your stuff. Thanks a bunch for linking! Would be neat to extract some common stuff at some stage though!

Brendan Zabarauskas (May 17 2018 at 06:24):

Have you put it under a License?

Sean Leather (May 17 2018 at 06:25):

Would be neat to extract some common stuff at some stage though!

Indeed. I try to put as much common stuff as I can in mathlib. There's still more of that I have planned.

Brendan Zabarauskas (May 17 2018 at 06:26):

Oooh, this is super handy :clap: https://github.com/spl/tts/blob/master/src/exp/core.lean

Sean Leather (May 17 2018 at 06:26):

Have you put it under a License?

Not at the moment. I suppose I should. Apache 2.0 since that what mathlib uses? I don't feel strongly about it.

Brendan Zabarauskas (May 17 2018 at 06:29):

Yeah, I normally go with Apache 2.0. Sometimes I dual license with MIT. But that's cause I'm used to the Rust ecosystem. I tend to adapt to whatever is generally accepted in the ecosystem

Sean Leather (May 17 2018 at 06:33):

LICENSE added.

Brendan Zabarauskas (May 17 2018 at 06:35):

Thanks! Might be a while till I actually get around to getting started on formalisation, but it's handy to have your stuff around as reference.


Last updated: Dec 20 2023 at 11:08 UTC