Automation

This is basically a catch-all category for tactics that do a lot of things at once. This category of tactics generally intends to solve a large category of simple goals to reduce the load of the proof writer.

auto

auto does a recursive search through a specified knowledge base in order to solve goals. If auto cannot completely solve a goal, it succeeds with no changes to the goal.

The knowledge bases that auto uses are called Hint Databases. Hint databases are provided by the standard library, and can also be created and added to by users. Hint databases can contain a variety of hint types, including but not limited to:

• Constructors: auto will now try to apply each of the constructors for a given Inductive type
• Unfold: auto will now try to unfold a given definition - helpful when trivial simplification isn’t enough
• Resolve: auto will now try to simple apply a given lemma

The default hint database used by auto when no other database is specified is core.

Syntax

(* Simple usage *)
auto.

(* Using a specific database *)
auto with bool.

(* Using a specific lemma *)
auto using example.

Examples

Before

-------------------------
1/1
0 = 0

auto.

After

Proof finished

Script

Create HintDb automation.
Lemma add_0_r : forall n, n * 1 = n. 
Proof. induction n. auto. simpl. now rewrite IHn. Qed.
Hint Resolve add_0_r : automation.

Lemma x : (forall n, n * 1 = n) /\ (true = true). 
Proof. auto with automation. Qed.

Resources

Reference Documentation

Hint Databases

---

trivial

trivial is essentially a non-recursive auto. trivial is best utilized when a lemma that exactly matches the goal already exists in the hint database.

Syntax

(* Simple usage *)
trivial.

(* Using a specific database *)
trivial with bool.

Examples

Script

Theorem trivial_example : forall {X : Type} (n : X), 
    n = n.
Proof.
    trivial.
Qed.

Resources

Reference Documentation

---

---