MapThenSumSet and several theorems for it.

[kape1395]

I introduced MapThenSumSet operator. It was useful for me to define decreasing sequences to prove termination. Then, I proved several theorems about it. The theorems are not general enough to port them to the Fold operator, but maybe that's still useful.

I have checked the proofs with TLAPS from PR https://github.com/tlaplus/tlapm/pull/93. The SANY parser says there is an error, but the TLAPS says OK on line 328 in modules/FiniteSetsExt_theorems_proofs.tla. I made a smaller case showing the same error. Documented it in https://github.com/tlaplus/tlapm/issues/119.

[lemmy]

LGTM - Anticipating more MapThen... operators, I would perhaps move MapThenSumSet after ReduceSet.

It probably makes sense to add TLAPS to our CI now that we start adding theorems.

[muenchnerkindl]

Thanks a lot for these theorems. In order to avoid the SANY / TLAPS issue, should we EXTEND Folds for the time being (I presume the other LOCAL INSTANCEs don't cause problems)?

[lemmy]

+1 for changing to EXTENDS Folds for the time being, given that Folds has a single, very verbose operator definition (MapThenFoldSet). Please include a comment in the EXTENDS section as a reminder or explanation for our future selves.

[kape1395]

It appears that it is not enough to use EXTENDS instead of LOCAL INSTANCE for Folds only. I have to add Functions as well, probably because it has LOCAL INSTANCE of Folds inside.

If I keep LOCAL INSTANCE for Functions, then the proof fails like this:

failed isabelle[auto; time-limit: 30]:
    (false)
failed smt[time-limit: 5]:
    (Trying to Boolify a non Boolean operator.)
failed zenon[time-limit: 10]:
    (timeout)

ASSUME NEW CONSTANT S,
       IsFiniteSet(S) ,
       NEW CONSTANT op(_),
       \A s \in S : op(s) \in Nat ,
       (CHOOSE F :
          F
          = [s \in SUBSET S |->
               IF s = {}
                 THEN 0
                 ELSE op(CHOOSE e \in s : TRUE)
                      + F[s \ {CHOOSE e \in s : TRUE}]])
       = [s \in SUBSET S |->
            Cardinality(UNION {NatAsSet(n, op(n)) : n \in s})] 
PROVE  (CHOOSE iter :
          iter
          = [s \in SUBSET S |->
               IF s = {}
                 THEN 0
                 ELSE op(CHOOSE x \in s : TRUE)
                      + iter[s \ {CHOOSE x \in s : TRUE}]])[S]
       = Cardinality(UNION {NatAsSet(n, op(n)) : n \in S})

Interestingly, the obligation looks identical if I keep the Functions module as a local instance (fails) or extend from it (passes).

[kape1395]

It probably makes sense to add TLAPS to our CI now that we start adding theorems.

Maybe it would be better first to set up the rolling updates for TLAPS before integrating it here. I think at least https://github.com/tlaplus/tlapm/pull/109 and https://github.com/tlaplus/tlapm/pull/96 should be merged for that.

[kape1395]

Is it OK to merge, or should it wait for TLAPM changes? I guess that will take a long time, because the existing branches should be merged before adding more changes.

[muenchnerkindl]

I support merging.

[lemmy]

     [java] "FiniteSetsExtTests"
     [java] Error: Assumption line 97, col 8 to line 99, col 55 of module FiniteSetsExtTests is false.
     [java] Finished in 08s at (2024-02-21 16:51:29)

[lemmy]

     [java] "FiniteSetsExtTests"
     [java] Error: Assumption line 97, col 8 to line 99, col 55 of module FiniteSetsExtTests is false.
     [java] Finished in 08s at (2024-02-21 16:51:29)

Taken care of by adjusting the line numbers in FiniteSetsExtTests.tla.