fix(simplify): honour the proof-local head filter on every path

src/ecHiGoal.ml

@@ -434,8 +434,11 @@ module LowRewrite = struct
             then Some (ptc, `Bool, (ax, f_true))
             else None
           else None
-        and pt3 = omap base
-          (EcReduction.h_red_opt EcReduction.full_red hyps ax)
+        and pt3 =
+          let ri =
+            { EcReduction.full_red with
+                EcReduction.user_local = pt.PT.ptev_env.PT.pte_lc } in
+          omap base (EcReduction.h_red_opt ri hyps ax)
         in pt1 @ (otolist pt2) @ (odfl [] pt3)) in
 
         let rec doit reduce =
@@ -862,7 +865,8 @@ let process_delta ?(rigid = false) ?target ((s :rwside), o, p) tc =
   in
 
   let ri = { EcReduction.full_red with
-               delta_p = (fun p -> if Some p = dp then `Force else `IfTransparent)} in
+               delta_p = (fun p -> if Some p = dp then `Force else `IfTransparent);
+               user_local = FApi.tc1_simplify_context tc; } in
   let na = List.length args in
 
   match s with

src/ecLowGoal.ml

@@ -421,7 +421,9 @@ let rec t_lazy_match ?(reduce = `Full) ?(texn = fun _ -> raise InvalidGoalShape)
     let strategy =
       match reduce with
       | `None    -> raise InvalidGoalShape
-      | `Full    -> EcReduction.full_red
+      | `Full    ->
+          { EcReduction.full_red with
+              user_local = FApi.tc1_simplify_context tc }
       | `NoDelta -> EcReduction.nodelta in
     FApi.t_seq (FApi.t_or (t_hred_with_info strategy) texn) (t_lazy_match ~reduce tx) tc
 
@@ -567,7 +569,8 @@ let t_intros_x (ids : (ident  option) mloc list) (tc : tcenv1) =
         intro1 ((hyps, concl), Fsubst.f_subst_id) id
 
     | _ ->
-        match h_red_opt full_red hyps concl with
+        let ri = { full_red with user_local = FApi.tc1_simplify_context tc } in
+        match h_red_opt ri hyps concl with
         | None       -> LowIntro.tc_no_product !!tc ?loc:(tg_tag id) ()
         | Some concl -> intro1 ((hyps, concl), sbt) id
   in
@@ -1187,7 +1190,9 @@ let t_elim_r ?(reduce = (`Full : lazyred)) txs tc =
           let strategy =
             match reduce with
             | `None    -> raise InvalidGoalShape
-            | `Full    -> EcReduction.full_red
+            | `Full    ->
+                { EcReduction.full_red with
+                    user_local = FApi.tc1_simplify_context tc }
             | `NoDelta -> EcReduction.nodelta in
 
             match h_red_opt strategy (FApi.tc1_hyps tc) f1 with

src/ecReduction.ml

@@ -769,7 +769,17 @@ let reduce_user_gen simplify ri env hyps f =
     | Fproj (_, i) -> `Proj i
     | _ -> raise nohead in
 
-  begin match ri.user_hd, p with
+  (* An explicit use-site head filter wins; otherwise the proof-local
+   * default one (set by [hint +[..]] / [hint -[..]]) applies. Resolving
+   * the default here, and not only in the [simplify]/[cbv] front-ends,
+   * makes every reduction path that threads [user_local] honour it:
+   * [/=], [done], [progress], rewriting, conversion checks, ... *)
+  let user_hd =
+    match ri.user_hd with
+    | Some _ as hd -> hd
+    | None -> EcEnv.SimplifyContext.default_hd ri.user_local in
+
+  begin match user_hd, p with
   | Some (`Include hs), `Path p when not (EcPath.Sp.mem p hs) -> raise nohead
   | Some (`Exclude hs), `Path p when EcPath.Sp.mem p hs -> raise nohead
   | _ -> ()

tests/hint_head_filter_default.ec

@@ -0,0 +1,97 @@
+require import AllCore.
+
+(* A proof-local default head filter ([hint -[f]] / [hint +[f]]) must be
+   honoured by every simplification path, not only by an explicit
+   [simplify]/[cbv]: [/=], [//], [done], [progress], [trivial], [auto]
+   and the conversion checks behind [apply]/[exact]. [f] and [g] are
+   abstract, so only the user-reduction rules below can reduce them: a
+   goal closes only when a rule actually fires, which makes [fail (...)]
+   and "the goal is still there afterwards" faithful witnesses. *)
+
+op f : int -> int.
+op g : int -> int.
+
+axiom fE (x : int) : f x = x + 1.
+axiom gE (x : int) : g x = x + 2.
+
+hint simplify fE.
+hint simplify gE.
+
+(* --- Sanity: without a filter, every path fires the rules ----------- *)
+
+lemma nofilter_done     : f 0 = 1. proof. done. qed.
+lemma nofilter_slash    : f 0 = 1. proof. by rewrite /=. qed.
+lemma nofilter_dslash   : f 0 = 1. proof. by rewrite //. qed.
+lemma nofilter_progress : f 0 = 1. proof. by progress. qed.
+lemma nofilter_trivial  : f 0 = 1. proof. by trivial. qed.
+lemma nofilter_auto     : f 0 = 1. proof. by auto. qed.
+lemma nofilter_apply    : f 0 = 1. proof. apply eq_refl. qed.
+lemma nofilter_exact    : f 0 = 1. proof. exact eq_refl. qed.
+
+(* --- Exclude filter: the [f]-headed rule is disabled ----------------- *)
+
+(* The explicit tactics already honoured the default filter. *)
+lemma exclude_simplify : f 0 = 1.
+proof. hint -[f]. simplify. rewrite fE. done. qed.
+
+lemma exclude_cbv : f 0 = 1.
+proof. hint -[f]. cbv. rewrite fE. done. qed.
+
+(* [/=] is a bare [simplify]: it must not rewrite [f 0]. *)
+lemma exclude_slash : f 0 = 1.
+proof. hint -[f]. rewrite /=. rewrite fE. done. qed.
+
+(* [done] must not close the goal. *)
+lemma exclude_done : f 0 = 1.
+proof. hint -[f]. fail done. rewrite fE. done. qed.
+
+(* ... nor its scoped form. *)
+lemma exclude_with_done : f 0 = 1.
+proof. fail with hint -[f] (done). done. qed.
+
+(* The non-failing closers must leave the goal open: if any of them had
+   closed it, the following [rewrite fE] would have no goal to act on. *)
+lemma exclude_dslash : f 0 = 1.
+proof. hint -[f]. rewrite //. rewrite fE. done. qed.
+
+lemma exclude_move : f 0 = 1.
+proof. hint -[f]. move => //. rewrite fE. done. qed.
+
+lemma exclude_progress : f 0 = 1.
+proof. hint -[f]. progress. rewrite fE. done. qed.
+
+lemma exclude_trivial : f 0 = 1.
+proof. hint -[f]. trivial. rewrite fE. done. qed.
+
+lemma exclude_auto : f 0 = 1.
+proof. hint -[f]. auto. rewrite fE. done. qed.
+
+(* The conversion check of [apply]/[exact] sees the filter too. *)
+lemma exclude_apply : f 0 = 1.
+proof. hint -[f]. fail (apply eq_refl). rewrite fE. done. qed.
+
+lemma exclude_exact : f 0 = 1.
+proof. hint -[f]. fail (exact eq_refl). rewrite fE. done. qed.
+
+(* The other rules are unaffected. *)
+lemma exclude_other : g 0 = 2.
+proof. hint -[f]. done. qed.
+
+(* The filter is undone by [hint clear default]. *)
+lemma exclude_cleared : f 0 = 1.
+proof. hint -[f]. fail done. hint clear default. done. qed.
+
+(* --- Include filter: only the [g]-headed rule fires ------------------ *)
+
+lemma include_done : f 0 = 1.
+proof. hint +[g]. fail done. rewrite fE. done. qed.
+
+lemma include_slash : f 0 = 1.
+proof. hint +[g]. rewrite /=. rewrite fE. done. qed.
+
+lemma include_other : g 0 = 2.
+proof. hint +[g]. done. qed.
+
+(* A filter set in one lemma does not leak into the next. *)
+lemma no_leak : f 0 = 1.
+proof. done. qed.