more theorems about folds

[muenchnerkindl]

This PR mainly adds theorems about folds on functions and sequences.

I haven't tried to include running proofs as part of the CI.

[muenchnerkindl]

Happy New Year to everybody! Would somebody have some time to look at this PR?

[kape1395]

I can try.

[muenchnerkindl]

I added some more functions, in particular about folding a function, and I believe this is now in a state that can be merged into the master branch.

[kape1395]

This fails for me with tlapm from the current main:

File "./FunctionTheorems_proofs.tla", line 882, characters 3-4:
[ERROR]: Could not prove or check:
           ASSUME Surjection(S, T) ==
                    {M \in [S -> T] : \A t \in T : \E s \in S : M[s] = t},
                  Bijection(S, T) == Injection(S, T) \cap Surjection(S, T),
                  NEW CONSTANT S,
                  NEW CONSTANT f \in 
                  Bijection(1..1, S),
                  1..1 = {1} 
           PROVE  \E s : S = {s}
File "./FunctionTheorems_proofs.tla", line 1, character 1 to line 1412, character 77:
[ERROR]: 1/732 obligations failed.

[muenchnerkindl]

This fails for me with tlapm from the current main:

File "./FunctionTheorems_proofs.tla", line 882, characters 3-4:
[ERROR]: Could not prove or check:
           ASSUME Surjection(S, T) ==
                    {M \in [S -> T] : \A t \in T : \E s \in S : M[s] = t},
                  Bijection(S, T) == Injection(S, T) \cap Surjection(S, T),
                  NEW CONSTANT S,
                  NEW CONSTANT f \in 
                  Bijection(1..1, S),
                  1..1 = {1} 
           PROVE  \E s : S = {s}
File "./FunctionTheorems_proofs.tla", line 1, character 1 to line 1412, character 77:
[ERROR]: 1/732 obligations failed.

That's annoying, in particular since I did not at all touch that proof (and of course tlapm --cleanfp FunctionTheorems_proofs.tla reports no error on my side). I just rebuilt tlapm (471b481-dirty) on MacOS 26.2, and Z3 proves the obligation in no time (0.3s). How can we track and fix such spurious errors?

[kape1395]

I retried it several times. TLAPM was built at the same commit as you mentioned. At Linux.
It failed for me even after adding Z3T(100).

The Z3 version is this:

$ ~/.opam/5.4.0/lib/tlapm/backends/bin/z3 --version
Z3 version 4.8.9 - 64 bit

Then I tried upgrading Z3 (to Z3 version 4.15.4 - 64 bit). It helped somewhat. That proof step is now proved fast by Z3, but some other steps started to fail. Moreover, some tests in tlapm are failing with the upgraded Z3. I will create a PR for that.

[kape1395]

The same theorem is formulated with n \in 0.. in the proofs file. Is the difference on purpose?

[muenchnerkindl]

Thanks for catching this – it must have been an oversight in a previous commit. The hypothesis n \in 0..Len(seq) is weaker and should therefore be preferred. Fixed.

[muenchnerkindl]

I retried it several times. TLAPM was built at the same commit as you mentioned. At Linux. It failed for me even after adding Z3T(100).

The Z3 version is this:

$ ~/.opam/5.4.0/lib/tlapm/backends/bin/z3 --version
Z3 version 4.8.9 - 64 bit

Then I tried upgrading Z3 (to Z3 version 4.15.4 - 64 bit). It helped somewhat. That proof step is now proved fast by Z3, but some other steps started to fail. Moreover, some tests in tlapm are failing with the upgraded Z3. I will create a PR for that.

Looks like "prove once, test everywhere" since Z3 apparently behaves differently for different operating systems (my TLAPS installation also has the version that you mention). Let me know if I can help with fixing the proofs that fail with the newer version of Z3.