# [tlaplus] The CASE keyword

Hi,

In the example of hierarchical proofs in the TLAPS tutorial (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html), the two possible actions of Next are considered in the proof using the CASE keyword:

Next == \/ /\ x < y /\ y' = y - x /\ x' = x \/ /\ y < x /\ x' = x-y /\ y' = y

THEOREM NextProperty == InductiveInvariant /\ Next => InductiveInvariant'
<1> SUFFICES ASSUME InductiveInvariant, Next PROVE InductiveInvariant' <1> USE DEF InductiveInvariant, Next <1>1 (x < y) \/ (y < x) <1>a CASE x < y <1>b CASE y < x <1>2 QED BY <1>1, <1>a, <1>b

It is quite intuitive because this can be read as "the two separate cases that can occur in the next step.".

However, in the proof for Paxos (https://github.com/tlaplus/v1-tlapm/blob/master/examples/paxos/Paxos.tla), in the proof of the intermediate Lemma SafeAtStable, the different cases that can happen in the next state are expressed by using ASSUME keyword:

 Next == \/ \E b \in Ballots : Phase1a(b) \/ Phase2a(b) \/ \E a \in Acceptors : Phase1b(a) \/ Phase2b(a)

LEMMA SafeAtStable == Inv /\ Next /\ TypeOK' =>
\A v \in Values, b \in Ballots:
SafeAt(v, b) => SafeAt(v, b)'
<1> SUFFICES ASSUME Inv, Next, TypeOK',
NEW v \in Values, NEW b \in Ballots, SafeAt(v, b)
PROVE SafeAt(v, b)'
OBVIOUS
<1> USE DEF Send, Inv, Ballots
<1> USE TRUE /\ TRUE
<1>1. ASSUME NEW bb \in Ballots, Phase1a(bb)
PROVE SafeAt(v, b)'
BY <1>1, SMT DEF SafeAt, Phase1a, VotedForIn, WontVoteIn
<1>2. ASSUME NEW a \in Acceptors, Phase1b(a)
PROVE SafeAt(v, b)'
BY <1>2, QuorumAssumption, SMTT(60) DEF TypeOK, SafeAt, WontVoteIn, VotedForIn, Phase1b
<1>3. ASSUME NEW bb \in Ballots, Phase2a(bb)
PROVE SafeAt(v, b)'
BY <1>3, QuorumAssumption, SMT DEF TypeOK, SafeAt, WontVoteIn, VotedForIn, Phase2a
<1>4. ASSUME NEW a \in Acceptors, Phase2b(a)
PROVE SafeAt(v, b)'
<2>1. PICK m \in msgs : Phase2b(a)!(m)
BY <1>4 DEF Phase2b
<2>2 \A aa \in Acceptors, bb \in Ballots, vv \in Values :
VotedForIn(aa, vv, bb) => VotedForIn(aa, vv, bb)'
BY <2>1 DEF TypeOK, VotedForIn
<2>3. \A aa \in Acceptors, bb \in Ballots : maxBal[aa] > bb => maxBal'[aa] > bb
BY <2>1 DEF TypeOK
<2>4. ASSUME NEW aa \in Acceptors, NEW bb \in Ballots,
WontVoteIn(aa, bb), NEW vv \in Values,
VotedForIn(aa, vv, bb)'
PROVE FALSE
<3> DEFINE mm == [type |-> "2b", val |-> vv, bal |-> bb, acc |-> aa]
<3>1. mm \notin msgs
BY <2>4 DEF WontVoteIn, VotedForIn
<3>2. mm \in msgs'
<4>1. PICK m1 \in msgs' :
/\ m1.type = "2b"
/\ m1.val = vv
/\ m1.bal = bb
/\ m1.acc = aa
BY <2>4 DEF VotedForIn
<4>. QED BY <4>1 DEF TypeOK, Messages \* proved by Zenon
<3>3. aa = a /\ m.bal = bb
BY <2>1, <3>1, <3>2 DEF TypeOK
<3>. QED
BY <2>1, <2>4, <3>3 DEF Phase2b, WontVoteIn, TypeOK
<2>5 \A aa \in Acceptors, bb \in Ballots : WontVoteIn(aa, bb) => WontVoteIn(aa, bb)'
BY <2>3, <2>4 DEF WontVoteIn
<2> QED
BY <2>2, <2>5, QuorumAssumption DEF SafeAt
My question is: Has the ASSUME construct been used in the proof of SafeAtStable because Next is a disjunction of two existential quantifiers? Or could this have been written using the CASE keyword somehow?

Thank you

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.