Coq策略语言中intro与intros两种策略的区别是什么？

Let me break down the core distinctions between these two foundational Coq tactics—they’re often confused, but their use cases are pretty distinct once you look under the hood.

1. Single vs. Multiple Hypothesis Binding #

The biggest difference comes down to granularity:

• intro works one step at a time. It targets the leftmost, outermost universal quantifier (forall) or implication (->) in your goal, binds it to a name (either one you specify or a default like H, H0, etc.), and moves it into your proof context.

  (* Initial goal: forall a b : nat, a = b -> b = a *)
  intro a. (* Context: a : nat; Goal: forall b : nat, a = b -> b = a *)
  intro b. (* Context: a, b : nat; Goal: a = b -> b = a *)
  intro H. (* Context: a, b : nat; H : a = b; Goal: b = a *)
  

• intros handles bulk binding in one go. You can list all the names you want to assign, use wildcards to skip variables you don’t need, or let Coq auto-generate names for you.

  (* Same initial goal *)
  intros a b H. (* Context: a, b : nat; H : a = b; Goal: b = a *)
  intros. (* Auto-generates default names: a, b, H; same end result *)
  

2. Pattern Matching for Complex Types #

intros supports direct pattern matching on complex types (like pairs, sums, or records)—a trick intro can’t pull off. With intro, you’d first bind the entire term, then use a separate tactic like destruct to unpack it.

(* Goal: forall p : nat * nat, fst p = snd p -> fst p = 0 *)
intros [x y] H. (* Context: x, y : nat; H : x = y; Goal: x = 0 *)
(* With intro, you’d have to do this instead: *)
intro p. (* Context: p : nat * nat; Goal: fst p = snd p -> fst p = 0 *)
destruct p as [x y]. (* Then proceed with intro H *)

3. Control Over Anonymous Variables #

When dealing with unnamed variables (marked with _ in the goal), intros gives you flexibility:

• Use intros _ to skip binding the variable entirely (great if you don’t need it in your proof).
• Use intros ? to let Coq auto-name the variable (same as omitting a name).
• intro will always bind anonymous variables to a default name (like H0)—you can’t skip it with this tactic.

4. Error Behavior for Empty Goals #

If your goal has no universal quantifiers or implications at the top level, intro will throw an error. intros (called with no arguments) will simply do nothing instead of failing, which makes it safer in scripts where you’re unsure if there are pending hypotheses to introduce.

内容的提问来源于stack exchange，提问作者nixon