# Re: [tlaplus] Trying to figure out how theorems work with this basic example

The assumptions can be used in proving the theorems.  You can write
proofs in TLA+ and check them with the TLAPS proof system.  The TLA+
Proof Track (chapters 10-13) of the TLA+ Hyperbook probably provides
the best introduction to TLAPS. However, I recommend that you stick
with TLC until you have a good basic understanding of TLA+.

Leslie

On Sunday, December 9, 2018 at 11:43:22 AM UTC-8, Dominykas Mostauskis wrote:
Thanks, that helped figure out quite a few things.

What I'm now trying to understand is the difference between ASSUME and THEOREM, or rather what to use THEOREM for. I've tried looking that up on Specifying Systems, but I'm still somewhat lost. Quoting from 17.7:

> More precisely, let A be the conjunction of all the assumptions in Ass. The module asserts that, for every theorem T in Thm, the formula A => T is valid.

So Thm defines what the assumptions in Ass imply. Is it just for the human reader? Or is there some way to use that in checking models or specs?

On Saturday, December 8, 2018 at 7:15:57 PM UTC+1, Stephan Merz wrote:
Hello,

first, TLC will not evaluate your definitions of Numbers because it involves a set comprehension whose base set (Nat) is infinite. I replaced it by

Numbers == 10 .. 99

which TLC can evaluate.

Concerning your question, you did not describe how exactly you ran the model checker. Your module does not contain a behavior specification, contrary to the most common use case for TLC. Perhaps you believe that TLC checks your THEOREM statement, this is not the case. If you just click on the green triangle in the model checking pane of the Toolbox, TLC doesn't find anything to do and simply terminates successfully.

You can however use TLC to check assumptions on constant module parameters: replacing THEOREM by ASSUME will either return in no output (e.g., when you choose the set {10, 14, 22} for input) or in the output "Assumption line ... is false." (when input is {10,16,22}, for example).

It is a little nicer to use TLC's facility of evaluating constant expressions. I replaced your THEOREM by the definition

ValidInput == input \subseteq NumbersThatDivideBy2Once

and then entered ValidInput in the field "Evaluate Constant _expression_" of the sub-pane "Model Checking Results". Running TLC will print TRUE or FALSE in the "Value" field.

You can use the same facility for evaluating the operator NumbersThatDivideBy2Once and make TLC output the entire set.

Below is the module that I used for my experiments.

Hope this helps,
Stephan

----------------------------- MODULE TestModule -----------------------------
EXTENDS Naturals

CONSTANT input

\* Numbers == { n \in Nat : n > 9 /\ n < 100 }

Numbers == 10 .. 99

DividesBy2(n) == (n % 2) = 0

DividesBy2Once(n) == DividesBy2(n) /\  ~DividesBy2(n \div 2)

NumbersThatDivideBy2Once == { n \in Numbers: DividesBy2Once(n) }

ValidInput == input \subseteq NumbersThatDivideBy2Once

=============================================================================

On 8 Dec 2018, at 18:53, dominy...@xxxxxxxxx wrote:

The below module declares a set of numbers that are in the range 10 to 99 that are divisible by 2 only once and call it NumbersThatDivideBy2Once. At the end it declares a theorem that the constant input is a subset of NumbersThatDivideBy2Once.


--------------------------- MODULE TestModule ---------------------------
EXTENDS Naturals

CONSTANT input

Numbers == { n \in Nat : n > 9 /\ n < 100 }

DividesBy2(n) == (n % 2) = 0

DividesBy2Once(n) == DividesBy2(n) /\  ~DividesBy2(n \div 2)

NumbersThatDivideBy2Once == { n \in Numbers: DividesBy2Once(n) }

THEOREM input \subseteq NumbersThatDivideBy2Once

=======================


How can I check if this theorem holds for a given input? If I run a model check with a provided set of numbers as input, even if some of those numbers are not part of NumbersThatDivideBy2Once I still get no errors.