[tlaplus] Where to put proofs on a SetSum?

[Karolis Petrauskas <k.petrauskas@xxxxxxxxx>]

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFteovLVZE3yxnP95yCMp0w5gqRfrboLSCv9OFSE_8zWn-cyfA%40mail.gmail.com.