Adding a syntax "enough" for the variant of "assert" with the order of

subgoals and the role of the "by tac" clause swapped.

12 files changed, 88 insertions, 40 deletions

diff --git a/CHANGES b/CHANGES
index 335b793ea..e3aa5d792 100644
--- a/CHANGES
+++ b/CHANGES
@@ -171,6 +171,8 @@ Tactics
   the relevant hypotheses).
 - New construct "uconstr:c" and "type_term c" to build untyped terms.
 - The good bullet (-/+/*) is suggested sometimes when user gives a wrong one.
+- New tactic "enough", symmetric to "assert", but with subgoals
+  swapped, as a more friendly replacement of "cut".
 
 Program
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9bba45bea..28d854eaa 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1179,22 +1179,6 @@ in the list of subgoals remaining to prove.
   This behaves as {\tt assert ( {\ident} :\ {\form} )} but
   {\ident} is generated by {\Coq}.
 
-\item{\tt assert ( {\ident} := {\term} )}
-
-  This behaves as {\tt assert ({\ident} :\ {\type});[exact
-    {\term}|idtac]} where {\type} is the type of {\term}.
-
-  \ErrMsg \errindex{Variable {\ident} is already declared}
-
-\item {\tt cut {\form}}\tacindex{cut}
-
-  This tactic applies to any goal. It implements the non-dependent
-  case of the ``App''\index{Typing rules!App} rule given in
-  Section~\ref{Typed-terms}. (This is Modus Ponens inference rule.)
-  {\tt cut U} transforms the current goal \texttt{T} into the two
-  following subgoals: {\tt U -> T} and \texttt{U}.  The subgoal {\tt U
-    -> T} comes first in the list of remaining subgoal to prove.
-
 \item \texttt{assert {\form} by {\tac}}\tacindex{assert by}
 
   This tactic behaves like \texttt{assert} but applies {\tac}
@@ -1217,6 +1201,14 @@ in the list of subgoals remaining to prove.
 
   This combines the two previous variants of {\tt assert}.
 
+\item{\tt assert ( {\ident} := {\term} )}
+
+  This behaves as {\tt assert ({\ident} :\ {\type});[exact
+      {\term}|idtac]} where {\type} is the type of {\term}. This is
+  deprecated in favor of {\tt pose proof}.
+
+  \ErrMsg \errindex{Variable {\ident} is already declared}
+
 \item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}}
 
   This tactic behaves like \texttt{assert T as {\intropattern} by
@@ -1227,6 +1219,41 @@ in the list of subgoals remaining to prove.
   {\disjconjintropattern}\tacindex{pose proof}} behaves
   like \texttt{destruct {\term} as {\disjconjintropattern}}.
 
+\item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough}
+
+  This adds a new hypothesis of name {\ident} asserting {\form} to the
+  goal the tactic \texttt{enough} is applied to. A new subgoal stating
+  \texttt{\form} is inserted after the initial goal rather than before
+  it as \texttt{assert} would do.
+
+\item \texttt{enough {\form}}\tacindex{enough}
+
+  This behaves like \texttt{enough ({\ident} :\ {\form})} with the name
+  {\ident} of the hypothesis generated by {\Coq}.
+
+\item \texttt{enough {\form} as {\intropattern}\tacindex{enough as}}
+
+  This behaves like \texttt{enough} {\form} using {\intropattern} to
+  name or destruct the new hypothesis.
+
+\item \texttt{enough ({\ident} :\ {\form}) by {\tac}}\tacindex{enough by}\\
+ \texttt{enough {\form} by {\tac}}\tacindex{enough by}\\
+ \texttt{enough {\form} as {\intropattern} by {\tac}}
+
+  This behaves as above but with {\tac} expected to solve the initial
+  goal after the extra assumption {\form} is added and possibly
+  destructed. If the \texttt{as} {\intropattern} clause generates more
+  than one subgoal, {\tac} is applied to all of them.
+
+\item {\tt cut {\form}}\tacindex{cut}
+
+  This tactic applies to any goal. It implements the non-dependent
+  case of the ``App''\index{Typing rules!App} rule given in
+  Section~\ref{Typed-terms}. (This is Modus Ponens inference rule.)
+  {\tt cut U} transforms the current goal \texttt{T} into the two
+  following subgoals: {\tt U -> T} and \texttt{U}.  The subgoal {\tt U
+    -> T} comes first in the list of remaining subgoal to prove.
+
 \item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize}} \\
       {\tt specialize {\ident} with \bindinglist}
 
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index d1f458791..2690cf867 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -336,9 +336,10 @@ let rec mlexpr_of_atomic_tactic = function
       let l = mlexpr_of_list f l in
       <:expr< Tacexpr.TacMutualCofix $id$ $l$ >>
 
-  | Tacexpr.TacAssert (t,ipat,c) ->
+  | Tacexpr.TacAssert (b,t,ipat,c) ->
       let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in
-      <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$
+      <:expr< Tacexpr.TacAssert $mlexpr_of_bool b$
+              $mlexpr_of_option mlexpr_of_tactic t$ $ipat$
 	      $mlexpr_of_constr c$ >>
   | Tacexpr.TacGeneralize cl ->
       <:expr< Tacexpr.TacGeneralize
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 22ec1b445..4174de123 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -117,7 +117,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacCofix of Id.t option
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
-      ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option *
+      bool * ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option *
       intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacGeneralizeDep of 'trm
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 4c328a3bf..c02f2d569 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -569,19 +569,27 @@ GEXTEND Gram
           p = clause_dft_all ->
           TacLetTac (na,c,p,false,e)
 
-      (* Begin compatibility *)
+      (* Alternative syntax for "pose proof c as id" *)
       | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
 	  c = lconstr; ")" ->
-	  TacAssert (None,Some (!@loc,IntroIdentifier id),c)
+	  TacAssert (true,None,Some (!@loc,IntroIdentifier id),c)
+
+      (* Alternative syntax for "assert c as id by tac" *)
       | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAssert (Some tac,Some (!@loc,IntroIdentifier id),c)
-      (* End compatibility *)
+	  TacAssert (true,Some tac,Some (!@loc,IntroIdentifier id),c)
+
+      (* Alternative syntax for "enough c as id by tac" *)
+      | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+	  c = lconstr; ")"; tac=by_tactic ->
+	  TacAssert (false,Some tac,Some (!@loc,IntroIdentifier id),c)
 
       | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAssert (Some tac,ipat,c)
+	  TacAssert (true,Some tac,ipat,c)
       | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
-	  TacAssert (None,ipat,c)
+	  TacAssert (true,None,ipat,c)
+      | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
+	  TacAssert (false,Some tac,ipat,c)
 
       | IDENT "generalize"; c = constr ->
 	  TacGeneralize [((AllOccurrences,c),Names.Anonymous)]
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c230a9896..4218286b0 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -735,7 +735,7 @@ let consider_tac c hyps gls =
     | _ ->
 	let id = pf_get_new_id (Id.of_string "_tmp") gls in
 	tclTHEN
-	  (Proofview.V82.of_tactic (forward None (Some (Loc.ghost, IntroIdentifier id)) c))
+	  (Proofview.V82.of_tactic (forward true None (Some (Loc.ghost, IntroIdentifier id)) c))
  	  (consider_match false [] [id] hyps) gls
 
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 0039a81bf..dbf83936a 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -682,11 +682,11 @@ and pr_atom1 = function
   | TacMutualCofix (id,l) ->
       hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
              str"with " ++ prlist_with_sep spc pr_cofix_tac l)
-  | TacAssert (Some tac,ipat,c) ->
-      hov 1 (str "assert" ++
+  | TacAssert (b,Some tac,ipat,c) ->
+      hov 1 (str (if b then "assert" else "enough") ++
              pr_assumption pr_lconstr pr_constr ipat c ++
              pr_by_tactic (pr_tac_level ltop) tac)
-  | TacAssert (None,ipat,c) ->
+  | TacAssert (_,None,ipat,c) ->
       hov 1 (str "pose proof" ++
              pr_assertion pr_lconstr pr_constr ipat c)
   | TacGeneralize l ->
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c2f85d534..e2f87062e 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -473,8 +473,8 @@ let rec intern_atomic lf ist x =
   | TacMutualCofix (id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
-  | TacAssert (otac,ipat,c) ->
-      TacAssert (Option.map (intern_pure_tactic ist) otac,
+  | TacAssert (b,otac,ipat,c) ->
+      TacAssert (b,Option.map (intern_pure_tactic ist) otac,
                  Option.map (intern_intro_pattern lf ist) ipat,
                  intern_constr_gen false (not (Option.is_empty otac)) ist c)
   | TacGeneralize cl ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e0d24e9e1..b52a3e7e9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1610,7 +1610,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	  (Tactics.mutual_cofix (interp_fresh_ident ist env id) l_interp 0)
           gl
       end
-  | TacAssert (t,ipat,c) ->
+  | TacAssert (b,t,ipat,c) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
@@ -1620,7 +1620,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let patt = interp_intro_pattern ist env in
         Tacticals.New.tclTHEN
           (Proofview.V82.tclEVARS sigma)
-          (Tactics.forward (Option.map (interp_tactic ist) t)
+          (Tactics.forward b (Option.map (interp_tactic ist) t)
               (Option.map patt ipat) c)
       end
   | TacGeneralize cl ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 30fffed91..428061463 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -146,8 +146,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacCofix idopt as x -> x
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
-  | TacAssert (b,na,c) ->
-      TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c)
+  | TacAssert (b,otac,na,c) ->
+      TacAssert (b,Option.map (subst_tactic subst) otac,na,subst_glob_constr subst c)
   | TacGeneralize cl ->
       TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 442f0a3cb..cb6894fef 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+let a = 1
+
 open Pp
 open Errors
 open Util
@@ -1738,6 +1740,7 @@ let assert_as first ipat c =
   end
 
 let assert_tac na = assert_as true (ipat_of_name na)
+let enough_tac na = assert_as false (ipat_of_name na)
 
 (* apply in as *)
 
@@ -1856,7 +1859,7 @@ let letin_pat_tac with_eq name c occs =
   letin_tac_gen with_eq (AbstractPattern (name,c,occs,false,tactic_infer_flags)) None
 
 (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
-let forward usetac ipat c =
+let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.raw_enter begin fun gl ->
@@ -1864,10 +1867,15 @@ let forward usetac ipat c =
       Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
       end
   | Some tac ->
-      Tacticals.New.tclTHENFIRST (assert_as true ipat c) tac
+      if b then
+        Tacticals.New.tclTHENFIRST (assert_as b ipat c) tac
+      else
+        Tacticals.New.tclTHENS3PARTS
+          (assert_as b ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
 
-let pose_proof na c = forward None (ipat_of_name na) c
-let assert_by na t tac = forward (Some tac) (ipat_of_name na) t
+let pose_proof na c = forward true None (ipat_of_name na) c
+let assert_by na t tac = forward true (Some tac) (ipat_of_name na) t
+let enough_by na t tac = forward false (Some tac) (ipat_of_name na) t
 
 (***************************)
 (*  Generalization tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 20b974a82..c2403d97a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -334,13 +334,15 @@ val assert_replacing            : Id.t -> types -> tactic -> tactic
 val cut_replacing               : Id.t -> types -> tactic -> tactic
 
 val assert_as : bool -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
-val forward   : unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
+val forward   : bool -> unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
 val letin_tac : (bool * intro_pattern_expr located) option -> Name.t ->
   constr -> types option -> clause -> unit Proofview.tactic
 val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t ->
   evar_map * constr -> clause -> unit Proofview.tactic
 val assert_tac : Name.t -> types -> unit Proofview.tactic
+val enough_tac : Name.t -> types -> unit Proofview.tactic
 val assert_by  : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
+val enough_by  : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
 val pose_proof : Name.t -> constr -> unit Proofview.tactic
 
 val generalize      : constr list -> tactic