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

On Saturday, May 17, 2025 at 8:38:34 PM UTC-3 Francisco José Letterio wrote:

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
On Saturday, May 17, 2025 at 8:36:31 PM UTC-3 Francisco José Letterio wrote:
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

On Saturday, May 17, 2025 at 7:57:47 PM UTC-3 Francisco José Letterio wrote:
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)

On Saturday, May 17, 2025 at 4:49:28 AM UTC-3 Stephan Merz wrote:
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

On 16 May 2025, at 08:17, Francisco José Letterio <fj.le...@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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/c8233fc9-e526-48df-994a-9c3325c05e00n%40googlegroups.com.