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

Answer

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.~ False
  (* does nothing *)
  intros.~ False
  (* unfolds `not`, revealing `False -> False`;
     moves the premise to the context *)
  intro.H: False
False
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.True -> True -> True
  (* Fail `intro t1 t2.` *)
  intros t1 t2.  (* or `intros` if names do not matter *)t1, t2: True
True
Abort.

intro does not support intro-patterns

Goal False -> False.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

1 subgoal

  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:

1 subgoal

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

and intro H4 after H1 will produce