Isabelle rejects a Zenon proof from FiniteSetTheorems_proofs if the operator Size is visible

[johnyf]

Following #22, I renamed the module Sequences to Sequences_copy, and used it within other modules, in order to see whether the proofs hold in absence of the unprovable (and I believe invalid) assertion Len(x) \in Nat for the operator Len from the module Sequences, which seems to be builtin to TLAPS v1.4.3 (see also #22 (comment)).

The module FiniteSets instantiates Sequences, so I copied it to FiniteSets_copy, and instantiated the module Sequences_copy instead of Sequences.

https://github.com/tlaplus/v2-tlapm/blob/12a046f21d0be1c057167d7a8a0f95ce22efb8c3/library/FiniteSets.tla#L3

I did similarly for the module FiniteSetTheorems_proofs. It turns out that TLAPS fails to check some proofs in the module FiniteSetTheorems_proofs after the above rearrangement. I had to refine those proofs in order for TLAPS to succeed. During this process, I encountered several cases where Isabelle (Isabelle2011-1: October 2011) never completed checking a proof until the proof was modified / refined, or Isabelle rejected proofs. I describe one case below.

Isabelle rejects the proof of step <1> QED in the module FiniteSetTheoremsDev below, which is:

https://github.com/tlaplus/v2-tlapm/blob/12a046f21d0be1c057167d7a8a0f95ce22efb8c3/library/FiniteSetTheorems_proofs.tla#L226

Changing <1> HIDE DEF SZ, CS, fn to <1> HIDE DEF Size, SZ, CS, fn leads to Isabelle accepting the proof of that step.

I have added the directive Zenon to the proof of step <1> QED in order to ensure TLAPS uses the same backend under both cases, and thus demonstrate that Isabelle succeeds when Size is hidden. A comment in the module below gives more details.

In other words, with or without the directive Zenon, the output of TLAPS reads (invoked with tlapm -v -C --cleanfp FiniteSetTheoremsDev.tla):

(* trying obligation 1 generated from file "./FiniteSetTheoremsDev.tla", line 51, characters 5-6 *)
...
(* Obligation checking trace follows. *)
(* +1 +6 *)
Isabelle/TLA+ rejected the proof of obligation 1.

(With the directive present, the second obligation is indexed as 7, but obligation 1 is relevant to this issue, and remains the same.)

After hiding the definition of the operator Size, and with the directive Zenon present, the output is:

(* trying obligation 1 generated from file "./FiniteSetTheoremsDev.tla", line 51, characters 5-6 *)
...
(* Obligation checking trace follows. *)
(* +1 +7 -1 -7 *)
Proof checking done. No errors found.

I had to make more changes in order for TLAPS to successfully check the proofs in FiniteSetTheorems_proofs when using the renamed Sequences module, but those changes are outside the scope of this issue.

--------------------- MODULE FiniteSetTheoremsDev ---------------------
(* Isabelle rejects the proof of <1> QED when DEF Size is not hidden. *)
EXTENDS
    FiniteSets_copy,
    Sequences_copy,
    FunctionTheorems,
    WellFoundedInduction,
    TLAPS


LEMMA FS_CountingElements ==
    ASSUME
        NEW S,
        NEW n \in Nat,
        ExistsBijection(1..n, S)
    PROVE
        Cardinality(S) = n
PROOF
<1> DEFINE
    Size(T)  == CHOOSE i \in Nat:  ExistsBijection(1..i,T)
    SZ       == [ T \in SUBSET S |-> Size(T) ]
    fn(CS,T) == IF T = {} THEN 0 ELSE 1 + CS[T \ {CHOOSE x : x \in T}]
    IsCS(CS) == CS = [T \in SUBSET S |-> fn(CS,T)]
    CS       == CHOOSE CS : IsCS(CS)
<1> HIDE DEF SZ, CS, fn
<1>1. IsCS(SZ)
<1>2. ASSUME
        NEW CS1, IsCS(CS1),
        NEW CS2, IsCS(CS2)
      PROVE
        CS1 = CS2
<1>3. IsCS(CS)
    BY <1>1 DEF CS
<1>4. CS = SZ
    BY <1>1, <1>2, <1>3
<1>5. Cardinality(S) = CS[S]
    BY DEF Cardinality, CS, fn, IsCS
<1>6. S \in SUBSET S
    OBVIOUS
<1>7. SZ[S] = Size(S)
    BY <1>6  DEF SZ
<1>8. Size(S) = n
    <2>1. /\ n \in Nat
          /\ ExistsBijection(1..n, S)
        OBVIOUS
    <2>2. Size(S) = CHOOSE i \in Nat:  ExistsBijection(1..i, S)
        BY DEF Size
    <2> QED
        BY <2>1, <2>2 DEF Size
<1> QED
    BY <1>4, <1>5, <1>7, <1>8, Zenon
        (* The directive `Zenon` is used to ensure that TLAPS chooses the same backend
           both when the definition of `Size` is visible, as well as when it is hidden.
           Otherwise, TLAPS on its own switches from Zenon to SMT when `Size` is hidden,
           which doesn't produce any proof, so it wouldn't demonstrate that Isabelle succeeds
           when `Size` is hidden. *)

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