deduce

Here is some advice about what to do next in a proof. Options 1, 3, and 4 make use of the table below.

1. Prove the goal by decomposing it into sub-goals. In the table below, look at the entry in the row for the current goal formula and the Prove column. The entry suggests the proof statement to use next. (This is the advice that Deduce outputs when you write ?.)

2. Work backwards from the goal using a suffices statement. After the by keyword, write the reason, often definition and/or rewrite, which transform the goal formula.

3. Work forwards from a given with a have statement. Look at the entry in the row for the given formula and the Use column. The table entry suggests what to write for the reason after the by keyword of your have statement. (This is the advice that Deduce outputs when you write help L where L is the label for the given.)

4. conclude the proof of the goal formula. For the reason after the by keyword, one can use a given according to the Use column in the table below, or one can prove the goal formula according to the Prove column.

Formula	Prove	Use
true	.	No uses
false	Contradiction	implicitly proves anything
P and Q	, Comma	(1) implicitly proves P, (2) implicitly proves Q
P or Q	(1) implicit from P, (2) implicit from Q	cases
if P then Q	assume	apply-to
all x:T. P	arbitrary, induction	brackets
some x:T. P	choose	obtain
x = y	symmetric, transitive, equations, definition, rewrite	symmetric, transitive, rewrite, rewrite-in