import MyNat.Definition

Tactics

rfl

rfl stands for "reflexivity", which is a fancy way of saying that it will prove any goal of the form A = A. It doesn't matter how complicated A is.

rewrite

The rewrite tactic is the way to "substitute in" the value of a variable. In general, if you have a hypothesis of the form A = B, and your goal mentions the left hand side A somewhere, then the rewrite tactic will replace the A in your goal with a B.

rw

The rw tactic is simply rewrite followed by rfl.

induction

The induction tactic applies induction on inductive type to the main goal, producing one goal for each constructor of the inductive type.

simp

The simp tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.

exact

If you can explicitly see how to make an element of your goal set, i.e. you have a formula for it, then you can just write exact <formula> and this will close the goal.

intro

If your goal is ⊢ P → Q then intro p will introduce a new hypothesis p : P and change the goal to ⊢ Q.

intros

The intros tactic is like intro only it can introduce multiple hypotheses at once.

have

have h : t := e adds the hypothesis h : t to the current goal if e is a term of type t.

apply

apply e tries to match the current goal against the conclusion of e's type.

assumption

The assumption tries to solve the goal using a hypothesis of compatible type

constructor

The constructor tactic tries to solve the goal using a hypothesis of compatible type.

cases

Assuming x is a variable in the local context with an inductive type, cases x splits the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor.

left/right

If ⊢ P ∨ Q is your goal, then left changes this goal to ⊢ P, and right changes it to ⊢ Q.

exfalso

exfalso converts a goal ⊢ tgt into ⊢ False by applying False.elim.

contradiction

The contradiction tactic closes the main goal if its hypotheses are "trivially contradictory".

by_cases

by_cases h : P does a cases split on whether P is true or false.

use

use is a tactic which works on goals of the form ⊢ ∃ c, P(c) where P(c) is some proposition which depends on c. You can specify one of the values of c that you would like to choose to proof thereby proving the existance is true.

revert

revert x is the opposite to intro x.

tauto

The tauto tactic (and its variant tauto!) will close various logic goals.

<;>

tac1 <;> tac2 runs tac1 on the main goal and tac2 on each produced goal, concatenating all goals produced by tac2.