TLAPS proves via SMT that `Len(x) \in Nat` for arbitrary x

[johnyf]

TLAPS v1.4.3 proves that any set x has Len(x) \in Nat. This is expected to be unprovable, and likely invalid, because Len is defined using CHOOSE (in the module Sequences). Pages below refer to the TLA+ book.

---- MODULE LenInNat ----
EXTENDS Sequences, Integers, TLAPS

(* The module Sequences from the TLA+ standard library defines (p. 341):
Len(s) == CHOOSE n \in Nat:  DOMAIN s = 1..n
*)

(* TLAPS v1.4.3 proves the claim `AllLenInNat` using an SMT backend,
even though this claim appears to be unprovable, based on the theorem
`NotNatDom` below. If there is a model of TLA+ where:

    (CHOOSE n:  FALSE) \notin Nat

then this claim is invalid (see also p. 295).
*)
THEOREM AllLenInNat ==
    ASSUME NEW x
    PROVE Len(x) \in Nat
OBVIOUS

(* There exists a set foo with domain that, for all n \in Nat,
is unequal to 1..n. So it is impossible to

    CHOOSE n \in Nat:  DOMAIN foo = 1..n

Thus, Len(foo) = CHOOSE n:  FALSE. As far as I know,
the TLA+ axioms leave unspecified whether this value is in Nat.
*)
THEOREM NotNatDom ==
    LET
        foo == [n \in Nat |-> n]
    IN
        ~ \E n:  /\ n \in Nat
                 /\ (DOMAIN foo) = (1..n)
OBVIOUS

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

(* The operator LenDup is defined with the same expression that defines the
operator Len in the module Sequences.
*)
LenDup(s) == CHOOSE n \in Nat:  DOMAIN s = 1..n

(* TLAPS cannot prove the following (as expected). *)
THEOREM
    ASSUME NEW x
    PROVE LenDup(x) \in Nat
OBVIOUS

The SMT encoding of the theorem AllLenInNat is (tlapm --debug tempfiles -v -C --cleanfp LenInNat.tla):

;; Proof obligation:
;;ASSUME NEW CONSTANT x
;; PROVE  Len(x) \in Nat
(set-logic AUFNIRA)
(declare-sort u 0)
;; Declaration of terms, predicates and strings
;; Axioms
;; Conclusion
(assert (not true))
;; Main assertions from the proof obligation
(check-sat)
(exit)

[johnyf]

The issue appears to arise due to the assertion Len(x) \in Nat about the Len operator of the module Sequences being builtin to TLAPS. Renaming the module Sequences to Sequences_copy makes TLAPS not prove AllLenInNat (as expected), and also not prove:

---- MODULE LenInNat_copy ----
EXTENDS
    Integers,
    Sequences_copy,
    TLAPS

THEOREM AllLenInNat ==
    ASSUME NEW x
    PROVE Len(x) \in Nat
BY DEF Len, Seq

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