Specific Solvers

Each tactic in this group exists to solve a very specific kind of goal. They’re fairly simple to learn about and use, because their goal targets are such small groups that there are hardly any degrees of freedom for automation to be required. Essentially all Coq proofs include some of these (whether they’re written by the programmer or called by more complex tactics).

reflexivity

reflexivity solves goals which state that a term is equal to itself. reflexivity has some simplification power, but not as much as simpl. This tactic will fail if it cannot solve the goal.

reflexivity makes an attempt to simplify the goal and then apply eq_refl, where eq_refl is the sole constructor of the eq Inductive Proposition, stating that forall {A : Type} (a : A), eq a a.

Syntax

(* Simple usage *)
reflexivity.

Examples

Before

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

reflexivity.

After

No more goals.

Resources

Reference Documentation

---

assumption

assumption solves goals in which there exists an assumption that directly proves the goal (no simplification). This tactic will fail if there does not exist such an assumption.

Syntax

(* Simple usage *)
assumption.

Examples

Before

P: Prop
H: P
=========================
1/1
P

assumption.

After

No more goals.

Resources

Reference Documentation

---

discriminate

discriminate solves goals that are trivial inequalities (something of the form x <> y)*. This tactic will fail if the goal is not an inequality or is non-trivial.

* Keep in mind that x <> y is actually shorthand for x = y -> False! This means that discriminate actually searches for trivial inequalities in assumptions.

Syntax

(* Simple usage *)
discriminate.

Examples

Before

=========================
1/1
1 <> 2

discriminate.

After

No more goals.

Before

=========================
1/1
"hello" <> "world"

discriminate.

After

No more goals.

Before

H: S n = O
==========================
1/1
False

discriminate.

After

No more goals.

Resources

Reference Documentation

---

exact

exact allows users to solve goals by providing a proof object directly. This tactic will fail if the provided proof object does not prove the goal.

Syntax

(* Simple usage *)
exact I.

Examples

Before

=========================
1/1
True

exact I.

After

No more goals.

Before

n: nat
=========================
1/1
n + 5 = n + 5

exact (eq_refl (n + 5)).

After

No more goals.

Resources

Reference Documentation

---

contradiction

contradiction solves goals in which there exist contradictory hypotheses. These contradictions generally take the form of a False hypothesis or a pair of hypotheses that state P and ~ P for some proposition. This tactic will fail if no such contradictions exist.

Syntax

(* Simple usage *)
contradiction.

Examples

Before

H: False
=========================
1/1
False

contradiction.

After

No more goals.

Before

x, y: nat
H: x = y
H0: x <> y
=========================
1/1
x = x + y

contradiction.

After

No more goals.

Resources

Reference Documentation

---

---