Hints: hint simplify
The hint simplify commands manage user reduction rules used by
simplify, cbv, and tactics that rely on the same simplification
machinery.
Hints can be declared globally in a theory, selected through named databases, and adjusted locally inside a proof.
Global declarations
Global declarations add lemmas to a simplification database.
Syntax
hint simplify {lemma}+ .
Add the listed lemmas to the default simplification database.
Syntax
hint simplify in {db} : {lemma}+ .
Add the listed lemmas to the named database {db}.
These commands are theory-level declarations: once imported, the corresponding rules are available to simplification.
The hint clause
simplify and cbv accept a single hint clause that controls which
user-reduction rules are used. The clause is introduced by the hint
keyword and is built from an unsigned base database selection followed by
any number of signed items:
Syntax
simplify hint {db}* {item}*
where each {item} is one of:
+ {db}/- {db}— activate / deactivate a database;+[ {op}+ ]/-[ {op}+ ]— head filter: keep only / drop rules headed by the listed operators (at most one filter per clause);{ {lemma}+ }— add lemmas to the default database for this call.
The delimiter disambiguates an item: a bare name is a database, […]
holds operators, {…} holds lemmas. 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 is accepted by cbv.
The database part of a clause is either an unsigned selection or
signed deltas, never both (mixing them is redundant and rejected). An
unsigned list hint d1 d2 replaces the consulted databases with
exactly {d1, d2}. Signed + {db} / - {db} instead modify the current
set (the proof-local default, else the active set): simplify hint +d2
adds d2 to it, simplify hint -d3 removes d3.
A head filter performs full simplification (like a bare simplify) with
user reduction restricted to the selected operators.
The hint clause is independent of the reduction arguments that
simplify and cbv already accept: a bare simplify performs full
simplification, simplify delta additionally unfolds all definitions,
simplify f g unfolds the operators f and g, and a keyword-less list
such as beta zeta performs only the named reductions. A hint clause
may follow any of these (for example simplify delta hint +[f]).
Proof-local commands
Inside a proof, the simplify configuration can be changed without
modifying the theory-level declarations. The hint command takes the
same clause as the simplify/cbv tactics, and each kind of item has a
persistent effect on the proof state:
Syntax
hint {db}* {item}* .
+ {db}/- {db}— activate / deactivate a database (for later baresimplify/cbv);{ {lemma}+ }— add lemmas to the default database;an unsigned database list
{db}+— set the proof-local default databases used by latersimplify/cbvcalls;+[ {op}+ ]/-[ {op}+ ]— set the proof-local default head filter.
As in the tactic clause, the database part is either an unsigned
selection or signed +/- deltas, never both.
Syntax
hint clear {db}? .
Clear the local lemma additions: for the default database when {db} is
omitted, or for the named database {db}. Note that hint clear default
is reserved for the form below, so a database named default cannot be
cleared this way.
Syntax
hint clear default .
Clear the proof-local default database and head filter.
These proof-local changes are part of the proof state and therefore
follow the usual subgoal branching behavior. Explicit arguments on
simplify/cbv take precedence over the proof-local defaults.
Scoped application
A hint command can be used as a scoped wrapper around a tactic, with the
same clause syntax.
Syntax
with hint {clause} ( {tactic} )
For example:
with hint +ring (simplify).
with hint {fooE} (rewrite foo /=).
with hint ring (cbv).
The wrapped tactic runs with the modified hint configuration, but the subgoals produced afterwards are restored to the original configuration.
Example
[easycrypt failed]