Skip to content

Commit cffcfd9

Browse files
muenchnerkindlmuenchnerkindl
authored
Merge pull request #108 from kape1395/finite-sets-ext-MapThenSumSet-monOp
A couple of theorems on monotonicity of MapThenSumSet.
2 parents e88d04f + 2de57b8 commit cffcfd9

File tree

2 files changed

+134
-0
lines changed

2 files changed

+134
-0
lines changed

‎modules/FiniteSetsExt_theorems.tla‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,27 @@ LEMMA MapThenSumSetMonotonic ==
3737
PROVE MapThenSumSet(op, S \cup {e}) >= MapThenSumSet(op, S)
3838
PROOF OMITTED \* Proof in FiniteSetsExt_theorems_proofs.tla
3939

40+
LEMMA MapThenSumSetMonotonicOpGE ==
41+
ASSUME
42+
NEW S, IsFiniteSet(S),
43+
NEW op1(_), \A s \in S : op1(s) \in Nat,
44+
NEW op2(_), \A s \in S : op2(s) \in Nat,
45+
\A s \in S : op2(s) >= op1(s)
46+
PROVE
47+
MapThenSumSet(op2, S) >= MapThenSumSet(op1, S)
48+
PROOF OMITTED \* Proof in FiniteSetsExt_theorems_proofs.tla
49+
50+
LEMMA MapThenSumSetMonotonicOpGT ==
51+
ASSUME
52+
NEW S, IsFiniteSet(S),
53+
NEW op1(_), \A s \in S : op1(s) \in Nat,
54+
NEW op2(_), \A s \in S : op2(s) \in Nat,
55+
\A s \in S : op2(s) >= op1(s),
56+
\E s \in S : op2(s) > op1(s)
57+
PROVE
58+
MapThenSumSet(op2, S) > MapThenSumSet(op1, S)
59+
PROOF OMITTED \* Proof in FiniteSetsExt_theorems_proofs.tla
60+
4061
LEMMA MapThenSumSetZero ==
4162
ASSUME NEW S, IsFiniteSet(S),
4263
NEW op(_), \A e \in S: op(e) \in Nat,

‎modules/FiniteSetsExt_theorems_proofs.tla‎

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,76 @@ LEMMA CardSumMonotonic ==
172172
<1>q. QED BY <1>1, <1>2, CardSumType
173173

174174

175+
LEMMA CardSumMonotonicOpGE ==
176+
ASSUME
177+
NEW S, IsFiniteSet(S),
178+
NEW op1(_), \A s \in S : op1(s) \in Nat,
179+
NEW op2(_), \A s \in S : op2(s) \in Nat,
180+
\A s \in S : op2(s) >= op1(s)
181+
PROVE
182+
CardSum(S, op2) >= CardSum(S, op1)
183+
PROOF
184+
<1> DEFINE P(s) == s \subseteq S => CardSum(s, op2) >= CardSum(s, op1)
185+
<1> HIDE DEF P
186+
<1> SUFFICES P(S) BY DEF P
187+
<1>1. IsFiniteSet(S) OBVIOUS
188+
<1>2. P({}) BY CardSumEmpty, Isa DEF P
189+
<1>3. ASSUME
190+
NEW CONSTANT T,
191+
NEW CONSTANT x,
192+
IsFiniteSet(T) ,
193+
P(T) ,
194+
x \notin T
195+
PROVE P(T \cup {x})
196+
<2> SUFFICES ASSUME
197+
T \cup {x} \subseteq S
198+
PROVE CardSum(T \cup {x}, op2) >= CardSum(T \cup {x}, op1)
199+
BY DEF P
200+
<2>2. \A s \in T : op1(s) \in Nat OBVIOUS
201+
<2>3. \A s \in T : op2(s) \in Nat OBVIOUS
202+
<2>4. op1(x) \in Nat OBVIOUS
203+
<2>5. op2(x) \in Nat OBVIOUS
204+
<2>6. CardSum(T \cup {x}, op1) = CardSum(T, op1) + op1(x) BY ONLY <1>3, <2>2, <2>4, CardSumAddElem, Isa
205+
<2>7. CardSum(T \cup {x}, op2) = CardSum(T, op2) + op2(x) BY ONLY <1>3, <2>3, <2>5, CardSumAddElem, Isa
206+
<2>8. CardSum(T, op2) >= CardSum(T, op1) BY <1>3 DEF P
207+
<2>9. op2(x) >= op1(x) BY <1>3
208+
<2>10. CardSum(T, op1) \in Nat BY CardSumType, <1>3, <2>2
209+
<2>11. CardSum(T, op2) \in Nat BY CardSumType, <1>3, <2>3
210+
<2>q. QED BY <2>4, <2>5, <2>6, <2>7, <2>8, <2>9, <2>10, <2>11
211+
<1>q. QED BY ONLY FS_Induction, <1>1, <1>2, <1>3, Isa
212+
213+
214+
LEMMA CardSumMonotonicOpGT ==
215+
ASSUME
216+
NEW S, IsFiniteSet(S),
217+
NEW op1(_), \A s \in S : op1(s) \in Nat,
218+
NEW op2(_), \A s \in S : op2(s) \in Nat,
219+
\A s \in S : op2(s) >= op1(s),
220+
\E s \in S : op2(s) > op1(s)
221+
PROVE
222+
CardSum(S, op2) > CardSum(S, op1)
223+
PROOF
224+
<1>1. PICK x \in S : op2(x) > op1(x) OBVIOUS
225+
<1> DEFINE T == S \ {x}
226+
<1> HIDE DEF T
227+
<1>2. S = T \cup {x} BY <1>1 DEF T
228+
<1>3. IsFiniteSet(T) BY FS_Singleton, FS_Difference DEF T
229+
<1>4. \A t \in T : op1(t) \in Nat BY DEF T
230+
<1>5. \A t \in T : op2(t) \in Nat BY DEF T
231+
<1>6. CardSum(T, op2) >= CardSum(T, op1)
232+
<2>4. \A t \in T : op2(t) >= op1(t) BY DEF T
233+
<2>q. QED BY ONLY CardSumMonotonicOpGE, <1>3, <1>4, <1>5, <2>4, Isa
234+
<1>7. op1(x) \in Nat OBVIOUS
235+
<1>8. op2(x) \in Nat OBVIOUS
236+
<1>9. x \notin T BY DEF T
237+
<1>10. CardSum(T \cup {x}, op1) = CardSum(T, op1) + op1(x) BY ONLY <1>3, <1>4, <1>9, <1>7, CardSumAddElem, Isa
238+
<1>11. CardSum(T \cup {x}, op2) = CardSum(T, op2) + op2(x) BY ONLY <1>3, <1>5, <1>9, <1>8, CardSumAddElem, Isa
239+
<1>12. op2(x) > op1(x) BY <1>1
240+
<1>13. CardSum(T, op1) \in Nat BY CardSumType, <1>3, <1>4
241+
<1>14. CardSum(T, op2) \in Nat BY CardSumType, <1>3, <1>5
242+
<1>q. QED BY <1>1, <1>2, <1>6, <1>7, <1>8, <1>10, <1>11, <1>12, <1>13, <1>14
243+
244+
175245
LEMMA CardSumZero ==
176246
ASSUME NEW S, IsFiniteSet(S),
177247
NEW op(_), \A e \in S: op(e) \in Nat,
@@ -380,6 +450,49 @@ PROOF
380450
<1>1. IsFiniteSet(S \cup {e}) BY FS_Union, FS_Singleton
381451
<1>q. QED BY <1>1, CardSumMonotonic, MapThenSumSetDefined
382452

453+
LEMMA MapThenSumSetMonotonicOpGE ==
454+
ASSUME
455+
NEW S, IsFiniteSet(S),
456+
NEW op1(_), \A s \in S : op1(s) \in Nat,
457+
NEW op2(_), \A s \in S : op2(s) \in Nat,
458+
\A s \in S : op2(s) >= op1(s)
459+
PROVE
460+
MapThenSumSet(op2, S) >= MapThenSumSet(op1, S)
461+
PROOF
462+
<1> DEFINE
463+
C1 == CardSum(S, op1)
464+
C2 == CardSum(S, op2)
465+
M1 == MapThenSumSet(op1, S)
466+
M2 == MapThenSumSet(op2, S)
467+
<1> HIDE DEF C1, C2, M1, M2
468+
<1> SUFFICES M2 >= M1 BY DEF M1, M2
469+
<1>1. C2 >= C1 BY CardSumMonotonicOpGE, Isa DEF C1, C2
470+
<1>2. M1 = C1 BY MapThenSumSetDefined, Isa DEF M1, C1
471+
<1>3. M2 = C2 BY MapThenSumSetDefined, Isa DEF M2, C2
472+
<1>q. QED BY <1>1, <1>2, <1>3
473+
474+
LEMMA MapThenSumSetMonotonicOpGT ==
475+
ASSUME
476+
NEW S, IsFiniteSet(S),
477+
NEW op1(_), \A s \in S : op1(s) \in Nat,
478+
NEW op2(_), \A s \in S : op2(s) \in Nat,
479+
\A s \in S : op2(s) >= op1(s),
480+
\E s \in S : op2(s) > op1(s)
481+
PROVE
482+
MapThenSumSet(op2, S) > MapThenSumSet(op1, S)
483+
PROOF
484+
<1> DEFINE
485+
C1 == CardSum(S, op1)
486+
C2 == CardSum(S, op2)
487+
M1 == MapThenSumSet(op1, S)
488+
M2 == MapThenSumSet(op2, S)
489+
<1> HIDE DEF C1, C2, M1, M2
490+
<1> SUFFICES M2 > M1 BY DEF M1, M2
491+
<1>1. C2 > C1 BY CardSumMonotonicOpGT, Isa DEF C1, C2
492+
<1>2. M1 = C1 BY MapThenSumSetDefined, Isa DEF M1, C1
493+
<1>3. M2 = C2 BY MapThenSumSetDefined, Isa DEF M2, C2
494+
<1>q. QED BY <1>1, <1>2, <1>3
495+
383496
LEMMA MapThenSumSetZero ==
384497
ASSUME NEW S, IsFiniteSet(S),
385498
NEW op(_), \A e \in S: op(e) \in Nat,

0 commit comments

Comments
 (0)