Proposal: remove INSTANCE and BY MODULE proof types from language

[ahelwer]

These are currently supported by SANY but not TLAPM. See tlaplus/tlapm#166 and tlaplus/tlapm#167, and also this recent discussion on the mailing list. Basically this is a way of importing all definitions from a module in various places. Stephan Merz (@muenchnerkindl) wrote:

IMHO, it would indeed be better to remove this syntax from the language, as well as the similar "BY MODULE" construct. These constructs look like a maintainer's headache because changes to a module could cause proof failures elsewhere that are hard to understand. Mild reformulations of facts and even additions of new theorems can confuse the provers to the point that existing proofs may fail. Instead, appealing to specific facts from a module indicates what is needed for a proof step to go through. Expanding all definitions contained in a module breaks the abstraction barrier: usually, one uses definitions to prove facts about operators and then uses those theorems, forgetting the actual definition.

Quoting from TLA Version 2: A Preliminary Guide [pdf], page 20:

The parser also allows the following two kinds of “facts” in a use or hide statement. However, they are not supported by TLAPS and are likely to be removed from the language:

• MODULE Name, indicating that all known facts obtained from the module Name are to be added or removed from the set of usable facts. The module name must appear in an extends or instance statement or else be the name of the current module.

Separately (but related), INSTANCE proof steps are defined in section 7.5.2 on page 27 of the same guide:

An INSTANCE step consists of a step-starting token followed by an ordinary INSTANCE statement (one that begins with the keyword INSTANCE). It has the same effect on the state as the corresponding (top-level) statement.

This seems like a good warm-up application for the Specification Language Committee (SLC). Currently TLAPM would not need to be modified, although SANY and the tree-sitter grammar would have to be modified to remove support for these constructs. This does not seem like a very large amount of work since nothing depends on the functionality.