Hi Stephan,
I am sorry, the exact _expression_ that raises the error I described has the other
```
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})
```
(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