Simpler definition of refine

Author: Patrick Nicodemus

theories/Algebra/AbGroups/Abelianization.v

@@ -248,7 +248,7 @@ Section AbelGroup.
     intros x y z; cbn beta.
     lhs nrapply ap.
     2: rhs nrapply ap.
-    1,3: lhs rapply inverse_sg_op; nrapply (ap (.* _)); rapply inverse_sg_op.
+    1,3: lhs apply inverse_sg_op; nrapply (ap (.* _)); rapply inverse_sg_op.
     change (abel_in z^ * abel_in y^ * abel_in x^
       = abel_in y^ * abel_in z^ * abel_in x^).
     apply (ap (.* _)).

theories/Algebra/AbSES/Core.v

@@ -734,7 +734,7 @@ Proof.
     refine (ap _ p^ @ _).
     refine (cx_isexact _).
   - apply isequiv_surj_emb.
-    1: rapply cancelR_conn_map.
+    1: exact (cancelR_conn_map _ _ _).
     apply isembedding_isinj_hset.
     srapply Quotient_ind2_hprop; intros x y.
     intro p.

theories/Algebra/AbSES/PullbackFiberSequence.v

@@ -396,6 +396,6 @@ Proof.
   srapply (equiv_ind (equiv_hfiber_abses (abses_pullback (inclusion E)) (point (AbSES B A)))).
   intros [F p].
   rapply contr_equiv'.
-  1: apply equiv_hfiber_cxfib'.
+  2: apply equiv_hfiber_cxfib'.
   apply contr_hfiber_cxfib'.
 Defined.

theories/Algebra/AbSES/Pushout.v

@@ -77,7 +77,7 @@ Definition abses_pushout_morphism_rec `{Univalence} {A B X Y : AbGroup}
 Proof.
   snrapply (Build_AbSESMorphism grp_homo_id _ (component3 f)).
   - rapply ab_pushout_rec.
-    apply left_square.
+    3: apply left_square.
   - intro x; simpl.
     rewrite grp_homo_unit.
     exact (right_identity _)^.

theories/Algebra/AbSES/SixTerm.v

@@ -18,7 +18,7 @@ Definition isexact_abses_sixterm_i `{Funext}
 Proof.
   apply isexact_purely_O.
   rapply isexact_homotopic_i.
-  2: apply iff_grp_isexact_isembedding.
+  3: apply iff_grp_isexact_isembedding.
   1: by apply phomotopy_homotopy_hset.
   exact _. (* [isembedding_precompose_surjection_ab] *)
 Defined.

theories/Algebra/Groups/FreeProduct.v

@@ -367,8 +367,7 @@ Section FreeProduct.
       { refine (word_inverse_ww _ _ @ _).
         apply ap; simpl.
         rapply (ap (fun s => [s])).
-        apply ap.
-        apply inverse_sg_op. }
+        2:apply ap, inverse_sg_op. }
       simpl.
       refine (ap amal_eta _^ @ _ @ ap amal_eta _).
       1,3: apply app_assoc.
@@ -380,8 +379,7 @@ Section FreeProduct.
       { refine (word_inverse_ww _ _ @ _).
         apply ap; simpl.
         rapply (ap (fun s => [s])).
-        apply ap.
-        apply inverse_sg_op. }
+        2: apply ap, inverse_sg_op. }
       simpl.
       refine (ap amal_eta _^ @ _ @ ap amal_eta _).
       1,3: apply app_assoc.
@@ -391,7 +389,7 @@ Section FreeProduct.
       1,3: refine (word_inverse_ww _ _ @ ap (fun s => s ++ _) _).
       1,2: cbn; refine (ap _ _).
       1,2: rapply (ap (fun s => [s])).
-      1,2: apply ap.
+      2,4: apply ap.
       1,2: symmetry; apply grp_homo_inv.
       refine (ap amal_eta _^ @ _ @ ap amal_eta _).
       1,3: apply app_assoc.
@@ -482,8 +480,8 @@ Section FreeProduct.
       refine (_ @ _).
       { apply ap, ap.
         rapply (ap (fun x => x ++ _)).
-        rapply (ap (fun x => [x])).
-        apply ap.
+        2: rapply (ap (fun x => [x])).
+        2: apply ap.
         apply right_inverse. }
       apply amal_omega_H.
     +  cbn.
@@ -499,8 +497,8 @@ Section FreeProduct.
       refine (_ @ _).
       { apply ap, ap.
         rapply (ap (fun x => x ++ _)).
-        rapply (ap (fun x => [x])).
-        apply ap.
+        2: rapply (ap (fun x => [x])).
+        2: apply ap.
         apply right_inverse. }
       apply amal_omega_K.
   Defined.

theories/Algebra/Groups/ShortExactSequence.v

@@ -21,7 +21,7 @@ Proposition grp_iso_cxfib_beta {A B C : Group} {i : A $-> B} {f : B $-> C}
   : i $o (grp_iso_inverse (grp_iso_cxfib ex)) $== subgroup_incl (grp_kernel f).
 Proof.
   rapply equiv_ind.
-  1: exact (isequiv_cxfib ex).
+  3: exact (isequiv_cxfib ex).
   intro x.
   exact (ap (fun y => i y) (eissect _ x)).
 Defined.

theories/Algebra/Rings/CRing.v

@@ -29,7 +29,7 @@ Definition Build_CRing' (R : AbGroup) `(!One R, !Mult R)
   : CRing.
 Proof.
   snrapply Build_CRing.
-  - rapply (Build_Ring R); only 1,2,4: exact _.
+  - rapply (Build_Ring R). 
     + intros x y z.
       lhs nrapply comm.
       lhs rapply dist_l.
@@ -133,7 +133,7 @@ Section IdealCRing.
     2: rapply ideal_sum_self.
     etransitivity.
     2: rapply ideal_sum_subset_pres_r.
-    2: rapply ideal_product_comm.
+    3: rapply ideal_product_comm.
     apply ideal_product_intersection_sum_subset.
   Defined.
 

theories/Algebra/Rings/ChineseRemainder.v

@@ -147,7 +147,7 @@ Theorem chinese_remainder_prod `{Univalence}
 Proof.
   etransitivity.
   { rapply rng_quotient_invar.
-    symmetry.
-    rapply ideal_intersection_is_product. }
+    2: symmetry; rapply ideal_intersection_is_product. 
+  }
   rapply chinese_remainder.
 Defined.

theories/Algebra/Rings/Ideal.v

@@ -1096,12 +1096,12 @@ Section IdealLemmas.
     1: rapply ideal_dist_l.
     etransitivity.
     1: rapply ideal_sum_subset_pres_r.
-    1: rapply ideal_product_subset_pres_l.
-    1: apply ideal_intersection_subset_l.
+    2: rapply ideal_product_subset_pres_l.
+    2: apply ideal_intersection_subset_l.
     etransitivity.
     1: rapply ideal_sum_subset_pres_l.
-    1: rapply ideal_product_subset_pres_l.
-    1: apply ideal_intersection_subset_r.
+    2: rapply ideal_product_subset_pres_l.
+    2: apply ideal_intersection_subset_r.
     rapply ideal_sum_comm.
   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 => try (try (nrefine x || fail 2); fail); refine x) term.
+  := do_with_holes (ltac:(fun x => unshelve nrefine x; try typeclasses eauto)) term.
 Tactic Notation "rapply'" uconstr(term)
   := do_with_holes' ltac:(fun x => refine x) term.
 

theories/Classes/implementations/binary_naturals.v

@@ -476,26 +476,26 @@ Section decidable.
     intros p.
     change ((fun x => match x with | double1 y => Unit | _ => Empty end) bzero).
     rapply (@transport binnat).
-    - exact p^.
-    - exact tt.
+    2: exact p^.
+    exact tt.
   Qed.
 
   Local Definition ineq_bzero_double2 n : bzero <> double2 n.
   Proof.
     intros p.
     change ((fun x => match x with | double2 y => Unit | _ => Empty end) bzero).
     rapply (@transport binnat).
-    - exact p^.
-    - exact tt.
+    2: exact p^.
+    exact tt.
   Qed.
 
   Local Definition ineq_double1_double2 m n : double1 m <> double2 n.
   Proof.
     intros p.
     change ((fun x => match x with | double2 y => Unit | _ => Empty end) (double1 m)).
     rapply (@transport binnat).
-    - exact p^.
-    - exact tt.
+    2: exact p^.
+    exact tt.
   Qed.
 
   Local Definition undouble (m : binnat) : binnat :=

theories/Classes/theory/rings.v

@@ -254,9 +254,9 @@ Section ring_props.
   Lemma negate_swap_r : forall x y, x - y = -(y - x).
   Proof.
     intros; symmetry.
-    lhs rapply groups.inverse_sg_op.
-    f_ap.
-    apply involutive.
+    Set Printing Implicit.
+    lhs apply groups.inverse_sg_op.
+    f_ap; apply involutive.
   Defined.
 
   Lemma negate_swap_l x y : -x + y = -(x - y).
@@ -465,7 +465,7 @@ Section ringmor_props.
 
   Definition preserves_negate x : f (- x) = - f x.
   Proof.
-    rapply preserves_inverse.
+    apply preserves_inverse.
   Defined.
 
   Lemma preserves_minus x y : f (x - y) = f x - f y.

theories/Colimits/Coeq.v

@@ -26,8 +26,7 @@ Definition Coeq_ind {B A f g} (P : @Coeq B A f g -> Type)
   : forall w, P w.
 Proof.
   rapply GraphQuotient_ind.
-  intros a b [x [[] []]].
-  exact (cglue' x).
+  2: intros a b [x [[] []]]; exact (cglue' x).
 Defined.
 
 Lemma Coeq_ind_beta_cglue {B A f g} (P : @Coeq B A f g -> Type)
@@ -43,8 +42,7 @@ Definition Coeq_rec {B A f g} (P : Type) (coeq' : A -> P)
   : @Coeq B A f g -> P.
 Proof.
   rapply GraphQuotient_rec.
-  intros a b [x [[] []]].
-  exact (cglue' x).
+  2: intros a b [x [[] []]]; exact (cglue' x).
 Defined.
 
 Definition Coeq_rec_beta_cglue {B A f g} (P : Type) (coeq' : A -> P)

theories/Colimits/CoeqUnivProp.v

@@ -128,10 +128,7 @@ Section UnivPropNat.
 
   (** Help Coq find the same graph structure for the sigma-groupoid of [Coeq_ind_data] when precomposing with [functor_coeq]. *)
   Local Instance isgraph_Coeq_ind_data_total
-    : IsGraph (sig (Coeq_ind_data f g (P o functor_coeq h k p q))).
-  Proof.
-    rapply isgraph_total.
-  Defined.
+    : IsGraph (sig (Coeq_ind_data f g (P o functor_coeq h k p q))) := isgraph_total _.
 
   (** Given a map out of [A'] that coequalizes the parallel pair [f'] and [g'], we construct a map out of [A] that coequalizes [f] and [g]. Precomposing with [k] yields a dependent map [forall a : A, P (coeq (k a))], and [functor_coeq_beta_cglue] gives us a way to relate the paths. *)
   Definition functor_Coeq_ind_data

theories/Colimits/Colimit_Flattening.v

@@ -226,7 +226,6 @@ Section Flattening.
     srapply colimit_unicity.
     3: apply iscolimit_colimit.
     rapply Build_IsColimit.
-    apply unicocone_cocone_E'.
   Defined.
 
 End Flattening.

theories/Colimits/Sequential.v

@@ -42,8 +42,8 @@ Proof.
     intros n.
     exact (const (a n.+1)). }
   rapply contr_equiv'.
-  1: rapply equiv_functor_colimit.
-  1: rapply (equiv_sequence B A).
+  2: rapply equiv_functor_colimit.
+  2: rapply (equiv_sequence B A).
   1: reflexivity.
   { intros n e.
     exists equiv_idmap.

theories/Extensions.v

@@ -719,9 +719,9 @@ Proof.
              ExtendableAlong 1 cyl (fun x:Cyl h => DPath C' (cglue x) (u x) (v x))).
   { intros u v.
     rapply extendable_postcompose'.
-    2:{ rapply (cancelL_extendable 1 _ cyl pr_cyl).
-        - rapply extendable_equiv.
-        - exact (eh (fun x => cglue x # u (cyr x)) (v o cyr)). }
+    3:{ rapply (cancelL_extendable 1 _ cyl pr_cyl).
+        2: rapply extendable_equiv.
+        2: exact (eh (fun x => cglue x # u (cyr x)) (v o cyr)). }
     intros x; subst C'.
     refine ((dp_compose (pr_cylcoeq p q) C _)^-1 oE _).
     symmetry; srapply equiv_ds_fill_lr.

theories/HFiber.v

@@ -126,7 +126,7 @@ Definition hfiber_functor_hfiber {A B C D}
   : hfiber (functor_hfiber p b) (c;q)
     <~> hfiber (functor_hfiber (fun x => (p x)^) c) (b;q^).
 Proof.
-  rapply (equiv_functor_sigma_id _ oE _ oE (equiv_functor_sigma_id _)^-1).
+  refine (equiv_functor_sigma_id _ oE _ oE (equiv_functor_sigma_id _)^-1).
   1,3:intros; rapply equiv_path_sigma.
   refine (equiv_sigma_assoc _ _ oE _ oE (equiv_sigma_assoc _ _)^-1).
   apply equiv_functor_sigma_id; intros a; cbn.

theories/Homotopy/BlakersMassey.v

@@ -266,7 +266,7 @@ Now we claim that the left-hand map of this span is also an equivalence.  Rather
           etransitivity.
           2:{ rapply equiv_functor_sigma_id; intros s.
               (** Here's frobnicate showing up again! *)
-              apply frobnicate. }
+              2: apply frobnicate. }
           make_equiv.
         Defined.
 

theories/Homotopy/ClassifyingSpace.v

@@ -96,8 +96,8 @@ Section Eliminators.
     intros x y.
     apply ds_const'.
     rapply sq_GGcc.
-    2: refine (_ @ ap _ (dp_const_pp _ _)).
-    1,2: symmetry; apply eissect.
+    4: refine (_ @ ap _ (dp_const_pp _ _)).
+    3, 4: symmetry; apply eissect.
     by apply sq_G1.
   Defined.
 
@@ -479,7 +479,7 @@ Proof.
       intro x.
       rapply equiv_sq_dp^-1.
       simpl.
-      rapply sq_ccGG.
+      refine (sq_ccGG _ _ _).
       1,2: symmetry.
       2: refine (ap_compose (ClassifyingSpace_rec _ _ _ (fun x y =>
         ap bloop (grp_homo_op g x y) @ bloop_pp (g x) (g y))) _ (bloop x)
@@ -510,7 +510,7 @@ Proof.
         rapply equiv_sq_dp^-1.
         rewrite ClassifyingSpace_rec_beta_bloop.
         simpl.
-        rapply sq_ccGc.
+        refine (sq_ccGc _ _).
         1: symmetry; rapply decode_encode.
         apply equiv_sq_path.
         rewrite concat_pp_p.
@@ -566,7 +566,7 @@ Proof.
   snrapply (cancelR_isequiv bloop).
   1: exact _.
   rapply isequiv_homotopic'; symmetry.
-  nrapply pClassifyingSpace_rec_beta_bloop.
+  2: nrapply pClassifyingSpace_rec_beta_bloop.
 Defined.
 
 Lemma natequiv_bg_pi1_adjoint `{Univalence} (X : pType) `{IsConnected 0 X}

theories/Homotopy/ExactSequence.v

@@ -151,7 +151,6 @@ Global Instance ishprop_isexact_hset `{Univalence} {F X Y : pType} `{IsHSet Y}
   : IsHProp (IsExact n i f).
 Proof.
   rapply (transport (fun A => IsHProp A) (x := { cx : IsComplex i f & IsConnMap n (cxfib cx) })).
-  2: exact _.
   apply path_universe_uncurried; issig.
 Defined.
 
@@ -288,7 +287,6 @@ Global Instance isequiv_cxfib {O : Modality} {F X Y : pType} {i : F ->* X} {f :
   : IsEquiv (cxfib cx_isexact).
 Proof.
   rapply isequiv_conn_ino_map.
-  1: apply ex.
   rapply (cancelL_mapinO _ _ pr1).
 Defined.
 
@@ -302,7 +300,7 @@ Proposition equiv_cxfib_beta {F X Y : pType} {i : F ->* X} {f : X ->* Y}
   : i o pequiv_inverse (equiv_cxfib ex) == pfib _.
 Proof.
   rapply equiv_ind.
-  1: exact (isequiv_cxfib ex).
+  3: exact (isequiv_cxfib ex).
   intro x.
   exact (ap (fun g => i g) (eissect _ x)).
 Defined.
@@ -555,7 +553,7 @@ Definition classify_fiberseq `{Univalence} {Y F : pType@{u}}
 Proof.
   refine (_ oE _).
   (** To apply [equiv_sigma_pfibration] we need to invert the equivalence on the fiber. *)
-  { do 2 (rapply equiv_functor_sigma_id; intro).
+  { do 2 (refine (equiv_functor_sigma_id _); intro).
     apply equiv_pequiv_inverse. }
   exact ((equiv_sigma_assoc _ _)^-1 oE equiv_sigma_pfibration).
 Defined.

theories/Homotopy/IdentitySystems.v

@@ -76,7 +76,7 @@ Definition contr_sigma_equiv_path {A : Type} {a0 : A}
   : Contr (sig R).
 Proof.
   rapply contr_equiv'.
-  1: exact (equiv_functor_sigma_id f).
+  2: exact (equiv_functor_sigma_id f).
   apply contr_basedpaths.
 Defined.
 

theories/Limits/Pullback.v

@@ -187,7 +187,7 @@ Proof.
   unfold IsPullback.
   apply isequiv_contr_map; intro x.
   rapply contr_equiv'.
-  - symmetry; apply hfiber_pullback_corec.
+  2: symmetry; apply hfiber_pullback_corec.
   - exact _.
 Defined.
 
@@ -417,11 +417,11 @@ Section Pullback3x3.
   Theorem pullback3x3 : Pullback fX1 fX3 <~> Pullback f1X f3X.
   Proof.
     refine (_ oE _ oE _).
-    1,3:do 2 (rapply equiv_functor_sigma_id; intro).
+    1,3:do 2 (refine (equiv_functor_sigma_id _); intro).
     1:apply equiv_path_pullback.
     1:symmetry; apply equiv_path_pullback.
     refine (_ oE _).
-    { do 4 (rapply equiv_functor_sigma_id; intro).
+    { do 4 (refine (equiv_functor_sigma_id _); intro).
       refine (sq_tr oE _).
       refine (sq_move_14^-1 oE _).
       refine (sq_move_31 oE _).