Trouble with proofs involving CHOOSE or EXCEPT

Francisco José Letterio

unread,

May 16, 2025, 2:17:11 AMMay 16

to tlaplus

Hi all,

I'm working through the hyperbook, currently trying to prove correctness of the Die Harder algorithm from section 5.2. However, I'm running into a lot of trouble proving stuff that has either CHOOSE or EXCEPT.

For example, I can't seem to manage to be able to prove that

\A \in SUBSET Int : IsFiniteSet(A) => \A a \in A : SetMax(A) \geq a

I expanded the proof until I had the relevant assumes and the only thing left to prove is SetMax(A) \geq a, but I don't know how to prove it at this point. I had to work around this by using a IsSetMax(m, A) that I defined myself and let me prove what I wanted about it, without using CHOOSE (I forgot to mention so far, but SetMax is defined with a CHOOSE)

Similarly, I seem to have trouble with definitions of functions that use an EXCEPT. I have a function injug \in [Jugs -> Nat] and I have

injug' = [injug EXCEPT ![j] = Capacity[j] ]

I can't prove, for example, that injug'[j] = Capacity[j]. I'm thinking of doing a similar workaround where I replace this EXCEPT with a named proposition

Has anyone else ran into these same problems?

Stephan Merz

unread,

May 17, 2025, 3:49:28 AMMay 17

to tla...@googlegroups.com

Hi Francisco,

would you mind sharing your proof attempt, that would make it easier to understand what is going on?

The first proof must rely on induction on finite sets.The corresponding theorem FS_Induction is found in module FiniteSetTheorems in the library modules for TLAPS [1]. But yes, proofs involving CHOOSE can be tricky.

The second problem should be easier to solve. It sounds like the prover cannot figure out that j \in DOMAIN injug. Is the assumption injug \in [Jugs -> Nat] (which probably comes from a type-correctness predicate) part of the hypotheses of the proof step?

Hope this helps,

Stephan

[1] https://github.com/tlaplus/tlapm/blob/main/library/FiniteSetTheorems.tla

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/c8233fc9-e526-48df-994a-9c3325c05e00n%40googlegroups.com.

Francisco José Letterio

unread,

May 17, 2025, 6:57:47 PMMay 17

to tlaplus

Hello Stephan,

thanks again for your help! I will actually come back to this one after I can fix another issue I'm having rn with TLC, then I'll attempt doing the proofs using what you said (I had scrapped all previous work)

Francisco José Letterio

unread,

May 17, 2025, 7:36:31 PMMay 17

to tlaplus

I'm rewriting the proof now, but I run into writing the following at some point:

<3>2. CASE Terminating

<4>1. Terminating
OBVIOUS

<4> QED

And TLAPS can't prove it. When I look at the assumptions on the error window on the right, it's not assuming Terminating, even though it's under a CASE statement

Francisco José Letterio

unread,

May 17, 2025, 7:38:34 PMMay 17

to tlaplus

Sorry I just realized the message was cut short. The thing is that I'm under a CASE statement where I'm trying to prove Terminating => P, but TLAPS is not assuming Terminating in the proof

Francisco José Letterio

unread,

May 17, 2025, 8:38:39 PMMay 17

to tlaplus

Here's another one:

<4>2. ASSUME /\ pc' = "Done"
/\ UNCHANGED <<injug>>
PROVE TypeOK'

<5>1. injug' = injug
BY UNCHANGED <<injug>>

<5>2. injug \in [Jugs -> Nat]
BY DEF TypeOK, InductiveInvariantSetGCDDividesAll

<5>3. \A j \in Jugs : injug[j] =< Capacity[j]
BY DEF TypeOK, InductiveInvariantSetGCDDividesAll

<5> QED
BY <5>1, <5>2, <5>3 DEF TypeOK

TypeOK is just the conjunction of <5>2 and <5>3. TLAPS Can prove everything but <5>1, and when I check why it seems that it's not assuming UNCHANGED <<injug>>, even though the ASSUME is right there

Francisco José Letterio

unread,

May 17, 2025, 9:12:06 PMMay 17

to tla...@googlegroups.com

For reference, here's the full spec with what I'm trying to prove:

--------------------------- MODULE DieHarderBook ---------------------------

EXTENDS Integers, GCD, FiniteSetTheorems

Min(n,m) == IF n < m THEN n ELSE m

CONSTANTS Goal, Jugs, Capacity

ASSUME CONSTANTS_OK == /\ Goal \in Nat
/\ Capacity \in [Jugs -> Nat \ {0}]

ASSUME TRANSITIVITY_NAT == \A p,q,r \in Nat : p \leq q /\ q \leq r => p \leq r

ASSUME SUB_DECREMENT == \A a,b \in Int : b \geq 0 => a-b \leq a

ASSUME MIN_STAYS_INT == \A a,b \in Int : Min(a,b) \in Int

(***************************************************************************
--fair algorithm DieHarder {
variable injug = [j \in Jugs |-> 0] ;
{ while (~\E j \in Jugs : injug[j] = Goal)
{ either with (j \in Jugs) \* fill jug j
{ injug[j] := Capacity[j] }
or with (j \in Jugs) \* empty jug j
{ injug[j] := 0 }
or with (j \in Jugs, k \in Jugs \ {j}) \* pour from jug j to jug k
{ with ( poured =
Min(injug[j] + injug[k], Capacity[k]) - injug[k] )
{ injug[j] := injug[j] - poured ||
injug[k] := injug[k] + poured
}
}
}
}
}
***************************************************************************)
\* BEGIN TRANSLATION (chksum(pcal) = "b157a2cd" /\ chksum(tla) = "88d18fa9")
VARIABLES injug, pc

vars == << injug, pc >>

Init == (* Global variables *)
/\ injug = [j \in Jugs |-> 0]
/\ pc = "Lbl_1"

Lbl_1 == \/ /\ ~\E j \in Jugs : injug[j] = Goal
/\ pc = "Lbl_1"
/\ pc' = "Lbl_1"
/\ \/ /\ \E j \in Jugs:

injug' = [injug EXCEPT ![j] = Capacity[j]]

\/ /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = 0]
\/ /\ \E j \in Jugs:
\E k \in Jugs \ {j}:
LET poured == Min(injug[j] + injug[k], Capacity[k]) - injug[k] IN
injug' = [injug EXCEPT ![j] = injug[j] - poured,
![k] = injug[k] + poured]
\/ /\ pc' = "Done"
/\ UNCHANGED <<injug>>

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == Lbl_1
\/ Terminating

Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)

Termination == <>(pc = "Done")

\* END TRANSLATION

-----------------------------------------------------------------------------------------------------------------------

TypeOK == /\ injug \in [Jugs -> Nat]
/\ \A j \in Jugs : injug[j] \leq Capacity[j]

CommonDivisorsOfSet(S) == {d \in Int : \A s \in S : Divides(d,s)}

IsSetGCD(g,S) == g \in CommonDivisorsOfSet(S) /\ \A d \in CommonDivisorsOfSet(S) : g \geq d

SetGCDDividesAll == \A j \in Jugs : \A g \in Nat : IsSetGCD(g, {Capacity[k] : k \in Jugs}) => Divides(g, injug[j])

InductiveInvariantSetGCDDividesAll == /\ TypeOK
/\ SetGCDDividesAll

THEOREM Spec => []SetGCDDividesAll
<1>1. Init => InductiveInvariantSetGCDDividesAll
<2> SUFFICES ASSUME Init
PROVE InductiveInvariantSetGCDDividesAll
OBVIOUS

<2>1. TypeOK
PROOF BY CONSTANTS_OK DEF Init, TypeOK
<2>2. SetGCDDividesAll
<3> SUFFICES ASSUME NEW j \in Jugs,
NEW g \in Nat,
IsSetGCD(g, {Capacity[k] : k \in Jugs})
PROVE Divides(g, injug[j])
BY DEF SetGCDDividesAll

<3>1. Init => \A k \in Jugs : injug[k] = 0
PROOF BY DEF Init

<3>2. \A n \in Nat : Divides(n,0)
<4> SUFFICES ASSUME NEW n \in Nat
PROVE Divides(n,0)
OBVIOUS

<4>1. 0 = n * 0
OBVIOUS

<4>2. 0 \in Int
OBVIOUS

<4> QED
PROOF BY <4>1, <4>2 DEF Divides

<3> QED
PROOF BY <3>1, <3>2

<2>3. QED
BY <2>1, <2>2 DEF InductiveInvariantSetGCDDividesAll

<1>2. InductiveInvariantSetGCDDividesAll /\ [Next]_vars => InductiveInvariantSetGCDDividesAll '
<2> SUFFICES ASSUME InductiveInvariantSetGCDDividesAll,
[Next]_vars
PROVE InductiveInvariantSetGCDDividesAll '
OBVIOUS
<2>1. CASE Lbl_1
<3>1. TypeOK'
<4>1. ASSUME /\ ~\E j \in Jugs : injug[j] = Goal
/\ pc = "Lbl_1"
/\ pc' = "Lbl_1"
/\ \/ /\ \E j \in Jugs:

injug' = [injug EXCEPT ![j] = Capacity[j]]

\/ /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = 0]
\/ /\ \E j \in Jugs:
\E k \in Jugs \ {j}:
LET poured == Min(injug[j] + injug[k], Capacity[k]) - injug[k] IN
injug' = [injug EXCEPT ![j] = injug[j] - poured,
![k] = injug[k] + poured]
PROVE TypeOK'
<5>1. ASSUME /\ \E j \in Jugs:

injug' = [injug EXCEPT ![j] = Capacity[j]]

PROVE TypeOK'
<5>2. ASSUME /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = 0]
PROVE TypeOK'
<5>3. ASSUME /\ \E j \in Jugs:
\E k \in Jugs \ {j}:
LET poured == Min(injug[j] + injug[k], Capacity[k]) - injug[k] IN
injug' = [injug EXCEPT ![j] = injug[j] - poured,
![k] = injug[k] + poured]
PROVE TypeOK'
<5>4. QED
BY <4>1, <5>1, <5>2, <5>3

<4>2. ASSUME /\ pc' = "Done"
/\ UNCHANGED <<injug>>
PROVE TypeOK'

<5>1. injug' = injug

BY UNCHANGED <<injug>> DEF vars

<5>2. injug \in [Jugs -> Nat]
BY DEF TypeOK, InductiveInvariantSetGCDDividesAll

<5>3. \A j \in Jugs : injug[j] =< Capacity[j]
BY DEF TypeOK, InductiveInvariantSetGCDDividesAll

<5> QED
BY <5>1, <5>2, <5>3 DEF TypeOK

<4>3. QED
BY <2>1, <4>1, <4>2 DEF Lbl_1
<3>2. SetGCDDividesAll'
<3>3. QED
BY <3>1, <3>2 DEF InductiveInvariantSetGCDDividesAll

<2>2. CASE Terminating
BY Terminating DEF InductiveInvariantSetGCDDividesAll, vars, TypeOK, SetGCDDividesAll, Terminating
<2>3. CASE UNCHANGED vars
BY UNCHANGED vars DEF InductiveInvariantSetGCDDividesAll, vars, TypeOK, SetGCDDividesAll
<2>4. QED
BY <2>1, <2>2, <2>3 DEF Next

<1>3. InductiveInvariantSetGCDDividesAll => SetGCDDividesAll
BY DEF InductiveInvariantSetGCDDividesAll

<1>4. QED
PROOF BY <1>1, <1>2, <1>3, PTL DEF Spec

=============================================================================

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/JaLnG5ENnO0/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/bababc28-5384-45ef-8a4b-ca65ccabcdcan%40googlegroups.com.

Stephan Merz

unread,

May 18, 2025, 2:35:52 AMMay 18

to tla...@googlegroups.com

In general, facts to be used in a proof have to be referred to explicitly, so you have to write

<4>1. Terminating

BY <3>2

Note that within the proof of a step, the step number refers to the assumption of the step, whereas outside its proof, the step number refers to the sequent asserted by the step. (Sounds weird initially, but we found that we quickly got used to that convention.)

Of course, there is no need to restate the case assumption within the proof of step <3>2, just refer to <3>2 whenever you need it.

Exceptions to the general rule of having to refer to facts explicitly are:

- top-level assumptions introduced in a LEMMA / THEOREM statement,

- domain assumptions introduced by NEW x \in S,

- facts asserted by unnumbered steps <4> P(x,y,z)

These rules are admittedly arbitrary and could perhaps change. I agree that having to explicitly refer to CASE assumptions is a particular nuisance because their presence is so obvious to the user.

Stephan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/35127ca0-5166-43d4-8b78-4bd9ec5314ffn%40googlegroups.com.

Stephan Merz

unread,

May 18, 2025, 2:37:09 AMMay 18

to tla...@googlegroups.com

Same here:

<5>1. injug’ = injug

BY <4>2

Stephan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/bababc28-5384-45ef-8a4b-ca65ccabcdcan%40googlegroups.com.

Francisco José Letterio

unread,

May 18, 2025, 3:27:03 AMMay 18

to tla...@googlegroups.com

Oh my god it's become way easier to prove stuff now, thank you so much! I have one more question regarding writing proofs like this:

I have a proposition P that is written as a conjunction of some not-so-small formulas, like the step with the big assume under CASE Lbl_1 for proving TypeOK' in the last spec. I would like to be able to name the formulas used in the conjunction with something similar to a LET IN expression. Is there a way of doing something like that inside a proof?

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/JaLnG5ENnO0/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/03E212DD-3F8E-440D-9B10-BFA54ECF93C1%40gmail.com.

Francisco José Letterio

unread,

May 18, 2025, 3:37:05 AMMay 18

to tla...@googlegroups.com

Regarding your reply earlier:

"The second problem should be easier to solve. It sounds like the prover cannot figure out that j \in DOMAIN injug. Is the assumption injug \in [Jugs -> Nat] (which probably comes from a type-correctness predicate) part of the hypotheses of the proof step?"

It was indeed a missing definition for the DOMAIN. Thanks for pointing it out

Francisco José Letterio

unread,

May 18, 2025, 6:45:51 PMMay 18

to tla...@googlegroups.com

I'm finally back at the proof I had earlier that uses a CHOOSE.

ASSUME
NEW CONSTANT Jugs,
NEW CONSTANT Capacity,
NEW CONSTANT g \in Nat,
g
= (CHOOSE i \in CommonDivisorsOfSet({Capacity[k] : k \in Jugs}) :
\A j_1 \in CommonDivisorsOfSet({Capacity[k] : k \in Jugs}) :
i >= j_1)' ,
PROVE g \in CommonDivisorsOfSet({Capacity[k] : k \in Jugs})

I feel like this one should be trivial, but maybe I need to assert that the CHOOSE is well-defined? Or why else is TLAPS not able to deduce that g is picked from that set?

Stephan Merz

unread,

May 19, 2025, 2:33:10 AMMay 19

to tla...@googlegroups.com

This one is non-trivial. You are taking the maximum value of a set of integers, which is well-defined only if the set is non-empty and finite. I suggest splitting this into two parts:

Max(S) == CHOOSE x \in S : \A y \in S : x >= y

LEMMA MaxLemma ==

ASSUME NEW S \in SUBSET Int, IsFiniteSet(S)

PROVE /\ Max(S) \in S

/\ \A y \in S : Max(S) >= y

LEMMA CDSLemma ==

ASSUME NEW S \in SUBSET Int, IsFiniteSet(S)

PROVE /\ CommonDivisorsOfSet(S) \in SUBSET Int

/\ IsFiniteSet(CommonDivisorsOfSet(S))

(By the way, the operator Max is defined like this in module FiniteSetsExt of the community modules [1].)

Omit the proofs of these two lemmas for now and use them to prove your overall goal (restating it in terms of the Max operator). This will in particular require proving

IsFiniteSet({Capacity[k] : k \in Jugs})

which can be done using lemma FS_Image from module FiniteSetTheorems.

The proof of the first lemma will eventually show up in module FiniteSetsExt_theorems in the community modules, but if you want to try your hand at proving it, using theorem FS_Induction will be helpful. The proof of the second lemma will also require some work with lemmas about finite sets.

Stephan

[1] https://github.com/tlaplus/CommunityModules/tree/master/modules

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAP%2BdMusPcopaYWvkeu9hi%2BmG0enDqRQpxSr1rLk3zPDsKJAK1A%40mail.gmail.com.

Stephan Merz

unread,

May 19, 2025, 2:38:05 AMMay 19

to tla...@googlegroups.com

TLA+ has a syntax for naming sub-formulas of a big formula, see [1]. For example, the n-th conjunct of a conjunction P can be referred to as P!n.

Stephan

tla2-guide

PDF Document · 344 KB

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAP%2BdMus%3Dkq4XWa98FUcv1h3fzxi5%3Dd7SDgRxsRNB7H9qbhOZVQ%40mail.gmail.com.

Reply all

Reply to author

Forward