intros

Typically the first tactic a Coq user ever utilizes. intros looks for assumptions in your goal and moves them to the goal’s assumption space.

More specifically, intros specializes a goal by looking for type inhabitation and proposition assumptions and moving them into the assumption space. For example, if you write forall (n : nat), n + 0 = n, the forall is acting as an assumption that there is a value of type nat that we can call n. Calling intros here will provide you an assumption n that there is a value of type nat.

intros will not introduce variables that are contained in opaque/wrapped definitions.

A simpler tactic, intro, acts similarly but can only introduce one assumption, and will introduce variables contained in opaque/wrapped definitions.

Syntax

(* Simple usage - introduces all named assumptions *)
intros.

(* Give specific names to assumptions as you introduce *)
intros n m x.

(* Split a conjunction or existential assumption upon introducing *)
intros [A B].

Examples

Before

-------------------------
forall (n : nat), n + 0 = n

intros x.

After

x: nat
-------------------------
1/1
x + 0 = x

Before

-------------------------
forall (A B C : Prop), A /\ B -> C -> A /\ C

intros A B C [ATrue BTrue].

After

A, B, C: Prop
ATrue: A
BTrue: B
-------------------------
1/1
C -> A /\ C

Before (assume P := forall (n : nat), n = n)

-------------------------
1/1
P

intros.

After

-------------------------
1/1
P

Alternatively,

intro.

After

n: nat
-------------------------
1/1
n = n

Resources

Reference Documentation

---