TLA+ Proof System

TLA+ proof constructs

`SUFFICES`

An ordinary expression or ASSUME … PROVE … in a step stands for an assertion of that step. Its subproof proves it, and the rest of the proof in the same level is allowed to use the assertion as an assumption. SUFFICES reverses these two roles. Succinctly, the following two proof fragments are equivalent.

<4>1. t₁ <5>1. s₁ <5>2. s₂ … <5>m. QED <4>2. t₂ <4>3. t₃ … <4>n. QED

<4>1. SUFFICES t₁ <5>1. t₂ <5>2. t₃ … <5>n-1. QED <4>2. s₁ <4>3. s₂ … <4>m+1. QED

In the proof on the left-hand side above, t₁ is known in proof-steps <4>2, <4>3, ..., <4>n, while in the proof on the right-hand side, t₁ is known in proof-steps <5>1, <5>2, ..., <5>n-1. SUFFICES is mainly used to rephrase the sequent to be proved in a more perspicuous form. For example, suppose we have:

This proof is unnatural because of the nested occurrences of ASSUME … PROVE …. The point where Next needs to be expanded, in <2>3, is potentially far removed from its relevant assertion, <1>1. It would be better instead to rephrase the theorem as a conjunction and then derive the conjuncts with a SUFFICES as follows:

In this form, the definition of Next is cited right next to the assertion where it is relevant. In the rest of the proof after step <1>1, the definition of Next is irrelevant. The proof is also shallower because we change an instance of a QED step into a BY leaf proof. This kind of restatement of the current goal can make proofs much easier to read and maintain.

(Strictly speaking, the SUFFICES step was not necessary in this simple proof because the DEF Next could have been folded into the proof of <1>4. However, in more complex proofs it is better to use SUFFICES as needed to rephrase the goal up front. These steps also serve as hints to the reader about the direction of the proof.)

`HAVE`, `TAKE` and `WITNESS`

TLAPS provides some shortcuts for proving implications and quantifications. They can be described with their equivalent SUFFICES construct:

goal step equivalent SUFFICES step

e => f
<n>l. HAVE g

<n>l. SUFFICES ASSUME g PROVE f OBVIOUS

\A x : P(x)
<n>l. TAKE y

<n>l. SUFFICES ASSUME NEW y PROVE P(y) OBVIOUS

\A x \in S : P(x)
<n>l. TAKE y \in T

<n>l. SUFFICES ASSUME NEW y \in T PROVE P(y) OBVIOUS

\E x : P(x)
<n>l. WITNESS e

<n>l. SUFFICES P(e) OBVIOUS

\E x \in S : P(x)
<n>l. WITNESS e \in T

<n>l. SUFFICES ASSUME e \in T PROVE P(e) <n+1>1. e \in T OBVIOUS <n+1>2. QED BY <n+1>1

goal	step	equivalent `SUFFICES` step
`e => f`	<n>l. HAVE g	<n>l. SUFFICES ASSUME g PROVE f OBVIOUS
`\A x : P(x)`	<n>l. TAKE y	<n>l. SUFFICES ASSUME NEW y PROVE P(y) OBVIOUS
`\A x \in S : P(x)`	<n>l. TAKE y \in T	<n>l. SUFFICES ASSUME NEW y \in T PROVE P(y) OBVIOUS
`\E x : P(x)`	<n>l. WITNESS e	<n>l. SUFFICES P(e) OBVIOUS
`\E x \in S : P(x)`	<n>l. WITNESS e \in T	<n>l. SUFFICES ASSUME e \in T PROVE P(e) <n+1>1. e \in T OBVIOUS <n+1>2. QED BY <n+1>1

One important deficiency of HAVE, TAKE and WITNESS steps is that the precise form of the rephrased goal is not textually present in the proof. The (human) reader might get confused by long chains of these steps, especially if interleaved with other kinds of steps. These constructs should therefore be used sparingly, preferably only in the lowest levels of proof where there is some actual benefit in linearizing the proof.

`PICK`

An assumption of the form \E x : P(x) can be used by picking a fresh x for which P(x) is assumed. This is done using the step PICK x : P(x). Note that \E x : P(x) need not be present exactly in the assumptions; this step accepts a subproof that supplies the justification for \E x : P(x). Here is a somewhat contrived example: