[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Where to put proofs on a SetSum?

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 ==
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


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.