MapThenSumSet and several theorems for it. (#99)

FiniteSetsExt!MapThenSumSet including and support TLAPS theorems. [Feature] Signed-off-by: Karolis Petrauskas <karolis.petrauskas@erisata.lt>
tlaplus · Feb 21, 2024 · b4deee7 · b4deee7
1 parent ea36000
commit b4deee7
Show file tree

Hide file tree

Showing 4 changed files with 468 additions and 5 deletions.
diff --git a/modules/FiniteSetsExt.tla b/modules/FiniteSetsExt.tla
@@ -1,8 +1,7 @@
 --------------------------- MODULE FiniteSetsExt ---------------------------
+EXTENDS Folds, Functions \* Replace with LOCAL INSTANCE when https://github.com/tlaplus/tlapm/issues/119 is resolved.
 LOCAL INSTANCE Naturals
 LOCAL INSTANCE FiniteSets
-LOCAL INSTANCE Functions
-LOCAL INSTANCE Folds
 
 FoldSet(op(_,_), base, set) ==
    (*************************************************************************)
@@ -38,6 +37,17 @@ ReduceSet(op(_, _), set, acc) ==
    (*************************************************************************)
    FoldSet(op, acc, set)
 
+MapThenSumSet(op(_), set) ==
+   (*************************************************************************)
+   (* Calculate the sum of projections of the elements in a set.            *)
+   (*                                                                       *)
+   (* Example:                                                              *)
+   (*         MapThenSumSet(                                                *)
+   (*             LAMBDA e : e.n,                                           *)
+   (*             {[n |-> 0], [n |-> 1], [n |-> 2]}                         *)
+   (*         ) = 3                                                         *)
+   (*************************************************************************)
+   MapThenFoldSet(+, 0, op, LAMBDA s : CHOOSE x \in s : TRUE, set)
 
 FlattenSet(S) ==
    UNION S

diff --git a/modules/FiniteSetsExt_theorems.tla b/modules/FiniteSetsExt_theorems.tla
@@ -0,0 +1,53 @@
+---- MODULE FiniteSetsExt_theorems ----
+EXTENDS FiniteSetsExt, FiniteSets, Naturals
+
+LEMMA MapThenSumSetEmpty ==
+    ASSUME NEW op(_)
+    PROVE MapThenSumSet(op, {}) = 0
+PROOF OMITTED \* Proof in FiniteSetsExt_theorems_proofs.tla
+
+
+LEMMA MapThenSumSetType ==
+    ASSUME NEW S, IsFiniteSet(S), NEW op(_), \A e \in S : op(e) \in Nat
+    PROVE MapThenSumSet(op, S) \in Nat
+PROOF OMITTED \* Proof in FiniteSetsExt_theorems_proofs.tla
+
+
+THEOREM MapThenSumSetAddElem ==
+    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 MapThenSumSet(op, S \cup {e}) = MapThenSumSet(op, S) + op(e)
+PROOF OMITTED \* Proof in FiniteSetsExt_theorems_proofs.tla
+
+LEMMA MapThenSumSetRemElem ==
+    ASSUME
+        NEW S, IsFiniteSet(S),
+        NEW op(_), \A s \in S : op(s) \in Nat,
+        NEW e \in S
+    PROVE MapThenSumSet(op, S) = MapThenSumSet(op, S \ {e}) + op(e)
+PROOF OMITTED \* Proof in FiniteSetsExt_theorems_proofs.tla
+
+LEMMA MapThenSumSetMonotonic ==
+    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 MapThenSumSet(op, S \cup {e}) >= MapThenSumSet(op, S)
+PROOF OMITTED \* Proof in FiniteSetsExt_theorems_proofs.tla
+
+LEMMA MapThenSumSetZero ==
+    ASSUME NEW S, IsFiniteSet(S),
+           NEW op(_), \A e \in S: op(e) \in Nat,
+           MapThenSumSet(op, S) = 0
+    PROVE \A e \in S: op(e) = 0
+PROOF OMITTED \* Proof in FiniteSetsExt_theorems_proofs.tla
+
+LEMMA MapThenSumSetZeros ==
+    ASSUME NEW S, IsFiniteSet(S),
+           NEW op(_), \A e \in S: op(e) = 0
+    PROVE MapThenSumSet(op, S) = 0
+PROOF OMITTED \* Proof in FiniteSetsExt_theorems_proofs.tla
+
+====