Zulip Chat Archive

Stream: general

Topic: metatheory libraries/frameworks


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Sean Leather (May 17 2018 at 06:19):

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

view this post on Zulip Sean Leather (May 17 2018 at 06:19):

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

view this post on Zulip Sean Leather (May 17 2018 at 06:20):

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

view this post on Zulip Sean Leather (May 17 2018 at 06:20):

Core ML is another term for it.

view this post on Zulip Sean Leather (May 17 2018 at 06:20):

exp has the expression language.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Brendan Zabarauskas (May 17 2018 at 06:24):

Have you put it under a License?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Sean Leather (May 17 2018 at 06:33):

LICENSE added.

view this post on Zulip 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: May 14 2021 at 12:18 UTC