Home

Source

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

Proof finished

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

Proof finished

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.

Syntax

(* Simple usage *)
discriminate.

Examples

Before

-------------------------
1/1
1 <> 2
discriminate.

After

Proof finished

Before

-------------------------
1/1
"hello" <> "world"
discriminate.

After

Proof finished

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

Proof finished

Before

n: nat
-------------------------
1/1
n + 5 = n + 5
exact (eq_refl (n + 5)).

After

Proof finished

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

Proof finished

Before

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

After

Proof finished

Resources

Reference Documentation