A table of simple tactics

Copied from Coq in a Hurry by Yves Bertot. Notably: read Section 3 for a fast introduction into proving in Coq.
In case the formula in the top row is in the context, labelled H, use the tactic in the Hypothesis row. In case the formula in the top row is the goal, use the tactic in the Goal row. Freely try the tactics mentioned and see what happens.

	A ->B	forall x : D, A	A /\ B	False
Hypothesis	apply H	apply H	elim H case H destruct H as [H1 H2]	elim H case H
Goal	intro H intros	intro x intros	split

	~A	exists x:D, A	A\/B
Hypothesis	elim H case H	elim H case H destruct H as [x H1]	elim H case H destruct H as [H1 \| H2]
Goal	intro H intros	exists t	left right

	t = q
Hypothesis	rewrite H rewrite <- H
Goal	reflexivity ring

Some other useful uses of tactics.

unfold t unfolds the definition of t in the goal. Example: unfold not replaces ~A by A -> False .
unfold t in H unfolds the definition of t in the hypothesis with label H
assert A
Given a goal G, assert A creates a new goal A and adds A to the context in which we have to prove G. This is typically used in case we first want to prove an intermediate results A. NB: In case A is a compound proposition, like P x, it has to be put between brackets, assert (P x) .
assert (H: A)
Same as above, but now you explicitly give the name of the hypothesis that you wish to use; of course H should be fresh.
rewrite H in H1
If H : t = q and H1 : ... t ... in the context, then rewrite H in H1 replaces the H1 hypothesis by H1 : ... q ...
Similarly rewrite <- H in H1 replaces q by t in the hypothesis with label H1
destruct (H a) as [H1 H2]
For example, if H : forall x:D,P x /\ Q x and a:A, this destructs the conjuction P a /\ Q a as H1 : P a and H2 : Q a.
apply H with y
For example, if H : forall x:D,P x -> Q and the goal is Q, this applies H with y as the instantiation for the universally quantified variable x. (In general Coq doesn't "guess" these instantiations.)