The Decompose Proof command is executed by placing the cursor in a proof obligation, either a proof step or
a theorem, and either typing Ctl+G Ctl+D
or right-clicking and selecting
the command.
There are two basic ways to decompose a proof obligation into simpler obligtions:
/\
decomposition P
equals
P1 /\ ... /\ Pn
,
then the proof of P
can be broken into the
proof of the n
formulas
P1, ... , Pn
.
\/
decomposition (case split)
P
equals
P1 \/ ... \/ Pn
,
then the proof of ASSUME P PROVE Q
can be broken into the
proof of the n
obligations
ASSUME P1 PROVE Q, ..., ASSUME Pn PROVE Q
.
Often, a proof obligation must be transformed into an equivalent one in order to be decomposed
by /\
or \/
decomposition. There are two transformations that can be
applied to the goal of an obligation. (The goal is the PROVE
formula of an ASSUME
/PROVE
obligation or the entire obligation, if it is a single formula.)
=>
splitting P => Q
is equivalent to the assumption P
and the goal Q
.
\A
splitting
\A x \in S : P
is equivalent to the assumption NEW x \in S
and the goal P
. The goal \A x : P
is similarly split.
ASSUME
/PROVE
obligation:
/\
splitting P1 /\ ... /\ Pn
, is equivalent to the n
assumptions
P1, ..., Pn .
\E
splitting
\E x \in S : P
is equivalent to the two assumptions
NEW x \in S, P
.
The goal \E x : P
is similarly split.
\/
and \E
splittings can be combined hierarchically.)
The proof is generated by clicking a button that is either labeled by P or (for an /\
decomposition) by a button with P next to it.
Instead of generating an /\
or \/
decomposition, the button labeled P
at the top of the command's dialog window generates a proof consisting of only a
SUFFICES ASSUME ... PROVE
step constructed by splitting the original obligation and a QED
step.
For example, starting from the obligation P => \E x \in S : Q
, performing
a =>
split followed by a \A
split on the goal and then clicking on this
button produces a proof like this:
<3> SUFFICES ASSUME P, NEW x \in S PROVE Q OBVIOUS <3> QED
The obligation to which you apply the Decompose Proof command must have either no proof or else a
leaf proof, such as a BY
proof or the proof OBVIOUS
). If it has a leaf proof, that proof
is made the proof of each of the simpler obligations into which the proof is decomposed. For a proof generated by
the top P button (which does no decomposing), the obligation's leaf proof becomes the
QED
step's proof.
SUFFICES
\E
assumption generates new assumptions.
Selecting this option causes those assumptions to be asserted by a
SUFFICES ASSUME/PROVE
step. Otherwise, these assumption are added to each of the decomposed proof steps.
CASE
\/
decomposition, CASE
steps should be used instead of ASSUME/PROVE
steps when possible. One reason not to choose this option is that
the Decompose Command does not decompose CASE
steps.
LET
definitions within the step. This can cause parsing
errors in the decomposed proof.