1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// ultra filter
class UltraFilter<G(==)> {
static function IsFilter(f: set<set<G>>, S: set<G>): bool
{
(forall A, B :: A in f && A <= B ==> B in f) &&
(forall C, D :: C in f && D in f ==> C * D in f) &&
S in f &&
{} !in f
}
static function IsUltraFilter(f: set<set<G>>, S: set<G>): bool
{
IsFilter(f, S) &&
(forall g :: IsFilter(g, S) && f <= g ==> f == g)
}
method Theorem(f: set<set<G>>, S: set<G>, M: set<G>, N: set<G>)
requires IsUltraFilter(f, S);
requires M + N in f;
ensures M in f || N in f;
{
if (M !in f) {
// instantiate 'g' with the following 'h'
var h := H(f, S, M);
Lemma_HIsFilter(h, f, S, M);
Lemma_FHOrdering0(h, f, S, M);
}
}
// Dafny currently does not have a set comprehension expression, so this method stub will have to do
method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>)
ensures (forall X :: X in h <==> M + X in f);
method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
requires IsFilter(f, S);
requires (forall X :: X in h <==> M + X in f);
requires M !in f;
ensures IsFilter(h, S);
{
// call Lemma_H0(h, f, S, M, *, *);
assume (forall A, B :: A in h && A <= B ==> B in h);
// call Lemma_H1(h, f, S, M, *, *);
assume (forall C, D :: C in h && D in h ==> C * D in h);
Lemma_H2(h, f, S, M);
Lemma_H3(h, f, S, M);
}
method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)
requires IsFilter(f, S);
requires (forall X :: X in h <==> M + X in f);
requires A in h && A <= B;
ensures B in h;
{
assert M + A <= M + B;
}
method Lemma_H1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, C: set<G>, D: set<G>)
requires IsFilter(f, S);
requires (forall X :: X in h <==> M + X in f);
requires C in h && D in h;
ensures C * D in h;
{
assert (M + C) * (M + D) == M + (C * D);
}
method Lemma_H2(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
requires IsFilter(f, S);
requires (forall X :: X in h <==> M + X in f);
ensures S in h;
{
// S is intended to stand for the universal set, but this is the only place where that plays a role
assume M <= S;
assert M + S == S;
}
method Lemma_H3(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
requires IsFilter(f, S);
requires (forall X :: X in h <==> M + X in f);
requires M !in f;
ensures {} !in h;
{
assert M + {} == M;
}
method Lemma_FHOrdering0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
requires IsFilter(f, S);
requires (forall X :: X in h <==> M + X in f);
requires IsFilter(h, S);
ensures f <= h;
{
// call Lemma_FHOrdering1(h, f, S, M, *);
assume (forall Y :: Y in f ==> Y in h);
assume f <= h; // hickup in boxing
}
method Lemma_FHOrdering1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, Y: set<G>)
requires IsFilter(f, S);
requires (forall X :: X in h <==> M + X in f);
ensures Y in f ==> Y in h;
{
assert Y <= M + Y;
}
}
|
