Merge pull request #2241 from patrick-nicodemus/rapply_timing

Alternate definitions of rapply

Author: Alizter

STYLE.md

@@ -932,7 +932,7 @@ Here are some acceptable tactics to use in transparent definitions
 - `case`, `elim`, `destruct`, `induction`
 - `apply`, `eapply`, `assumption`, `eassumption`, `exact`
 - `refine`, `nrefine`, `srefine`, `snrefine` (see below for the last three)
-- `rapply`, `nrapply`, `srapply`, `snrapply` (see below)
+- `rapply`, `napply`, `tapply`, `srapply`, `snapply`, `stapply` (see below)
 - `lhs`, `lhs_V`, `rhs`, `rhs_V`
 - `reflexivity`, `symmetry`, `transitivity`, `etransitivity`
 - `by`, `done`
@@ -1197,31 +1197,58 @@ 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.
+- `napply`, `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`.
+  `napply 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 `napply`, (`rapply` succeeds iff
+  `napply` 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.) 
+  
+- `snapply`, `srapply`, `stapply`: Sibling tactics to `napply`,
+  `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`.
-    But it's better to use `nrapply` if it works.
+    have, try `napply`, and then `rapply` if `napply` generates
+	typeclass goals.
+  - If you want to use type class resolution as well, try `tapply`.
+    But it's better to use `napply` 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
-  of an equality.  E.g. `lhs nrapply concat_1p.`
+  of an equality.  E.g. `lhs napply concat_1p.`
 
 - `transparent assert`: Defined in `Basics/Overture`, this tactic is
   like `assert` but produces a transparent subterm rather than an

contrib/HoTTBookExercises.v

@@ -723,8 +723,8 @@ Section Book_2_17_prod.
     : Book_2_17_ii_prod = Book_2_17_i_prod.
   Proof.
     apply path_equiv; simpl.
-    lhs nrapply Book_2_17_eq_prod'.
-    snrapply ap011.
+    lhs napply Book_2_17_eq_prod'.
+    snapply ap011.
     - apply transport_idmap_path_universe_uncurried.
     - apply transport_idmap_path_universe_uncurried.
   Qed.
@@ -748,7 +748,7 @@ Section Book_2_17_sigma.
     : {a : A & B a} <~> {a' : A' & B' a'}.
   Proof.
     apply equiv_path.
-    snrapply ap011D.
+    snapply ap011D.
     - exact (path_universe_uncurried f).
     - apply Book_2_17_path_fibr_1.
       apply path_arrow; intro a.
@@ -773,12 +773,12 @@ Section Book_2_17_sigma.
     : Book_2_17_ii_sigma = Book_2_17_i_sigma.
   Proof.
     apply path_equiv; simpl.
-    lhs nrapply Book_2_17_eq_sigma'.
-    snrapply ap011D.
+    lhs napply Book_2_17_eq_sigma'.
+    snapply ap011D.
     - apply transport_idmap_path_universe_uncurried.
     - destruct (transport_idmap_path_universe_uncurried f); simpl.
       apply path_forall; intro a.
-      lhs nrapply (ap (fun h => _ (h _)) (eisretr _ _)).
+      lhs napply (ap (fun h => _ (h _)) (eisretr _ _)).
       apply transport_idmap_path_universe_uncurried.
   Defined.
 End Book_2_17_sigma.
@@ -808,8 +808,8 @@ Section Book_2_17_arrow.
     : Book_2_17_ii_arrow = Book_2_17_i_arrow.
   Proof.
     apply path_equiv; simpl.
-    lhs nrapply Book_2_17_eq_arrow'.
-    snrapply ap011.
+    lhs napply Book_2_17_eq_arrow'.
+    snapply ap011.
     - apply transport_idmap_path_universe_uncurried.
     - exact (ap (fun g0 _ => g0)
         (transport_idmap_path_universe_uncurried g)).
@@ -833,12 +833,12 @@ Section Book_2_17_forall.
     : (forall a, B a) <~> (forall a', B' a').
   Proof.
     apply equiv_path.
-    snrapply (ap011D (fun A0 B0 => forall a0, B0 a0)).
+    snapply (ap011D (fun A0 B0 => forall a0, B0 a0)).
     - exact (path_universe_uncurried f)^.
     - apply Book_2_17_path_fibr_2.
       apply path_arrow; intro a.
       apply path_universe_uncurried.
-      nrapply (transport (fun f0 => B (f0 _) <~> _)
+      napply (transport (fun f0 => B (f0 _) <~> _)
         (transport_idmap_path_universe_uncurried f)^).
       apply g.
   Defined.
@@ -859,12 +859,12 @@ Section Book_2_17_forall.
     : Book_2_17_ii_forall = Book_2_17_i_forall.
   Proof.
     apply path_equiv; simpl.
-    lhs nrapply Book_2_17_eq_forall'.
-    snrapply ap011D.
+    lhs napply Book_2_17_eq_forall'.
+    snapply ap011D.
     - apply transport_idmap_path_universe_uncurried.
     - destruct (transport_idmap_path_universe_uncurried f); simpl.
       apply path_forall; intro a.
-      lhs nrapply (ap (fun h => _ (h _)) (eisretr _ _)).
+      lhs napply (ap (fun h => _ (h _)) (eisretr _ _)).
       apply transport_idmap_path_universe_uncurried.
   Defined.
 End Book_2_17_forall.
@@ -894,8 +894,8 @@ Section Book_2_17_sum.
     : Book_2_17_ii_sum = Book_2_17_i_sum.
   Proof.
     apply path_equiv; simpl.
-    lhs nrapply Book_2_17_eq_sum'.
-    snrapply ap011.
+    lhs napply Book_2_17_eq_sum'.
+    snapply ap011.
     - apply transport_idmap_path_universe_uncurried.
     - apply transport_idmap_path_universe_uncurried.
   Qed.
@@ -1064,7 +1064,7 @@ Section Book_3_8_ctx.
   Definition Book_3_8_equiv {A B : Type} (f : A -> B)
     : Trunc (-1) (Book_3_8_qinv f) <~> (isequiv _ _ f).
   Proof.
-    snrapply equiv_iff_hprop.
+    snapply equiv_iff_hprop.
     - exact _.
     - apply cond_iii.
     - apply Trunc_rec, cond_ii.
@@ -1115,7 +1115,7 @@ Definition Book_3_10_impred@{i j k | i < j, j < k} `{Univalence}
   (LEM : Book_3_10_LEM@{j})
   : IsEquiv@{j k} Book_3_10_Lift@{i j}.
 Proof.
-  snrapply isequiv_adjointify.
+  snapply isequiv_adjointify.
   { intro A. destruct (LEM A).
     - exact (Build_HProp Unit).
     - exact (Build_HProp Empty).
@@ -1342,7 +1342,7 @@ Definition Book_3_17 {A : Type} {B : Trunc (-1) A -> HProp}
   : (forall a : A, B (tr a)) -> (forall x : Trunc (-1) A, B x).
 Proof.
   intros f x.
-  nrapply (Trunc_rec _ x).
+  napply (Trunc_rec _ x).
   - exact _.
   - intro a.
     exact (transport B (path_ishprop (tr a) x) (f a)).
@@ -1693,7 +1693,7 @@ Defined.
 Definition Book_4_6_iii (qua1 qua2 : QInv_Univalence_type) : Empty.
 Proof.
   apply (Book_4_6_ii qua1 qua2).
-  nrapply istrunc_succ.
+  napply istrunc_succ.
   apply (Build_Contr _ (fun A => 1)); intros u.
   exact (allqinv_coherent qua2 _ _ (idmap; (idmap; (fun A => 1, u)))).
 Defined.

test/Tactics/napply.v

@@ -0,0 +1,19 @@
+From HoTT Require Import Basics.Overture Basics.Tactics.
+From HoTT Require Import Spaces.Nat.Core.
+
+Local Open Scope nat_scope.
+
+(** Testing the different [apply] tacitcs in the library. *)
+
+Definition test1_type := {n : nat & n < 3}.
+Fail Definition test1 : test1_type := ltac:(apply exist).
+Fail Definition test1 : test1_type := ltac:(rapply exist).
+Fail Definition test1 : test1_type := ltac:(napply exist).
+Fail Definition test1 : test1_type := ltac:(tapply exist).
+Succeed Definition test1 : test1_type := ltac:(napply exist; exact _).
+
+(** Testing deprecated tactics *)
+Fail Definition test1 : test1_type := ltac:(nrapply exist).
+Fail Definition test1 : test1_type := ltac:(snrapply exist).
+
+

theories/Algebra/AbGroups/AbHom.v

@@ -21,7 +21,7 @@ Instance inverse_hom {A : Group} {B : AbGroup}
 (** For [A] and [B] groups, with [B] abelian, homomorphisms [A $-> B] form an abelian group. *)
 Definition grp_hom `{Funext} (A : Group) (B : AbGroup) : Group.
 Proof.
-  snrapply (Build_Group' (GroupHomomorphism A B) sgop_hom grp_homo_const inverse_hom).
+  snapply (Build_Group' (GroupHomomorphism A B) sgop_hom grp_homo_const inverse_hom).
   1: exact _.
   all: hnf; intros; apply equiv_path_grouphomomorphism; intro; cbn.
   - apply associativity.
@@ -31,7 +31,7 @@ Defined.
 
 Definition ab_hom `{Funext} (A : Group) (B : AbGroup) : AbGroup.
 Proof.
-  snrapply (Build_AbGroup (grp_hom A B)).
+  snapply (Build_AbGroup (grp_hom A B)).
   intros f g; cbn.
   apply equiv_path_grouphomomorphism; intro x; cbn.
   apply commutativity.
@@ -52,7 +52,7 @@ Definition ab_coeq_glue {A B : AbGroup} {f g : A $-> B}
   : ab_coeq_in (f:=f) (g:=g) $o f $== ab_coeq_in $o g.
 Proof.
   intros x.
-  nrapply qglue.
+  napply qglue.
   apply tr.
   by exists x.
 Defined.
@@ -61,14 +61,14 @@ Definition ab_coeq_rec {A B : AbGroup} {f g : A $-> B}
   {C : AbGroup} (i : B $-> C) (p : i $o f $== i $o g) 
   : ab_coeq f g $-> C.
 Proof.
-  snrapply (grp_quotient_rec _ _ i).
+  snapply (grp_quotient_rec _ _ i).
   cbn.
   intros b H.
   strip_truncations.
   destruct H as [a q].
   destruct q; simpl.
-  lhs nrapply grp_homo_op.
-  lhs nrapply (ap (+ _)).
+  lhs napply grp_homo_op.
+  lhs napply (ap (+ _)).
   1: apply grp_homo_inv.
   apply grp_moveL_M1^-1.
   exact (p a)^.
@@ -101,7 +101,7 @@ Definition functor_ab_coeq {A B : AbGroup} {f g : A $-> B} {A' B' : AbGroup} {f'
   (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
   : ab_coeq f g $-> ab_coeq f' g'.
 Proof.
-  snrapply ab_coeq_rec.
+  snapply ab_coeq_rec.
   1: exact (ab_coeq_in $o b).
   refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
   refine ((_ $@L p^$) $@ _ $@ (_ $@L q)).
@@ -116,7 +116,7 @@ Definition functor2_ab_coeq {A B : AbGroup} {f g : A $-> B} {A' B' : AbGroup} {f
   (s : b $== b')
   : functor_ab_coeq a b p q $== functor_ab_coeq a' b' p' q'.
 Proof.
-  snrapply ab_coeq_ind_homotopy.
+  snapply ab_coeq_ind_homotopy.
   intros x.
   exact (ap ab_coeq_in (s x)).
 Defined.
@@ -130,14 +130,14 @@ Definition functor_ab_coeq_compose {A B : AbGroup} {f g : A $-> B}
   : functor_ab_coeq a' b' p' q' $o functor_ab_coeq a b p q
   $== functor_ab_coeq (a' $o a) (b' $o b) (hconcat p p') (hconcat q q').
 Proof.
-  snrapply ab_coeq_ind_homotopy.
+  snapply ab_coeq_ind_homotopy.
   simpl; reflexivity.
 Defined.
 
 Definition functor_ab_coeq_id {A B : AbGroup} (f g : A $-> B)
   : functor_ab_coeq (f:=f) (g:=g) (Id _) (Id _) (hrefl _) (hrefl _) $== Id _.
 Proof.
-  snrapply ab_coeq_ind_homotopy.
+  snapply ab_coeq_ind_homotopy.
   reflexivity.
 Defined.
 
@@ -146,24 +146,24 @@ Definition grp_iso_ab_coeq {A B : AbGroup} {f g : A $-> B}
   (a : A $<~> A') (b : B $<~> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
   : ab_coeq f g $<~> ab_coeq f' g'.
 Proof.
-  snrapply cate_adjointify.
+  snapply cate_adjointify.
   - exact (functor_ab_coeq a b p q).
   - 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.
+    tapply cate_isretr.
   - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
       $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
-    rapply cate_issect.
+    tapply cate_issect.
 Defined.
 
 (** ** The bifunctor [ab_hom] *)
 
 Instance is0functor_ab_hom01 `{Funext} {A : Group^op}
   : Is0Functor (ab_hom A).
 Proof.
-  snrapply (Build_Is0Functor _ AbGroup); intros B B' f.
-  snrapply Build_GroupHomomorphism.
+  snapply (Build_Is0Functor _ AbGroup); intros B B' f.
+  snapply Build_GroupHomomorphism.
   1: exact (fun g => grp_homo_compose f g).
   intros phi psi.
   apply equiv_path_grouphomomorphism; intro a; cbn.
@@ -173,8 +173,8 @@ Defined.
 Instance is0functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
   : Is0Functor (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B).
 Proof.
-  snrapply (Build_Is0Functor (Group^op) AbGroup); intros A A' f.
-  snrapply Build_GroupHomomorphism.
+  snapply (Build_Is0Functor (Group^op) AbGroup); intros A A' f.
+  snapply Build_GroupHomomorphism.
   1: exact (fun g => grp_homo_compose g f).
   intros phi psi.
   by apply equiv_path_grouphomomorphism.
@@ -183,7 +183,7 @@ Defined.
 Instance is1functor_ab_hom01 `{Funext} {A : Group^op}
   : Is1Functor (ab_hom A).
 Proof.
-  nrapply Build_Is1Functor.
+  napply Build_Is1Functor.
   - intros B B' f g p phi.
     apply equiv_path_grouphomomorphism; intro a; cbn.
     exact (p (phi a)).
@@ -196,7 +196,7 @@ Defined.
 Instance is1functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
   : Is1Functor (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B).
 Proof.
-  nrapply Build_Is1Functor.
+  napply Build_Is1Functor.
   - intros A A' f g p phi.
     apply equiv_path_grouphomomorphism; intro a; cbn.
     exact (ap phi (p a)).
@@ -215,7 +215,7 @@ Defined.
 Instance is1bifunctor_ab_hom `{Funext}
   : Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
 Proof.
-  nrapply Build_Is1Bifunctor''.
+  napply Build_Is1Bifunctor''.
   1,2: exact _.
   intros A A' f B B' g phi; cbn.
   by apply equiv_path_grouphomomorphism.