[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Ioannis Filippidis <jfili...@xxxxxxxxx>*Date*: Thu, 11 May 2017 14:45:20 -0700*References*: <CAMDXC8KdhqUTyU35hVbWYFqsCZy6gMspqAH5N6tMm4E3u7Ompg@mail.gmail.com> <1A886A09-E833-4CF4-8DA8-23CFFF4C6464@gmail.com> <b60079f6-ec32-3b61-6ddf-25f25700c299@gmail.com> <AF5262A2-D741-46EE-AF3C-9DBE23BF8CFE@gmail.com>

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})

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

```

```

------------------------------- 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.

```

```

$ 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

```

```

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

(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

On Thu, May 11, 2017 at 5:08 AM, Stephan Merz <stepha...@xxxxxxxxx> wrote:

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 acceptsLEMMAASSUME 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

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.

Visit this group at https://groups.google.com/group/tlaplus .

For more options, visit https://groups.google.com/d/optout .

**Follow-Ups**:**Re: [tlaplus] Arity of NEW operator in `tlapm`***From:*Ioannis Filippidis

**References**:**Arity of NEW operator in `tlapm`***From:*Ioannis Filippidis

**Re: [tlaplus] Arity of NEW operator in `tlapm`***From:*Stephan Merz

**Re: [tlaplus] Arity of NEW operator in `tlapm`***From:*Ioannis Filippidis

**Re: [tlaplus] Arity of NEW operator in `tlapm`***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Arity of NEW operator in `tlapm`** - Next by Date:
**Re: [tlaplus] Arity of NEW operator in `tlapm`** - Previous by thread:
**Re: [tlaplus] Arity of NEW operator in `tlapm`** - Next by thread:
**Re: [tlaplus] Arity of NEW operator in `tlapm`** - Index(es):