rapply

Author: Patrick Nicodemus

theories/Algebra/AbGroups/AbHom.v

@@ -150,10 +150,10 @@ Proof.
   - exact (functor_ab_coeq a^-1$ b^-1$ (hinverse _ _ p) (hinverse _ _ q)).
   - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
       $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
-    rapply cate_isretr.
+      exact (cate_isretr _).
   - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
       $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
-    rapply cate_issect.
+      exact (cate_issect _).
 Defined.
 
 (** ** The bifunctor [ab_hom] *)

theories/Algebra/AbGroups/TensorProduct.v

@@ -695,7 +695,7 @@ Proof.
     + rapply (fmap01 ab_tensor_prod A).
       nrapply ab_coeq_in.
     + refine (_^$ $@ fmap02 ab_tensor_prod _ _ $@ _).
-      1,3: rapply fmap01_comp.
+      1,3: exact (fmap01_comp _ _ _ _).
       nrapply ab_coeq_glue.
   - snrapply ab_tensor_prod_rec'.
     + intros a.

theories/Algebra/AbSES/Core.v

@@ -403,7 +403,7 @@ Proof.
   induction p.
   refine (ap (ap f) (eisretr _ _) @ _).
   nrefine (_ @ ap equiv_path_abses_iso _).
-  2: { rapply path_hom.
+  2: { refine (path_hom _).
        srefine (_ $@ fmap2 _ _).
        2: exact (Id E).
        2: intro x; reflexivity.
@@ -426,7 +426,7 @@ Proof.
   2: apply (abses_ap_fmap g).
   nrefine (_ @ (abses_path_data_compose_beta _ _)^).
   nrapply (ap equiv_path_abses_iso).
-  rapply path_hom.
+  refine (path_hom _).
   reflexivity.
 Defined.
 
@@ -575,7 +575,7 @@ Proof.
   apply path_sigma_hprop; cbn.
   apply grp_cancelL1.
   refine (ap (fun x => - s x) _ @ _).
-  1: rapply cx_isexact.
+  1: refine (cx_isexact  _ ).
   exact (ap _ (grp_homo_unit _) @ grp_inv_unit).
 Defined.
 
@@ -629,7 +629,7 @@ Proof.
   lhs nrapply ab_biprod_functor_beta.
   *)
   nrapply path_prod'.
-  2: rapply cx_isexact.
+  2: refine (cx_isexact _).
   (* The LHS of the remaining goal is definitionally equal to
        (grp_iso_inverse (grp_iso_cxfib (isexact_inclusion_projection E)) $o
          (projection_split_to_kernel E h $o inclusion E)) a
@@ -686,12 +686,12 @@ Lemma abses_kernel_iso `{Funext} {A E B : AbGroup} (i : A $-> E) (p : E $-> B)
 Proof.
   snrapply Build_GroupIsomorphism.
   - apply (grp_kernel_corec i).
-    rapply cx_isexact.
+    refine cx_isexact.
   - apply isequiv_surj_emb.
-    2: rapply (cancelL_mapinO _ (grp_kernel_corec _ _) _).
+    2: refine (cancelL_mapinO _ (grp_kernel_corec _ _) _ _ _).
     intros [y q].
     assert (a : Tr (-1) (hfiber i y)).
-    1: by rapply isexact_preimage.
+    1: by refine (isexact_preimage _ _ _ _ _).
     strip_truncations; destruct a as [a r].
     rapply contr_inhabited_hprop.
     refine (tr (a; _)); cbn.
@@ -732,7 +732,7 @@ Proof.
   - snrapply (quotient_abgroup_rec _ _ g).
     intros e; rapply Trunc_rec; intros [a p].
     refine (ap _ p^ @ _).
-    rapply cx_isexact.
+    refine (cx_isexact _).
   - apply isequiv_surj_emb.
     1: rapply cancelR_conn_map.
     apply isembedding_isinj_hset.

theories/Algebra/AbSES/Pullback.v

@@ -460,7 +460,7 @@ Proof.
     { refine (ap _ (abses_path_data_V p) @ _).
       apply eissect. }
     refine (ap (fun x => x $@ _) _).
-    rapply gpd_strong_1functor_V. }
+    exact (gpd_strong_1functor_V _ _). }
   refine (equiv_path_sigma_hprop _ _ oE _).
   apply equiv_path_groupisomorphism.
 Defined.

theories/Algebra/AbSES/PullbackFiberSequence.v

@@ -105,13 +105,13 @@ Proof.
       revert_opaque f; apply Trunc_rec; intros [f q0].
       (* Since [projection F f] is in the kernel of [projection E], we find a preimage in [B]. *)
       assert (b : merely (hfiber (inclusion E) (projection F f))).
-      1: { rapply isexact_preimage.
+      1: { refine (isexact_preimage _ _ _ _ _).
            exact (ap _ q0 @ q). }
       revert_opaque b; apply Trunc_rec; intros [b q1].
       (* The difference [f - b] in [F] is in the kernel of [projection F], hence lies in [A]. *)
       assert (a : merely (hfiber (inclusion F)
                                  (sg_op f (-(grp_pullback_pr1 _ _ (p^$.1 (ab_biprod_inr b))))))).
-      1: { rapply isexact_preimage.
+      1: { refine (isexact_preimage _ _ _ _ _).
            refine (grp_homo_op _ _ _ @ _).
            refine (ap (fun x => _ + x) (grp_homo_inv _ _) @ _).
            refine (ap (fun x => _ - x) (abses_pullback_inclusion_transpose_beta (inclusion E) F p b @ q1) @ _).
@@ -171,7 +171,7 @@ Proof.
   change (equiv_ptransformation_phomotopy (iscomplex_abses_pullback' _ _ (iscomplex_abses E)) U)
     with (equiv_path_abses_iso ((iscomplex_abses_pullback' _ _ (iscomplex_abses E)).1 U)).
   apply (ap equiv_path_abses_iso).
-  rapply path_hom.
+  refine (path_hom _ ).
   refine (_ $@R abses_pullback_compose' (inclusion E) (projection E) U);
     unfold trans_comp.
   refine (_ $@R abses_pullback_homotopic' (projection E $o inclusion E) grp_homo_const (iscomplex_abses E) U).
@@ -248,7 +248,7 @@ Proof.
        apply eissect. }
   refine (equiv_concat_l _ _ oE _).
   1: { refine (ap (fun x => (x $@ _).1) _).
-       rapply gpd_strong_1functor_V. }
+       exact (gpd_strong_1functor_V _ _). }
   apply equiv_path_groupisomorphism.
 Defined.
 
@@ -366,8 +366,8 @@ Lemma hfiber_cxfib'_induced_path' `{Univalence} {A B C : AbGroup} (E : AbSES C B
   : path_hfiber_cxfib' (hfiber_cxfib'_inhabited E F p) Y.
 Proof.
   exists (hfiber_cxfib'_induced_path'0 E F p Y).
-  rapply gpd_moveR_Vh.
-  rapply gpd_moveL_hM.
+  refine (gpd_moveR_Vh _).
+  refine (gpd_moveL_hM _).
   rapply gpd_moveR_Vh.
   intro x.
   srapply equiv_path_pullback_hset; split.

theories/Algebra/ooGroup.v

@@ -133,7 +133,7 @@ Proof.
   rewrite <- p.
   rewrite !loops_functor_group.
   apply ap.
-  symmetry; rapply (fmap_comp loops).
+  symmetry; exact (fmap_comp loops _ _ _).
 Qed.
 
 Definition grouphom_idmap (G : ooGroup) : ooGroupHom G G
@@ -285,13 +285,13 @@ Global Instance is0functor_group_to_oogroup : Is0Functor group_to_oogroup.
 Proof.
   snrapply Build_Is0Functor.
   intros G H f.
-  by rapply (fmap pClassifyingSpace).
+  by exact (fmap pClassifyingSpace f).
 Defined.
 
 Global Instance is1functor_group_to_oogroup : Is1Functor group_to_oogroup.
 Proof.
   snrapply Build_Is1Functor; hnf; intros.
-  1: by rapply (fmap2 pClassifyingSpace).
-  1: by rapply (fmap_id pClassifyingSpace).
-  by rapply (fmap_comp pClassifyingSpace).
+  1: by exact (fmap2 pClassifyingSpace X).
+  1: by exact (fmap_id pClassifyingSpace _).
+  by exact (fmap_comp pClassifyingSpace _ _).
 Defined.

theories/Basics/Tactics.v

@@ -320,7 +320,7 @@ Tactic Notation "snrefine" uconstr(term) := simple notypeclasses refine term; gl
 
 (** Note that the Coq standard library has a [rapply], but it is like our [rapply'] with many-holes first.  We prefer fewer-holes first, for instance so that a theorem producing an equivalence will by preference be used to produce an equivalence rather than to apply the coercion of that equivalence to a function. *)
 Tactic Notation "rapply" uconstr(term)
-  := do_with_holes ltac:(fun x => refine x) term.
+  := do_with_holes ltac:(fun x => try (try (nrefine x || fail 2); fail); refine x) term.
 Tactic Notation "rapply'" uconstr(term)
   := do_with_holes' ltac:(fun x => refine x) term.
 

theories/Homotopy/Bouquet.v

@@ -82,7 +82,7 @@ Section AssumeUnivalence.
     intros f.
     refine (_ @ @is1natural_equiv_pi1bouquet_rec S _ _ f grp_homo_id).
     simpl; f_ap; symmetry.
-    rapply (cat_idr_strong f).
+    exact (cat_idr_strong f).
   Defined.
 
 End AssumeUnivalence.

theories/Homotopy/EMSpace.v

@@ -62,7 +62,7 @@ Section EilenbergMacLane.
     : pTr n.+2 X <~>* pTr n.+2 (loops (psusp X)).
   Proof.
     snrapply Build_pEquiv.
-    1: rapply (fmap (pTr _) (loop_susp_unit _)).
+    1: exact (fmap (pTr _) (loop_susp_unit _)).
     nrapply O_inverts_conn_map.
     nrapply (isconnmap_pred_add n.-2).
     rewrite 2 trunc_index_add_succ.

theories/Homotopy/ExactSequence.v

@@ -48,7 +48,7 @@ Definition iscomplex_ptr (n : trunc_index) {F X Y : pType}
 Proof.
   refine ((fmap_comp (pTr n) i f)^* @* _).
   refine (_ @* ptr_functor_pconst n).
-  rapply (fmap2 (pTr _)); assumption.
+  refine (fmap2 (pTr _) _); assumption.
 Defined.
 
 (** Loop spaces preserve complexes. *)
@@ -57,7 +57,7 @@ Definition iscomplex_loops {F X Y : pType}
   : IsComplex (fmap loops i) (fmap loops f).
 Proof.
   refine ((fmap_comp loops i f)^$ $@ _ $@ fmap_zero_morphism _).
-  rapply (fmap2 loops); assumption.
+  refine (fmap2 loops _); assumption.
 Defined.
 
 Definition iscomplex_iterated_loops {F X Y : pType}
@@ -387,7 +387,7 @@ Proof.
     (isexact_purely_fiberseq (fiberseq_loops (fiberseq_isexact_purely i f)))).
   transitivity (fmap loops (pfib f) o* fmap loops (cxfib cx_isexact)).
   - refine (_ @* fmap_comp loops _ _).
-    rapply (fmap2 loops).
+    refine (fmap2 loops _).
     symmetry; apply pfib_cxfib.
   - refine (_ @* pmap_compose_assoc _ _ _).
     refine (pmap_prewhisker (fmap loops (cxfib cx_isexact)) _).

theories/Homotopy/HSpace/Core.v

@@ -151,8 +151,8 @@ Proof.
     exact (fmap loops (pmap_hspace_left_op a o* (pequiv_hspace_left_op pt)^-1*)).
   - lazy beta.
     transitivity (fmap (b:=A) loops pmap_idmap).
-    2: rapply (fmap_id loops).
-    rapply (fmap2 loops).
+    2: exact (fmap_id loops _).
+    refine (fmap2 loops _).
     nrapply peisretr.
 Defined.
 

theories/Homotopy/HomotopyGroup.v

@@ -122,8 +122,8 @@ Proof.
   apply Build_Is0Functor.
   intros X Y f.
   snrapply Build_GroupHomomorphism.
-  { rapply (fmap (Tr 0)).
-    rapply (fmap loops).
+  { refine (fmap (Tr 0) _).
+    refine (fmap loops _).
     assumption. }
   (** Note: we don't have to be careful about which paths we choose here since we are trying to inhabit a proposition. *)
   intros x y.
@@ -197,7 +197,7 @@ Definition pi_loops n X : Pi n.+1 X <~>* Pi n (loops X).
 Proof.
   destruct n.
   1: reflexivity.
-  rapply (emap (pTr 0 o loops)).
+  refine (emap (pTr 0 o loops) _).
   apply unfold_iterated_loops'.
 Defined.
 
@@ -289,7 +289,7 @@ Global Instance isequiv_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X
   : IsEquiv (fmap (pPi n) f).
 Proof.
   (* For [n = 0] and [n] a successor, [fmap (pPi n) f] is definitionally equal to the map in the previous result as a map of types. *)
-  destruct n; rapply isequiv_pi_connmap'.
+  destruct n; exact (isequiv_pi_connmap' _ _).
 Defined.
 
 Definition pequiv_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y)
@@ -340,10 +340,10 @@ Proposition isembedding_pi_psect {n : nat} {X Y : pType}
   : IsEmbedding (fmap (pPi n) s).
 Proof.
   apply isembedding_isinj_hset.
-  rapply (isinj_section (r:=fmap (pPi n) r)).
+  refine (isinj_section (r:=fmap (pPi n) r) _).
   intro x.
-  lhs_V rapply (fmap_comp (pPi n) s r x).
-  lhs rapply (fmap2 (pPi n) k x).
+  lhs_V refine (fmap_comp (pPi n) s r x).
+  lhs refine (fmap2 (pPi n) k x).
   exact (fmap_id (pPi n) X x).
 Defined.
 

theories/Homotopy/Hopf.v

@@ -42,7 +42,7 @@ Proof.
       snrapply equiv_functor_sigma_id.
       intros x.
       exact (Build_Equiv _ _ (.* x) _). }
-    1,2: rapply (equiv_contr_sigma (Unit_ind (pointed_type X))).
+    1,2: exact (equiv_contr_sigma (Unit_ind (pointed_type X))).
     1,2: reflexivity. }
   reflexivity.
 Defined.
@@ -183,9 +183,9 @@ Definition pequiv_ptr_psusp_loops `{Univalence} (X : pType) (n : nat) `{IsConnec
   : pTr n.+2 (psusp (loops X)) <~>* pTr n.+2 X.
 Proof.
   snrapply Build_pEquiv.
-  1: rapply (fmap (pTr _) (loop_susp_counit _)).
+  1: exact (fmap (pTr _) (loop_susp_counit _)).
   nrapply O_inverts_conn_map.
   nrapply (isconnmap_pred_add n.-2).
   rewrite 2 trunc_index_add_succ.
-  rapply (conn_map_loop_susp_counit X).
+  exact (conn_map_loop_susp_counit X).
 Defined.

theories/Homotopy/InjectiveTypes/TypeFamKanExt.v

@@ -31,14 +31,14 @@ Section UniverseStructure.
     (P : X -> Type@{w}) (j : X -> Y) (isem : IsEmbedding@{u v uv} j) (x : X)
     : Equiv@{uvw w} (LeftKanFam@{} P j (j x)) (P x).
   Proof.
-    rapply (@equiv_contr_sigma (hfiber j (j x)) _ _).
+    exact (@equiv_contr_sigma (hfiber j (j x)) _ _).
   Defined.
 
   Definition isext_equiv_rightkanfam@{} `{Funext} {X : Type@{u}} {Y : Type@{v}}
     (P : X -> Type@{w}) (j : X -> Y) (isem : IsEmbedding@{u v uv} j) (x : X)
     : Equiv@{uvw w} (RightKanFam@{} P j (j x)) (P x).
   Proof.
-    rapply (@equiv_contr_forall _ (hfiber j (j x)) _ _).
+    exact (@equiv_contr_forall _ (hfiber j (j x)) _ _).
   Defined.
 
   Definition isext_leftkanfam@{suvw | uvw < suvw} `{Univalence} {X : Type@{u}} {Y : Type@{v}}

theories/Homotopy/Join/Core.v

@@ -691,7 +691,7 @@ Section JoinSym.
   Definition equiv_join_sym' (A B : Type)
     : Join A B <~> Join B A.
   Proof.
-    rapply (opyon_equiv_0gpd (A:=Type)).
+    refine (opyon_equiv_0gpd (A:=Type) _).
     apply joinrecdata_fun_sym.
   Defined.
 
@@ -725,7 +725,7 @@ Section JoinSym.
   Proof.
     symmetry.
     (** Both sides are [join_rec] applied to [JoinRecData]: *)
-    rapply (fmap join_rec).
+    refine (fmap join_rec _).
     bundle_joinrecpath; intros; cbn.
     refine (ap inverse _).
     apply ap_idmap.

theories/Homotopy/Join/JoinAssoc.v

@@ -80,7 +80,7 @@ Definition trijoinrecdata_fun_twist (A B C : Type)
 Definition equiv_trijoin_twist' (A B C : Type)
   : TriJoin A B C <~> TriJoin B A C.
 Proof.
-  rapply (opyon_equiv_0gpd (A:=Type)).
+  refine (opyon_equiv_0gpd (A:=Type) _).
   apply trijoinrecdata_fun_twist.
 Defined.
 
@@ -122,7 +122,7 @@ Definition trijoin_twist_homotopic (A B C : Type)
 Proof.
   symmetry.
   (** Both sides are [trijoin_rec] applied to [TriJoinRecData]: *)
-  rapply (fmap trijoin_rec).
+  refine (fmap trijoin_rec _).
   bundle_trijoinrecpath; intros; cbn.
   1: refine (ap inverse _).
   1, 2, 3: apply ap_idmap.
@@ -375,7 +375,7 @@ Definition hexagon_join_twist_sym A B C
     == trijoin_twist B C A o trijoin_id_sym B A C o trijoin_twist A B C.
 Proof.
   (* It's enough to show that both sides induces the same natural transformation under the covariant Yoneda embedding, i.e., after postcomposing with a general function [f]. *)
-  rapply (opyon_faithful_0gpd (A:=Type)).
+  refine (opyon_faithful_0gpd (A:=Type) _ _ _ _ _).
   intros P f.
   (* We replace [f] by [trijoin_rec t] for generic [t].  This will allow induction later. *)
   pose proof (p := issect_trijoin_rec_inv f).

theories/Homotopy/Join/TriJoin.v

@@ -793,7 +793,7 @@ Definition functor2_trijoin {A B C A' B' C'}
   : functor_trijoin f g h == functor_trijoin f' g' h'.
 Proof.
   unfold functor_trijoin.
-  rapply (fmap trijoin_rec).
+  refine (fmap trijoin_rec _).
   apply (trijoinrecdata_tricomp2 _ p q r).
 Defined.
 

theories/Homotopy/WhiteheadsPrinciple.v

@@ -104,7 +104,7 @@ Proof.
     intros y q. destruct q.
     snrefine (isequiv_homotopic _ _).
     1: exact (fmap (Pi k.+1) (fmap loops (pmap_from_point f x))).
-    2:{ rapply (fmap2 (Pi k.+1)); srefine (Build_pHomotopy _ _).
+    2:{ refine (fmap2 (Pi k.+1) _); srefine (Build_pHomotopy _ _).
         - intros p; cbn.
           refine (concat_1p _ @ concat_p1 _).
         - reflexivity. }

theories/Modalities/Topological.v

@@ -119,13 +119,13 @@ Proof.
           intros x; unfold composeD; cbn.
           apply equiv_path_arrow. }
         refine ((isconnected_elim (Nul D) (A := D (inl a)) _ _).1).
-        { rapply isconnected_acc_ngen. }
+        { exact (isconnected_acc_ngen _ _). }
         intros b; cbn in b. strip_truncations.
         assert (bc : IsConnMap (Nul D) (unit_name b)).
         { intros x; unfold hfiber.
           apply (isconnected_equiv (Nul D) (b = x)
                                    (equiv_contr_sigma _)^-1).
-          rapply (isconnected_acc_ngen (Nul D) (inr (a;(b,x)))). }
+          exact (isconnected_acc_ngen (Nul D) (inr (a;(b,x)))). }
         pose (p := conn_map_elim (Nul D) (unit_name b)
                                  (fun u => f b = f u) (fun _ => 1)).
         apply (Build_Contr _ (f b ; p)); intros [x q].