Add named and local simplify hint databases

[strub]

Introduce named simplify databases, a head-symbol filter, and proof-local
control over which user-reduction rules simplify/cbv apply. These are
all expressed through one hint clause, used in three places: after a
simplify/cbv tactic, as a standalone hint command, and in the
with hint … (…) scoped wrapper.

Theory-level declarations register lemmas into a database (unchanged):

hint simplify {lemma}+ .             (* default database *)
hint simplify in {db} : {lemma}+ .   (* named database   *)

On the simplify/cbv tactics, a hint clause chooses the rules for
that call. The clause is hint followed by items disambiguated by their
delimiter -- a bare name is a database, […] holds operators, {…} holds
lemmas:

simplify hint d1 d2                  (* consult exactly d1, d2     *)
simplify hint +d1 -d2                (* +/- a db on the active set *)
simplify hint +[f g]                 (* restrict user rules to f,g *)
simplify hint {L}                    (* add lemma L for this call  *)
cbv hint d1 {M}

The database part is either an unsigned selection (replace) or signed +/-
deltas (on the active set), never both; at most one head filter is
allowed; and lemma sets {…} are add-only -- a clause never removes
lemmas from a database (use the head filter to restrict which rules
apply).

The same clause, written as a standalone command, changes the proof state
persistently:

hint +d1 -d2 .                       (* activate / deactivate DBs  *)
hint {L} .                           (* add local lemmas           *)
hint d1 d2 .                         (* set default databases      *)
hint +[f g] .                        (* set default head filter    *)
hint clear [ {db} ] .                (* clear local additions      *)
hint clear default .                 (* clear proof-local defaults *)

and as a scoped wrapper, in effect only for the wrapped tactic and
restored on the resulting subgoals:

with hint {clause} ( {tactic} ) .

Implementation: the proof-local simplify context lives in a new
EcSimplifyContext module (extracted from EcEnv); it is threaded through
proof goals so the active DB set, added lemmas, default database, and
head filter propagate across subgoals and are consulted by simplify and
cbv. Reduction storage and simplify-hint printing support named
databases and head filtering.

Document the syntax in doc/tactics/hint-simplify.rst and add regression
tests (tests/hint_simplify_db.ec, tests/local_hint_simplify.ec,
tests/simplify_head_filter.ec).

[Gustavo2622]

Partially answers #918 by wrapping exponent simplification lemmas.

[bgregoir]

General comment:
I think the syntax is a little bit to verbose.
More importantly, if I have well understood only one database can be selected. I don't understand this restriction.

[strub]

General comment:
I think the syntax is a little bit to verbose.
More importantly, if I have well understood only one database can be selected. I don't understand this restriction.

Several databases should be selectable. I'll check and fix if needed.

For the syntax, I agree. If you have a better proposition, I take it.

[bgregoir]

selection of database and symbol :
hint simplify (+|-)({ sym+})? db*.
I think the syntax for adding lemmas to data base is ok.

[bgregoir]

Also it will be nice to be able to provide a lemma locally for simplification.
something like
with hint simplify toto (simplify)

[strub]

Following up on the syntax suggestions:

The use-site/command syntax has been reworked into a single unified hint clause shared by the simplify/cbv tactics, the standalone hint command, and the with hint … (…) wrapper. Within a clause, items are disambiguated by delimiter:

• +d / -d — activate / deactivate a database;
• +[f g] / -[f g] — head filter (operators);
• +{L} — add lemmas (default DB);
• a bare unsigned list d1 d2 — select (replace) the databases.

So your two points are covered:

• Selecting databases + symbols together (hint simplify (+|-)({sym}+)? db*): e.g. simplify hint d1 d2 +[f g], and multiple databases can now be selected/active at once (the single-DB restriction is gone).
• Providing a lemma locally: with hint +{toto} (simplify) (and hint +{toto}. as a command). I kept the explicit + (vs your with hint simplify toto) so add/remove are symmetric and unambiguous from database selection.

Full grammar is documented in doc/tactics/hint-simplify.rst.