learning_tla/learn_tla/core/03-writing-invariants.md

3. Writing invariants

IF/THEN/ELSE equivalences

IsCorrect == IF pc == "Done" THEN is_unique = IsUnique(seq) ELSE TRUE
\* can be written as
IsCorrect == pc == "Done" => is_unique = IsUnique(seq)

More generally,

(IF p THEN q ELSE TRUE) = (IF !p THEN TRUE ELSE q)
                        = !p \/ q
                        = p => q

(IF p THEN q ELSE FALSE) = p /\ q

Quantifiers

Caution:

• \A x \in {}: whatever is ALWAYS true.
• \E x \in {}: whatever is ALWAYS false
• This is the ONLY case where "forall" can be true when "exists" is not.

Do not use => with \E, e.g.:

WARNING: the duplicates.tla which the page says fails actually succeeds.

---- MODULE foo ----
HasDuplicates(seq) == 
  \E i, j \in 1..Len(seq):
    i # j => seq[i] = seq[j]
(* Consider seq = <<1>>
    The single case is i = j = 1, 
    => i # j = FALSE
    => seq[i] = seq[j]
    => HasDuplicates(seq) = TRUE
    
Instead do:
*)    
HasDuplicates(seq) ==
  \E i, j \in 1..Len(seq):
    i # j /\ seq[i] = seq[j]
====

Quantifiers cannot be used on sequences, because they are not sets, but the sequence indices are a set.