Where to put proofs on a SetSum?

[Karolis Petrauskas]

I have proved several properties on a function similar to SumSet from the community modules [1].

SetSum(S, op(_)) ==

LET iter[s \in SUBSET S] ==

IF s = {} THEN 0

ELSE LET e == CHOOSE e \in s : TRUE

IN iter[s \ {e}] + op(e)

IN iter[S]

E.g., the following and similar.

THEOREM SetSumAddElem ==

ASSUME

NEW S, IsFiniteSet(S),

NEW op(_), \A s \in S : op(s) \in Nat,

NEW e, e \notin S, op(e) \in Nat

PROVE SetSum(S \cup {e}, op) = SetSum(S, op) + op(e)

Where should I put these proofs to make them reusable?

  - The community modules repo [2] currently doesn't contain any proofs.

  - The examples repo [3] contains proofs but doesn't sound like a library of reusable modules.

[1] https://github.com/tlaplus/CommunityModules/blob/243fa679bfa80fc5099f9911cf99fa0f029d9b2b/modules/FiniteSetsExt.tla#L16

[2] https://github.com/tlaplus/CommunityModules

[3] https://github.com/tlaplus/Examples

Karolis

[Markus Kuppe]

The idea [1] was to add at least some theorems to the CommunityModules.

Markus

[1] https://github.com/tlaplus/CommunityModules/issues/60#issuecomment-1015689013