Adding eassert, eset, epose, etc.

CHANGES

@@ -26,6 +26,10 @@ Tactics
   now uses type classes and rejects terms with unresolved holes, like
   entry "constr" does. To get the former behavior use
   "open_constr_with_bindings" (possible source of incompatibility.
+- New e-variants eassert, eenough, epose proof, eset, eremember, epose
+  which behave like the corresponding variants with no "e" but turn
+  unresolved implicit arguments into existential variables, on the
+  shelf, rather than failing.
 
 Vernacular Commands
 

doc/refman/RefMan-tac.tex

@@ -1155,6 +1155,15 @@ \subsection{\tt set ( {\ident} := {\term} )}
 
   These are the general forms that combine the previous possibilities.
 
+\item {\tt eset ( {\ident$_0$} \nelistnosep{\binder} := {\term} ) in {\occgoalset}}\tacindex{eset}\\
+      {\tt eset {\term} in {\occgoalset}}
+
+  While the different variants of \texttt{set} expect that no
+  existential variables are generated by the tactic, \texttt{eset}
+  removes this constraint. In practice, this is relevant only when
+  \texttt{eset} is used as a synonym of \texttt{epose}, i.e. when the
+  term does not occur in the goal.
+
 \item {\tt remember {\term} as {\ident}}\tacindex{remember}
 
   This behaves as {\tt set ( {\ident} := {\term} ) in *} and using a
@@ -1170,6 +1179,15 @@ \subsection{\tt set ( {\ident} := {\term} )}
   This is a more general form of {\tt remember} that remembers the
   occurrences of {\term} specified by an occurrences set.
 
+\item
+  {\tt eremember {\term} as {\ident}}\tacindex{eremember}\\
+  {\tt eremember {\term} as {\ident} in {\occgoalset}}\\
+  {\tt eremember {\term} as {\ident} eqn:{\ident}}
+
+  While the different variants of \texttt{remember} expect that no
+  existential variables are generated by the tactic, \texttt{eremember}
+  removes this constraint.
+
 \item {\tt pose ( {\ident} := {\term} )}\tacindex{pose}
 
   This adds the local definition {\ident} := {\term} to the current
@@ -1187,6 +1205,14 @@ \subsection{\tt set ( {\ident} := {\term} )}
   This behaves as {\tt pose ( {\ident} := {\term} )} but
   {\ident} is generated by {\Coq}.
 
+\item {\tt epose ( {\ident} := {\term} )}\tacindex{epose}\\
+      {\tt epose ( {\ident} \nelistnosep{\binder} := {\term} )}\\
+      {\tt epose {\term}}
+
+  While the different variants of \texttt{pose} expect that no
+  existential variables are generated by the tactic, \texttt{epose}
+  removes this constraint.
+
 \end{Variants}
 
 \subsection{\tt decompose [ {\qualid$_1$} \dots\ {\qualid$_n$} ] \term}
@@ -1284,6 +1310,14 @@ \subsection{\tt assert ( {\ident} :\ {\form} )}
 
   \ErrMsg \errindex{Variable {\ident} is already declared}
 
+\item \texttt{eassert {\form} as {\intropattern} by {\tac}}\tacindex{eassert}\tacindex{eassert as}\tacindex{eassert by}\\
+  {\tt assert ( {\ident} := {\term} )}
+
+  While the different variants of \texttt{assert} expect that no
+  existential variables are generated by the tactic, \texttt{eassert}
+  removes this constraint. This allows not to specify the asserted
+  statement completely before starting to prove it.
+
 \item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}}
 
   This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by
@@ -1294,6 +1328,11 @@ \subsection{\tt assert ( {\ident} :\ {\form} )}
     as {\intropattern}} is the same as applying
   the {\intropattern} to {\term}.
 
+\item \texttt{epose proof {\term} \zeroone{as {\intropattern}}\tacindex{epose proof}}
+
+  While \texttt{pose proof} expects that no existential variables are generated by the tactic,
+  \texttt{epose proof} removes this constraint.
+
 \item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough}
 
   This adds a new hypothesis of name {\ident} asserting {\form} to the
@@ -1320,6 +1359,14 @@ \subsection{\tt assert ( {\ident} :\ {\form} )}
   destructed. If the \texttt{as} {\intropattern} clause generates more
   than one subgoal, {\tac} is applied to all of them.
 
+\item \texttt{eenough ({\ident} :\ {\form}) by {\tac}}\tacindex{eenough}\tacindex{eenough as}\tacindex{eenough by}\\
+ \texttt{eenough {\form} by {\tac}}\tacindex{enough by}\\
+ \texttt{eenough {\form} as {\intropattern} by {\tac}}
+
+  While the different variants of \texttt{enough} expect that no
+  existential variables are generated by the tactic, \texttt{eenough}
+  removes this constraint.
+
 \item {\tt cut {\form}}\tacindex{cut}
 
   This tactic applies to any goal. It implements the non-dependent

engine/evarutil.ml

@@ -367,10 +367,10 @@ let push_rel_context_to_named_context env sigma typ =
 
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
-let restrict_evar evd evk filter candidates =
+let restrict_evar evd evk filter ?src candidates =
   let evd = Sigma.to_evar_map evd in
   let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
-  let evd, evk' = Evd.restrict evk filter ?candidates evd in
+  let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
   Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
 
 let new_pure_evar_full evd evi =

engine/evarutil.mli

@@ -57,7 +57,7 @@ val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
 val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
-  constr list option -> (existential_key, 'r) Sigma.sigma
+  ?src:Evar_kinds.t Loc.located -> constr list option -> (existential_key, 'r) Sigma.sigma
 
 (** Polymorphic constants *)
 

engine/evd.ml

@@ -653,12 +653,13 @@ let define evk body evd =
   let evar_names = EvNames.remove_name_defined evk evd.evar_names in
   { evd with defn_evars; undf_evars; last_mods; evar_names }
 
-let restrict evk filter ?candidates evd =
+let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
   let evar_info' =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
+      evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
       evar_extra = Store.empty } in
   let last_mods = match evd.conv_pbs with
   | [] ->  evd.last_mods

engine/evd.mli

@@ -240,7 +240,7 @@ val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
 (** {6 Misc} *)
 
 val restrict : evar -> Filter.t -> ?candidates:constr list ->
-  evar_map -> evar_map * evar
+  ?src:Evar_kinds.t located -> evar_map -> evar_map * evar
 (** Restrict an undefined evar into a new evar by filtering context and
     possibly limiting the instances to a set of candidates *)
 

engine/proofview.ml

@@ -696,6 +696,12 @@ let mark_in_evm ~goal evd content =
   let info =
     if goal then
       { info with Evd.evar_source = match info.Evd.evar_source with
+            (* Two kinds for goal evars:
+               - GoalEvar (morally not dependent)
+               - VarInstance (morally dependent of some name).
+               This is a heuristic for naming these evars. *)
+            | loc, (Evar_kinds.QuestionMark (_,Names.Name id) |
+                    Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
             | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
             | loc,_ -> loc,Evar_kinds.GoalEvar }
     else info

engine/termops.ml

@@ -112,6 +112,7 @@ let pr_evar_suggested_name evk sigma =
   | None -> match evi.evar_source with
   | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
   | _,Evar_kinds.VarInstance id -> id
+  | _,Evar_kinds.QuestionMark (_,Name id) -> id
   | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
   | _ ->
       let env = reset_with_named_context evi.evar_hyps (Global.env()) in

interp/constrintern.ml

@@ -1081,8 +1081,8 @@ let sort_fields ~complete loc fields completer =
           let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
             match projs with
               | [] -> (idx, acc_first_idx, acc)
-              | (Some name) :: projs ->
-                 let field_glob_ref = ConstRef name in
+              | (Some field_glob_id) :: projs ->
+                 let field_glob_ref = ConstRef field_glob_id in
                  let first_field = eq_gr field_glob_ref first_field_glob_ref in
                  begin match proj_kinds with
                     | [] -> anomaly (Pp.str "Number of projections mismatch")
@@ -1099,7 +1099,7 @@ let sort_fields ~complete loc fields completer =
                          build_proj_list projs proj_kinds idx ~acc_first_idx acc
                        else
                          build_proj_list projs proj_kinds (idx+1) ~acc_first_idx
-                                         ((idx, field_glob_ref) :: acc)
+                                         ((idx, field_glob_id) :: acc)
                  end
               | None :: projs ->
                  if complete then
@@ -1121,7 +1121,7 @@ let sort_fields ~complete loc fields completer =
                  user_err ?loc:(loc_of_reference field_ref) ~hdr:"intern"
                                (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
                let remaining_projs, (field_index, _) =
-                 let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
+                 let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
                    user_err ?loc 
@@ -1646,7 +1646,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
 	 sort_fields ~complete:true loc fs
-	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)),
                                                            Misctypes.IntroAnonymous, None))
        in
        begin
@@ -1726,7 +1726,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
            (match naming with
            | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
-           | _ -> Evar_kinds.QuestionMark st)
+           | _ -> Evar_kinds.QuestionMark (st,Anonymous))
         | Some k -> k
         in
         let solve = match solve with

intf/evar_kinds.mli

@@ -21,7 +21,7 @@ type t =
      * bool (** Force inference *)
   | BinderType of Name.t
   | NamedHole of Id.t (* coming from some ?[id] syntax *)
-  | QuestionMark of obligation_definition_status
+  | QuestionMark of obligation_definition_status * Name.t
   | CasesType of bool (* true = a subterm of the type *)
   | InternalHole
   | TomatchTypeParameter of inductive * int

plugins/ltac/extratactics.ml4

@@ -636,7 +636,7 @@ let subst_var_with_hole occ tid t =
            else
 	     (incr locref;
               CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),
+	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
                      Misctypes.IntroAnonymous, None)))
         else x
     | c -> map_glob_constr_left_to_right substrec c in
@@ -648,13 +648,13 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } ->
+    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
            CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
+	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s))
     | c -> map_glob_constr_left_to_right substrec c
   in
   substrec t

plugins/ltac/g_tactic.ml4

@@ -538,38 +538,64 @@ GEXTEND Gram
 	  TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd))
 
       | IDENT "pose"; (id,b) = bindings_with_parameters ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,b,Locusops.nowhere,true,None))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,b,Locusops.nowhere,true,None))
       | IDENT "pose"; b = constr; na = as_name ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,b,Locusops.nowhere,true,None))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None))
+      | IDENT "epose"; (id,b) = bindings_with_parameters ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None))
+      | IDENT "epose"; b = constr; na = as_name ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None))
       | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,c,p,true,None))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,c,p,true,None))
       | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
-          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,true,None))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None))
+      | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,c,p,true,None))
+      | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl ->
+          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,true,None))
       | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
           p = clause_dft_all ->
-          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,false,e))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,false,e))
+      | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat;
+          p = clause_dft_all ->
+          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e))
 
       (* Alternative syntax for "pose proof c as id" *)
       | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
 	  c = lconstr; ")" ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+	  c = lconstr; ")" ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (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 ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+	  c = lconstr; ")"; tac=by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (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 ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+	  c = lconstr; ")"; tac=by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
 
       | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c))
+      | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,ipat,c))
       | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,ipat,c))
+      | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,ipat,c))
       | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,ipat,c))
+      | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c))
 
       | IDENT "generalize"; c = constr ->
 	  TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)])

plugins/ltac/pptactic.ml

@@ -768,15 +768,15 @@ type 'a extra_genarg_printer =
             primitive "cofix" ++ spc () ++ pr_id id ++ spc()
             ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
           )
-        | TacAssert (b,Some tac,ipat,c) ->
+        | TacAssert (ev,b,Some tac,ipat,c) ->
           hov 1 (
-            primitive (if b then "assert" else "enough") ++
+            primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++
               pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
               pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
           )
-        | TacAssert (_,None,ipat,c) ->
+        | TacAssert (ev,_,None,ipat,c) ->
           hov 1 (
-            primitive "pose proof"
+            primitive (if ev then "epose proof" else "pose proof")
             ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
           )
         | TacGeneralize l ->
@@ -786,11 +786,11 @@ type 'a extra_genarg_printer =
               pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
               l
           )
-        | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
-          hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
-        | TacLetTac (na,c,cl,b,e) ->
+        | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl ->
+          hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+        | TacLetTac (ev,na,c,cl,b,e) ->
           hov 1 (
-            (if b then primitive "set" else primitive "remember") ++
+            primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++
               (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
                 else pr_pose_as_style pr.pr_constr na c) ++
               pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++

plugins/ltac/tacexpr.mli

@@ -141,10 +141,10 @@ type 'a gen_atomic_tactic_expr =
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
-      bool * 'tacexpr option option *
+      evars_flag * bool * 'tacexpr option option *
       'dtrm intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
-  | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
+  | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
       intro_pattern_naming_expr located option
 
   (* Derived basic tactics *)