# Form of intros in Coq specifically for forall and explicitly for ->

Are there tactics in Coq that are more limited versions (subtactics?) of intros?

I'm curious if there are any specifically for forall ... and specifically for ->.

intros in Coq is capable of undoing the outermost forall as well as the outermost ->.

It introduces hypotheses with provided or arbitrary names.

I suspect the reason for this generality is the fact that coq is built on top of the calculus of inductive constructions and forall and -> really are both special cases of the dependent $$\Pi$$-type. (Also, now that I think about it, forall might actually be the general construction. I'm not sure.)

Here is an example from the Basics.v file from Software Foundations. This is a theorem and proof provided by authors, not a completed exercise from SF. (I mention this because the authors ask people not to post solutions to SF problems online.)

Theorem plus_id_example : forall n m:nat,
n = m ->
n + n = m + m.

Proof.
(* move both quantifiers into the context: *)
intros n m.
(* move the hypothesis into the context: *)
intros H.
(* rewrite the goal using the hypothesis: *)
rewrite -> H.
reflexivity.  Qed.


Anyway, the generality of intros is nice in theory, but it can make tactic scripts harder to read. Are there weaker tactics than intros that can only unpack -> or only unpack forall? That would make it easier to tell at a glance what roughly what "part" of a theorem is being addressed by a tactic appearing in the middle of a tactic script.

• forall (x : nat), 1 = 1 is equal to nat -> 1 = 1. So how would that tactic behave in this case?
– Trebor
Feb 27 at 4:55
• @Trebor I would treat that as an instance of forall because the type of the bound variable isn't Prop. But your point is well taken. Whether a forall/->/$\Pi$ ignores its bound variable or not is completely orthogonal to what type the bound variable has. I guess this question doesn't really make sense since there's no principled way to distinguish "uses that look like $\to$ in logic" and "uses that look like $\forall$ in logic", which is what I was really trying to do. Thanks. Feb 27 at 5:33
• Your question has two interpretations. You can make a tactic that rejects bad usages; you can also use two alias of the same tactic, and use them in a principled, but unenforced way.
– Trebor
Feb 27 at 5:41
• Those are both interesting and I don't know how to do either. I'm primarily interested in rejecting bad usages, though. Feb 27 at 5:44

intros * only unpacks forall. Example from the reference manual:
    ============================