Add a mechanisation of System Fsub in "well-scoped" style

[Linyxus]

This adds a mechanisation of System Fsub in a home-brewed style which I call "well-scoped" style. The two key ingredients are intrinsically scoped de Bruijn indices for by-construction well-formedness and context morphisms for a uniform infrastructure of context manipulation (weakening, narrowing, substitution, etc). See the entry file for more details.

[chenson2018]

I have left review comments mostly pertaining to style and making proofs more compact. I think grind would help here, but do not consider it a blocking requirement.

As I mentioned on the Zulip, the biggest thing we do require is documentation, ideally for every theorem, definition, and inductive.

[chenson2018]

I'm not sure that this style of reexports is necessary, do you have any thoughts @fmontesi?

[Linyxus]

Thanks @chenson2018 a lot for your reviews! My bandwidth is a bit jammed recently so I didn't improve the documentation as promised. I will get back to it, addressing the reviews, improving docs and compacting proofs ASAP.

[Linyxus]

I have populated the files and definitions with documentation, and addressed most of the comments (except for those I didn't mark as resolved). Thanks again for these feedbacks!

[Linyxus]

regarding paper references for this approach, I believe the one used by AutoSubst2 is really close.

[chenson2018]

Thanks for addressing the review comments. I will take a look again this week. Regarding your comment:

regarding paper references for this approach, I believe the one used by AutoSubst2 is really close.

I have also been looking at porting some formalization in the Autosubst2 style to Lean. I think what we may want to do is first add well-scoped STLC. This may make this PR take a little more time, but ensure we end up with consistency between them. (I am not asking you to do this, I will write it).

[Linyxus]

Sure! I just finished a draft on a tutorial of this "well-scoped" approach and am putting it on arXiv. Can be an interesting reference too for this PR.

Regarding autosubst2, I think another thing that is really interesting & valuable to have is a "port" of it in Lean (or something like it that generates boilerplates). I have repeated the boilerplate of this approach for various calculi and am a bit tired of it. 😂 I can image such a tool will be a hyper productivity boost.

[chenson2018]

Regarding autosubst2, I think another thing that is really interesting & valuable to have is a "port" of it in Lean (or something like it that generates boilerplates). I have repeated the boilerplate of this approach for various calculi and am a bit tired of it. 😂 I can image such a tool will be a hyper productivity boost.

Yes, I agree! I have been thinking this over for a while actually. Regarding the implementation, I think because of Lean's metaprogramming features, we could natively write something that looks like the MetaCoq implementation of Austosubst2. (I've also been tossing around the idea of if features like attributes could change the user interface for the better)

I am currently auditing a semantics course using Autosubst2 and was planning to try to follow along with making a Lean port. When I have the start of something I'll ping you for your thoughts!