Since Stdlib2 will also mean rethinking the hint databases, what about setting the Loose Hint Behavior option to "Strict"? cc coq/coq#7710

@CohenCyril and I will extend https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md#statements-of-lemmas-theorems-and-definitions

These conventions will be used in stdlib2.

Their description should be moved to the stdlib2 repository, and missing/unclear conventions can be discussed here.

Opening a discusison:

I am not sure this is in the scope of stdlib2 or if this is already thought of, but it would be nice to move all default auto-generated schemes (foo_ind... beq_foo etc) into there own modules (or record) and have a command to change the default "default scheme module". For instance the current "_ind" name trick is painful at least for the 2 following reasons

• we cannot change the default induction principle
• We cannot easily blacklist induction principles from Search... Yes we can but with the "_ind" which may blacklist other lemmas.

A gitter discussion suggested making stdlib2 compatible with stdpp. Is that a realistic goal?

@robbertkrebbers @RalfJung

I wish all types (type families) in the standard library came with a distinguished notions of validity and equivalence, ideally expressed using a partial equivalence relations. For example

nat_per := Logic.eq
prod_per {A B} A_per B_per := fun '(x1, y1) '(x2, y2) => A_per x2 x2 /\ B_per y1 y2
Q_per := fun '(n1, d1) '(n2, d2) => d1 <> 0 /\ d2 <> 0 /\ n1*d2 /\ n2*d1
option_per {T} T_per := fun a b => match a, b with Some x, Some y => T_per x y | None, None => True | _ => False end.
Prop_per := iff
proof_per (P : Prop) := fun pf1 pf2 : P => True
int_per := fun a b => pair_per _ _ (nat_and_sign_of_int a) (nat_and_sign_of_int b)

All this would be proven symmetric and transitive, and also reflexive if they are.

In addition to the important question of what goes in the prelude, another question is: "What goes in the library?"

Is there a list somewhere of the functionality we will include?

• bool/numbers
• list/option/sums/products
• string, ascii
• finite sets
• finite maps
• vector, hlist, member, fin

How about concepts (e.g. common type classes from Haskell)?

• functor/applicative/monad
• monoid/semi-group
• lens
• classes for maps, sets, etc
• decidable equality

I imagine that some of the things that I've listed here should be split into other libraries (luckily with opam/nix it should be easy). Other pieces should be in here. So, where will we draw the line?

Personally, I lean a bit towards a collection of repositories that focus on individual concepts but standardized in some way, though small repos have their own downsides as well

There are a lot of finite map and finite set implementations out there and I think it would be good to discuss what the shape of these types should be in stdlib2. Off the top of my head there are implementations in the stdlib, coq-containers, coq-stdpp and probably others I am not aware of or familiar with. Each of these implementations have different characteristics. Here is an incomplete list of some of them:

stdlib

• Finite maps and finite sets based on modules (no inference)
• Finite sets (but not maps) based on typeclasses
• Different implementations:
  • Ordered and unordered lists of key-value pairs
  • AVL trees

coq-containers

• Based on typeclasses
• Requires a total decidable order on keys, and exhibits many instances:
  • Z, nat, positive, bool, unit
  • Pairs and sums of ordered types
  • Lists of ordered types
  • Finite maps and finite sets of ordered types
• Includes plugin to automatically derive orders for user types which is very convenient
• No extensionality (even for implementations with canonical representations)
• Different implementations:
  • Ordered lists of key-value pairs
  • AVL trees

stdpp

• Based on typeclasses
• Only few types of keys allowed: Z, nat, positive, string (and from a cursory glance seems a little difficult to implement maps with other key types) Maps implemented for any countable type of keys (see comments below)
• Sets implemented in terms of maps
• Extensionality for its maps

If I have gotten anything wrong here then feel free to correct or in general just expand on it.

Personally, as a user coming from object oriented languages, I think that coq-containers was the easiest to use in terms of just working like I would expect. For instance, declaring a map with type Map[A, B] just worked out of the box for even complicated A's. In stdpp it appears you need to find a concrete implementation of a map with your key (Zmap, Nmap, etc.) which is much less discoverable (wrong, there is a finite map for any countable type of keys -- see below). I have not used stdlib extensively, but in my attempts it also seemed to suffer from poor discoverability due to the use of modules. Just figuring out how to make a function that takes an stdlib MSet was a task in itself.

This repository is not well known yet, but even among the people that know it, how to contribute and what is expected from them (or what is the plan) is not clear at all.

There should be ASAP a README with a small explanation of what the project is (including a link to coq/coq#7711 and https://github.com/orgs/coq/projects/1). It would probably be a good idea to indicate that there currently is infrastructure work going on such as coq/coq#186.

There should also be a CONTRIBUTING guide even if it is really small at the beginning explaining how people can contribute as of today (by opening issues) and explaining that contributions in the form of Coq code will be welcome in a later phase of the project.

I would like to mention an approach which has been useful in uniformizing the layout of files of the standard library and giving a feeling of homogeneity of style, which is the use of a standardized pretty-printer (aka "beautifier").

I've produced a short and much elementary proof of P=NP (without an efficient algorithm presented). I sent it to a reputable CS journal and insofar there were no errors noticed by the editor. (However, I myself found several errors, that are already corrected in the attached file.)

You should check my proof.

p=np-merkle.pdf

Here is some lore about abstraction and modularity mechanisms in Coq and Lean which I think may be relevant for setting conventions for stdlib2:

• example of where module functors are not good for defining the algebraic hierarchy: the final theorem of a development quantifies over n and talks about the ring of integers mod n, instantiating a library of lemmas about arbitrary rings with that n. If that library is implemented as a module functor, the top-level theorem of the development would also need to be a module functor. Then every other development would need to be defined using functors when calling that theorem with arguments that in turn depend on universally quantified variables. I hear people find this very inconvenient, and there is also the current limitation that a module functor cannot be instantiated by an Ltac script.

• https://github.com/leanprover/lean/wiki/Refactoring-structures highlights downsides of "bundled" and "unbundled" patters of using typeclasses as modules:

generally, it is relevant in any domain where we have transformations, an identity transformation, a composition operator, and an inverse. It feels weird to tell users that whenever they have a group in their application, they MUST use the constants mul or add. Otherwise, the automation will not work. The list.append and list.nil example emphasizes this issue. It is a monoid, a left_cancel_semigroup, and a right_cancel_semigroup. We want users to be able to use the algebraic normalizer without forcing them to use add for list.append and zero for list.nil.

The unbundled approach doesn't work with the simplifier as is. The problem is that the lemmas are hard to index. For example: the left hand side of the assoc lemma is (?op (?op ?a ?b) ?c)
where ?op, ?a, ?b and ?c are metavariables (aka matching variables). We don't have a single constant that we can use to filter the locations where this lemma can be applied.

mit-plv/fiat-crypto#233 and the RecordImport feature request coq/coq#7808 are my half-baked attempt of working around this dilemma...
For an example of emulating this using current Coq features, see mit-plv/bedrock2#14 (later discussion on that issue comes back to other modularity mechanisms which may be also relevant).

Note that the question of modularity interacts with what kind of unification is expected of tactics. For example, if it is expected that code will contain both @ring_add Zring and Z.add, we will likely want tactics to treat them interchangably, and for performance reasons this will likely need to use some restricted form of unification ("alias unification" using Tarjan's algorithm).

User developments often use stdlib functions with inputs whose natural equivalence relation does not coincide with Logc.eq: most importantly functions, but also Q, non-hprop sigma types, etc. Then they eventually need the fact that (forall x y, x = y -> f x = g y) -> stdlibfunc f a = stdlibfunc g a. stdlib should make lemmas of this form easily accessible, ideally in a systematic auto-generated form.

First of all, I'm excited about this effort. As a new Coq user, it can be very difficult to figure out which aspects of the standard library reflect current best practices, and which are in an old style.

I think this project will be most successful if it is explicit about when it's releases will start being backwards compatible with themselves (v1.0, basically). When this happens, it would be good to have a thorough, long term plan for implementing breaking changes (how to warn users, how long things stay deprecated, etc).

Note that I'm referring to internal backwards compatibility, not compatibility with, say, Coq's current stdlib.

This discussion is bound to happen at some point, so we might just as well start a new thread now, with this quote from @HuStmpHrrr on Coq-Club:

I am not sure if stdlib2 plans to make things primarily in Type and make use of sProp whenever necessary. If that's the case, it would make the future much brighter.

I'm not really expecting any answer now, just recording this for later.

The prelude is the set of definitions / plugins loaded as soon as Coq starts. I would like to keep it minimal.

I imagine we would like to get at least the -> notation, and maybe a definition of equality.

Should it load ltac? @ppedrot, is Ltac2 meant to become independent of Ltac1? If so, can you say when that is expected to happen?

As part of the stdlib2 project, I plan to take/adapt code from at least:

• the current stdlib (LGPL 2.1)
• the mathcomp library (Cecill B)
• stdpp (BSD)
• coq-ext-lib (FreeBSD)

So I'll probably stick with LGPL 2.1, but if there's a reason to do otherwise, please let me know.

Many people are eager to contribute to the stdlib2 project so it would be very useful if a more specific roadmap could be shared and regularly updated, and it should ideally include dates of expected milestones. In particular, we need to ensure that the preliminary phases do not last too long so that the collaborative phases can start (even if only for experimenting). In any case, more transparency on what's being done would help people hold their breath.