| 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 On 18 May 2025, at 01:36, Francisco José Letterio <fj.letterio@xxxxxxxxx> 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
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/35127ca0-5166-43d4-8b78-4bd9ec5314ffn%40googlegroups.com.
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/0148BC73-214C-46A3-8088-0D7DB1220A41%40gmail.com.
|