Backport PR #12246: Adding support for applying in several hypotheses…

… at the same time (granting #9816)

doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  `apply in` supports several hypotheses
+  (`#12246 <https://github.com/coq/coq/pull/12246>`_,
+  by Hugo Herbelin; grants
+  `#9816 <https://github.com/coq/coq/pull/9816>`_).

doc/sphinx/proof-engine/tactics.rst

@@ -878,38 +878,38 @@ Applying theorems
       This happens if the conclusion of :token:`ident` does not match any of
       the non-dependent premises of the type of :token:`term`.
 
-   .. tacv:: apply {+, @term} in @ident
+   .. tacv:: apply {+, @term} in {+, @ident}
 
-      This applies each :token:`term` in sequence in :token:`ident`.
+      This applies each :token:`term` in sequence in each hypothesis :token:`ident`.
 
-   .. tacv:: apply {+, @term with @bindings} in @ident
+   .. tacv:: apply {+, @term with @bindings} in {+, @ident}
 
-      This does the same but uses the bindings in each :n:`(@ident := @term)` to
-      instantiate the parameters of the corresponding type of :token:`term`
-      (see :ref:`bindings`).
+      This does the same but uses the bindings to instantiate
+      parameters of :token:`term` (see :ref:`bindings`).
 
-   .. tacv:: eapply {+, @term {? with @bindings } } in @ident
+   .. tacv:: eapply {+, @term {? with @bindings } } in {+, @ident}
 
       This works as :tacn:`apply … in` but turns unresolved bindings into
       existential variables, if any, instead of failing.
 
-   .. tacv:: apply {+, @term {? with @bindings } } in @ident as @simple_intropattern
+   .. tacv:: apply {+, @term {? with @bindings } } in {+, @ident {? as @simple_intropattern}}
       :name: apply … in … as
 
-      This works as :tacn:`apply … in` then applies the :token:`simple_intropattern`
-      to the hypothesis :token:`ident`.
+      This works as :tacn:`apply … in` but applying an associated
+      :token:`simple_intropattern` to each hypothesis :token:`ident`
+      that comes with such clause.
 
-   .. tacv:: simple apply @term in @ident
+   .. tacv:: simple apply @term in {+, @ident}
 
       This behaves like :tacn:`apply … in` but it reasons modulo conversion
       only on subterms that contain no variables to instantiate and does not
       traverse tuples. See :ref:`the corresponding example <simple_apply_ex>`.
 
-   .. tacv:: {? simple} apply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern}
-             {? simple} eapply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern}
+   .. tacv:: {? simple} apply {+, @term {? with @bindings}} in {+, @ident {? as @simple_intropattern}}
+             {? simple} eapply {+, @term {? with @bindings}} in {+, @ident {? as @simple_intropattern}}
 
-      This summarizes the different syntactic variants of :n:`apply @term in @ident`
-      and :n:`eapply @term in @ident`.
+      This summarizes the different syntactic variants of :n:`apply @term in {+, @ident}`
+      and :n:`eapply @term in {+, @ident}`.
 
 .. tacn:: constructor @natural
    :name: constructor

plugins/ltac/g_tactic.mlg

@@ -407,8 +407,8 @@ GRAMMAR EXTEND Gram
       | -> { [] } ] ]
   ;
   in_hyp_as:
-    [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) }
-      | -> { None } ] ]
+    [ [ "in"; l = LIST1 [id = id_or_meta; ipat = as_ipat -> { (id,ipat) } ] SEP "," -> { l }
+      | -> { [] } ] ]
   ;
   orient_rw:
     [ [ "->" -> { true }

plugins/ltac/pptactic.ml

@@ -458,8 +458,7 @@ let string_of_genarg_arg (ArgumentType arg) =
     | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
 
   let pr_in_hyp_as prc pr_id = function
-    | None -> mt ()
-    | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
+    | (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
 
   let pr_in_clause pr_id = function
     | { onhyps=None; concl_occs=NoOccurrences } ->
@@ -756,7 +755,7 @@ let pr_goal_selector ~toplevel s =
             (if a then mt() else primitive "simple ") ++
               primitive (with_evars ev "apply") ++ spc () ++
               prlist_with_sep pr_comma pr_with_bindings_arg cb ++
-              pr_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
+              prlist_with_sep spc (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
           )
         | TacElim (ev,cb,cbo) ->
           hov 1 (

plugins/ltac/tacexpr.ml

@@ -108,7 +108,7 @@ type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
-      ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+      ('nam * 'dtrm intro_pattern_expr CAst.t option) list
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list

plugins/ltac/tacexpr.mli

@@ -107,7 +107,7 @@ type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
-      ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+      ('nam * 'dtrm intro_pattern_expr CAst.t option) list
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list

plugins/ltac/tacintern.ml

@@ -444,11 +444,11 @@ let intern_red_expr ist = function
   | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
 
-let intern_in_hyp_as ist lf (id,ipat) =
-  (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
-
 let intern_hyp_list ist = List.map (intern_hyp ist)
 
+let intern_in_hyp_as ist lf (idl,ipat) =
+  (intern_hyp ist idl, Option.map (intern_intro_pattern lf ist) ipat)
+
 let intern_inversion_strength lf ist = function
   | NonDepInversion (k,idl,ids) ->
       NonDepInversion (k,intern_hyp_list ist idl,
@@ -527,7 +527,7 @@ let rec intern_atomic lf ist x =
       TacIntroPattern (ev,List.map (intern_intro_pattern lf ist) l)
   | TacApply (a,ev,cb,inhyp) ->
       TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb,
-                Option.map (intern_in_hyp_as ist lf) inhyp)
+                List.map (intern_in_hyp_as ist lf) inhyp)
   | TacElim (ev,cb,cbo) ->
       TacElim (ev,intern_constr_with_bindings_arg ist cb,
                Option.map (intern_constr_with_bindings ist) cbo)

plugins/ltac/tacinterp.ml

@@ -1667,10 +1667,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
             (k,(make ?loc f))) cb
         in
         let sigma,tac = match cl with
-          | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
-          | Some cl ->
-              let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in
-              sigma, Tactics.apply_delayed_in a ev id l cl in
+          | [] -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
+          | cl ->
+              let sigma,cl = List.fold_left_map (interp_in_hyp_as ist env) sigma cl in
+              sigma, List.fold_right (fun (id,ipat) -> Tactics.apply_delayed_in a ev id l ipat) cl Tacticals.New.tclIDTAC in
         Tacticals.New.tclWITHHOLES ev tac sigma
       end
       end

plugins/ltac/tacsubst.ml

@@ -128,7 +128,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Basic tactics *)
   | TacIntroPattern (ev,l) -> TacIntroPattern (ev,List.map (subst_intro_pattern subst) l)
   | TacApply (a,ev,cb,cl) ->
-      TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
+      TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,
+                List.map (on_snd (Option.map (subst_intro_pattern subst))) cl)
   | TacElim (ev,cb,cbo) ->
       TacElim (ev,subst_glob_with_bindings_arg subst cb,
                Option.map (subst_glob_with_bindings subst) cbo)

tactics/tactics.ml

@@ -2635,7 +2635,7 @@ let assert_as first hd ipat t =
 (* apply in as *)
 
 let general_apply_in ?(respect_opaque=false) with_delta
-    with_destruct with_evars id lemmas ipat =
+    with_destruct with_evars id lemmas ipat then_tac =
   let tac (naming,lemma) tac id =
     apply_in_delayed_once ~respect_opaque with_delta
       with_destruct with_evars naming id lemma tac in
@@ -2653,7 +2653,8 @@ let general_apply_in ?(respect_opaque=false) with_delta
     List.map (fun lem -> (NamingMustBe (CAst.make id),lem)) first, (naming,last)
   in
   (* We chain apply_in_once, ending with an intro pattern *)
-  List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
+  List.fold_right tac lemmas_target
+    (tac last_lemma_target (fun id -> Tacticals.New.tclTHEN (ipat_tac id) then_tac)) id
   end
 
 (*
@@ -2666,10 +2667,10 @@ let general_apply_in ?(respect_opaque=false) with_delta
 
 let apply_in simple with_evars id lemmas ipat =
   let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in
-  general_apply_in simple simple with_evars id lemmas ipat
+  general_apply_in simple simple with_evars id lemmas ipat Tacticals.New.tclIDTAC
 
-let apply_delayed_in simple with_evars id lemmas ipat =
-  general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat
+let apply_delayed_in simple with_evars id lemmas ipat then_tac =
+  general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat then_tac
 
 (*****************************)
 (* Tactics abstracting terms *)

tactics/tactics.mli

@@ -233,7 +233,7 @@ val apply_in :
 val apply_delayed_in :
   advanced_flag -> evars_flag -> Id.t ->
     (clear_flag * delayed_open_constr_with_bindings CAst.t) list ->
-    intro_pattern option -> unit Proofview.tactic
+    intro_pattern option -> unit Proofview.tactic -> unit Proofview.tactic
 
 (** {6 Elimination tactics. } *)
 

test-suite/success/apply.v

@@ -530,6 +530,16 @@ rewrite H0.
 change (x+0=0).
 Abort.
 
+Goal (forall x y, x <= y -> y + x = 0 /\ True)  -> exists x y, (x <= 0 -> y <= 1 -> 0 = 0 /\ 1 = 0).
+intros.
+do 2 eexists.
+intros.
+eapply H in H0 as (H0,_), H1 as (H1,_).
+split.
+- exact H0.
+- exact H1.
+Qed.
+
 (* 2nd order apply used to have delta on local definitions even though
    it does not have delta on global definitions; keep it by
    compatibility while finding a more uniform way to proceed. *)
@@ -582,3 +592,22 @@ intros. eexists ?[p]. split. rewrite H.
 reflexivity.
 exact H0.
 Qed.
+
+(* apply and side conditions: we check that apply in iterates only on
+   the main subgoals *)
+
+Goal (forall x, x=0 -> x>=0 -> x<=0 \/ x<=1) -> 0>=0 -> 1>=0 -> 1=0 -> True.
+intros f H H0 H1.
+apply f in H as [], H0 as [].
+1-3: change (0 <= 0) in H.
+4-6: change (0 <= 1) in H.
+1: change (1 <= 0) in H0.
+4: change (1 <= 0) in H0.
+2: change (1 <= 1) in H0.
+5: change (1 <= 1) in H0.
+1-2,4-5: exact I.
+1,2: exact H1.
+change (0 >= 0) in H.
+change (1 >= 0) in H0.
+exact (eq_refl 0).
+Qed.

user-contrib/Ltac2/tac2tactics.ml

@@ -106,7 +106,7 @@ let apply adv ev cb cl =
   | None -> Tactics.apply_with_delayed_bindings_gen adv ev cb
   | Some (id, cl) ->
     let cl = Option.map mk_intro_pattern cl in
-    Tactics.apply_delayed_in adv ev id cb cl
+    Tactics.apply_delayed_in adv ev id cb cl Tacticals.New.tclIDTAC
 
 let mk_destruction_arg = function
 | ElimOnConstr c ->