Skip to content

Commit 17cbb9a

Browse files
lemmylemmy
committed
Theorems for sum of constant function
Add SumFunctionOnSetConst and SumFunctionConst stating that summing a constant function over a finite set equals the constant times the cardinality of the set, together with corresponding proofs and an example in the doc comments. [Feature] Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
1 parent dc9c597 commit 17cbb9a

2 files changed

Lines changed: 119 additions & 0 deletions

File tree

‎modules/FunctionTheorems.tla‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -767,6 +767,29 @@ THEOREM SumFunctionOnSetZero ==
767767
NEW fun, \A x \in S : fun[x] \in Nat
768768
PROVE SumFunctionOnSet(fun, S) = 0 <=> \A x \in S : fun[x] = 0
769769

770+
(*************************************************************************)
771+
(* Given any Int-valued function f and finite set S such that f[s] = c *)
772+
(* for all s \in S, summing f over S yields c multiplied by the *)
773+
(* cardinality of S. For example, for *)
774+
(* f == [s \in {"a", "b", "c"} |-> IF s = "c" THEN 42 ELSE 5], *)
775+
(* SumFunctionOnSet(f, {"a","b"}) = 10. *)
776+
(*************************************************************************)
777+
THEOREM SumFunctionOnSetConst ==
778+
ASSUME NEW D, NEW S \in SUBSET D, IsFiniteSet(S),
779+
NEW f \in [D -> Int], NEW c \in Int, \A x \in S : f[x] = c
780+
PROVE SumFunctionOnSet(f, S) = c * Cardinality(S)
781+
782+
(*************************************************************************)
783+
(* Summing a constant function over a finite set yields the constant *)
784+
(* multiplied by the cardinality of the set. For example, *)
785+
(* SumFunctionOnSet([s \in {"a","b","c"} |-> 5], {"a","b","c"}) = 15. *)
786+
(*************************************************************************)
787+
(*
788+
THEOREM SumFunctionOnSetConst ==
789+
ASSUME NEW S, IsFiniteSet(S), NEW c \in Int
790+
PROVE SumFunctionOnSet([s \in S |-> c], S) = c * Cardinality(S)
791+
*)
792+
770793
(*************************************************************************)
771794
(* Summing a function is monotonic in the function argument. *)
772795
(*************************************************************************)
@@ -825,6 +848,15 @@ THEOREM SumFunctionZero ==
825848
\A x \in DOMAIN fun : fun[x] \in Nat
826849
PROVE SumFunction(fun) = 0 <=> \A x \in DOMAIN fun : fun[x] = 0
827850

851+
(*************************************************************************)
852+
(* Summing a constant function yields the constant multiplied by the *)
853+
(* cardinality of its domain. For example, *)
854+
(* SumFunction([s \in {"a","b","c"} |-> 5]) = 15. *)
855+
(*************************************************************************)
856+
THEOREM SumFunctionConst ==
857+
ASSUME NEW S, IsFiniteSet(S), NEW c \in Int
858+
PROVE SumFunction([s \in S |-> c]) = c * Cardinality(S)
859+
828860
THEOREM SumFunctionMonotonic ==
829861
ASSUME NEW f, IsFiniteSet(DOMAIN f), NEW g, DOMAIN g = DOMAIN f,
830862
\A x \in DOMAIN f : f[x] \in Int,

‎modules/FunctionTheorems_proofs.tla‎

Lines changed: 87 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1310,6 +1310,78 @@ THEOREM SumFunctionOnSetZero ==
13101310
<2>. P(S) BY <1>1, <1>2, FS_Induction, IsaM("iprover")
13111311
<2>. QED BY DEF P
13121312

1313+
(*************************************************************************)
1314+
(* Given any Int-valued function f and finite set S such that f[s] = c *)
1315+
(* for all s \in S, summing f over S yields c multiplied by the *)
1316+
(* cardinality of S. *)
1317+
(*************************************************************************)
1318+
THEOREM SumFunctionOnSetConst ==
1319+
ASSUME NEW D, NEW S \in SUBSET D, IsFiniteSet(S),
1320+
NEW f \in [D -> Int], NEW c \in Int, \A x \in S : f[x] = c
1321+
PROVE SumFunctionOnSet(f, S) = c * Cardinality(S)
1322+
<1>. DEFINE P(T) == SumFunctionOnSet(f, T) = c * Cardinality(T)
1323+
<1>1. P({})
1324+
<2>1. SumFunctionOnSet(f, {}) = 0
1325+
BY SumFunctionOnSetEmpty
1326+
<2>2. Cardinality({}) = 0
1327+
BY FS_EmptySet
1328+
<2>. QED BY <2>1, <2>2
1329+
<1>2. ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW x \in S \ T
1330+
PROVE P(T \union {x})
1331+
<2>1. SumFunctionOnSet(f, T \union {x}) = c + SumFunctionOnSet(f, T)
1332+
BY <1>2, SumFunctionOnSetAddIndex
1333+
<2>2. Cardinality(T \union {x}) = Cardinality(T) + 1
1334+
BY <1>2, FS_AddElement
1335+
<2>3. Cardinality(T) \in Nat
1336+
BY <1>2, FS_CardinalityType
1337+
<2>. QED BY <1>2, <2>1, <2>2, <2>3
1338+
<1>. QED BY <1>1, <1>2, FS_Induction, IsaM("iprover")
1339+
1340+
(*************************************************************************)
1341+
(* Summing a constant function over a finite set yields the constant *)
1342+
(* multiplied by the cardinality of the set. *)
1343+
(*************************************************************************)
1344+
(*
1345+
THEOREM SumFunctionOnSetConst ==
1346+
ASSUME NEW S, IsFiniteSet(S), NEW c \in Int
1347+
PROVE SumFunctionOnSet([s \in S |-> c], S) = c * Cardinality(S)
1348+
<1>. DEFINE fun == [s \in S |-> c]
1349+
<1>. DEFINE P(T) == SumFunctionOnSet(fun, T) = c * Cardinality(T)
1350+
<1>1. P({})
1351+
<2>1. SumFunctionOnSet(fun, {}) = 0
1352+
BY SumFunctionOnSetEmpty
1353+
<2>2. Cardinality({}) = 0
1354+
BY FS_EmptySet
1355+
<2>3. c * Cardinality({}) = 0
1356+
BY <2>2
1357+
<2>. QED BY <2>1, <2>3
1358+
<1>2. ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW x \in S \ T
1359+
PROVE P(T \union {x})
1360+
<2>1. \A j \in T \union {x} : fun[j] = c
1361+
BY <1>2
1362+
<2>2. \A j \in T \union {x} : fun[j] \in Int
1363+
BY <2>1, c \in Int
1364+
<2>3. SumFunctionOnSet(fun, T \union {x}) = fun[x] + SumFunctionOnSet(fun, T)
1365+
BY <1>2, <2>2, SumFunctionOnSetAddIndex
1366+
<2>4. fun[x] = c
1367+
BY <1>2
1368+
<2>5. Cardinality(T \union {x}) = Cardinality(T) + 1
1369+
BY <1>2, FS_AddElement
1370+
<2>6. Cardinality(T) \in Nat
1371+
BY <1>2, FS_CardinalityType
1372+
<2>7. SumFunctionOnSet(fun, T \union {x}) = c + c * Cardinality(T)
1373+
BY <1>2, <2>3, <2>4
1374+
<2>8. c + c * Cardinality(T) = c * (Cardinality(T) + 1)
1375+
BY <2>6
1376+
<2>9. c * (Cardinality(T) + 1) = c * Cardinality(T \union {x})
1377+
BY <2>5
1378+
<2>. QED BY <2>7, <2>8, <2>9
1379+
<1>. QED
1380+
<2>. HIDE DEF P
1381+
<2>. P(S) BY <1>1, <1>2, FS_Induction, IsaM("iprover")
1382+
<2>. QED BY DEF P
1383+
*)
1384+
13131385
(*************************************************************************)
13141386
(* Summing a function is monotonic in the function argument. *)
13151387
(*************************************************************************)
@@ -1401,6 +1473,21 @@ THEOREM SumFunctionZero ==
14011473
PROVE SumFunction(fun) = 0 <=> \A x \in DOMAIN fun : fun[x] = 0
14021474
BY SumFunctionOnSetZero DEF SumFunction
14031475

1476+
THEOREM SumFunctionConst ==
1477+
ASSUME NEW S, IsFiniteSet(S), NEW c \in Int
1478+
PROVE SumFunction([s \in S |-> c]) = c * Cardinality(S)
1479+
BY SumFunctionOnSetConst DEF SumFunction
1480+
(*
1481+
<1>. DEFINE fun == [s \in S |-> c]
1482+
<1>1. DOMAIN fun = S
1483+
OBVIOUS
1484+
<1>2. SumFunction(fun) = SumFunctionOnSet(fun, S)
1485+
BY <1>1 DEF SumFunction
1486+
<1>3. SumFunctionOnSet(fun, S) = c * Cardinality(S)
1487+
BY SumFunctionOnSetConst
1488+
<1>. QED BY <1>2, <1>3
1489+
*)
1490+
14041491
THEOREM SumFunctionMonotonic ==
14051492
ASSUME NEW f, IsFiniteSet(DOMAIN f), NEW g, DOMAIN g = DOMAIN f,
14061493
\A x \in DOMAIN f : f[x] \in Int,

0 commit comments

Comments
 (0)