Locally nameless System F and ForMathlib directory

Stream: CSLib

[Chris Henson]

I am about a half dozen sorry away from proving type safety for a locally nameless System F with subtyping. I should have a PR ready in a week or so and I'll post here when it's ready. (I am especially excited to showcase how well grind works)

Along with this are some lemmas that should eventually be added to Mathlib.Data.List.Sigma. I propose we follow the convention from other projects and add a top level ForMathlib directory where we stage things we intend to upstream. Does this sound good to everyone?

[Kim Morrison]

Could I encourage limiting how much ends up in For Mathlib? It's a trade-off between moving quickly, and risking material getting stuck/abandoned there.

What about one of the following:

• It's okay during review, but needs to be PRd into mathlib before merging.
• Don't merge any PRs by authors who have files in ForMathlib from previous PRs that don't have corresponding open PRs at Mathlib?

The problem is, sadly, that someone has to do this work, and ForMathlib can easily become a repository of wishful thinking that someone else will do it. :-)

I appreciate that many projects do it, but I hope Cslib can err on the more responsible side here!

[Bas Spitters]

@Chris Henson sounds like great work. How does your work compare to the POPLmark?
https://www.seas.upenn.edu/~plclub/poplmark/

[Fabrizio Montesi]

I second @Kim Morrison's opinion. ForMathlib sounds nice, but it will likely become a great source of technical debt. I suggest we just put whatever theorems we like elsewhere in Foundations and let the mathlib people know that there is cool stuff in there every now and then (through PRs and/or discussions in this Zulip, for example).
But I wouldn't 'leak' project management in the repo's structure.

[Fabrizio Montesi]

(For System F, GREAT! :))

[Fabrizio Montesi]

For example, we have some stuff in Foundations.Data.Relationthat would make sense for mathlib.

[Chris Henson]

Okay, sounds like the consensus is there's a technical debt danger. So maybe we keep it decentralized and either add a comment or open an issue as a reminder.

[Chris Henson]

Bas Spitters said:

Chris Henson sounds like great work. How does your work compare to the POPLmark?
https://www.seas.upenn.edu/~plclub/poplmark/

Thanks! I closely follow Arthur Charguéraud's locally nameless solution linked there.

[Chris Henson]

In particular, porting this has been a good case study in comparing grind to Rocq's eauto/eapply. I'm still refining annotations, but currently grind will sometimes infer a bit more, sometimes a bit less. At this point it's roughly comparable in length overall, but I think I can shave it down to be a bit smaller. (While still being careful to not over-annotate in a way that's misleading or hurts performance).

[Bas Spitters]

Yes, it would be interesting to have a careful comparison. It will hopefully give ideas on how to improve the automation on both sides.

In case you get bored ;-)
https://poplmark-reloaded.github.io/

[Chris Henson]

Bas Spitters said:

In case you get bored ;-)
https://poplmark-reloaded.github.io/

Yes, this is on my todo list :) I was thinking (mostly for the sake of simplicity) of first trying strong normalization/logical relations when I get around to doing well-scoped de Bruijn indices.

[Bas Spitters]

Regarding logical relations it would be nice to explore the gluing approach. I believe I've seen a formalization of it, but I cannot directly find it now...
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.25/LIPIcs.FSCD.2019.25.pdf

[Chris Henson]

I agree, this would be great! This paper discusses a Rocq formalization of the categorical NbE cited above, but I'm not sure the code is public yet.

In general, I have been working on formalizing categorical semantics in Lean for some time, but had some difficulties. For instance even in formalizing semantics of simple types following Crole, two things are difficult formally:

• In Lean, it is likely more idiomatic to have typing derivations in Prop, while morphisms must be in Type. You can ULift, but it's awkward.
• If your lambda calculus has contexts and types that are not definitionally equal types, you end up needing docs#CategoryTheory.eqToHom (though you can sometimes get away with defining their interpretations in terms of each other and avoid this).

I also tried formalizing CwFs a while back. As they mention in the paper you linked, the term-level definitions require casting of the type-level definitions. Not impossible, but I wasn't sure how usable what I ended up with was.

[Bas Spitters]

Oh yes, that paper was on my reading list. It would be interesting to see how much of that could be done in Lean. I guess it might work with sufficient use of "Computable".

The universe problem can perhaps be avoided if Lean adopt's the new algebraic universes which are making their way into Rocq...

I guess there are CwFs/natural models in HoTT-lean, aren't there?

[Chris Henson]

Okay the PR cslib#68 is open! I'd like to again highlight the extensive use of grind here:

• This is just over a 40% LOC reduction from the Rocq formalization I was following, which already made extensive use of eapply, eauto, etc.
• Working with contexts is done by augmenting Mathlib's List.Sigma with grind annotations. I found I only needed a small handful of additional lemmas.
• This formalization continues to use the free_union tactic, which allows you to extensibility select variables free from existing contexts, terms, etc. which grind can then work with. Note that this tactic is very general, and is not specialized at all to this formalization or even lambda calculi.

@Fabrizio Montesi I realize this is a bit of a large PR, I will try to be better about that in the future! The docs/boilerplate make it seem longer than it really is. I think it'd have been more awkward to do it in pieces while I was working through the grind automation.

[Fabrizio Montesi]

Wonderful!! I'll start going through it.

[Fabrizio Montesi]

How's this related to https://github.com/leanprover/cslib/pull/28 ?

[Chris Henson]

Fabrizio Montesi said:

How's this related to https://github.com/leanprover/cslib/pull/28 ?

That PR uses well-scoped de Bruijn indices (similar to the style of Austosubst2), so would begin a separate directory at the level of LambdaCalculus/Named and LambdaCalculus/LocallyNameless. I do want to add that formalization, but would like to first do well-scoped STLC to make sure we get the design correct.

[Chris Henson]

In my mind these are the three most prominent choices of formalizing binding: explicit names, well-scoped, and locally nameless. As we've discussed previously, I think it would be great to have all three and some equivalence proofs.