suggested additions / changes for SequencesExt

[muenchnerkindl]

I added / strengthened a few lemmas in SequencesExtTheorems. I also suggest moving the operator IsInjective to Functions.tla where it really seems to belong (but what does this mean for the Java override?). I also copied the new lemmas to the TLAPS modules. We could therefore retire SequencesExtTheorems from CommunityModules (and rename SequenceOps to SequenceExt in the TLAPS library).

[lemmy]

I added / strengthened a few lemmas in SequencesExtTheorems. I also suggest moving the operator IsInjective to Functions.tla where it really seems to belong (but what does this mean for the Java override?). I also copied the new lemmas to the TLAPS modules. We could therefore retire SequencesExtTheorems from CommunityModules (and rename SequenceOps to SequenceExt in the TLAPS library).

Agreed, IsInjective should move to Functions.tla. I will move the Java module override for IsInjective. What's going to happen to Functions.tla in TLAPS?

Since the CommunityModules are now part of the Toolbox, we should probably have the compatibility with TLAPS figured out by then (whenever that is).

[muenchnerkindl]

I made the proposed change to Functions.tla in the TLAPS library and also copied SequencesExt.tla there (and renamed SequenceOpTheorems[_proofs] to SequencesExtTheorems[_proofs]). While doing so, I noticed that SequencesExt in CommunityModules misses the Cons operator:

Cons(elt, seq) ==
()
( The sequence formed by prepending elt to seq. )
()
<> \o seq

I suggest adding it to the community module because it is a useful in proofs: Cons/Last/Front are the counterparts to Append/Head/Tail from the standard Sequences module.

Once the Community Modules are officially part of the Toolbox distribution and in the search path, we'll remove Functions and SequencesExt from the TLAPS library, but keep the corresponding theorem library modules.

[lemmy]

I've added Cons and moved the Java module override. What remains broken is the proof part. Should we just delete SequencesExtTheorems_proofs.tla & SequencesExtTheorems.tla and disable the TLAPS Github action step?

[muenchnerkindl]

I suggest deleting the modules containing proofs from Community Modules, as they are included in the more comprehensive proof modules in the TLAPS standard library.

[lemmy]

Corresponding TLAPM pull requeset: tlaplus/tlapm#27