Re: [tlaplus] Where to put proofs on a SetSum?

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.