search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
67 stars 20 forks source link

Contradictory warning with ExpandENABLED #40

Open lemmy opened 3 years ago

lemmy commented 3 years ago

"A has expression level 2 within the scope of ENABLED or \cdot where soundness requires expanding expressions of level >= 2."

THEOREM ASSUME NEW ACTION A PROVE (ENABLED A) BY ExpandENABLED
Error: The expression that results from applying the declared operator `A` has expression level 2 within the scope of `ENABLED` or `\cdot` where soundness requires expanding expressions of level >= 2. A declared operator cannot be expanded.
The operator `A` is declared at:
File "./frob.tla", line 25, characters 20-27
 and has level: 2
 and arity: 0
johnyf commented 3 years ago

This error means that tlapm needs to expand the operator A, but cannot expand A, because A is a declared operator. So tlapm cannot proceed with trying to prove this sequent.

The reason that tlapm raises this error is because the proof directive ExpandENABLED has been given, and the sequent has this form. The proof directive ExpandENABLED means that tlapm is requested to replace ENABLED with quantification. So if, for any reason, tlapm cannot proceed with this replacement, tlapm raises an error.

When replacing ENABLED with quantification, any expressions within the scope of ENABLED that have expression level 2 (higher expression level is syntactically impossible to appear within the scope of ENABLED) need to be expanded, so that if the expression level is caused by the presence of primed variables, then those primed variables will appear, and thus be converted to constants bound by existential quantification \E.

The expression A is within the scope of ENABLED and has expression level 2. The expression A also contains something unexpanded, namely the operator A. So the occurrence of the operator A needs to be expanded. However, such an expansion is impossible, because A is a declared operator, and not a defined operator (in which case it would have been possible to replace the identifier A with its definition).

As a result, tlapm raises an error. In this case, tlapm cannot proceed with further reasoning about this occurrence of ENABLED, because sound replacement of ENABLED by quantification \E requires that first A be expanded.

The error message refers to "expanding expressions", instead of expansion of operators, because in general what may need to be expanded can be an expression that is not the occurrence of only an operator. For example, the expression with high level could be the application of a first-order operator:

ASSUME ACTION B(_)
PROVE ENABLED B(TRUE)

Writing BY ExpandENABLED for the above sequent would raise a similar error, about the expression B(TRUE) (with the difference that it would say that operator B has "arity: 1"). This expression is the application of an operator, and has expression level 2. So the expression needs expansion, which, if B was a defined and not a declared operator, would involve expanding B and applying it to TRUE.

(Note: The phrase "if the expression level is caused by the presence of primed variables" above alludes to the case of a defined operator that has expression level 2, but contains no primed variables, for example R == TRUE' is such a defined operator.)

The "or \cdot" in the error message is present for cases that the error would be raised when using the proof directive ExpandCdot. For example:

ASSUME ACTION B
PROVE B \cdot TRUE