Separate some concerns: let notations do as little logic as possible

Author: jim-portegies

theories/Tactics/By.v

@@ -57,12 +57,8 @@ Ltac2 Notation "By"
   let xtr_dbs := List.filter (fun z => Constr.equal (Constr.type z) constr:(string)) parsed_args in
   let xtr_dbs := List.map rocq_string_to_ltac2_string xtr_dbs in
   if String.equal x "it holds" then
-    panic_if_goal_wrapped();
-    (wp_assert_by claim label xtr_lemmas xtr_dbs)
+    (wp_assert_by_with_checks claim label xtr_lemmas xtr_dbs)
   else if String.equal x "we conclude" then
-    unwrap_state_goal_no_check ();
-    panic_if_goal_wrapped();
-    guarantee_stated_goal_matches claim;
-    (conclude_by xtr_lemmas xtr_dbs)
+    (wp_conclude_by_with_checks claim xtr_lemmas xtr_dbs)
   else
-    (wp_enough_by claim xtr_lemmas xtr_dbs).
+    (wp_enough_by_with_checks claim xtr_lemmas xtr_dbs).

theories/Tactics/Conclusion.v

@@ -71,7 +71,7 @@ Local Ltac2 target_equals_goal_judgementally (target : constr) :=
 *)
 
 
-Ltac2 guarantee_stated_goal_matches (sttd_goal : constr) :=
+Local Ltac2 guarantee_stated_goal_matches (sttd_goal : constr) :=
   let sttd_goal := correct_type_by_wrapping sttd_goal in
   let sttd_goal := (eval unfold subset_type, ge_op, R_ge_type, nat_ge_type, gt_op, R_gt_type, nat_gt_type in $sttd_goal) in
   let current_goal := Control.goal () in
@@ -145,7 +145,7 @@ Local Ltac2 core_conclude_by (xtr_lemmas : constr list) (xtr_dbs : hint_db_name
 
 (** Adaptation of [core_conclude_by] that turns the [FailedToUse] errors
   which might be thrown into user readable errors. *)
-Ltac2 conclude_by (xtr_lemmas : constr list) (xtr_dbs : hint_db_name list) :=
+Local Ltac2 conclude_by (xtr_lemmas : constr list) (xtr_dbs : hint_db_name list) :=
   wrapper_core_by_tactic core_conclude_by xtr_lemmas xtr_dbs.
 
 (** Adaptation of [core_conclude_by] that allows user to use mathematical statements themselves
@@ -164,7 +164,7 @@ Local Ltac2 conclude_since (xtr_claim : constr) :=
   Does:
     - Removes the wrapper [StateGoal.Wrapper G].
 *)
-Ltac2 unwrap_state_goal_no_check () :=
+Local Ltac2 unwrap_state_goal_no_check () :=
   lazy_match! goal with
     | [|- StateGoal.Wrapper _] => apply StateGoal.wrap
     | [|- VerifyGoal.Wrapper _] => apply VerifyGoal.wrap
@@ -203,12 +203,19 @@ Ltac2 Notation "It" "follows" _(opt("that")) target_goal(lconstr) :=
 
   Arguments:
     - [target_goal: constr], expression that should equal the goal under focus.
-    - [xtr_lemma: constr], lemma that can be and has to be used for proof of [target_goal].
+    - [xtr_lemmas: constr list], extra lemmas that can be used for proof of [target_goal].
+    - [xtr_dbs: hint_db_name list], extra hint databases that can be used for proof of [target_goal].
 
   Raises exceptions:
     - [AutomationFailure], if [waterprove] fails the prove the goal (i.e. the goal is too difficult, or does not hold).
     - [ConcludeError], if [target_goal] is not equivalent to the actual goal under focus, even after rewriting.
 *)
+Ltac2 wp_conclude_by_with_checks (target_goal : constr) (xtr_lemmas : constr list) (xtr_dbs : hint_db_name list) :=
+  unwrap_state_goal_no_check ();
+  panic_if_goal_wrapped ();
+  guarantee_stated_goal_matches target_goal;
+  conclude_by xtr_lemmas xtr_dbs.
+
 Ltac2 Notation "Since" xtr_claim(lconstr) "we" "conclude" _(opt("that")) target_goal(lconstr) :=
   unwrap_state_goal_no_check ();
   panic_if_goal_wrapped ();

theories/Tactics/ItHolds.v

@@ -118,7 +118,7 @@ Local Ltac2 core_wp_assert_by (claim : constr) (label : ident option) (xtr_lemma
 
 (** Adaptation of [core_wp_assert_by] that turns the [FailedToUse] errors
   which might be thrown into user readable errors. *)
-Ltac2 wp_assert_by (claim : constr) (label : ident option) (xtr_lemmas : constr list) (xtr_dbs : hint_db_name list) :=
+Local Ltac2 wp_assert_by (claim : constr) (label : ident option) (xtr_lemmas : constr list) (xtr_dbs : hint_db_name list) :=
   wrapper_core_by_tactic (core_wp_assert_by claim label) xtr_lemmas xtr_dbs;
   (* Print suggestion on how to use new statement. *)
   HelpNewHyp.suggest_how_to_use claim label.
@@ -146,7 +146,9 @@ Local Ltac2 wp_assert_since (claim : constr) (label : ident option) (xtr_claim :
     - (fatal) if [rwaterprove] fails to prove the claim using the specified lemma.
     - [[label] is already used], if there is already another hypothesis with identifier [label].
 *)
-
+Ltac2 wp_assert_by_with_checks (claim : constr) (label : ident option) (xtr_lemmas : constr list) (xtr_dbs : hint_db_name list) :=
+  panic_if_goal_wrapped ();
+  wp_assert_by claim label xtr_lemmas xtr_dbs.
 
 
 (** Attempts to prove that proposed goal is enough to show current goal,

theories/Tactics/ItSuffices.v

@@ -62,9 +62,25 @@ Local Ltac2 core_wp_enough_by (new_goal : constr) (xtr_lemmas : constr list) (xt
 
 (** Adaptation of [core_wp_enough_by] that turns the [FailedToUse] errors
   which might be thrown into user readable errors. *)
-Ltac2 wp_enough_by (claim : constr) (xtr_lemmas : constr list) (xtr_dbs : hint_db_name list) :=
+Local Ltac2 wp_enough_by (claim : constr) (xtr_lemmas : constr list) (xtr_dbs : hint_db_name list) :=
   wrapper_core_by_tactic (core_wp_enough_by claim) xtr_lemmas xtr_dbs.
 
+(**
+  Proves that proposed goal is enough to show current goal.
+
+  Arguments:
+  - [claim]: proposed goal.
+  - [xtr_lemmas]: list of extra lemmas that can be used in the proof.
+  - [xtr_dbs]: list of extra hint databases to use in the proof.
+
+  Throws:
+  - [FailedToProve] if [rwaterprove] fails to prove that [claim] is enough to show current goal using the specified lemmas and hint databases.
+  - [FailedToUse] if [rwaterprove] fails to use a lemma in the proof while it should have used it.
+*)
+Ltac2 wp_enough_by_with_checks (claim : constr) (xtr_lemmas : constr list) (xtr_dbs : hint_db_name list) :=
+  panic_if_goal_wrapped ();
+  wp_enough_by claim xtr_lemmas xtr_dbs.
+
 (** Adaptation of [core_wp_assert_by] that allows user to use mathematical statements themselves
   instead of references to them as extra information for the automation system.
   Uses the code in [Since.v]. *)