← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/AIM4/bag/Bag.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/AIM4/bag/Bag.agda
1
 
{-# OPTIONS --allow-unsolved-metas --no-termination-check
2
 
  #-}
3
 
module Bag where
4
 
 
5
 
  import Prelude
6
 
  import Equiv
7
 
  import Datoid
8
 
  import Eq
9
 
  import Nat
10
 
  import List
11
 
  import Pos
12
 
 
13
 
  open Prelude
14
 
  open Equiv
15
 
  open Datoid
16
 
  open Eq
17
 
  open Nat
18
 
  open List
19
 
 
20
 
  abstract
21
 
 
22
 
  ----------------------------------------------------------------------
23
 
  -- Bag type
24
 
 
25
 
    private
26
 
      -- If this were Coq then the invariant should be a Prop. Similar
27
 
      -- remarks apply to some definitions below. Since I have to write
28
 
      -- the supporting library myself I can't be bothered to
29
 
      -- distinguish Set and Prop right now though.
30
 
 
31
 
      data BagType (a : Datoid) : Set where
32
 
        bt :  (pairs : List (Pair Pos.Pos (El a)))
33
 
           -> NoDuplicates a (map snd pairs)
34
 
           -> BagType a
35
 
 
36
 
      list : {a : Datoid} -> BagType a -> List (Pair Pos.Pos (El a))
37
 
      list (bt l _) = l
38
 
 
39
 
      contents : {a : Datoid} -> BagType a -> List (El a)
40
 
      contents b = map snd (list b)
41
 
 
42
 
      invariant :  {a : Datoid} -> (b : BagType a)
43
 
                -> NoDuplicates a (contents b)
44
 
      invariant (bt _ i) = i
45
 
 
46
 
    private
47
 
      elemDatoid : Datoid -> Datoid
48
 
      elemDatoid a = pairDatoid Pos.posDatoid a
49
 
 
50
 
      BagEq : (a : Datoid) -> BagType a -> BagType a -> Set
51
 
      BagEq a b1 b2 = rel' (Permutation (elemDatoid a)) (list b1) (list b2)
52
 
 
53
 
      eqRefl : {a : Datoid} -> (x : BagType a) -> BagEq a x x
54
 
      eqRefl {a} x = refl (Permutation (elemDatoid a)) {list x}
55
 
 
56
 
      eqSym :  {a : Datoid} -> (x y : BagType a)
57
 
            -> BagEq a x y -> BagEq a y x
58
 
      eqSym {a} x y = sym (Permutation (elemDatoid a)) {list x} {list y}
59
 
 
60
 
      eqTrans :  {a : Datoid} -> (x y z : BagType a)
61
 
            -> BagEq a x y -> BagEq a y z -> BagEq a x z
62
 
      eqTrans {a} x y z = trans (Permutation (elemDatoid a))
63
 
                                {list x} {list y} {list z}
64
 
 
65
 
      eqDec : {a : Datoid} -> (x y : BagType a)
66
 
            -> Either (BagEq a x y) _
67
 
      eqDec {a} x y = decRel (Permutation (elemDatoid a)) (list x) (list y)
68
 
 
69
 
      BagEquiv : (a : Datoid) -> DecidableEquiv (BagType a)
70
 
      BagEquiv a = decEquiv (equiv (BagEq a) eqRefl eqSym eqTrans) (dec eqDec)
71
 
 
72
 
    Bag : Datoid -> Datoid
73
 
    Bag a = datoid (BagType a) (BagEquiv a)
74
 
 
75
 
  ----------------------------------------------------------------------
76
 
  -- Bag primitives
77
 
 
78
 
    empty : {a : Datoid} -> El (Bag a)
79
 
    empty = bt nil unit
80
 
 
81
 
    private
82
 
      data LookupResult (a : Datoid) (x : El a) (b : El (Bag a)) : Set where
83
 
        lr :  Nat
84
 
           -> (b' : El (Bag a))
85
 
           -> Not (member a x (contents b'))
86
 
           -> ({y : El a} -> Not (member a y (contents b))
87
 
                          -> Not (member a y (contents b')))
88
 
           -> LookupResult a x b
89
 
 
90
 
      lookup1 :  {a : Datoid}
91
 
              -> (n : Pos.Pos)
92
 
              -> (y : El a)
93
 
              -> (b' : El (Bag a))
94
 
              -> (nyb' : Not (member a y (contents b')))
95
 
              -> (x : El a)
96
 
              -> Either (datoidRel a x y) _
97
 
              -> LookupResult a x b'
98
 
              -> LookupResult a x (bt (pair n y :: list b')
99
 
                                      (pair nyb' (invariant b')))
100
 
      lookup1 n y b' nyb' x (left xy) _ =
101
 
        lr (Pos.toNat n) b'
102
 
           (contrapositive (memberPreservesEq xy (contents b')) nyb')
103
 
           (\{y'} ny'b -> snd (notDistribIn ny'b))
104
 
      lookup1 {a} n y b' nyb' x (right nxy)
105
 
              (lr n' (bt b'' ndb'') nxb'' nmPres) =
106
 
        lr n' (bt (pair n y :: b'') (pair (nmPres nyb') ndb''))
107
 
           (notDistribOut {datoidRel a x y} nxy nxb'')
108
 
           (\{y'} ny'b -> notDistribOut (fst (notDistribIn ny'b))
109
 
                                        (nmPres (snd (notDistribIn ny'b))))
110
 
 
111
 
      lookup2
112
 
        :  {a : Datoid}
113
 
        -> (x : El a)
114
 
        -> (b : El (Bag a))
115
 
        -> LookupResult a x b
116
 
      lookup2 x (bt nil nd) = lr zero (bt nil nd) (not id) (\{_} _ -> not id)
117
 
      lookup2 {a} x (bt (pair n y :: b) (pair nyb ndb)) =
118
 
        lookup1 n y (bt b ndb) nyb x
119
 
                (decRel (datoidEq a) x y)
120
 
                (lookup2 x (bt b ndb))
121
 
 
122
 
      lookup3 :  {a : Datoid} -> {x : El a} -> {b : El (Bag a)}
123
 
              -> LookupResult a x b -> Pair Nat (El (Bag a))
124
 
      lookup3 (lr n b _ _) = pair n b
125
 
 
126
 
    lookup : {a : Datoid} -> El a -> El (Bag a) -> Pair Nat (El (Bag a))
127
 
    lookup x b = lookup3 (lookup2 x b)
128
 
 
129
 
    private
130
 
      insert' :  {a : Datoid} -> (x : El a) -> {b : El (Bag a)}
131
 
              -> LookupResult a x b -> El (Bag a)
132
 
      insert' x (lr n (bt b ndb) nxb _) =
133
 
        bt (pair (Pos.suc' n) x :: b) (pair nxb ndb)
134
 
 
135
 
    insert : {a : Datoid} -> El a -> El (Bag a) -> El (Bag a)
136
 
    insert x b = insert' x (lookup2 x b)
137
 
 
138
 
    private
139
 
 
140
 
      postulate
141
 
        insertLemma1
142
 
          :  {a : Datoid}
143
 
          -> (x : El a)
144
 
          -> (b : El (Bag a))
145
 
          -> (nxb : Not (member a x (contents b)))
146
 
          -> datoidRel (Bag a)
147
 
                       (insert x b)
148
 
                       (bt (pair Pos.one x :: list b) (pair nxb (invariant b)))
149
 
 
150
 
        insertLemma2
151
 
          :  {a : Datoid}
152
 
          -> (n : Pos.Pos)
153
 
          -> (x : El a)
154
 
          -> (b : El (Bag a))
155
 
          -> (nxb : Not (member a x (contents b)))
156
 
          -> datoidRel (Bag a)
157
 
                       (insert x (bt (pair n x :: list b)
158
 
                                     (pair nxb (invariant b))))
159
 
                       (bt (pair (Pos.suc n) x :: list b)
160
 
                           (pair nxb (invariant b)))
161
 
 
162
 
  ----------------------------------------------------------------------
163
 
  -- Bag traversals
164
 
 
165
 
  data Traverse (a : Datoid) : Set where
166
 
    Empty  : Traverse a
167
 
    Insert : (x : El a) -> (b : El (Bag a)) -> Traverse a
168
 
 
169
 
  run : {a : Datoid} -> Traverse a -> El (Bag a)
170
 
  run Empty        = empty
171
 
  run (Insert x b) = insert x b
172
 
 
173
 
  abstract
174
 
 
175
 
    traverse : {a : Datoid} -> El (Bag a) -> Traverse a
176
 
    traverse     (bt nil _)                          = Empty
177
 
    traverse {a} (bt (pair n x :: b) (pair nxb ndb)) = traverse' (Pos.pred n)
178
 
      where
179
 
      private
180
 
        traverse' :  Maybe Pos.Pos -> Traverse a
181
 
        traverse' Nothing  = Insert x (bt b ndb)
182
 
        traverse' (Just n) = Insert x (bt (pair n x :: b) (pair nxb ndb))
183
 
 
184
 
    traverseTraverses
185
 
      :  {a : Datoid} -> (b : El (Bag a))
186
 
      -> datoidRel (Bag a) (run (traverse b)) b
187
 
    traverseTraverses {a} (bt nil unit) = dRefl (Bag a) {empty}
188
 
    traverseTraverses {a} (bt (pair n x :: b) (pair nxb ndb)) =
189
 
      tT (Pos.pred n) (Pos.predOK n)
190
 
      where
191
 
      private
192
 
        postulate
193
 
          subst' :  {a : Datoid} -> (P : El a -> Set) -> (x y : El a)
194
 
                 -> datoidRel a x y -> P x -> P y
195
 
 
196
 
        tT :  (predN : Maybe Pos.Pos)
197
 
           -> Pos.Pred n predN
198
 
           -> datoidRel (Bag a)
199
 
                        (run (traverse (bt (pair n x :: b) (pair nxb ndb))))
200
 
                        (bt (pair n x :: b) (pair nxb ndb))
201
 
        tT Nothing  (Pos.ok eq) = ?
202
 
          -- subst' (\p -> datoidRel (Bag a)
203
 
          --                 (run (traverse (bt (pair p x :: b) (pair nxb ndb))))
204
 
          --                 (bt (pair p x :: b) (pair nxb ndb)))
205
 
          --        Pos.one n eq (insertLemma1 x (bt b ndb) nxb)
206
 
 
207
 
          -- eq : one == n
208
 
          -- data Pred (p : Pos) (mP : Maybe Pos) : Set where
209
 
          --   ok : datoidRel posDatoid (sucPred mP) p -> Pred p mP
210
 
          -- insert x (bt b ndb) == bt (pair n x :: b) (pair nxb ndb)
211
 
        tT (Just n) (Pos.ok eq) = ? -- insertLemma2 n x (bt b ndb) nxb
212
 
          -- insert x (bt (pair n x :: b) (pair nxb btb) ==
213
 
          -- bt (pair (suc n) x :: b) (pair nxb btb)
214
 
 
215
 
    bagElim
216
 
      :  {a : Datoid}
217
 
      -> (P : El (Bag a) -> Set)
218
 
      -> Respects (Bag a) P
219
 
      -> P empty
220
 
      -> ((x : El a) -> (b : El (Bag a)) -> P b -> P (insert x b))
221
 
      -> (b : El (Bag a))
222
 
      -> P b
223
 
    bagElim {a} P Prespects e i b =
224
 
      bagElim' b (traverse b) (traverseTraverses b)
225
 
      where
226
 
      private
227
 
        bagElim'
228
 
          :  (b : El (Bag a))
229
 
          -> (t : Traverse a)
230
 
          -> datoidRel (Bag a) (run t) b
231
 
          -> P b
232
 
        bagElim' b Empty         eq = subst Prespects empty b eq e
233
 
        bagElim' b (Insert x b') eq =
234
 
          subst Prespects (insert x b') b eq
235
 
                (i x b' (bagElim' b' (traverse b') (traverseTraverses b')))
236
 
 
237
 
  ----------------------------------------------------------------------
238
 
  -- Respect and equality preservation lemmas
239
 
 
240
 
    postulate
241
 
      insertPreservesRespect
242
 
        :  {a : Datoid}
243
 
        -> (P : El (Bag a) -> Set)
244
 
        -> (x : El a)
245
 
        -> Respects (Bag a) P
246
 
        -> Respects (Bag a) (\b -> P (insert x b))
247
 
 
248
 
      lookupPreservesRespect
249
 
        :  {a : Datoid}
250
 
        -> (P : El (Bag a) -> Set)
251
 
        -> (x : El a)
252
 
        -> Respects (Bag a) P
253
 
        -> Respects (Bag a) (\b -> P (snd $ lookup x b))
254
 
 
255
 
      -- This doesn't type check without John Major equality or some
256
 
      -- ugly substitutions...
257
 
      -- bagElimPreservesEquality
258
 
      --   :  {a : Datoid}
259
 
      --   -> (P : El (Bag a) -> Set)
260
 
      --   -> (r : Respects (Bag a) P)
261
 
      --   -> (e : P empty)
262
 
      --   -> (i : (x : El a) -> (b : El (Bag a)) -> P b -> P (insert x b))
263
 
      --   -> (   (x1 x2 : El a) -> (b1 b2 : El (Bag a))
264
 
      --       -> (p1 : P b1) -> (p2 : P b2)
265
 
      --       -> (eqX : datoidRel a x1 x2) -> (eqB : datoidRel (Bag a) b1 b2)
266
 
      --       -> i x1 b1 p1 =^= i x2 b2 p2
267
 
      --      )
268
 
      --   -> (b1 b2 : El (Bag a))
269
 
      --   -> datoidRel (Bag a) b1 b2
270
 
      --   -> bagElim P r e i b1 =^= bagElim P r e i b2