# Re: [tlaplus] tuples in function constructors using tlapm ?

Hi Stephan,

Thank you for explaining this behavior and suggesting currying as a workaround.
I used a definition of the form:

H(f) == [t \in Z \X Z |-> f[t[2], t[1]]]

and that led to some reasoning in the proofs about the domain having the
form of a Cartesian product. In this case it was convenient to keep working
with functions of tuples, but I will try currying the next time this arises.

About the error messages from the backends, I was running tlapm -v from the
command line, and there it prints fewer details about the kind of backend
errors. It did record the following messages in the file test.tlaps/fingerprints
(which can be viewed in readable form with tlapm --printfp):

isabelle : unsupported operator function (tuple)
Zenon: unsupported operator Fcn (tuple)

(I should have used the toolbox.)

Best regards,
ioannis

On Thu, Apr 20, 2017 at 1:03 AM, Stephan Merz wrote:
Hi Ioannis,

as you noticed (and as stated on the Web site), the parser of the PM rejects any bindings involving tuples, such as

\E <<x,y>> \in S : ...   or    { ... : <<x,y>> \in S }

The next major release of TLAPS will be based on the SANY parser, so this limitation will disappear, but we don't know yet when the release will be ready.

Additionally, the backends currently have extremely poor support for functions that take more than one argument, such as in your example

g == [a, b \in S |-> TRUE]
THEOREM g = [a, b \in S |-> TRUE]
BY DEF g

If you look at the messages in the TLAPM console, you'll see that SMT, Zenon and Isabelle all complain about unsupported constructs. For the moment, I recommend as a workaround that you use "curried" functions instead and replace

[a,b \in S |-> TRUE]   by   [a \in S |-> [b \in S |-> TRUE]]

and similarly

[S \X T -> U]   by   [S -> [T -> U]]

Regards,
Stephan

On 19 Apr 2017, at 22:41, Ioannis Filippidis <jfili...@xxxxxxxxx> wrote:

This question seems to be answered by the documentation about partially supported features [1],
but I would like to confirm I am not doing something wrongly.

tlapm does not parse syntax of the form: 
[<< a, b >> \in S |-> TRUE], so it appears to be unsupported.
tlapm parses [a \in S, b \in S |-> TRUE] and [a, b \in S |-> TRUE], but it does not prove equality,
as shown in the module below. Is such syntax unsupported by tlapm == 1.4.3?

Does the development version of tlapm support syntax of this form?
Searching through the repository for usage of |->, I couldn't find any example of this form, except for a comment [2].

[1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html
[2] https://github.com/tlaplus/v2-tlapm/blob/fd345f78c7e356b53c67e24f17e99df449d7b3a3/src/oldpm/expr.ml#L81

Best regards,
ioannis

------------------------------- MODULE test --------------------------------
(* tlapm --version
1.4.3 (build 34695)
*)
CONSTANT S

(* tla2sany test.tla confirms that the theorem below is well formed (p.304).

tlapm -v -C test.tla raises:

File "./test.tla", line 3, character 8
required expressions(s) missing before '['
File "<unknown>":
Error: Could not parse "./test.tla" successfully.
tlapm ending abnormally with Failure("Module.Parser.parse_file")
*)
(*
f == [<< a, b >> \in S |-> TRUE]
THEOREM f = [<< a, b >> \in S |-> TRUE]
BY DEF f
*)

(* The below is well formed too, but tlapm raises:

Error: Could not prove or check:
ASSUME NEW CONSTANT S,
g == [a, b \in S |-> TRUE]
PROVE  g = [a, b \in S |-> TRUE]
*)
g == [a, b \in S |-> TRUE]
THEOREM g = [a, b \in S |-> TRUE]
BY DEF g

(* tlapm can prove the following claims. *)
h == [a \in S |-> TRUE]
THEOREM h = [a \in S |-> TRUE]
BY DEF h

p == [t \in S \X S |-> << t[1], t[0] >> ]
THEOREM p = [t \in S \X S |-> << t[1], t[0] >> ]
BY DEF p
================================================================================

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.