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 tactics a Coq user ever utilizes. intros finds assumptions builtin to your goal (usually in the form of a forall quantifier) and moves them to the goal’s context (a.k.a. hypothesis space, assumption space). This is similar to the first step of many informal, paper proofs, when the prover states “let there be some number n, …”

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 - unless an explicit name is provided for them.

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.

clear - ... can also be used to erase all assumptions not depended on by a provided set of assumptions.

Syntax

(* Simple usage *)
clear H.

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

(* Clear anything that x, z, or c do not depend on *)
clear - x z c.

Examples

Before

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

clear Hr1 Hr2.

After

n: nat
H: n = 0
IHn: n = 1
=========================
1/1
True

Before

a, b, c, x, y, z: nat
H: a = z
=========================
1/1
True

clear - a x H.

After

a, x, z: nat
H: a = z
=========================
1/1
True

Resources

Reference Documentation

---

---