Re: [tlaplus] Using the primed variables in proofs

On Fri, Oct 18, 2019 at 12:48 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

Hello,

I don't understand your question. What is the overall assertion that you would like to prove?

It sounds like you want to chain two actions together in a single line of reasoning. But what would this be good for: you don't control how actions are scheduled. In a behavior of your specification, after a first occurrence of the F action there might be another occurrence of the same action? And anyway a proof is purely declarative, there is no notion of dynamic system behavior or "implicit update" of state.

You may want to prove an invariant of your system, and then you need to prove that both F and G maintain the invariant from any state that satisfies it, independently if they directly follow each other or not.

Also note that your definition of action G looks suspicious: if SomeSet \cap var contains, say, two elements d and e, then you'd have to satisfy both SomeAction(d) and SomeAction(e), which is unlikely to work.

To answer your precise question, you cannot use <n>1 to prove your step <n>3 but you can (of course) use it to prove

<n>3a. \E x \in SomeSet : x \in var' \* equivalent to "SomeSet \cap var' # {}"

although this is not likely to be very useful.

Regards,
Stephan

On 18 Oct 2019, at 18:30, Saswata Paul <paulsaswata1@xxxxxxxxx> wrote:

HI,

I was wondering if there is a smart way to use the primed variables in the proofs in order to use them for implication chaining.

For example:

Let us assume we have a variable var.

var = {} initially

If we have two rules F == \E x \in SomeSet : (var' = var \cup {x})

and G == \A x \in SomeSet : x \in var => SomeAction(x)

What should be the approach to prove SomeAction(x) using these two rules?

...
<n>1. \E x \in SomeSet : (var' = var \cup {x})
PROOF

<n>2. \A x \in SomeSet : x \in var => SomeAction(x)
PROOF

<n>3. \E x \in SomeSet : x \in var
** Is there any inherent property of the primed variables that can be used to prove this from step <n>1? **

<n>4. \E x \in SomeSet : SomeAction(x)
BY <n>2, <n>3
...

Basically, the essence of my question is - since var' represents the new state of var, can we use this new state to prove something that depends on the current state? Doesn't the new state implicitly become the current state once it is updated?

Thank you

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/21faa3af-ecde-490a-b824-246ceea7bc07%40googlegroups.com.

--
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/J18UWKvR24c/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/00FFDC65-91F4-4E66-A0F6-F2F7D50997F5%40gmail.com.