Skip to content

Commit 8d6a226

Browse files
muenchnerkindlmuenchnerkindl
authored
Merge pull request #116 from tlaplus/fold_proofs
theorem library for fold operators
2 parents f5db5ee + 8b5fc35 commit 8d6a226

File tree

7 files changed

+1163
-588
lines changed

7 files changed

+1163
-588
lines changed

‎modules/FiniteSetsExt.tla‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
--------------------------- MODULE FiniteSetsExt ---------------------------
22
EXTENDS Folds, Functions \* Replace with LOCAL INSTANCE when https://github.com/tlaplus/tlapm/issues/119 is resolved.
3-
LOCAL INSTANCE Naturals
3+
LOCAL INSTANCE Integers
44
LOCAL INSTANCE FiniteSets
55

66
(*************************************************************************)

‎modules/FiniteSetsExtTheorems.tla‎

Lines changed: 286 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,286 @@
1+
-------------------------- MODULE FiniteSetsExtTheorems -------------------
2+
EXTENDS FiniteSetsExt, FiniteSets, Integers
3+
(*************************************************************************)
4+
(* This module only lists theorem statements for reference. The proofs *)
5+
(* can be found in module FiniteSetsExtTheorems_proofs.tla. *)
6+
(*************************************************************************)
7+
8+
(*************************************************************************)
9+
(* Folding over an empty set produces the base value. *)
10+
(*************************************************************************)
11+
THEOREM FoldSetEmpty ==
12+
ASSUME NEW op(_,_), NEW base
13+
PROVE FoldSet(op, base, {}) = base
14+
15+
(*************************************************************************)
16+
(* Folding over a finite non-empty set corresponds to applying the *)
17+
(* underlying binary operator to some element of the set and the result *)
18+
(* of folding the remaining set elements. *)
19+
(*************************************************************************)
20+
THEOREM FoldSetNonempty ==
21+
ASSUME NEW op(_,_), NEW base, NEW S, S # {}, IsFiniteSet(S)
22+
PROVE \E x \in S : FoldSet(op, base, S) = op(x, FoldSet(op, base, S \ {x}))
23+
24+
(*************************************************************************)
25+
(* The type of folding a set corresponds to the type associated with the *)
26+
(* binary operator that underlies the fold. *)
27+
(*************************************************************************)
28+
THEOREM FoldSetType ==
29+
ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ,
30+
NEW S \in SUBSET Typ, IsFiniteSet(S),
31+
\A t,u \in Typ : op(t,u) \in Typ
32+
PROVE FoldSet(op, base, S) \in Typ
33+
34+
(*************************************************************************)
35+
(* If the binary operator is associative and commutative, the result of *)
36+
(* folding over a non-empty set corresponds to applying the operator to *)
37+
(* an arbitrary element of the set and the result of folding the *)
38+
(* remainder of the set. *)
39+
(*************************************************************************)
40+
THEOREM FoldSetAC ==
41+
ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ,
42+
\A t,u \in Typ : op(t,u) \in Typ,
43+
\A t,u \in Typ : op(t,u) = op(u,t),
44+
\A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v),
45+
NEW S \in SUBSET Typ, IsFiniteSet(S),
46+
NEW x \in S
47+
PROVE FoldSet(op, base, S) = op(x, FoldSet(op, base, S \ {x}))
48+
49+
\* reformulation in terms of adding an element to the set
50+
THEOREM FoldSetACAddElement ==
51+
ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ,
52+
\A t,u \in Typ : op(t,u) \in Typ,
53+
\A t,u \in Typ : op(t,u) = op(u,t),
54+
\A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v),
55+
NEW S \in SUBSET Typ, IsFiniteSet(S),
56+
NEW x \in Typ \ S
57+
PROVE FoldSet(op, base, S \union {x}) = op(x, FoldSet(op, base, S))
58+
59+
(*************************************************************************)
60+
(* For an AC operator `op` for which `base` is the neutral element, *)
61+
(* folding commutes with set union, for disjoint sets. *)
62+
(*************************************************************************)
63+
THEOREM FoldSetDisjointUnion ==
64+
ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ,
65+
\A t,u \in Typ : op(t,u) \in Typ,
66+
\A t,u \in Typ : op(t,u) = op(u,t),
67+
\A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v),
68+
\A t \in Typ : op(base, t) = t,
69+
NEW S \in SUBSET Typ, IsFiniteSet(S),
70+
NEW T \in SUBSET Typ, IsFiniteSet(T), S \cap T = {}
71+
PROVE FoldSet(op, base, S \union T) =
72+
op(FoldSet(op, base, S), FoldSet(op, base, T))
73+
74+
---------------------------------------------------------------------------
75+
76+
(*************************************************************************)
77+
(* The sum of a set of natural numbers, resp. integers is a natural *)
78+
(* number, resp. an integer. *)
79+
(*************************************************************************)
80+
THEOREM SumSetNat ==
81+
ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S)
82+
PROVE SumSet(S) \in Nat
83+
84+
THEOREM SumSetInt ==
85+
ASSUME NEW S \in SUBSET Int, IsFiniteSet(S)
86+
PROVE SumSet(S) \in Int
87+
88+
(*************************************************************************)
89+
(* The sum of the empty set is 0. *)
90+
(*************************************************************************)
91+
THEOREM SumSetEmpty == SumSet({}) = 0
92+
93+
(*************************************************************************)
94+
(* The sum of a finite non-empty set is the sum of an arbitrary element *)
95+
(* and the sum of the remaining elements. *)
96+
(*************************************************************************)
97+
THEOREM SumSetNonempty ==
98+
ASSUME NEW S \in SUBSET Int, IsFiniteSet(S), NEW x \in S
99+
PROVE SumSet(S) = x + SumSet(S \ {x})
100+
101+
\* reformulation of the above in terms of adding an element to a set
102+
THEOREM SumSetAddElement ==
103+
ASSUME NEW S \in SUBSET Int, IsFiniteSet(S), NEW x \in Int \ S
104+
PROVE SumSet(S \union {x}) = x + SumSet(S)
105+
106+
(*************************************************************************)
107+
(* Set summation distributes over union, for disjoint sets of integers. *)
108+
(*************************************************************************)
109+
THEOREM SumSetDisjointUnion ==
110+
ASSUME NEW S \in SUBSET Int, IsFiniteSet(S),
111+
NEW T \in SUBSET Int, IsFiniteSet(T), S \cap T = {}
112+
PROVE SumSet(S \union T) = SumSet(S) + SumSet(T)
113+
114+
(*************************************************************************)
115+
(* The sum of a subset of a set of natural numbers is bounded by the sum *)
116+
(* of the full set. *)
117+
(*************************************************************************)
118+
THEOREM SumSetNatSubset ==
119+
ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S),
120+
NEW T \in SUBSET S
121+
PROVE SumSet(T) <= SumSet(S)
122+
123+
(*************************************************************************)
124+
(* The sum of a set of natural numbers is zero only if the set is empty *)
125+
(* or the singleton {0}. *)
126+
(*************************************************************************)
127+
THEOREM SumSetNatZero ==
128+
ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S)
129+
PROVE SumSet(S) = 0 <=> S \subseteq {0}
130+
131+
---------------------------------------------------------------------------
132+
133+
(*************************************************************************)
134+
(* The product of a set of natural numbers, resp. integers is a natural *)
135+
(* number, resp. an integer. *)
136+
(*************************************************************************)
137+
THEOREM ProductSetNat ==
138+
ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S)
139+
PROVE ProductSet(S) \in Nat
140+
141+
THEOREM ProductSetInt ==
142+
ASSUME NEW S \in SUBSET Int, IsFiniteSet(S)
143+
PROVE ProductSet(S) \in Int
144+
145+
(*************************************************************************)
146+
(* The product of the empty set is 1. *)
147+
(*************************************************************************)
148+
THEOREM ProductSetEmpty == ProductSet({}) = 1
149+
150+
(*************************************************************************)
151+
(* The product of a finite non-empty set is the product of an arbitrary *)
152+
(* element and the product of the remaining elements. *)
153+
(*************************************************************************)
154+
THEOREM ProductSetNonempty ==
155+
ASSUME NEW S \in SUBSET Int, IsFiniteSet(S), NEW x \in S
156+
PROVE ProductSet(S) = x * ProductSet(S \ {x})
157+
158+
\* reformulation of the above in terms of adding an element to the set
159+
THEOREM ProductSetAddElement ==
160+
ASSUME NEW S \in SUBSET Int, IsFiniteSet(S), NEW x \in Int \ S
161+
PROVE ProductSet(S \union {x}) = x * ProductSet(S)
162+
163+
(*************************************************************************)
164+
(* Set product distributes over union, for disjoint sets of integers. *)
165+
(*************************************************************************)
166+
THEOREM ProductSetDisjointUnion ==
167+
ASSUME NEW S \in SUBSET Int, IsFiniteSet(S),
168+
NEW T \in SUBSET Int, IsFiniteSet(T), S \cap T = {}
169+
PROVE ProductSet(S \union T) = ProductSet(S) * ProductSet(T)
170+
171+
(*************************************************************************)
172+
(* The product of a set of natural numbers is one only if the set is *)
173+
(* empty or the singleton {1}. *)
174+
(*************************************************************************)
175+
THEOREM ProductSetNatOne ==
176+
ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S)
177+
PROVE ProductSet(S) = 1 <=> S \subseteq {1}
178+
179+
(*************************************************************************)
180+
(* The product of a set of integers is zero only if the set contains 0. *)
181+
(*************************************************************************)
182+
THEOREM ProductSetZero ==
183+
ASSUME NEW S \in SUBSET Int, IsFiniteSet(S)
184+
PROVE ProductSet(S) = 0 <=> 0 \in S
185+
186+
(*************************************************************************)
187+
(* The product of a subset of a set of non-zero natural numbers is *)
188+
(* bounded by the product of the full set. *)
189+
(*************************************************************************)
190+
THEOREM ProductSetNatSubset ==
191+
ASSUME NEW S \in SUBSET Nat \ {0}, IsFiniteSet(S),
192+
NEW T \in SUBSET S
193+
PROVE ProductSet(T) <= ProductSet(S)
194+
195+
---------------------------------------------------------------------------
196+
197+
(*************************************************************************)
198+
(* For an operator that maps set elements to natural numbers, resp. *)
199+
(* integers, MapThenSumSet yields a natural number, resp. an integer. *)
200+
(*************************************************************************)
201+
THEOREM MapThenSumSetNat ==
202+
ASSUME NEW S, IsFiniteSet(S),
203+
NEW op(_), \A s \in S : op(s) \in Nat
204+
PROVE MapThenSumSet(op, S) \in Nat
205+
206+
THEOREM MapThenSumSetInt ==
207+
ASSUME NEW S, IsFiniteSet(S),
208+
NEW op(_), \A s \in S : op(s) \in Int
209+
PROVE MapThenSumSet(op, S) \in Int
210+
211+
(*************************************************************************)
212+
(* The sum of mapping the empty set is 0. *)
213+
(*************************************************************************)
214+
THEOREM MapThenSumSetEmpty ==
215+
ASSUME NEW op(_)
216+
PROVE MapThenSumSet(op, {}) = 0
217+
218+
(*************************************************************************)
219+
(* The sum of mapping a finite non-empty set is the sum of the image of *)
220+
(* an arbitrary element and the sum of mapping the remaining elements. *)
221+
(*************************************************************************)
222+
THEOREM MapThenSumSetNonempty ==
223+
ASSUME NEW S, IsFiniteSet(S), NEW x \in S,
224+
NEW op(_), \A s \in S : op(s) \in Int
225+
PROVE MapThenSumSet(op, S) = op(x) + MapThenSumSet(op, S \ {x})
226+
227+
\* reformulation of the above in terms of adding an element to the set
228+
THEOREM MapThenSumSetAddElement ==
229+
ASSUME NEW S, IsFiniteSet(S), NEW x, x \notin S,
230+
NEW op(_), \A s \in S \union {x} : op(s) \in Int
231+
PROVE MapThenSumSet(op, S \union {x}) = op(x) + MapThenSumSet(op, S)
232+
233+
(*************************************************************************)
234+
(* Mapping then summing distributes over union, for disjoint finite sets *)
235+
(* of integers. *)
236+
(*************************************************************************)
237+
THEOREM MapThenSumSetDisjointUnion ==
238+
ASSUME NEW S, IsFiniteSet(S),
239+
NEW T, IsFiniteSet(T), S \cap T = {},
240+
NEW op(_), \A x \in S \union T : op(x) \in Int
241+
PROVE MapThenSumSet(op, S \union T) =
242+
MapThenSumSet(op, S) + MapThenSumSet(op, T)
243+
244+
(*************************************************************************)
245+
(* The map-sum of a subset of a finite set of natural numbers is bounded *)
246+
(* by the product of the full set. *)
247+
(*************************************************************************)
248+
THEOREM MapThenSumSetNatSubset ==
249+
ASSUME NEW S, IsFiniteSet(S),
250+
NEW T \in SUBSET S,
251+
NEW op(_), \A x \in S : op(x) \in Nat
252+
PROVE MapThenSumSet(op, T) <= MapThenSumSet(op, S)
253+
254+
(*************************************************************************)
255+
(* The map-sum of a finite set of natural numbers is zero only if all *)
256+
(* set elements are mapped to zero. *)
257+
(*************************************************************************)
258+
THEOREM MapThenSumSetZero ==
259+
ASSUME NEW S, IsFiniteSet(S),
260+
NEW op(_), \A s \in S : op(s) \in Nat
261+
PROVE MapThenSumSet(op, S) = 0 <=> \A s \in S : op(s) = 0
262+
263+
(*************************************************************************)
264+
(* The map-sum of a finite set of natural numbers is monotonic in the *)
265+
(* function argument *)
266+
(*************************************************************************)
267+
THEOREM MapThenSumSetMonotonic ==
268+
ASSUME NEW S, IsFiniteSet(S),
269+
NEW f(_), \A s \in S : f(s) \in Int,
270+
NEW g(_), \A s \in S : g(s) \in Int,
271+
\A s \in S : f(s) <= g(s)
272+
PROVE MapThenSumSet(f, S) <= MapThenSumSet(g, S)
273+
274+
(*************************************************************************)
275+
(* Moreover, if the second function returns a larger value for at least *)
276+
(* one element of the set, then the map-sum will be strictly larger. *)
277+
(*************************************************************************)
278+
THEOREM MapThenSumSetStrictlyMonotonic ==
279+
ASSUME NEW S, IsFiniteSet(S),
280+
NEW f(_), \A s \in S : f(s) \in Int,
281+
NEW g(_), \A s \in S : g(s) \in Int,
282+
\A s \in S : f(s) <= g(s),
283+
NEW s \in S, f(s) < g(s)
284+
PROVE MapThenSumSet(f, S) < MapThenSumSet(g, S)
285+
286+
===========================================================================

0 commit comments

Comments
 (0)