In the coq tactics language, what is the difference between intro and intros

Question

In the Coq tactics language, what is the difference between

intro

and

intros?

Tarpon

Answer 1

intro and intros behave differently if no argument is supplied

According to the reference manual:

If the goal is neither a product nor starting with a let definition, the tactic intro applies the tactic hnf until the tactic intro can be applied or the goal is not head-reducible.

On the other hand, intros, as a variant of intro tactic,

repeats intro until it meets the head-constant. It never reduces head-constants and it never fails.

Example:

Goal not False.
  (* does nothing *)
  intros.
  (* unfolds `not`, revealing `False -> False`;
     moves the premise to the context *)      
  intro.
Abort.       

Note: both intro and intros do the same thing if an argument is supplied (intro contra / intros contra).

intros is polyvariadic, intro can only take 0 or 1 arguments

Goal True -> True -> True.
  Fail intro t1 t2.
  intros t1 t2.  (* or `intros` if names do not matter *)
Abort.

intro does not support intro-patterns

Goal False -> False.
  Fail intro [].
  intros [].
Qed.

Some information about intro-patterns can be found in the manual or in the Software Foundations book. See also this example of not-so-trivial combination of several intro-patterns.

intros does not support after / before / at top / at bottom switches

Let's say we have a proof state like this

H1 : True
H2 : True /\ True
H3 : True /\ True /\ True
==========
True /\ True /\ True /\ True -> True

then e.g. intro H4 after H3 will modify the proof state like so:

H1 : True
H2 : True /\ True
H4 : True /\ True /\ True /\ True 
H3 : True /\ True /\ True
==========
True

and intro H4 after H1 will produce

H4 : True /\ True /\ True /\ True 
H1 : True
H2 : True /\ True
H3 : True /\ True /\ True
==========
True

Silvanus

The manual is a bit incorrect in saying intros repeats intro - it never unfolds definitions, so repeat intro is different from intros. What it repeats is intro without the hnf step. – Ringtailed

I think the manual says what you are saying in the second sentence: "It never reduces head-constants ..." – Silvanus

Yes, that does help clarify, but I still think intros doesn't repeat intro and the manual could emphasize this difference (I consider unexpected unfolding a big deal). This difference really surprised me when I ran into github.com/coq/coq/issues/5394. – Ringtailed