Here is some advice about what to do next in a proof. Options 1, 4, and 5 make use of the table below.
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 ?.) When the goal is an all formula on a union type, you need to choose between arbitrary or induction. If the all variable in your goal appears in the formula as the first argument of a recursive function, then induction is a good choice. Otherwise choose arbitrary.
If the goal formula involves a function that is defined using a switch, then it is a good idea to use the switch proof statement.
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.
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.)
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 |