Generalization

This group of tactics is often found at the beginnings of proofs. Generalization and its counterpart Specialization (both are included here) are concepts used to fine-tune how strong of a theorem is needed to continue. Theorems that are too strong (specific) aren’t useful for many different kinds of goals. Theorems that are too weak (general) are frequently unprovable (even if their specified counterparts are!) and those that are provable are frequently harder to prove!

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

---

clear

clear erases assumptions from the assumption space. Multiple assumptions may be erased in one tactic via a space-separated list of assumptions. clear will fail if an assumption passed into it contains as subterms other variables that still exist in the goal state.

Syntax

(* Simple usage *)
clear H.

(* Clear multiple assumptions *)
clear H Heq X Y n.

Examples

Before

n: nat
H, Hr1, Hr2: n = 0
IHn: n = 1
-------------------------
1/1
False

clear Hr1 Hr2.

After

n: nat
H: n = 0
IHn: n = 1
-------------------------
1/1
False

Resources

Reference Documentation

---

---