[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Arity of NEW operator in `tlapm`
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...@xxxxxxxxx <mailto:jfili...@xxxxxxxxx>> 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...@xxxxxxxxxxxxxxxx <mailto:tlaplus+u...@xxxxxxxxxxxxxxxx>.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx <mailto:tla...@xxxxxxxxxxxxxxxx>.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.