Add named and local simplify hint databases by strub · Pull Request #954 · EasyCrypt/easycrypt

strub · 2026-03-25T18:40:57Z

Introduce named simplify databases, proof-local control over the active
DBs and lemmas, head-symbol filtering, and proof-local defaults for the
simplify/cbv simplification machinery.

Global declarations:

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

Selecting a database and filtering by head symbol on simplify/cbv:

simplify hint {db}                   (* use named database         *)
cbv      hint {db}
simplify with {sym}+                 (* only rules headed by sym   *)
simplify with - {sym}+               (* all rules except those     *)
simplify with {sym}+ hint {db}       (* filter + named database    *)

Proof-local modifications of the active configuration:

hint +db simplify {db}+ .            (* activate named DBs         *)
hint -db simplify {db}+ .            (* deactivate named DBs       *)
hint +simplify [in {db}] {lemma}+ .  (* add lemmas locally         *)
hint -simplify [in {db}] {lemma}+ .  (* remove lemmas locally      *)
hint clear simplify [in {db}] .      (* clear local add/remove     *)

Proof-local defaults consulted by later bare simplify/cbv calls:

hint simplify hint {db} .            (* default database           *)
hint simplify with [-] {sym}+ .      (* default head filter        *)
hint simplify clear .                (* clear local defaults       *)

Scoped application around a tactic, restored on the resulting subgoals:

with hint {command} ( {tactic} ) .

Thread the local simplify context through proof goals so the active DB
set, lemma overrides, default database, and head filter propagate across
subgoals and are consulted by simplify and cbv. Update simplify-hint
printing and reduction storage to support named databases and head
filtering.

Document all syntax forms 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 · 2026-03-25T23:23:16Z

Partially answers #918 by wrapping exponent simplification lemmas.

Introduce named simplify databases, proof-local control over the active DBs and lemmas, head-symbol filtering, and proof-local defaults for the `simplify`/`cbv` simplification machinery. Global declarations: hint simplify {lemma}+ . (* default database *) hint simplify in {db} : {lemma}+ . (* named database *) Selecting a database and filtering by head symbol on simplify/cbv: simplify hint {db} (* use named database *) cbv hint {db} simplify with {sym}+ (* only rules headed by sym *) simplify with - {sym}+ (* all rules except those *) simplify with {sym}+ hint {db} (* filter + named database *) Proof-local modifications of the active configuration: hint +db simplify {db}+ . (* activate named DBs *) hint -db simplify {db}+ . (* deactivate named DBs *) hint +simplify [in {db}] {lemma}+ . (* add lemmas locally *) hint -simplify [in {db}] {lemma}+ . (* remove lemmas locally *) hint clear simplify [in {db}] . (* clear local add/remove *) Proof-local defaults consulted by later bare simplify/cbv calls: hint simplify hint {db} . (* default database *) hint simplify with [-] {sym}+ . (* default head filter *) hint simplify clear . (* clear local defaults *) Scoped application around a tactic, restored on the resulting subgoals: with hint {command} ( {tactic} ) . Thread the local simplify context through proof goals so the active DB set, lemma overrides, default database, and head filter propagate across subgoals and are consulted by `simplify` and `cbv`. Update simplify-hint printing and reduction storage to support named databases and head filtering. Document all syntax forms 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).

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.

bgregoir · 2026-06-02T07:56:10Z

+  | EcTheory.Th_reduction { red_base; _ } ->
      (* FIXME: section we should add the lemma in the reduction *)
-      Format.fprintf fmt "hint simplify."
+      begin match red_base with


I think the printing info is partial here. Lemmas added or removed from the database are not printed

bgregoir · 2026-06-02T07:57:12Z


-  | EcTheory.Th_reduction _ ->
+  | EcTheory.Th_reduction { red_base; _ } ->
      (* FIXME: section we should add the lemma in the reduction *)


Maybe this comment explain what should be done

bgregoir · 2026-06-02T07:59:32Z

-  val get  : topsym -> env -> rule list
+  type base = symbol
+
+  val dname : symbol


dname is for "default name" ?

bgregoir · 2026-06-02T08:03:18Z

-  val add1 : path * rule_option * rule option -> env -> env
-  val add  : ?import:bool -> (path * rule_option * rule option) list -> env -> env
-  val get  : topsym -> env -> rule list
+  type base = symbol


Why a database name is a symbol and not a path?
I don't claim that it should be, just asking the question.

bgregoir · 2026-06-02T08:29:05Z

+
+(* Name of the default simplify database. Must agree with
+   [EcEnv.Reduction.dname]. *)
+let dname : symbol = ""


Why dname is defined here and also in ecEnv

bgregoir · 2026-06-02T08:31:31Z

+(* -------------------------------------------------------------------- *)
+let normbase (base : symbol option) : symbol =
+  match base with
+  | Some "default" | None -> dname


Why do we have Some "default" ? I think either option should be remove or "default" should

bgregoir · 2026-06-02T08:33:45Z

+(* -------------------------------------------------------------------- *)
+type simplify_context = {
+  ls_active     : Ssym.t;
+  ls_default_db : symbol option option;


Some comment will be welcome on the meaning of symbol option option...

bgregoir · 2026-06-02T08:35:33Z

+  : simplify_context
+=
+  let hd = hd |> omap (fun (mode, paths) ->
+    let paths = List.fold_left (fun acc p -> Sp.add p acc) Sp.empty paths in


There is no Sp.of_list function ?

bgregoir · 2026-06-02T13:01:16Z

  logic   : rlogic_info;       (* perform logical simplification *)
  modpath : bool;              (* reduce module path *)
  user    : bool;              (* reduce user defined rules *)
+  user_db : EcSymbols.symbol option; (* user reduction database *)


Does it means that only one user reduction database can be added?

Gustavo2622 · 2026-06-02T16:33:58Z

+  box (wrap_default x) = box (x + 1).
+proof.
+  hint -db simplify default.
+  simplify.


Should make sure it is disabling, maybe add "fail trivial" after first simplify?

Gustavo2622 · 2026-06-02T16:34:23Z

+proof.
+  hint +simplify wrap_localE.
+  hint -simplify wrap_localE.
+  simplify.


Same as above, should make sure that simplify is failing

Gustavo2622 · 2026-06-02T16:36:18Z

+  trivial.
+qed.
+
+lemma cbv_named_with_exclude (x : int) :


Does this actually test whether wrap1 hint is excluded?

strub · 2026-06-02T16:56:20Z

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.

strub self-assigned this Mar 25, 2026

strub added enhancement tactics labels Mar 25, 2026

strub force-pushed the hint-simplify-db branch from b23f632 to fab0ba7 Compare March 25, 2026 18:43

strub force-pushed the hint-simplify-db branch 6 times, most recently from 3ae8c0e to 38c60c2 Compare June 2, 2026 06:22

strub force-pushed the hint-simplify-db branch from 38c60c2 to 0fbdba0 Compare June 2, 2026 06:25

bgregoir reviewed Jun 2, 2026

View reviewed changes

Gustavo2622 reviewed Jun 2, 2026

View reviewed changes

Gustavo2622 approved these changes Jun 2, 2026

View reviewed changes

Conversation

strub commented Mar 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Gustavo2622 commented Mar 25, 2026

Uh oh!

bgregoir left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

strub commented Jun 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

strub commented Mar 25, 2026 •

edited

Loading