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,StephanOn 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 aI 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 haveinjug' = [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 propositionHas 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.