Actually name the unfold actions

Author: jim-portegies

src/g_waterproof.mlg

@@ -209,43 +209,43 @@ END
 }
 
 VERNAC COMMAND EXTEND RegisterUnfold CLASSIFIED AS SIDEFF
-  | [ "Waterproof" "Register" "Unfold" ne_string_list(s) ref(id) ] => { Vernacextend.(VtSideff ([], VtNow)) }
+  | [ "Waterproof" "Register" "Unfold" ne_string_list(s) ref(id) ";" string(name)] => { Vernacextend.(VtSideff ([], VtNow)) }
     SYNTERP AS notation_data_and_ref
     {
       let located_id = Nametab.locate id in
-      (register_unfold s (Nametab.locate id), located_id)
+      (register_unfold s (Nametab.locate id), located_id, name)
     } ->
     {
-      let (notation_data, id) = notation_data_and_ref in
+      let (notation_data, id, name) = notation_data_and_ref in
       register_notation_interpretation notation_data;
-      register_unfold_entry id Unfold_entry
+      register_unfold_entry id (Unfold_entry name)
     }
 END
 
 VERNAC COMMAND EXTEND RegisterUnfoldRewrite CLASSIFIED AS SIDEFF
-  | [ "Waterproof" "Register" "Unfold" "Rewrite" ne_string_list(s) ref(id) ";" constr(e)] => { Vernacextend.(VtSideff ([], VtNow)) }
+  | [ "Waterproof" "Register" "Unfold" "Rewrite" ne_string_list(s) ref(id) ";" string(name) ";" constr(e)] => { Vernacextend.(VtSideff ([], VtNow)) }
     SYNTERP AS notation_data_and_ref_and_constr_expr
     {
       let located_id = Nametab.locate id in
-      (register_unfold s located_id, located_id, e)
+      (register_unfold s located_id, located_id, name, e)
     } ->
     {
-      let (notation_data, id, e) = notation_data_and_ref_and_constr_expr in
+      let (notation_data, id, name, e) = notation_data_and_ref_and_constr_expr in
       register_notation_interpretation notation_data;
-      register_unfold_entry id (Rewrite_entry e)
+      register_unfold_entry id (Rewrite_entry (name, e))
     }
 END
 
 VERNAC COMMAND EXTEND RegisterUnfoldApply CLASSIFIED AS SIDEFF
-  | [ "Waterproof" "Register" "Unfold" "Apply" ne_string_list(s) ref(id) ";" constr(e)] => { Vernacextend.(VtSideff ([], VtNow)) }
+  | [ "Waterproof" "Register" "Unfold" "Apply" ne_string_list(s) ref(id) ";" string(name) ";"constr(e)] => { Vernacextend.(VtSideff ([], VtNow)) }
     SYNTERP AS notation_data_and_ref_and_constr_expr
     {
       let located_id = Nametab.locate id in
-      (register_unfold s located_id, located_id, e)
+      (register_unfold s located_id, located_id, name, e)
     } ->
     {
-      let (notation_data, id, e) = notation_data_and_ref_and_constr_expr in
+      let (notation_data, id, name, e) = notation_data_and_ref_and_constr_expr in
       register_notation_interpretation notation_data;
-      register_unfold_entry id (Apply_entry e)
+      register_unfold_entry id (Apply_entry (name, e))
     }
 END

src/unfold_framework.ml

@@ -33,11 +33,11 @@ open Names
 
 module StringMap = Map.Make(String)
 
-(** A type to represent the different unfold actions, and the data they need. *)
+(** A type to represent the different unfold actions, a name for the action, and the data they need. *)
 type unfold_action =
-  | Unfold of GlobRef.t
-  | Apply of EConstr.constr
-  | Rewrite of EConstr.constr
+  | Unfold of string * GlobRef.t
+  | Apply of string * EConstr.constr
+  | Rewrite of string * EConstr.constr
 
 (** The map that associate notation strings to references *)
   let wp_unfold_map = Summary.ref ~name:"wp_unfold_map" StringMap.empty
@@ -105,9 +105,9 @@ let register_unfold (toks : string list) (id : GlobRef.t) : notation_interpretat
     to an unfold action.
 *)
 type unfold_entry =
-  | Unfold_entry
-  | Apply_entry of Constrexpr.constr_expr
-  | Rewrite_entry of Constrexpr.constr_expr
+  | Unfold_entry of string
+  | Apply_entry of string * Constrexpr.constr_expr
+  | Rewrite_entry of string * Constrexpr.constr_expr
 
 (** Registers a new entry in the table that stores a list of
     unfold actions associated to a reference.
@@ -126,11 +126,11 @@ let register_unfold_entry (id : GlobRef.t) (ue : unfold_entry) : unit =
     let (constr_e, _) = Constrintern.interp_constr env sigma e in
     constr_e in
   match ue with
-  | Unfold_entry -> add_to_unfold_tbl id (Unfold id)
-  | Apply_entry e ->
-      add_to_unfold_tbl id (Apply (f e))
-  | Rewrite_entry e ->
-      add_to_unfold_tbl id (Rewrite (f e))
+  | Unfold_entry s -> add_to_unfold_tbl id (Unfold (s,  id))
+  | Apply_entry (s, e) ->
+      add_to_unfold_tbl id (Apply (s, f e))
+  | Rewrite_entry (s, e) ->
+      add_to_unfold_tbl id (Rewrite (s, f e))
 
 let get_all_references () : GlobRef.t list =
   let lst = !wp_unfold_tbl |> Hashtbl.to_seq_keys |> List.of_seq in

src/unfold_framework.mli

@@ -33,17 +33,17 @@ introduced notations, and the global reference they are associated with
 
 (** A type to represent the different unfold actions, and the data they need. *)
 type unfold_action =
-  | Unfold of GlobRef.t
-  | Apply of EConstr.constr
-  | Rewrite of EConstr.constr
+  | Unfold of string * GlobRef.t
+  | Apply of string * EConstr.constr
+  | Rewrite of string * EConstr.constr
 
 (** A type that represents the datastructure that can be added
     to the unfold table. When it is added, it will be converted
     to an unfold action. *)
 type unfold_entry =
-  | Unfold_entry
-  | Apply_entry of Constrexpr.constr_expr
-  | Rewrite_entry of Constrexpr.constr_expr
+  | Unfold_entry of string
+  | Apply_entry of string * Constrexpr.constr_expr
+  | Rewrite_entry of string * Constrexpr.constr_expr
 
 module StringMap : Map.S with type key = string
 

src/wp_ffi.ml

@@ -173,14 +173,14 @@ let feedback_lvl_from_valexpr (value : valexpr): Feedback.level = match value wi
 
 let of_unfold_action =
   function
-  | Unfold gr -> of_block (0, [|of_reference gr|])
-  | Apply c -> of_block (1, [|of_constr c|])
-  | Rewrite c -> of_block(2, [|of_constr c|])
+  | Unfold (s, gr) -> of_block (0, [|of_string s; of_reference gr|])
+  | Apply (s, c) -> of_block (1, [|of_string s; of_constr c|])
+  | Rewrite (s, c) -> of_block(2, [|of_string s; of_constr c|])
 
 let to_unfold_action = let open Ltac2_plugin.Tac2val in function
-  | ValBlk (0, [|gr|]) -> Unfold (to_reference gr)
-  | ValBlk (1, [|c|]) -> Apply (to_constr c)
-  | ValBlk (2, [|c|]) -> Rewrite (to_constr c)
+  | ValBlk (0, [|s; gr|]) -> Unfold (to_string s, to_reference gr)
+  | ValBlk (1, [|s; c|]) -> Apply (to_string s, to_constr c)
+  | ValBlk (2, [|s; c|]) -> Rewrite (to_string s, to_constr c)
   | _ -> assert false
 
 let unfold_action_repr = make_repr of_unfold_action to_unfold_action

tests/libs/Analysis/OpenAndClosed.v

@@ -45,7 +45,8 @@ Proof.
   (fun () => Expand the definition of open)
 "Remove this line in the final version of your proof.")
   Info
-["Expanded definition in statements where applicable.";
+["open";
+"Expanded definition in statements where applicable.";
 "Hint, insert: We need to show that (∀ a ∈ A, a is an _interior point_ of A).";
 "Hint, insert: It holds that (∀ a ∈ A, a is an _interior point_ of A)."].
 Abort.

tests/tactics/Unfold.v

@@ -101,7 +101,7 @@ Abort.
 Local Parameter P Q R : Prop.
 Local Parameter HPQ : P <-> Q.
 
-Waterproof Register Unfold Apply "notation" "for" "P" P ; (HPQ).
+Waterproof Register Unfold Apply "notation" "for" "P" P ; "Alternative characterization of P"; (HPQ).
 
 (* Test 8: Use alternative characterization, with concept in conclusion,
 but without having the automation able to prove the alternative
@@ -150,7 +150,8 @@ Proof.
   (fun () => Unfold the definition of notation for P)
 "Remove this line in the final version of your proof.")
   Info
-["Applied alternative characterizations in statements where applicable.";
+["Alternative characterization of P";
+"Applied alternative characterizations in statements where applicable.";
 "Hint, replace with: It suffices to show that Q."].
 It suffices to show that Q.
 Abort.
@@ -165,7 +166,8 @@ Proof.
   (fun () => Unfold the definition of notation for P)
 "Remove this line in the final version of your proof.")
   Info
-["Applied alternative characterizations in statements where applicable.";
+["Alternative characterization of P";
+"Applied alternative characterizations in statements where applicable.";
 "Hint, replace with: It holds that Q."].
 It holds that Q.
 Abort.
@@ -178,7 +180,7 @@ Proof.
 assert_constr_equal (tactic_in_constr constr:(HPR) constr:(P -> Q)) constr:(R -> Q).
 Abort.
 
-Waterproof Register Unfold Rewrite "characterization" "of" "P" P ; HPR.
+Waterproof Register Unfold Rewrite "characterization" "of" "P" P ; "Characterization of P"; HPR.
 
 Local Hint Extern 1 => rewrite HPR : core.
 
@@ -193,8 +195,10 @@ intros.
   (fun () => Unfold the definition of notation for P)
 "Remove this line in the final version of your proof.")
   Info
-["Applied alternative characterizations in statements where applicable.";
+["Characterization of P";
+"Applied alternative characterizations in statements where applicable.";
 "Hint, replace with: It suffices to show that R.";
+"Alternative characterization of P";
 "Applied alternative characterizations in statements where applicable.";
 "Hint, replace with: It suffices to show that Q."].
 It suffices to show that Q.
@@ -223,11 +227,13 @@ assert_feedback_with_strings
   (fun () => Unfold the definition of infimum)
 "Remove this line in the final version of your proof.")
   Info
-["Expanded definition in statements where applicable.";
+["Definition infimum";
+"Expanded definition in statements where applicable.";
 "Hint, insert: We need to show that (3 is a _lower bound_ for A
                       ∧ (∀ l ∈ ℝ, l is a _lower bound_ for A ⇨ l ≤ 3)).";
 "Hint, insert: It holds that (4 is a _lower bound_ for A
                ∧ (∀ l ∈ ℝ, l is a _lower bound_ for A ⇨ l ≤ 4)).";
+"Alternative characterization infimum";
 "Applied alternative characterizations in statements where applicable.";
 "Hint, insert: It suffices to show that (3 is a _lower bound_ for A
                           ∧ (∀ ε > 0, ∃ a ∈ A, a < 3 + ε)).";
@@ -244,11 +250,13 @@ assert_feedback_with_strings
   (fun () => Unfold the definition of supremum)
 "Remove this line in the final version of your proof.")
   Info
-["Expanded definition in statements where applicable.";
+["Definition supremum";
+"Expanded definition in statements where applicable.";
 "Hint, insert: We need to show that (3 is an _upper bound_ for A
                       ∧ (∀ L ∈ ℝ, L is an _upper bound_ for A ⇨ 3 ≤ L)).";
 "Hint, insert: It holds that (4 is an _upper bound_ for A
                ∧ (∀ L ∈ ℝ, L is an _upper bound_ for A ⇨ 4 ≤ L)).";
+"Alternative characterization supremum";
 "Applied alternative characterizations in statements where applicable.";
 "Hint, insert: It suffices to show that (3 is an _upper bound_ for A
                           ∧ (∀ ε > 0, ∃ a ∈ A, 3 - ε < a)).";
@@ -265,15 +273,20 @@ assert_feedback_with_strings
   (fun () => Unfold All)
 "Remove this line in the final version of your proof.")
   Info
-["Expanded definition in statements where applicable.";
+[
+"Definition infimum";
+"Expanded definition in statements where applicable.";
 "Hint, replace with: We need to show that (3 is a _lower bound_ for A
                       ∧ (∀ l ∈ ℝ, l is a _lower bound_ for A ⇨ l ≤ 3)).";
+"Alternative characterization infimum";
 "Applied alternative characterizations in statements where applicable.";
 "Hint, replace with: It suffices to show that (3 is a _lower bound_ for A
                           ∧ (∀ ε > 0, ∃ a ∈ A, a < 3 + ε)).";
+"Definition supremum";
 "Expanded definition in statements where applicable.";
 "Hint, replace with: It holds that (4 is an _upper bound_ for A
                ∧ (∀ L ∈ ℝ, L is an _upper bound_ for A ⇨ 4 ≤ L)).";
+"Alternative characterization supremum";
 "Applied alternative characterizations in statements where applicable.";
 "Hint, replace with: It holds that (4 is an _upper bound_ for A ∧ (∀ ε > 0, ∃ a ∈ A, 4 - ε < a))."].
 Abort.

tests/util/Unfold_framework.v

@@ -824,8 +824,8 @@ Qed.
 
 Local Ltac2 unfold_is_inf (statement : constr) := eval unfold is_inf in $statement.
 
-Waterproof Register Unfold Apply "infimum" is_inf; (alt_char_inf).
-Waterproof Register Unfold "infimum" is_inf.
+Waterproof Register Unfold Apply "infimum" is_inf; "Alternative characterization infimum"; (alt_char_inf).
+Waterproof Register Unfold "infimum" is_inf; "Definition infimum".
 
 Ltac2 Notation "Expand" "the" "definition" "of" "infimum" x(opt(seq("in", constr))) :=
   wp_unfold unfold_is_inf (Some "infimum") false true x;
@@ -842,8 +842,8 @@ Ltac2 Notation "Expand" "the" "definition" "of" "supremum" x(opt(seq("in", const
 Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "supremum" x(opt(seq("in", constr))) :=
   wp_unfold unfold_is_sup (Some "supremum") false true x.
 
-Waterproof Register Unfold Apply "supremum" is_sup; (alt_char_sup).
-Waterproof Register Unfold "supremum" is_sup.
+Waterproof Register Unfold Apply "supremum" is_sup; "Alternative characterization supremum";(alt_char_sup).
+Waterproof Register Unfold "supremum" is_sup; "Definition supremum".
 
 #[export] Hint Resolve bounded_by_upper_bound_propform : wp_reals.
 #[export] Hint Resolve bounded_by_lower_bound_propform : wp_reals.

theories/Libs/Analysis/SupAndInf.v

@@ -28,9 +28,9 @@ Require Import Util.Goals.
 Require Import Util.MessagesToUser.
 
 Ltac2 Type unfold_action := [
-  | Unfold (reference)
-  | Apply (constr)
-  | Rewrite (constr)
+  | Unfold (string, reference)
+  | Apply (string, constr)
+  | Rewrite (string, constr)
 ].
 
 Ltac2 @ external extract_def_ffi : string -> reference option := "rocq-runtime.plugins.coq-waterproof" "extract_def_external".
@@ -128,9 +128,9 @@ Ltac2 tactic_in_constr (equality : constr) (x : constr) : constr :=
 
 Ltac2 unfold_method_for_action (ua : unfold_action) (stmt : constr) : constr :=
   match ua with
-  | Unfold r => eval unfold $r in $stmt
-  | Apply equiv => apply_in_constr equiv stmt
-  | Rewrite eq => tactic_in_constr eq stmt
+  | Unfold _ name => eval unfold $name in $stmt
+  | Apply _ equiv => apply_in_constr equiv stmt
+  | Rewrite _ eq => tactic_in_constr eq stmt
   end.
 
 (**
@@ -171,6 +171,10 @@ Ltac2 unfold_in_all (unfold_method: constr -> constr)
   (* Print output *)
   if (Bool.or did_unfold_goal (Bool.neg (_is_empty only_unfolded_hyps)))
     then
+      match def_name with
+      | Some s => info_notice (of_string s)
+      | _ => ()
+      end;
       (* Print initial statement *)
       if definitional then
         (info_notice (of_string "Expanded definition in statements where applicable."))
@@ -267,14 +271,22 @@ Ltac2 Notation "Expand" "the" "definition" "of" targets(list1(seq(reference, occ
 
   wp_unfold (eval_unfold targets) None true true None.
 
+Ltac2 name_from_action (ua : unfold_action) : string :=
+  match ua with
+  | Unfold name _ => name
+  | Apply name _ => name
+  | Rewrite name _ => name
+  end.
+
 Local Ltac2 wp_unfold_from_action_list (ua_list : unfold_action list) :=
   let definitional_for_action (ua : unfold_action) := match ua with
-  | Unfold _ => true
-  | Apply _ => false
-  | Rewrite _ => false
+  | Unfold _ _ => true
+  | Apply _ _ => false
+  | Rewrite _ _ => false
   end in
   List.iter (fun z =>
-      wp_unfold (unfold_method_for_action z) None false (definitional_for_action z) None)
+      wp_unfold (unfold_method_for_action z)
+      (Some (name_from_action z)) false (definitional_for_action z) None)
     ua_list.