Changed other tactics.

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 _ _).
-      exact (cate_isretr _).
+    exact (cate_isretr _).
   - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
       $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
-      exact (cate_issect _).
+    exact (cate_issect _).
 Defined.
 
 (** ** The bifunctor [ab_hom] *)

theories/Algebra/AbGroups/TensorProduct.v

@@ -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 f g _ _).
+  srapply (let f := _ in let g := _ in cate_adjointify (A:=AbGroup) f g _ _).
   - snrapply ab_tensor_prod_rec.
     + intros a bc.
       exact (tensor a (fst bc), tensor a (snd bc)).

theories/Algebra/AbSES/Core.v

@@ -686,7 +686,7 @@ Lemma abses_kernel_iso `{Funext} {A E B : AbGroup} (i : A $-> E) (p : E $-> B)
 Proof.
   snrapply Build_GroupIsomorphism.
   - apply (grp_kernel_corec i).
-    refine cx_isexact.
+    exact cx_isexact.
   - apply isequiv_surj_emb.
     2: refine (cancelL_mapinO _ (grp_kernel_corec _ _) _ _ _).
     intros [y q].

theories/Basics/Tactics.v

@@ -319,15 +319,18 @@ 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 _ _ _). *)
+(** 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 => refine x) 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. *)
 Tactic Notation "srapply" uconstr(term)
-  := do_with_holes ltac:(fun x => srefine x) term.
+  := do_with_holes ltac:(fun x => try (try (simple notypeclasses refine x || fail 2); fail); srefine x) term.
 Tactic Notation "srapply'" uconstr(term)
-  := do_with_holes' ltac:(fun x => srefine x) term.
+  := do_with_holes' ltac:(fun x => try (try (simple notypeclasses refine x || fail 2); fail); srefine x) term.
 
 Tactic Notation "nrapply" uconstr(term)
   := do_with_holes ltac:(fun x => nrefine x) term.
@@ -339,6 +342,12 @@ 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. *)
+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.
+
 (** 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

@@ -149,13 +149,13 @@ Global Instance cds_susp_cdi {A} `(CayleyDicksonImaginaroid A)
 Global Instance cdi_conjugate_susp_left_inverse {A} `(CayleyDicksonImaginaroid A)
   : LeftInverse hspace_op (conjugate_susp A cdi_negate) mon_unit.
 Proof.
-  srapply cds_conjug_left_inv.
+  exact cds_conjug_left_inv.
 Defined.
 
 Global Instance cdi_conjugate_susp_right_inverse {A} `(CayleyDicksonImaginaroid A)
   : RightInverse hspace_op (conjugate_susp A cdi_negate) mon_unit.
 Proof.
-  srapply cds_conjug_right_inv.
+  exact (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.
-  srapply cds_factorneg_l.
+  exact (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/Pointed/Core.v

@@ -994,8 +994,8 @@ Defined.
 (** pType has equivalences *)
 Global Instance hasequivs_ptype : HasEquivs pType.
 Proof.
-  srapply (
-    Build_HasEquivs _ _ _ _ _ pEquiv (fun A B f => IsEquiv f));
+  snrapply (
+    Build_HasEquivs _ isgraph_ptype _ _ _ pEquiv (fun A B f => IsEquiv f));
   intros A B f; cbn; intros.
   - exact f.
   - exact _.

theories/WildCat/ZeroGroupoid.v

@@ -129,7 +129,7 @@ Definition isequiv_0gpd_issurjinj {G H : ZeroGpd} (F : G $-> H)
   : Cat_IsBiInv F.
 Proof.
   destruct e as [e0 e1]; unfold SplEssSurj in e0.
-  srapply catie_adjointify.
+  srapply (catie_adjointify (H0:=hasequivs_0gpd)).
   - snrapply Build_Morphism_0Gpd.
     1: exact (fun y => (e0 y).1).
     snrapply Build_Is0Functor; cbn beta.