| Hi Ioannis,
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
|