Re: [tlaplus] Question about importance of "⊨ F⇒ G implies ⊨ □F ⇒□G"

In https://lamport.azurewebsites.net/pubs/lamport-actions.pdf, Figure 5 mentions various rules of
Simple Temporal Logic, Basic and Additional Rules of TL.

Further is mentioned that The validity of TLA1–SF2 can be proved using STL1–STL6 and
the RTLA rule □P ≡ P ∧ □(P ⇒ P ′). It would be instructive to prove any of TLA1-SF2 and see

how rule STL4 is used (Rules TLA1-SF2 can be used to prove invariants, leads to proofs when

action is weakly fair and strongly fair etc).

When I tried to prove WF1 I reached out to STL4.

Using backward chain of reasoning

To prove □[N]_f ∧ WF_f (A) ⇒ (P ~> Q),
I need to prove □([N]_f ∧ ([]Enabled <A>_f ⇒ ◇ <A>_f)) ⇒ (P ~> Q) (Rule STL5),

I need to prove [N]_f ∧ ([]Enabled (A)_f ⇒ ◇ A_f) ⇒ (P ⇒ ◇ Q) (Rule STL4) ...

Thanks

Divyanshu Ranjan

On Mon, Dec 2, 2024 at 7:36 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

Also think of refinement: infer [][LowNext]_lv => [][HighNext]_hv from [LowNext]_lv => [HighNext]_hv. In practice, we generalize a bit and infer []Inv /\ [][LowNext]_lv => [][HighNext]_hv from Inv /\ [LowNext]_lv => [HighNext]_hv, but this essentially just combines the basic rule with the fact that [](A /\ B) <=> []A /\ []B.

And in general, that rule underlies a lot of "simple temporal reasoning".

Stephan

On 2 Dec 2024, at 14:52, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

--
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/08616DEF-ACE0-42DA-8DC3-3753448405F8%40gmail.com.