Upstreaming `List.Sublist`, `Pairwise`, and `Nodup`.

Stream: batteries

[Kim Morrison]

I'm putting upstreaming Sublist, Pairwise and Nodup on my TODO list, for the leansat project (which won't be able to depend on Batteries).

My intention is that these will initially only have the minimal API needed to support leansat, and further down the track as I finish completing the List API for the existing functions/predicates in Lean I will return to these.

[Mario Carneiro]

Kim Morrison said:

for the leansat project (which won't be able to depend on Batteries).

I'm not going to push too hard on this, but why?

[Mario Carneiro]

in any case it sounds fine by me, I'm sure you will need this anyway for some hashmap lemmas. (You probably should have taken Sublist already in the first wave instead of rewriting proofs to avoid it)

[François G. Dorais]

Okay, no major issues. But you do realize that you're also upstreaming maintenance and putting it behind a FRO wall (to coin a phrase).

[Shreyas Srinivas]

Why can't these projects depend on batteries?

[Henrik Böving]

The plan for LeanSAT is to move it into the core repository. This is in line with the general vision for core to have good support for the core types, among which we have BitVec. Once LeanSAT lands in core users will get both a nice BitVec library in terms of available lemmas (this is what core already has, for the past few months the lemmas that LeanSAT demands to verify its decision procedures have been pushing the BitVec theory in core a lot further), as well as a complete decision procedure for fixed width BitVec things which is of course very interesting for software and hardware verifiaction purposes.

[Ruben Van de Velde]

I hope we won't regret this close coupling with the compiler

[Henrik Böving]

What close coupling with the compiler are you thinking about here? The idea is to merely put LeanSAT into core such that it is available out of the box, not to make any core specific changes.

Note that, to our knowledge, the ability to have a verified decision procedure for fixed width BitVec would be unique to Lean among the ITP world. Isabelle doesn't have this, Agda doesn't have this, Coq does actually have a verified bitblaster but it targets SMTLIB and is not available as a tactic. Given that software and hardware verification users are very interested in fixed width BitVec reasoning this is hopefully going to be a notable point in favor of using Lean in the future.

[Eric Wieser]

Do we have a lake new my_project batteries command for creating a larger box for new users to start with?

[Eric Wieser]

(since we have lake new my_project math)

[Shreyas Srinivas]

That would be really nice. Adding a cache would also be nice (at least local cache).