Re: [tlaplus] Trouble with proofs involving CHOOSE or EXCEPT

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

On 16 May 2025, at 08:17, Francisco José Letterio <fj.letterio@xxxxxxxxx> wrote:

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?

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