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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Sun, 14 Jan 2024 10:49:24 -0800*References*: <CAFteovLVZE3yxnP95yCMp0w5gqRfrboLSCv9OFSE_8zWn-cyfA@mail.gmail.com>

The idea [1] was to add at least some theorems to the CommunityModules. Markus [1] https://github.com/tlaplus/CommunityModules/issues/60#issuecomment-1015689013 > On Jan 14, 2024, at 10:36 AM, Karolis Petrauskas <k.petrauskas@xxxxxxxxx> wrote: > > 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/A67ED15F-5CB5-42A9-8B4D-5F10C5422EF8%40lemmster.de.

**References**:**[tlaplus] Where to put proofs on a SetSum?***From:*Karolis Petrauskas

- Prev by Date:
**[tlaplus] Where to put proofs on a SetSum?** - Next by Date:
**RE: [tlaplus] Re: Draft of New TLA Book** - Previous by thread:
**[tlaplus] Where to put proofs on a SetSum?** - Next by thread:
**[tlaplus] timers** - Index(es):