Refactor databases

[jim-portegies]

Set up the databases in a more flexible way, that also separates theory from tactics better.

In particular:

• Every database is populated in its own file.
• The global database lists are now lists of names of the databases, rather than lists of the WaterproofDatabase type. This is useful because then outside users do not necessarily have to change the waterproof code to use a new database in the automation.
• The "first attempt" part of the waterprove tactic is now based on a global database collection, allowing for separation between theory and tactics here.
• A new database waterproof_core takes care of basics that we want the waterproof library to (almost) always use.

[jim-portegies]

Importing now works according to database configuration modules. Here is an example.

Require Import Waterproof.populate_database.
Require Import Waterproof.load.

Module DBExample <: db_config.
Module preload_module := wp_all.
Ltac2 append_databases := true.
Ltac2 global_databases () := [ @arith; @zarith; @real; @wp_core; @wp_classical_logic; @wp_constructive_logic; @wp_integers; @wp_reals; @wp_subsets].
Ltac2 decidability_databases () := [ @nocore; @wp_decidability_nat; @wp_decidability_reals].
Ltac2 negation_databases () := [ @nocore; @wp_negation_nat; @wp_negation_int; @wp_negation_reals].
Ltac2 first_attempt_databases () := [ @core; @wp_subsets; @wp_classical_logic].
End DBExample.

(** Importing now works as follows: *)
Module Import db_DBExample := databases(DBExample).

In the above code, wp_all is a database preload module defined in populate_databases.v. One can define custom preload modules too:

Module my_preload_module <: preload_module.
(** Add lemmas to databases here. *)
End my_preload_module.