easy

easy throws many common “closing tactics” at a goal to solve a large category of simple problems. easy will attempt to use:

• trivial

• reflexivity

• symmetry

• contradiction

• inversion

• intros

• split (this begins a recursive call of easy)

• destruct (on hypotheses with conjunctions)

easy is the base form of the now tactical.

Syntax

easy.

Examples

Before

P: Prop
H: P
=========================
1/1
True /\ 42 = 14 * 3 /\ P

easy.

After

No more goals.

Resources

Reference Documentation

---