rapply

Author: Patrick Nicodemus

STYLE.md

@@ -1197,27 +1197,54 @@ They are described more fully, usually with examples, in the files
 where they are defined.
 
 - `nrefine`, `srefine`, `snrefine`:
-  Defined in `Basics/Overture`, these are shorthands for
+  Defined in `Basics/Tactics`, these are shorthands for
   `notypeclasses refine`, `simple refine`, and `simple notypeclasses refine`.
   It's good to avoid typeclass search if it isn't needed.
 
-- `rapply`, `nrapply`, `srapply`, `snrapply`:
-  Defined in `Basics/Overture`, these tactics use `refine`,
-  `nrefine`, `srefine` and `snrefine`, except that additional holes
-  are added to the function so they behave like `apply` does.
-  The unification algorithm used by `apply` is different and often
-  less powerful than the one used by `refine`, though it is
-  occasionally better at pattern matching.
+- `nrapply`, `rapply`, `tapply`:
+  Defined in `Basics/Tactics`, each of these is similar to `apply`,
+  except that they use the unification engine of `refine`, which
+  is different and often stronger than that of `apply`.
+  `nrapply t` computes the type of `t`
+  (possibly with holes, if `t` has holes) and tries to unify the type
+  of `t` with the goal; if this succeeds, it generates goals for each
+  hole in `t` not solved by unification; otherwise, it repeats this
+  process with `t _`, `t _ _ `, and so on until it has the correct
+  number of arguments to unify with the goal.
+  `rapply` is like `nrapply`, (`rapply` succeeds iff
+  `nrapply` does) except that after it succeeds in unifying with the
+  goal, it solves all typeclass goals it can. `tapply` is stronger
+  than `rapply`: if Coq cannot compute a type for `t` or successfully
+  unify the type of `t` with the goal, it will elaborate all typeclass
+  holes in `t` that it can, and then try again to compute the type of
+  `t` and unify it with the goal. (Like `rapply`, `tapply` also
+  instantiates typeclass goals after successful unification with the
+  goal as well: if `rapply` succeeds, so does `tapply` and their
+  outcomes are equivalent.) 
+  
+- `snrapply`, `srapply`, `stapply`: Sibling tactics to `nrapply`,
+  `rapply` and `tapply`, except that they use `simple refine` instead
+  of `refine` (beta reduction is not attempted when unifying with the
+  goal, and no new goals are shelved)
 
   Here are some tips:
   - If `apply` fails with a unification error you think it shouldn't
-    have, try `nrapply`.
-  - If you want to use type class resolution as well, try `rapply`.
+    have, try `nrapply`, and then `rapply` if `nrapply` generates
+	typeclass goals.
+  - If you want to use type class resolution as well, try `tapply`.
     But it's better to use `nrapply` if it works.
   - You could add a prime to the tactic, to try with many arguments
     first, decreasing the number on each try.
-  - If you don't want Coq to create evars for certain subgoals,
-    add an `s` to the tactic name to make it use `simple refine`.
+  - If you are trying to construct an element of a sum type `sig (A :
+    Type) (P: A->Type)` (or something equivalent, such as a `NatTrans`
+    record consisting of a `Transformation` and a proof that it
+    `Is1Natural`) and you want to manually construct `t : A` first and
+    then prove that `P t` holds for the given `t`, then use the
+    `simple` version of the tactic, like `srapply exist` or `srapply
+    Build_Record`, so that the first goal generated is `A`. If it's
+    more convenient to instantiate `a : A` while proving `P`, then use
+    `rapply exist` - for example, `Goal { x & x = 0 }. rapply exist;
+    reflexivity. Qed.`
 
 - `lhs`, `lhs_V`, `rhs`, `rhs_V`:  Defined in `Basics/Tactics`.
   These are tacticals that apply a specified tactic to one side

theories/Algebra/AbGroups/AbHom.v

@@ -151,10 +151,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 _ _).
-    exact (cate_isretr _).
+    tapply cate_isretr.
   - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
       $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
-    exact (cate_issect _).
+    tapply 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: exact (fmap01_comp _ _ _ _).
+      1,3: tapply fmap01_comp.
       nrapply ab_coeq_glue.
   - snrapply ab_tensor_prod_rec'.
     + intros a.
@@ -811,7 +811,7 @@ Definition ab_tensor_prod_dist_l {A B C : AbGroup}
   : ab_tensor_prod A (ab_biprod B C)
     $<~> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C).
 Proof.
-  srapply (let f := _ in let g := _ in cate_adjointify (A:=AbGroup) f g _ _).
+  stapply (let f := _ in let g := _ in cate_adjointify f g _ _).
   - snrapply ab_tensor_prod_rec.
     + intros a bc.
       exact (tensor a (fst bc), tensor a (snd bc)).

theories/Algebra/AbSES/Core.v

@@ -403,7 +403,7 @@ Proof.
   induction p.
   refine (ap (ap f) (eisretr _ _) @ _).
   nrefine (_ @ ap equiv_path_abses_iso _).
-  2: { refine (path_hom _).
+  2: { tapply 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).
-  refine (path_hom _).
+  tapply path_hom.
   reflexivity.
 Defined.
 
@@ -575,7 +575,7 @@ Proof.
   apply path_sigma_hprop; cbn.
   apply grp_cancelL1.
   refine (ap (fun x => - s x) _ @ _).
-  1: refine (cx_isexact  _ ).
+  1: tapply 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: refine (cx_isexact _).
+  2: tapply 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
@@ -688,10 +688,10 @@ Proof.
   - apply (grp_kernel_corec i).
     exact cx_isexact.
   - apply isequiv_surj_emb.
-    2: refine (cancelL_mapinO _ (grp_kernel_corec _ _) _ _ _).
+    2: tapply (cancelL_mapinO _ (grp_kernel_corec _ _) _).
     intros [y q].
     assert (a : Tr (-1) (hfiber i y)).
-    1: by refine (isexact_preimage _ _ _ _ _).
+    1: by tapply 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^ @ _).
-    refine (cx_isexact _).
+    tapply 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 $@ _) _).
-    exact (gpd_strong_1functor_V _ _). }
+    tapply 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: { refine (isexact_preimage _ _ _ _ _).
+      1: { tapply 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: { refine (isexact_preimage _ _ _ _ _).
+      1: { tapply 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).
-  refine (path_hom _ ).
+  tapply 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) _).
-       exact (gpd_strong_1functor_V _ _). }
+       tapply 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).
-  refine (gpd_moveR_Vh _).
-  refine (gpd_moveL_hM _).
+  tapply gpd_moveR_Vh.
+  tapply gpd_moveL_hM.
   rapply gpd_moveR_Vh.
   intro x.
   srapply equiv_path_pullback_hset; split.

theories/Algebra/AbSES/SixTerm.v

@@ -37,8 +37,7 @@ Proof.
     apply isexact_inclusion_projection. }
   hnf. intros [f q]; rapply contr_inhabited_hprop.
   srefine (tr (_; _)).
-  { refine (grp_homo_compose _
-              (abses_cokernel_iso (inclusion E) (projection E))^-1$).
+  { refine (grp_homo_compose _ (abses_cokernel_iso (inclusion E) (projection E))^-1$).
     apply (quotient_abgroup_rec _ _ f).
     intros e; rapply Trunc_ind.
     intros [b r].

theories/Algebra/Categorical/MonoidObject.v

@@ -278,7 +278,6 @@ End MonoidEnriched.
 
 (** ** Preservation of monoid objects by lax monoidal functors *)
 
-Local Set Typeclasses Depth 2.
 Definition mo_preserved {A B : Type}
   {tensorA : A -> A -> A} {tensorB : B -> B -> B} {IA : A} {IB : B} 
   (F : A -> B) `{IsMonoidalFunctor A B tensorA tensorB IA IB F} (x : A)

theories/Algebra/Universal/Homomorphism.v

@@ -69,7 +69,6 @@ Defined.
 Instance hset_homomorphism `{Funext} {σ} (A B : Algebra σ)
   : IsHSet (A $-> B).
 Proof.
-  Search (IsHSet (SigHomomorphism _ _)).
   apply (istrunc_equiv_istrunc _ (issig_homomorphism A B)).
 Qed.
 

theories/Algebra/ooGroup.v

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

theories/Basics/Tactics.v

@@ -319,14 +319,14 @@ Tactic Notation "nrefine" uconstr(term) := notypeclasses refine term; global_axi
 Tactic Notation "snrefine" uconstr(term) := simple notypeclasses refine term; global_axiom.
 
 (** 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. *)
-(** This tactic is weaker than tapply, and equivalent in strength to nrapply, i.e., it should succeed iff nrapply succeeds, but it solves all possible typeclasses afterward. The implementation is: try nrefine t, t _, t _ _, ... until success; upon success, revert the last (successful) application of nrefine and call refine (t _ _ _). *)
+(** This tactic is weaker than [tapply], and equivalent in strength to [nrapply], i.e., it should succeed iff [nrapply] succeeds, but it solves all possible typeclasses afterward. The implementation is: try [nrefine t, t _, t _ _], ... until success; upon success, revert the last (successful) application of [nrefine] and call [refine (t _ _ _)]. *)
 (** TODO: Find a nicer implementation of this tactic. *)
 Tactic Notation "rapply" uconstr(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 => try (try (nrefine x || fail 2); fail); refine x) term.
 
-(** See comment for rapply. This cannot be simplified to snrefine x because we don't want the global_axiom tactic to run here. *)
+(** See comment for [rapply]. This cannot be simplified to [snrefine x] because we don't want the [global_axiom] tactic to run here. *)
 Tactic Notation "srapply" uconstr(term)
   := do_with_holes ltac:(fun x => try (try (simple notypeclasses refine x || fail 2); fail); srefine x) term.
 Tactic Notation "srapply'" uconstr(term)
@@ -342,12 +342,17 @@ Tactic Notation "snrapply" uconstr(term)
 Tactic Notation "snrapply'" uconstr(term)
   := do_with_holes' ltac:(fun x => snrefine x) term.
 
-(** This tactic is strictly stronger than rapply, because if the type of the argument term t (with holes) cannot be unified with the goal type, it calls typeclass search on all typeclass holes within t (independently of the goal) and then tries to unify with the goal again. Our implementation of rapply requires that the type (with holes) of the argument term unifies with the goal directly, without any help from typeclass search to fill in the holes in the type. The typeclass search after unification is more robust than the typeclass search before unification, because there is more information available to guide the typeclass search. *)
+(** This tactic is strictly stronger than [rapply], because if the type of the argument term [t] (with holes) cannot be unified with the goal type, it calls typeclass search on all typeclass holes within [t] (independently of the goal) and then tries to unify with the goal again. Our implementation of [rapply] requires that the type (with holes) of the argument term unifies with the goal directly, without any help from typeclass search to fill in the holes in the type. The typeclass search after unification is more robust than the typeclass search before unification, because there is more information available to guide the typeclass search. *)
 Tactic Notation "tapply" uconstr(term)
   := do_with_holes ltac:(fun x => refine x) term.
 Tactic Notation "tapply'" uconstr(term)
   := do_with_holes' ltac:(fun x => refine x) term.
 
+Tactic Notation "stapply" uconstr(term)
+  := do_with_holes ltac:(fun x => srefine x) term.
+Tactic Notation "stapply'" uconstr(term)
+  := do_with_holes' ltac:(fun x => srefine x) term.
+
 (** Apply a tactic to one side of an equation.  For example, [lhs rapply lemma].  [tac] should produce a path. *)
 
 Tactic Notation "lhs" tactic3(tac) := nrefine (ltac:(tac) @ _).

theories/Homotopy/CayleyDickson.v

@@ -155,7 +155,7 @@ Defined.
 Global Instance cdi_conjugate_susp_right_inverse {A} `(CayleyDicksonImaginaroid A)
   : RightInverse hspace_op (conjugate_susp A cdi_negate) mon_unit.
 Proof.
-  exact (cds_conjug_right_inv _).
+  stapply cds_conjug_right_inv.
 Defined.
 
 Global Instance cdi_susp_left_identity {A} `(CayleyDicksonImaginaroid A)
@@ -169,7 +169,7 @@ Global Instance cdi_susp_right_identity {A} `(CayleyDicksonImaginaroid A)
 Global Instance cdi_negate_susp_factornegleft {A} `(CayleyDicksonImaginaroid A)
   : FactorNegLeft (negate_susp A cdi_negate) hspace_op.
 Proof.
-  exact (cds_factorneg_l _).
+  stapply cds_factorneg_l.
 Defined.
 
 (** A Cayley-Dickson imaginaroid [A] whose multiplciation on the suspension is associative gives rise to an H-space structure on the join of the suspension of [A] with itself. *)

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).
-  refine (fmap2 (pTr _) _); assumption.
+  tapply (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 _).
-  refine (fmap2 loops _); assumption.
+  tapply (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 _ _).
-    refine (fmap2 loops _).
+    tapply (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: exact (fmap_id loops _).
-    refine (fmap2 loops _).
+    2: tapply (fmap_id loops).
+    tapply (fmap2 loops).
     nrapply peisretr.
 Defined.
 

theories/Homotopy/HomotopyGroup.v

@@ -122,8 +122,8 @@ Proof.
   apply Build_Is0Functor.
   intros X Y f.
   snrapply Build_GroupHomomorphism.
-  { refine (fmap (Tr 0) _).
-    refine (fmap loops _).
+  { tapply (fmap (Tr 0)).
+    tapply (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.
-  refine (emap (pTr 0 o loops) _).
+  tapply (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; exact (isequiv_pi_connmap' _ _).
+  destruct n; tapply isequiv_pi_connmap'.
 Defined.
 
 Definition pequiv_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y)
@@ -340,7 +340,7 @@ Proposition isembedding_pi_psect {n : nat} {X Y : pType}
   : IsEmbedding (fmap (pPi n) s).
 Proof.
   apply isembedding_isinj_hset.
-  refine (isinj_section (r:=fmap (pPi n) r) _).
+  tapply (isinj_section (r:=fmap (pPi n) r)).
   intro x.
   lhs_V refine (fmap_comp (pPi n) s r x).
   lhs refine (fmap2 (pPi n) k x).