Proposal: Remove `[]ASSUME`/`[]PROVE` construct from the language

[ahelwer]

In the same vein as #17 and #18, some "janitorial"-level changes to the language spec. Actually it isn't really clear that this construct was ever fully part of the language spec, but it is fully supported by SANY so that probably elevates it to the level of deserving discussion.

Many TLAPM users will be familiar with the ASSUME/PROVE construct:

---- MODULE Test ----
THEOREM
  ASSUME TRUE
  PROVE TRUE
====

SANY also supports another construct, seemingly a temporal variant:

---- MODULE Test ----
THEOREM
  []ASSUME TRUE
  []PROVE TRUE
====

TLAPM does not parse this file. What the construct does or means I have no idea, as it is not covered in the TLA+2 language guide nor in any other document I can find. It is, however, supported at both the syntactic and semantic level of the SANY TLA+ parser; see references to it here: https://github.com/search?q=repo%3Atlaplus%2Ftlaplus%20%5B%5DASSUME&type=code

A comment reveals it was added by Leslie Lamport February 9th, 2011.

Unless this construct enables writing proofs that can currently not be written or could be associated with some compelling feature, I propose removing it from (not adding it to?) the TLA+ language specification. Work entailed:

1. Remove SANY support for this construct at the semantic level
2. Remove SANY support for this construct at the syntax level
3. Amend the various standardized test corpora to ensure all TLA+ parsers reject this syntax

Found during work on tlaplus/tlaplus#1140

[muenchnerkindl]

Short answer: []ASSUME []PROVE is not part of the TLA+ language, and SANY support for the construct should be removed.

Explanation:

Unlike in first-order logic, in temporal logic a sequent F |- G (that would naturally be written ASSUME F PROVE G in the TLA+ proof language) does not have the same meaning as F => G being valid. Instead, you want the assumptions on the left-hand side of the sequent to have an implicit []. For example, the necessitation rule F |- []F is a staple of reasoning in modal and temporal logic.

When we designed the proof language, we discussed introducing a variant of ASSUME PROVE for use in temporal reasoning, which would have been called []ASSUME []PROVE. After a lot of back and forth, we finally decided that having an extra construct would be too confusing for users. Instead, the PM checks if all assumptions in the context of a temporal-logic proof are indeed "boxed" and then implicitly promotes any conclusions G to []G. This is why steps that will be used in PTL reasoning must usually be written as implications such as

Inv /\ [Next]_v => Inv'

rather than

ASSUME Inv, [Next]_v PROVE Inv'

– the latter would introduce non-boxed assumptions. And the check for boxed contexts is still brittle, cf. tlaplus/tlapm#196.

In his quest for simplicity, Leslie vigorously opposed the idea of a distinguished form of temporal ASSUME PROVE constructs, so I am surprised that he nevertheless added support for them in SANY. But indeed that support should be removed.

[ahelwer]

Thanks for the explanation! Does F ⊢ G mean the same thing as ⊨ F ⇒ G, the notation used in A Science of Concurrent Programs?

[muenchnerkindl]

No, in modal or temporal logic the sequent F |- G corresponds to |- []F => G.