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

*From*: Karolis Petrauskas <k.petrauskas@xxxxxxxxx>*Date*: Sun, 14 Jan 2024 20:36:55 +0200

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.

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.

**Follow-Ups**:**Re: [tlaplus] Where to put proofs on a SetSum?***From:*Markus Kuppe

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