summaryrefslogtreecommitdiff
path: root/Test/dafny1/UltraFilter.dfy
blob: c78d5e819d172cf7a3a7ed01c4cfcfe38f0293c2 (plain)
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
// 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;
  }
}