From ccb7bd2948e9bd84997f3461257b2ce1c7ad3e6a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 23 Feb 2018 11:14:54 +0100
Subject: Added tacticals assert_succeeds/assert_fails (courtesy of Jason
 Gross).

---
 CHANGES                    |  3 +++
 doc/refman/RefMan-ltac.tex | 18 ++++++++++++++++++
 theories/Init/Tactics.v    | 11 +++++++++++
 3 files changed, 32 insertions(+)

diff --git a/CHANGES b/CHANGES
index 7ea23eeb7c..9dcd07ebab 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,6 +54,9 @@ Tactics
   with let bindings in the parameters.
 - The tactic "dtauto" now handles some inductives such as
   "@sigT A (fun _ => B)" as non-dependent conjunctions.
+- Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure
+  properties of the executation of a tactic without keeping the effect
+  of the execution.
 
 Focusing
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index c4c0435c5f..921e807439 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -156,6 +156,8 @@ is understood as
 & | & {\tt type\_term} {\term}\\
 & | & {\tt numgoals} \\
 & | & {\tt guard} {\it test}\\
+& | & {\tt assert\_fails} {\tacexprpref}\\
+& | & {\tt assert\_succeds} {\tacexprpref}\\
 & | & \atomictac\\
 & | & {\qualid} \nelist{\tacarg}{}\\
 & | & {\atom}
@@ -598,6 +600,22 @@ The experimental status of this tactic pertains to the fact if $v$ performs side
 
 \ErrMsg \errindex{This tactic has more than one success}
 
+\subsubsection[Checking the failure]{Checking the failure\tacindex{assert\_fails}\index{Tacticals!assert\_fails@{\tt assert\_fails}}}
+
+Coq provides a derived tactic to check that a tactic \emph{fails}:
+\begin{quote}
+{\tt assert\_fails} {\tacexpr}
+\end{quote}
+This behaves like {\tt tryif {\tacexpr} then fail 0 tac "succeeds" else idtac}.
+
+\subsubsection[Checking the success]{Checking the success\tacindex{assert\_succeeds}\index{Tacticals!assert\_succeeds@{\tt assert\_succeeds}}}
+
+Coq provides a derived tactic to check that a tactic has \emph{at least one} success:
+\begin{quote}
+{\tt assert\_succeeds} {\tacexpr}
+\end{quote}
+This behaves like {\tt tryif (assert\_fails tac) then fail 0 tac "fails" else idtac}.
+
 \subsubsection[Solving]{Solving\tacindex{solve}
 \index{Tacticals!solve@{\tt solve}}}
 
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 47a971ef09..287b44fd0b 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -313,3 +313,14 @@ Ltac time_constr tac :=
   let ret := tac () in
   let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in
   ret.
+
+(** Useful combinators *)
+
+Ltac assert_fails tac :=
+  tryif tac then fail 0 tac "succeeds" else idtac.
+Ltac assert_succeeds tac :=
+  tryif (assert_fails tac) then fail 0 tac "fails" else idtac.
+Tactic Notation "assert_succeeds" tactic3(tac) :=
+  assert_succeeds tac.
+Tactic Notation "assert_fails" tactic3(tac) :=
+  assert_fails tac.
-- 
cgit v1.2.3


From aa95d82692684a416d7a1c25fce38b4eca1e49c9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 23 Feb 2018 11:20:26 +0100
Subject: Uniform spacing layout in Tactics.v.

---
 theories/Init/Tactics.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 287b44fd0b..c36494c9ed 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -253,6 +253,7 @@ Tactic Notation "dependent" "induction" ident(H) :=
     writing a version of [inversion] / [dependent destruction] which
     does not lose information, i.e., does not turn a goal which is
     provable into one which requires axiom K / UIP.  *)
+
 Ltac simpl_proj_exist_in H :=
   repeat match type of H with
          | context G[proj1_sig (exist _ ?x ?p)]
@@ -308,6 +309,7 @@ Ltac inversion_sigma_step :=
 Ltac inversion_sigma := repeat inversion_sigma_step.
 
 (** A version of [time] that works for constrs *)
+
 Ltac time_constr tac :=
   let eval_early := match goal with _ => restart_timer end in
   let ret := tac () in
-- 
cgit v1.2.3