diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 18 | ||||
| -rw-r--r-- | theories/Init/Tactics.v | 11 |
3 files changed, 32 insertions, 0 deletions
@@ -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 c4c0435c5..921e80743 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 47a971ef0..287b44fd0 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. |