Arity of NEW operator in `tlapm`

[Ioannis Filippidis]

I am trying to prove that the image of a finite set under an operator is finite (relevant to [1]),

to reuse it at multiple places. If I write a proof similar to that of `ImageOfFinite` below
for some specific operator `Op`, for example:

<2> DEFINE

    Op(u, a, b) == u

    f == [u \in S |-> Op(u, arg1, arg2)]
<2>1. f \in Surjection(S, H)
    BY DEF Surjection, Hdef
<2> QED
    BY <2>1, ..., FS_Surjection

then `tlapm -v -C` proves it, and I don't see any intermediate errors (using version 1.4.3).

`tlapm` proves correct also the module `test2` below, but with an error from the SMT backend (see below),

which can probably be ignored, because only the Isabelle backend supports the declaration `NEW Op(_)` [2].

However, if I change the assumption to `NEW Op(_, _)` in `ImageOfFinite`,
or the operator application to `Op(x)` in `ImageOfFinite2`,
then the proof is again successful, but SANY detects the errors.

Question 1: If SANY detects no errors and `tlapm` proves module `test2` correct,

should I assume that the arity of operator declarations as those in module `test2`

has been taken into account correctly?

Question 2: Is there an approach simpler/better than a couple of theorems for different arities to

prove that `IsFiniteSet(S)` implies `IsFiniteSet( { Op(x, ...):  x \in S } )`

as a theorem that we can reuse?

Sidenote: To invoke `ImageOfFinite3` successfully, I had to hide the definition of `S`,

but at least I didn't rewrite a proof like that of `ImageOfFinite`.

```
*** Fatal exception:
Type Checking error: Expected function type for:

a_Opunde_1a

 but got this: u

 in function application:

(_APPLY {a_Opunde_1a} x)
test2.tlaps/tlapm_d7953c.smt:50: this is the location of the error

...

Checking the proofs with Isabelle. This may take a long time.
(* Isabelle interaction log in "test2.tlaps/isabelle.log" *)
(* Isabelle parsing "test2.tlaps/test2.thy" ... done *)
(* Obligation checking trace follows. *)
(* +5 -5 +7 -7 *)
Proof checking done. No errors found.
```


------------------------------- MODULE test2 --------------------------------
LEMMA ImageOfFinite ==
    ASSUME
        NEW S, NEW Op(_),
        IsFiniteSet(S)
    PROVE
        LET
            Img == { Op(x):  x \in S }
        IN
            /\ IsFiniteSet(Img)
            /\ Cardinality(Img) <= Cardinality(S)
    <1> DEFINE
        Img == { Op(x):  x \in S }
        f == [x \in S |-> Op(x)]
    <1>1. f \in Surjection(S, Img)
        BY DEF Surjection
    <1> QED
        BY <1>1, FS_Surjection

COROLLARY ImageOfFinite2 ==
    ASSUME
        NEW S, NEW arg2, NEW Op(_, _),
        IsFiniteSet(S)
    PROVE
        LET
            Img == { Op(x, arg2):  x \in S }
        IN
            /\ IsFiniteSet(Img)
            /\ Cardinality(Img) <= Cardinality(S)
    BY ImageOfFinite

COROLLARY ImageOfFinite3 ==
    ASSUME
        NEW S, NEW arg2, NEW arg3, NEW Op(_, _, _),
        IsFiniteSet(S)
    PROVE
        LET
            Img == { Op(x, arg2, arg3):  x \in S }
        IN
            /\ IsFiniteSet(Img)
            /\ Cardinality(Img) <= Cardinality(S)
    BY ImageOfFinite
============================================================================

[1] https://github.com/tlaplus/v2-tlapm/blob/fd345f78c7e356b53c67e24f17e99df449d7b3a3/library/FiniteSetTheorems.tla#L108
[2] http://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html

Best regards,

ioannis

[Stephan Merz]

Hi Ioannis,

On 9 May 2017, at 08:09, Ioannis Filippidis <jfili...@gmail.com> wrote:

I am trying to prove that the image of a finite set under an operator is finite (relevant to [1]),

to reuse it at multiple places.

thanks, this is a useful corollary to FS_Surjection (please also note the comment in FiniteSetTheorems indicating that the theorem implies that the image of a finite set under any function is finite).

If I write a proof similar to that of `ImageOfFinite` below
for some specific operator `Op`, for example:

<2> DEFINE

    Op(u, a, b) == u

    f == [u \in S |-> Op(u, arg1, arg2)]
<2>1. f \in Surjection(S, H)
    BY DEF Surjection, Hdef
<2> QED
    BY <2>1, ..., FS_Surjection

then `tlapm -v -C` proves it, and I don't see any intermediate errors (using version 1.4.3).

`tlapm` proves correct also the module `test2` below, but with an error from the SMT backend (see below),

which can probably be ignored, because only the Isabelle backend supports the declaration `NEW Op(_)` [2].

Yes: the message from the SMT backend indicates a limitation of the backend, which stumbles over the apparent "mismatch" of arities. This is one of the situations where the Isabelle backend is useful, due to higher-order unification.

However, if I change the assumption to `NEW Op(_, _)` in `ImageOfFinite`,
or the operator application to `Op(x)` in `ImageOfFinite2`,
then the proof is again successful, but SANY detects the errors.

This is indeed a syntax error and should be rejected. Our working hypothesis is that the prover is called only on input that has been checked by SANY (if you use the Toolbox, the prover will not be started on modules that contain a syntax error). The next (major) release of TLAPS will be based on the SANY parser, so you will not be able to run the prover on that module anymore.

Question 1: If SANY detects no errors and `tlapm` proves module `test2` correct,

should I assume that the arity of operator declarations as those in module `test2`

has been taken into account correctly?

Yes.

Question 2: Is there an approach simpler/better than a couple of theorems for different arities to

prove that `IsFiniteSet(S)` implies `IsFiniteSet( { Op(x, ...):  x \in S } )`

as a theorem that we can reuse?

In fact, I'd simply apply ImageOfFinite, just as you do in the proofs of the theorems for operators of different arities. Since the other arguments must be fixed, the operator is effectively unary. For example:

LEMMA

  ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S), NEW n \in Nat

  PROVE  IsFiniteSet({x+n : x \in S})

BY ImageOfFinite

However, this again requires higher-order unification, so only Isabelle will prove the step, and you may have to "isolate" the application of the theorem and not combine it with, say, arithmetic reasoning.

Sidenote: To invoke `ImageOfFinite3` successfully, I had to hide the definition of `S`,

but at least I didn't rewrite a proof like that of `ImageOfFinite`.

Indeed, if S is a complex expression, there may be some rewriting going on before Isabelle's classical prover gets to see the term, preventing successful unification. In such cases, you may be successful using "BY IsaM("blast")", which essentially disables rewriting. We'd like to hide these backend-specific idiosyncrasies from users, but we're not there yet.

```
*** Fatal exception:
Type Checking error: Expected function type for:

a_Opunde_1a

 but got this: u

 in function application:

(_APPLY {a_Opunde_1a} x)
test2.tlaps/tlapm_d7953c.smt:50: this is the location of the error

...

As mentioned above, this only indicates a failure of the backend and doesn't mean that there is something wrong with your input.

Checking the proofs with Isabelle. This may take a long time.
(* Isabelle interaction log in "test2.tlaps/isabelle.log" *)
(* Isabelle parsing "test2.tlaps/test2.thy" ... done *)
(* Obligation checking trace follows. *)
(* +5 -5 +7 -7 *)
Proof checking done. No errors found.
```

Please note that at this point we can only check proofs found by Zenon, not those found by SMT.

Regards,

Stephan

[Ioannis Filippidis]

Hi Stephan,

Thank you very much for the detailed answer.
Please find comments inline below.

Best regards,
ioannis

On 5/8/17 11:50 PM, Stephan Merz wrote:
> Hi Ioannis,
>

>> On 9 May 2017, at 08:09, Ioannis Filippidis <jfili...@gmail.com <mailto:jfili...@gmail.com>> wrote:
>>
>> I am trying to prove that the image of a finite set under an operator is finite (relevant to [1]),
>> to reuse it at multiple places.
>
> thanks, this is a useful corollary to FS_Surjection (please also note the comment in FiniteSetTheorems indicating that the theorem implies that the image of a finite set under any function is finite).
>

Thanks for pointing at that comment. Initially I was considering using `FS_Surjection` together with
`Fun_RangeProperties` [1], but the result would be about functions, and I wanted to use it for operators.

For posterity, an alternative approach is to first prove that the image of a finite set under
a function is finite, and use that to prove the same result about the image of a finite set under
a unary operator (all functions are unary (p.50 of the TLA+ book), so we don't need cases for them).
This can be done as follows:


------------------------------- MODULE Images ----------------------------------
EXTENDS FiniteSetTheorems, FunctionTheorems


LEMMA FuncImageOfFinite ==
ASSUME
NEW S, NEW T, NEW f \in [S -> T],
IsFiniteSet(S)
PROVE
LET
Img == { f[x]: x \in S }

IN
/\ IsFiniteSet(Img)
/\ Cardinality(Img) <= Cardinality(S)

<1> DEFINE Img == { f[x]: x \in S }

<1>1. f \in Surjection(S, Img)

BY Fun_RangeProperties DEF Range

<1> QED
BY <1>1, FS_Surjection

LEMMA OpImageOfFinite ==

ASSUME
NEW S, NEW Op(_),
IsFiniteSet(S)
PROVE
LET
Img == { Op(x): x \in S }
IN
/\ IsFiniteSet(Img)
/\ Cardinality(Img) <= Cardinality(S)
<1> DEFINE

f == [x \in S |-> Op(x)]

fImg == { f[x]: x \in S }
<1>1. f \in [S -> fImg]
OBVIOUS (* Though obvious, the provers appear to need some help
about new objects: here to observe that `T == fImg`. *)
<1>2. /\ IsFiniteSet(fImg)
/\ Cardinality(fImg) <= Cardinality(S)
BY <1>1, FuncImageOfFinite
<1> QED
BY <1>2
================================================================================


Whether to use the function or operator version of this theorem depends on what specification style
is being used. I am using operators defined with `CHOOSE`, which is why I selected the operator version.

[1] https://github.com/tlaplus/v2-tlapm/blob/fd345f78c7e356b53c67e24f17e99df449d7b3a3/library/FunctionTheorems.tla#L34

>> If I write a proof similar to that of `ImageOfFinite` below
>> for some specific operator `Op`, for example:
>>
>> <2> DEFINE
>> Op(u, a, b) == u
>> f == [u \in S |-> Op(u, arg1, arg2)]
>> <2>1. f \in Surjection(S, H)
>> BY DEF Surjection, Hdef
>> <2> QED
>> BY <2>1, ..., FS_Surjection
>>
>> then `tlapm -v -C` proves it, and I don't see any intermediate errors (using version 1.4.3).
>> `tlapm` proves correct also the module `test2` below, but with an error from the SMT backend (see below),
>> which can probably be ignored, because only the Isabelle backend supports the declaration `NEW Op(_)` [2].
>
> Yes: the message from the SMT backend indicates a limitation of the backend, which stumbles over the apparent "mismatch" of arities. This is one of the situations where the Isabelle backend is useful, due to higher-order unification.
>

Thanks for the hint, I will read about higher-order unification.

>>
>> However, if I change the assumption to `NEW Op(_, _)` in `ImageOfFinite`,
>> or the operator application to `Op(x)` in `ImageOfFinite2`,
>> then the proof is again successful, but SANY detects the errors.
>
> This is indeed a syntax error and should be rejected. Our working hypothesis is that the prover is called only on input that has been checked by SANY (if you use the Toolbox, the prover will not be started on modules that contain a syntax error). The next (major) release of TLAPS will be based on the SANY parser, so you will not be able to run the prover on that module anymore.
>

The above comment relates to another error that SANY raises, which I have been considering
opening an issue about. The error has the form:

"Function 'f' is defined with 1 parameters, but is applied to 2 arguments."

when SANY sees `f[a, b]` after a definition of the form `f == [t \in S \X S |-> e(t[1], t[2]) ]`.
I understand the motivation for raising an error in this case, to avoid what will usually indicate
a reasoning error, but based on my understanding of TLA+ this seems valid TLA+ (p.303 in the TLA+ book
and the untyped nature of TLA+). The function application can always be rewritten equivalently
without syntactic sugar as `f[ << a, b >> ]`, thus avoiding the SANY error. So raising this error
does not restrict what one can express.

The syntactic sugar makes a proof that contains multiple occurrences of such function applications
more readable. This is why I have continued using `f[a, b]`, despite the errors by SANY
(of course I correct all other errors that SANY reports). When the proofs are completed,
I can replace the syntactic sugar. One possibility could be for SANY to raise a warning instead of
an error for this case.

Regarding why not replacing the function definition with one of the form `[u, v \in S \X S |-> ...]`,
the reason is to be able to use `tlapm` (relevant discussion can be found at [2]).

[2] https://groups.google.com/forum/#!topic/tlaplus/iWjdemXFdSU

>>
>>
>> Question 1: If SANY detects no errors and `tlapm` proves module `test2` correct,
>> should I assume that the arity of operator declarations as those in module `test2`
>> has been taken into account correctly?
>
> Yes.
>
>>
>> Question 2: Is there an approach simpler/better than a couple of theorems for different arities to
>> prove that `IsFiniteSet(S)` implies `IsFiniteSet( { Op(x, ...): x \in S } )`
>> as a theorem that we can reuse?
>
> In fact, I'd simply apply ImageOfFinite, just as you do in the proofs of the theorems for operators of different arities. Since the other arguments must be fixed, the operator is effectively unary. For example:
>
> LEMMA
> ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S), NEW n \in Nat
> PROVE IsFiniteSet({x+n : x \in S})
> BY ImageOfFinite
>
> However, this again requires higher-order unification, so only Isabelle will prove the step, and you may have to "isolate" the application of the theorem and not combine it with, say, arithmetic reasoning.
>

Indeed, replacing the invocation of `ImageOfFinite3` with `ImageOfFinite` worked.

I think what happened was that initially I saw the arity errors, didn't realize that they were
only about the SMT backend, and that the Isabelle backend was actually performing the proof,
then developed lemmata for different arities, and after consulting the list of supported
features in later analysis recognized that the backend errors were irrelevant to the proof.

>>
>>
>> Sidenote: To invoke `ImageOfFinite3` successfully, I had to hide the definition of `S`,
>> but at least I didn't rewrite a proof like that of `ImageOfFinite`.
>
> Indeed, if S is a complex expression, there may be some rewriting going on before Isabelle's classical prover gets to see the term, preventing successful unification. In such cases, you may be successful using "BY IsaM("blast")", which essentially disables rewriting. We'd like to hide these backend-specific idiosyncrasies from users, but we're not there yet.
>
>>
>>
>> ```
>> *** Fatal exception:
>> Type Checking error: Expected function type for:
>>
>> a_Opunde_1a
>>
>> but got this: u
>>
>> in function application:
>>
>> (_APPLY {a_Opunde_1a} x)
>> test2.tlaps/tlapm_d7953c.smt:50: this is the location of the error
>>
>> ...
>
> As mentioned above, this only indicates a failure of the backend and doesn't mean that there is something wrong with your input.
>
>>
>> Checking the proofs with Isabelle. This may take a long time.
>> (* Isabelle interaction log in "test2.tlaps/isabelle.log" *)
>> (* Isabelle parsing "test2.tlaps/test2.thy" ... done *)
>> (* Obligation checking trace follows. *)
>> (* +5 -5 +7 -7 *)
>> Proof checking done. No errors found.
>> ```
>
> Please note that at this point we can only check proofs found by Zenon, not those found by SMT.

Thanks for mentioning this--I was incorrectly assuming that all proofs are checked with Isabelle.
Looking forward to a version of `tlapm` that will check also proofs constructed by SMT solvers.


>
> Regards,
> Stephan
>
> --
> 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+u...@googlegroups.com <mailto:tlaplus+u...@googlegroups.com>.
> To post to this group, send email to tla...@googlegroups.com <mailto:tla...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Stephan Merz]

Hi Ioannis,

The above comment relates to another error that SANY raises, which I have been considering
opening an issue about. The error has the form:

   "Function 'f' is defined with 1 parameters, but is applied to 2 arguments."

when SANY sees `f[a, b]` after a definition of the form `f == [t \in S \X S |-> e(t[1], t[2]) ]`.
I understand the motivation for raising an error in this case, to avoid what will usually indicate
a reasoning error, but based on my understanding of TLA+ this seems valid TLA+ (p.303 in the TLA+ book
and the untyped nature of TLA+). The function application can always be rewritten equivalently
without syntactic sugar as `f[ << a, b >> ]`, thus avoiding the SANY error. So raising this error
does not restrict what one can express.

I am unable to reproduce this issue. For example, SANY accepts

LEMMA

  ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)

  PROVE  LET f == [x \in S \X S |-> e(x[1], x[2])]

         IN  \A x \in S : IsFiniteSet({f[x,y] : y \in S})

Could you please expand?

Thanks,

Stephan

[Ioannis Filippidis]

Hi Stephan,

I am sorry, the exact expression that raises the error I described has the other

form of function definition:

```

LEMMA
  ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)

  PROVE  LET f[x \in S \X S] == e(x[1], x[2])

         IN  \A x \in S : IsFiniteSet({f[x,y] : y \in S})

```

but as I was describing it, I both was convinced that I used the form `f == ...`

(because I use it at most places), and did not consider the possibility that

different (syntactically similar) function definitions would yield a different result from SANY.

To be more precise this time, when the module:

```
------------------------------- MODULE test --------------------------------
EXTENDS FiniteSets

LEMMA
  ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
  PROVE  LET f == [x \in S \X S |-> e(x[1], x[2])]
         IN  \A x \in S : IsFiniteSet({f[x,y] : y \in S})


LEMMA
  ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)

  PROVE  LET f[x \in S \X S] == e(x[1], x[2])

         IN  \A x \in S : IsFiniteSet({f[x,y] : y \in S})

================================================================================
```

is given to SANY with:

```
$ java -cp /some/path/tlatools/tla/ -DTLA-Library=/some/path/v2-tlapm/library tla2sany.SANY test.tla
```

then the output is:

```
****** SANY2 Version 2.1 created 24 February 2014

Parsing file test.tla
Parsing file /some/path/v2-tlapm/library/FiniteSets.tla
Parsing file /some/path/tlatools/tla/tla2sany/StandardModules/Naturals.tla
Parsing file /some/path/tlatools/tla/tla2sany/StandardModules/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module test
Semantic errors:

*** Errors: 1

line 14, col 40 to line 14, col 45 of module test

Function 'f' is defined with 1 parameters, but is applied to 2 arguments.

```

So SANY indicates that the function application in the second lemma is

in error, even though `tlapm` proves that the functions in the two lemmata

are equal (as described on p.304):

```

LEMMA
  ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
  PROVE  LET

            f1 == [x \in S \X S |-> e(x[1], x[2])]
            f2[x \in S \X S] == e(x[1], x[2])
         IN  f1 = f2
    OBVIOUS
```

Other comments:

1. Yesterday I switched to using the syntax `f[<< a, b >>]`, so that the proofs will be both

checked by `tlapm`, and compliant to SANY (because proving something "modulo errors from

the syntax checker" is not a convincing claim, and because if others attempt to confirm the

results using the toolbox, instead of `tlapm` directly, they will be required to first

correct errors reported by SANY).

This change reminded me that another reason for preferring the syntax  `f[a, b]` was

difficulties in automated proof. It was possible to prove the same claims, but some

refinement of the proofs or hiding of definitions was needed, for some steps
(few compared to the total number of steps).

It may be worth noting that the failures were not by the backends (I think in all cases),
but Isabelle was rejecting some of the proofs found by Zenon

(with a "Failed to finish proof" in the Isabelle log and looking in the `*.thy`

file it seems that these were proofs generated by Zenon).

There are more details, and some suggestions about the command line interface of `tlapm`,
from that process that seem worth reporting, but the issue in this thread is different,
so another thread or a GitHub issue is probably more appropriate for reporting more details.

2. Yet another way to use the combination of function definition and application that

would raise a SANY error, but avoid the error is by passing the defined function as

argument to an operator that is defined using the syntax `f[a, b]`.

Best regards,

ioannis

--
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...@googlegroups.com.

[Ioannis Filippidis]

On Thu, May 11, 2017 at 2:45 PM, Ioannis Filippidis <jfili...@gmail.com> wrote:

```
****** SANY2 Version 2.1 created 24 February 2014

Parsing file test.tla
Parsing file /some/path/v2-tlapm/library/FiniteSets.tla
Parsing file /some/path/tlatools/tla/tla2sany/StandardModules/Naturals.tla
Parsing file /some/path/tlatools/tla/tla2sany/StandardModules/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module test
Semantic errors:

*** Errors: 1

line 14, col 40 to line 14, col 45 of module test

Function 'f' is defined with 1 parameters, but is applied to 2 arguments.
```

This message appears to originate from the following area of code [1]:

```
            // If the function appears with numArgs >= 2 argument
            // expressions, it must be declared with exactly numArgs
            // parameters; and a function with numParms parameters in
            // its definition should be applied to exactly numParms
            // expressions, or 1 expression (representing arguments in
            // tuple form), or 0 expressions (representing the
            // function itself).  Note: one cannot define a function
            // with 0 arguments in TLA+.
            if ( numArgs >= 2 && numParms != numArgs ) {
              errors.addError(treeNode.getLocation(),
                              "Function '" +
                                ((OpApplNode)sns[0]).getOperator().getName() +
                              "' is defined with " + numParms +
                              " parameters, but is applied to " +
                              numArgs + " arguments.");
              return nullOAN;
```

[1] https://github.com/tlaplus/tlaplus/blob/5527a0c0f6bbc18e0685bd1db302cda52f2236d3/tlatools/src/tla2sany/semantic/Generator.java#L3317

Best regards,

ioannis