Skip to content

Commit b0c15d0

Browse files
stefan-awsstefan-aws
authored
Unique Maximum Element (#113)
* Unique minimum proof * adding unique maximum and updating structure * format * format * remove duplicates in dafny subfolder * remove empty line * space fix * remove equivalence relation and symmetric * format space * comment style * comments again * refinement * naming * naming * fix typos * remove empty space * remove line * format * newline * format
1 parent 8cfeb0d commit b0c15d0

File tree

4 files changed

+232
-19
lines changed

4 files changed

+232
-19
lines changed

‎src/Collections/Sets/Sets.dfy

+85
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,12 @@
1414
*******************************************************************************/
1515

1616
include "../../Functions.dfy"
17+
include "../../Relations.dfy"
1718

1819
module {:options "-functionSyntax:4"} Sets {
1920

2021
import opened Functions
22+
import opened Relations
2123

2224
/* If all elements in set x are in set y, x is a subset of y. */
2325
lemma LemmaSubset<T>(x: set<T>, y: set<T>)
@@ -236,4 +238,87 @@ module {:options "-functionSyntax:4"} Sets {
236238
LemmaSubsetSize(x, range);
237239
}
238240

241+
/** In a pre-ordered set, a greatest element is necessarily maximal. */
242+
lemma LemmaGreatestImpliesMaximal<T(!new)>(R: (T, T) -> bool, max: T, s: set<T>)
243+
requires PreOrdering(R)
244+
ensures IsGreatest(R, max, s) ==> IsMaximal(R, max, s)
245+
{
246+
}
247+
248+
/** In a pre-ordered set, a least element is necessarily minimal. */
249+
lemma LemmaLeastImpliesMinimal<T(!new)>(R: (T, T) -> bool, min: T, s: set<T>)
250+
requires PreOrdering(R)
251+
ensures IsLeast(R, min, s) ==> IsMinimal(R, min, s)
252+
{
253+
}
254+
255+
/** In a totally-ordered set, an element is maximal if and only if it is a greatest element. */
256+
lemma LemmaMaximalEquivalentGreatest<T(!new)>(R: (T, T) -> bool, max: T, s: set<T>)
257+
requires TotalOrdering(R)
258+
ensures IsGreatest(R, max, s) <==> IsMaximal(R, max, s)
259+
{
260+
}
261+
262+
/** In a totally-ordered set, an element is minimal if and only if it is a least element. */
263+
lemma LemmaMinimalEquivalentLeast<T(!new)>(R: (T, T) -> bool, min: T, s: set<T>)
264+
requires TotalOrdering(R)
265+
ensures IsLeast(R, min, s) <==> IsMinimal(R, min, s)
266+
{
267+
}
268+
269+
/** In a partially-ordered set, there exists at most one least element. */
270+
lemma LemmaLeastIsUnique<T(!new)>(R: (T, T) -> bool, s: set<T>)
271+
requires PartialOrdering(R)
272+
ensures forall min, min' | IsLeast(R, min, s) && IsLeast(R, min', s) :: min == min'
273+
{}
274+
275+
/** In a partially-ordered set, there exists at most one greatest element. */
276+
lemma LemmaGreatestIsUnique<T(!new)>(R: (T, T) -> bool, s: set<T>)
277+
requires PartialOrdering(R)
278+
ensures forall max, max' | IsGreatest(R, max, s) && IsGreatest(R, max', s) :: max == max'
279+
{}
280+
281+
/** In a totally-ordered set, there exists at most one minimal element. */
282+
lemma LemmaMinimalIsUnique<T(!new)>(R: (T, T) -> bool, s: set<T>)
283+
requires TotalOrdering(R)
284+
ensures forall min, min' | IsMinimal(R, min, s) && IsMinimal(R, min', s) :: min == min'
285+
{}
286+
287+
/** In a totally-ordered set, there exists at most one maximal element. */
288+
lemma LemmaMaximalIsUnique<T(!new)>(R: (T, T) -> bool, s: set<T>)
289+
requires TotalOrdering(R)
290+
ensures forall max, max' | IsMaximal(R, max, s) && IsMaximal(R, max', s) :: max == max'
291+
{}
292+
293+
/** Any totally-ordered set contains a unique minimal (equivalently, least) element. */
294+
lemma LemmaFindUniqueMinimal<T(!new)>(R: (T, T) -> bool, s: set<T>) returns (min: T)
295+
requires |s| > 0 && TotalOrdering(R)
296+
ensures IsMinimal(R, min, s) && (forall min': T | IsMinimal(R, min', s) :: min == min')
297+
{
298+
var x :| x in s;
299+
if s == {x} {
300+
min := x;
301+
} else {
302+
var min' := LemmaFindUniqueMinimal(R, s - {x});
303+
if
304+
case R(min', x) => min := min';
305+
case R(x, min') => min := x;
306+
}
307+
}
308+
309+
/** Any totally ordered set contains a unique maximal (equivalently, greatest) element. */
310+
lemma LemmaFindUniqueMaximal<T(!new)>(R: (T, T) -> bool, s: set<T>) returns (max: T)
311+
requires |s| > 0 && TotalOrdering(R)
312+
ensures IsMaximal(R, max, s) && (forall max': T | IsMaximal(R, max', s) :: max == max')
313+
{
314+
var x :| x in s;
315+
if s == {x} {
316+
max := x;
317+
} else {
318+
var max' := LemmaFindUniqueMaximal(R, s - {x});
319+
if
320+
case R(max', x) => max := x;
321+
case R(x, max') => max := max';
322+
}
323+
}
239324
}

‎src/Relations.dfy

+31-19
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,17 @@ module {:options "-functionSyntax:4"} Relations {
4949
&& Connected(R)
5050
}
5151

52+
ghost predicate PreOrdering<T(!new)>(R: (T, T) -> bool) {
53+
&& Reflexive(R)
54+
&& Transitive(R)
55+
}
56+
57+
ghost predicate PartialOrdering<T(!new)>(R: (T, T) -> bool) {
58+
&& Reflexive(R)
59+
&& Transitive(R)
60+
&& AntiSymmetric(R)
61+
}
62+
5263
ghost predicate EquivalenceRelation<T(!new)>(R: (T, T) -> bool) {
5364
&& Reflexive(R)
5465
&& Symmetric(R)
@@ -59,25 +70,26 @@ module {:options "-functionSyntax:4"} Relations {
5970
forall i, j | 0 <= i < j < |a| :: lessThan(a[i], a[j])
6071
}
6172

62-
/* An element in an ordered set is called minimal, if it is less than every element of the set. */
63-
ghost predicate IsMinimum<T>(R: (T, T) -> bool, m: T, s: set<T>) {
64-
m in s && forall y: T | y in s :: R(m, y)
65-
}
66-
67-
/* Any totally ordered set contains a unique minimal element. */
68-
lemma LemmaUniqueMinimum<T(!new)>(R: (T, T) -> bool, s: set<T>) returns (m: T)
69-
requires |s| > 0 && TotalOrdering(R)
70-
ensures IsMinimum(R, m, s) && (forall n: T | IsMinimum(R, n, s) :: m == n)
71-
{
72-
var x :| x in s;
73-
if s == {x} {
74-
m := x;
75-
} else {
76-
var m' := LemmaUniqueMinimum(R, s - {x});
77-
if
78-
case R(m', x) => m := m';
79-
case R(x, m') => m := x;
80-
}
73+
/** An element in an ordered set is called a least element (or a minimum), if it is less than
74+
every other element of the set. */
75+
ghost predicate IsLeast<T>(R: (T, T) -> bool, min: T, s: set<T>) {
76+
min in s && forall x | x in s :: R(min, x)
77+
}
78+
79+
/** An element in an ordered set is called a minimal element, if no other element is less than it. */
80+
ghost predicate IsMinimal<T>(R: (T, T) -> bool, min: T, s: set<T>) {
81+
min in s && forall x | x in s && R(x, min) :: R(min, x)
82+
}
83+
84+
/** An element in an ordered set is called a greatest element (or a maximum), if it is greater than
85+
every other element of the set. */
86+
ghost predicate IsGreatest<T>(R: (T, T) -> bool, max: T, s: set<T>) {
87+
max in s && forall x | x in s :: R(x, max)
88+
}
89+
90+
/** An element in an ordered set is called a maximal element, if no other element is greater than it. */
91+
ghost predicate IsMaximal<T>(R: (T, T) -> bool, max: T, s: set<T>) {
92+
max in s && forall x | x in s && R(max, x) :: R(x, max)
8193
}
8294

8395
lemma LemmaNewFirstElementStillSortedBy<T>(x: T, s: seq<T>, lessThan: (T, T) -> bool)

‎src/dafny/Collections/Sets.dfy

+83
Original file line numberDiff line numberDiff line change
@@ -236,4 +236,87 @@ module {:options "-functionSyntax:4"} Dafny.Collections.Sets {
236236
LemmaSubsetSize(x, range);
237237
}
238238

239+
/** In a pre-ordered set, a greatest element is necessarily maximal. */
240+
lemma LemmaGreatestImpliesMaximal<T(!new)>(R: (T, T) -> bool, max: T, s: set<T>)
241+
requires PreOrdering(R)
242+
ensures IsGreatest(R, max, s) ==> IsMaximal(R, max, s)
243+
{
244+
}
245+
246+
/** In a pre-ordered set, a least element is necessarily minimal. */
247+
lemma LemmaLeastImpliesMinimal<T(!new)>(R: (T, T) -> bool, min: T, s: set<T>)
248+
requires PreOrdering(R)
249+
ensures IsLeast(R, min, s) ==> IsMinimal(R, min, s)
250+
{
251+
}
252+
253+
/** In a totally-ordered set, an element is maximal if and only if it is a greatest element. */
254+
lemma LemmaMaximalEquivalentGreatest<T(!new)>(R: (T, T) -> bool, max: T, s: set<T>)
255+
requires TotalOrdering(R)
256+
ensures IsGreatest(R, max, s) <==> IsMaximal(R, max, s)
257+
{
258+
}
259+
260+
/** In a totally-ordered set, an element is minimal if and only if it is a least element. */
261+
lemma LemmaMinimalEquivalentLeast<T(!new)>(R: (T, T) -> bool, min: T, s: set<T>)
262+
requires TotalOrdering(R)
263+
ensures IsLeast(R, min, s) <==> IsMinimal(R, min, s)
264+
{
265+
}
266+
267+
/** In a partially-ordered set, there exists at most one least element. */
268+
lemma LemmaLeastIsUnique<T(!new)>(R: (T, T) -> bool, s: set<T>)
269+
requires PartialOrdering(R)
270+
ensures forall min, min' | IsLeast(R, min, s) && IsLeast(R, min', s) :: min == min'
271+
{}
272+
273+
/** In a partially-ordered set, there exists at most one greatest element. */
274+
lemma LemmaGreatestIsUnique<T(!new)>(R: (T, T) -> bool, s: set<T>)
275+
requires PartialOrdering(R)
276+
ensures forall max, max' | IsGreatest(R, max, s) && IsGreatest(R, max', s) :: max == max'
277+
{}
278+
279+
/** In a totally-ordered set, there exists at most one minimal element. */
280+
lemma LemmaMinimalIsUnique<T(!new)>(R: (T, T) -> bool, s: set<T>)
281+
requires TotalOrdering(R)
282+
ensures forall min, min' | IsMinimal(R, min, s) && IsMinimal(R, min', s) :: min == min'
283+
{}
284+
285+
/** In a totally-ordered set, there exists at most one maximal element. */
286+
lemma LemmaMaximalIsUnique<T(!new)>(R: (T, T) -> bool, s: set<T>)
287+
requires TotalOrdering(R)
288+
ensures forall max, max' | IsMaximal(R, max, s) && IsMaximal(R, max', s) :: max == max'
289+
{}
290+
291+
/** Any totally-ordered set contains a unique minimal (equivalently, least) element. */
292+
lemma LemmaFindUniqueMinimal<T(!new)>(R: (T, T) -> bool, s: set<T>) returns (min: T)
293+
requires |s| > 0 && TotalOrdering(R)
294+
ensures IsMinimal(R, min, s) && (forall min': T | IsMinimal(R, min', s) :: min == min')
295+
{
296+
var x :| x in s;
297+
if s == {x} {
298+
min := x;
299+
} else {
300+
var min' := LemmaFindUniqueMinimal(R, s - {x});
301+
if
302+
case R(min', x) => min := min';
303+
case R(x, min') => min := x;
304+
}
305+
}
306+
307+
/** Any totally ordered set contains a unique maximal (equivalently, greatest) element. */
308+
lemma LemmaFindUniqueMaximal<T(!new)>(R: (T, T) -> bool, s: set<T>) returns (max: T)
309+
requires |s| > 0 && TotalOrdering(R)
310+
ensures IsMaximal(R, max, s) && (forall max': T | IsMaximal(R, max', s) :: max == max')
311+
{
312+
var x :| x in s;
313+
if s == {x} {
314+
max := x;
315+
} else {
316+
var max' := LemmaFindUniqueMaximal(R, s - {x});
317+
if
318+
case R(max', x) => max := x;
319+
case R(x, max') => max := max';
320+
}
321+
}
239322
}

‎src/dafny/Relations.dfy

+33
Original file line numberDiff line numberDiff line change
@@ -75,9 +75,42 @@ module {:options "-functionSyntax:4"} Dafny.Relations {
7575
&& Connected(R)
7676
}
7777

78+
ghost predicate PreOrdering<T(!new)>(R: (T, T) -> bool) {
79+
&& Reflexive(R)
80+
&& Transitive(R)
81+
}
82+
83+
ghost predicate PartialOrdering<T(!new)>(R: (T, T) -> bool) {
84+
&& Reflexive(R)
85+
&& Transitive(R)
86+
&& AntiSymmetric(R)
87+
}
88+
7889
ghost predicate EquivalenceRelation<T(!new)>(R: (T, T) -> bool) {
7990
&& Reflexive(R)
8091
&& Symmetric(R)
8192
&& Transitive(R)
8293
}
94+
95+
/** An element in an ordered set is called a least element (or a minimum), if it is less than
96+
every other element of the set. */
97+
ghost predicate IsLeast<T>(R: (T, T) -> bool, min: T, s: set<T>) {
98+
min in s && forall x | x in s :: R(min, x)
99+
}
100+
101+
/** An element in an ordered set is called a minimal element, if no other element is less than it. */
102+
ghost predicate IsMinimal<T>(R: (T, T) -> bool, min: T, s: set<T>) {
103+
min in s && forall x | x in s && R(x, min) :: R(min, x)
104+
}
105+
106+
/** An element in an ordered set is called a greatest element (or a maximum), if it is greater than
107+
every other element of the set. */
108+
ghost predicate IsGreatest<T>(R: (T, T) -> bool, max: T, s: set<T>) {
109+
max in s && forall x | x in s :: R(x, max)
110+
}
111+
112+
/** An element in an ordered set is called a maximal element, if no other element is greater than it. */
113+
ghost predicate IsMaximal<T>(R: (T, T) -> bool, max: T, s: set<T>) {
114+
max in s && forall x | x in s && R(max, x) :: R(x, max)
115+
}
83116
}

0 commit comments

Comments
 (0)