← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/AIM5/yoshiki/SET.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/AIM5/yoshiki/SET.agda
1
 
-------------------------------------------------------------------------------
2
 
 
3
 
--
4
 
--
5
 
module SET where
6
 
  ----------------------------------------------------------------------------
7
 
  -- Auxiliary.
8
 
  ----------------------------------------------------------------------------
9
 
  -- no : (x : A) -> B : Set  if A : Set B : Set
10
 
  -- yes : (x : A) -> B type   if A type  B type
11
 
  -- El M type   if  M : Set
12
 
 
13
 
  data Unop (A : Set) : Set1 where
14
 
    unopI : (A -> A) -> Unop A
15
 
  data Pred (A : Set) : Set1 where
16
 
    PredI : (A -> Set) -> Pred A
17
 
  data Rel (A : Set) : Set1 where
18
 
    RelI : (A -> A -> Set) -> Rel A
19
 
  data Reflexive {A : Set} (R : A -> A -> Set) : Set where
20
 
    reflexiveI : ((a : A) -> R a a) -> Reflexive R
21
 
  data Symmetrical {A : Set} (R : A -> A -> Set) : Set where
22
 
    symmetricalI : ({a b : A} -> R a b -> R a b) -> Symmetrical R
23
 
  data Transitive {A : Set} (R : A -> A -> Set) : Set where
24
 
    transitiveI : ({a b c : A} -> R a b -> R b c -> R a c) -> Transitive R
25
 
  compositionalI : 
26
 
    {A : Set} -> (R : A -> A -> Set)
27
 
    -> ({a b c : A} -> R b c -> R a b -> R a c) -> Transitive R
28
 
  compositionalI {A} R f =
29
 
    transitiveI (\{a b c : A} -> \(x : R a b) -> \(y : R b c) -> f y x)
30
 
  data Substitutive {A : Set} (R : A -> A -> Set) : Set1 where
31
 
    substitutiveI : ((P : A -> Set) -> {a b : A} -> R a b -> P a -> P b)
32
 
                   -> Substitutive R
33
 
  data Collapsed (A : Set) : Set1 where
34
 
    collapsedI : ((P : A -> Set) -> {a b : A} -> P a -> P b) -> Collapsed A
35
 
 
36
 
  cmp : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
37
 
  cmp f g a = f (g a)
38
 
  seq : {A B C : Set} -> (A -> B) -> (B -> C) -> A -> C
39
 
  seq f g = cmp g f
40
 
 
41
 
  S : {A B C : Set} -> (C -> B -> A) -> (C -> B) -> C -> A
42
 
  S x y z = x z (y z)
43
 
  K : {A B : Set} -> A -> B -> A
44
 
  K x y = x
45
 
  I : {A : Set} -> A -> A
46
 
  I a = a
47
 
  -- of course I = S K K
48
 
 
49
 
  id = \{A : Set} -> I {A}
50
 
 
51
 
  const = \{A B : Set} -> K {A}{B}
52
 
 
53
 
  -- Set version
54
 
  pS : {P Q R : Set} -> (R -> Q -> P) -> (R -> Q) -> R -> P
55
 
  pS x y z = x z (y z)
56
 
  pK : {P Q : Set} -> P -> Q -> P
57
 
  pK x y = x
58
 
  pI : {P : Set} -> P -> P
59
 
  pI a = a
60
 
 
61
 
  proj : {A : Set} -> (B : A -> Set) -> (a : A) -> (f : (aa : A) -> B aa) -> B a
62
 
  proj B a f = f a
63
 
 
64
 
  flip : {A B C : Set} (f : A -> B -> C) (b : B) (a : A) -> C
65
 
  flip f b a = f a b
66
 
 
67
 
  -- separate definition of FlipRel is necessary because it is not the case
68
 
  -- that Set : Set.
69
 
  FlipRel : {A : Set} -> (R : A -> A -> Set) -> (a b : A) -> Set
70
 
  FlipRel R a b = R b a
71
 
 
72
 
  ----------------------------------------------------------------------------
73
 
  -- Product sets.
74
 
  ----------------------------------------------------------------------------
75
 
  data Prod (A : Set) (B : A -> Set) : Set where
76
 
    prodI : ((a : A) -> B a) -> Prod A B
77
 
  mapProd : {A : Set} -> {B C : A -> Set} -> ((a : A) -> B a -> C a)
78
 
           -> Prod A B -> Prod A C
79
 
  mapProd {A} f (prodI g) = prodI (\(a : A) -> f a (g a))
80
 
 
81
 
  Fun : Set -> Set -> Set
82
 
  Fun A B = Prod A (\(_ : A) -> B)
83
 
 
84
 
  mapFun : {A B C D : Set} -> (B -> A) -> (C -> D) -> (A -> C) -> B -> D
85
 
  mapFun {A} {B} {C} {D} f g h x = g (h (f x))
86
 
 
87
 
 
88
 
---------------------------------------------------------------------------
89
 
---------------------------------------------------------------------------
90
 
--
91
 
--
92
 
--
93
 
--
94
 
--
95
 
--
96
 
--
97
 
 
98
 
  ----------------------------------------------------------------------------
99
 
  -- The empty set.
100
 
  ----------------------------------------------------------------------------
101
 
  data Zero : Set where
102
 
--
103
 
--
104
 
----------------------------------------------------------------------------
105
 
----------------------------------------------------------------------------
106
 
  data Unit : Set where
107
 
    uu : Unit
108
 
  elUnit = uu
109
 
  elimUnit : (C : Unit -> Set) -> C uu -> (u : Unit) -> C u
110
 
  elimUnit C c uu = c
111
 
---------------------------------------------------------------------------
112
 
---------------------------------------------------------------------------
113
 
 
114
 
  data Succ (A : Set) : Set where
115
 
    zerS : Succ A
116
 
    sucS : A -> Succ A
117
 
  zerSucc = \{A : Set} -> zerS {A}
118
 
  sucSucc = \{A : Set} -> sucS {A}
119
 
  elimSucc : {X : Set} -> (C : Succ X -> Set)
120
 
            -> C zerS -> ((x : X) -> C (sucS x)) -> (xx : Succ X) -> (C xx)
121
 
  elimSucc C c_z c_s zerS = c_z
122
 
  elimSucc C c_z c_s (sucS x) = c_s x
123
 
  whenSucc : {X Y : Set} -> Y -> (X -> Y) -> (Succ X) -> Y
124
 
  whenSucc y_z y_s zerS = y_z
125
 
  whenSucc y_z y_s (sucS x) = y_s x
126
 
  mapSucc : {X Y : Set} -> (X -> Y) -> Succ X -> Succ Y
127
 
  mapSucc {X} {_} f
128
 
    = whenSucc zerS (\(x : X) -> sucS (f x))
129
 
 
130
 
---------------------------------------------------------------------------
131
 
---------------------------------------------------------------------------
132
 
 
133
 
  data Plus (A B : Set) : Set where
134
 
    inl : A -> Plus A B
135
 
    inr : B -> Plus A B
136
 
  elimPlus : {X Y : Set} ->
137
 
            (C : Plus X Y -> Set) ->
138
 
            ((x : X) -> C (inl x)) ->
139
 
            ((y : Y) -> C (inr y)) ->
140
 
            (z : Plus X Y) ->
141
 
            C z
142
 
  elimPlus {X} {Y} C c_lft c_rgt (inl x) = c_lft x
143
 
  elimPlus {X} {Y} C c_lft c_rgt (inr x) = c_rgt x
144
 
  when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> Plus X Y -> Z
145
 
  when {X} {Y} {Z} f g (inl x) = f x
146
 
  when {X} {Y} {Z} f g (inr y) = g y
147
 
  whenplus : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> Plus X Y -> Z
148
 
  whenplus = when
149
 
  mapPlus : {X1 X2 Y1 Y2 : Set} -> (X1 -> X2) -> (Y1 -> Y2)
150
 
           -> Plus X1 Y1 -> Plus X2 Y2
151
 
  mapPlus f g = when (\x1 -> inl (f x1)) (\y1 -> inr (g y1))
152
 
  swapPlus : {X Y : Set} -> Plus X Y -> Plus Y X
153
 
  swapPlus = when inr inl
154
 
 
155
 
----------------------------------------------------------------------------
156
 
----------------------------------------------------------------------------
157
 
 
158
 
  data Sum (A : Set) (B : A -> Set) : Set where
159
 
    sumI : (fst : A) -> B fst -> Sum A B
160
 
  depPair : {A : Set} -> {B : A -> Set} -> (a : A) -> B a -> Sum A B
161
 
  depPair a b = sumI a b
162
 
  depFst : {A : Set} -> {B : A -> Set} -> (c : Sum A B) -> A
163
 
  depFst (sumI fst snd) = fst
164
 
  depSnd : {A : Set} -> {B : A -> Set} -> (c : Sum A B) -> B (depFst c)
165
 
  depSnd (sumI fst snd) = snd
166
 
  depCur : {A : Set} -> {B : A -> Set} -> {C : Set} -> (f : Sum A B -> C)
167
 
           -> (a : A) -> B a -> C
168
 
  depCur f = \a -> \b -> f (depPair a b)
169
 
  -- the above works but the below does not---why?
170
 
  -- depCur : {X : Set} -> {Y : X -> Set} -> {Z : Set} -> (f : Sum X Y -> Z)
171
 
  --         -> {x : X} -> Y x -> Z
172
 
  -- depCur {X} {Y} {Z} f = \{x} -> \y ->  f (depPair  x  y)
173
 
  -- Error message : 
174
 
  -- When checking that the expression \{x} -> \y -> f (depPair x y)
175
 
  -- has type Y _x -> Z
176
 
  -- found an implicit lambda where an explicit lambda was expected
177
 
  depUncur : {A : Set} -> {B : A -> Set} -> {C : Set}
178
 
    -> ((a : A) -> B a -> C) -> Sum A B -> C
179
 
  depUncur f ab = f (depFst ab) (depSnd ab)
180
 
  depCurry : {A : Set} ->
181
 
             {B : A -> Set} ->
182
 
             {C : Sum A B -> Set} ->
183
 
             (f : (ab : Sum A B) -> C ab) ->
184
 
             (a : A) ->
185
 
             (b : B a) ->
186
 
             C (depPair a b)
187
 
  depCurry f a b = f (depPair a b)
188
 
  depUncurry : {A : Set} ->
189
 
               {B : A -> Set} ->
190
 
               {C : Sum A B -> Set} ->
191
 
               (f : (a : A) -> (b : B a) -> C (depPair a b)) ->
192
 
               (ab : Sum A B) ->
193
 
               C ab
194
 
  depUncurry f (sumI fst snd) = f fst snd
195
 
  mapSum : {A : Set} -> {B1 : A -> Set} -> {B2 : A -> Set}
196
 
          -> (f : (a : A) -> B1 a -> B2 a)
197
 
          -> Sum A B1 -> Sum A B2
198
 
  mapSum f (sumI fst snd) = depPair fst (f fst snd)
199
 
  elimSum = \{A : Set}{B : A -> Set}{C : Sum A B -> Set} -> depUncurry{A}{B}{C}
200
 
---------------------------------------------------------------------------
201
 
---------------------------------------------------------------------------
202
 
  Times : Set -> Set -> Set
203
 
  Times A B = Sum A (\(_ : A) -> B)
204
 
  pair : {A : Set} -> {B : Set} -> A -> B -> Times A B
205
 
  pair a b = sumI a b
206
 
  fst : {A : Set} -> {B : Set} -> Times A B -> A
207
 
  fst (sumI a _) = a
208
 
  snd : {A : Set} -> {B : Set} -> Times A B -> B
209
 
  snd (sumI _ b) = b
210
 
  pairfun : {C : Set} -> {A : Set} -> {B : Set}
211
 
           -> (C -> A) -> (C -> B) -> C -> Times A B
212
 
  pairfun f g c = pair (f c) (g c)
213
 
  mapTimes : {A1 : Set} -> {A2 : Set} -> {B1 : Set} -> {B2 : Set}
214
 
            -> (A1 -> A2) -> (B1 -> B2) -> Times A1 B1 -> Times A2 B2
215
 
  mapTimes f g (sumI a b) = pair (f a) (g b)
216
 
  swapTimes : {A : Set} -> {B : Set} -> Times A B -> Times B A
217
 
  swapTimes (sumI a b) = sumI b a
218
 
  cur : {A : Set} -> {B : Set} -> {C : Set} -> (f : Times A B -> C) -> A -> B -> C
219
 
  cur f a b = f (pair a b)
220
 
  uncur : {A : Set} -> {B : Set} -> {C : Set} -> (A -> B -> C) -> Times A B -> C
221
 
  uncur f (sumI a b) = f a b
222
 
  curry : {A : Set} -> {B : Set} -> {C : Times A B -> Set}
223
 
         -> ((p : Times A B) -> C p) -> (a : A) ->(b : B) -> C (pair a b)
224
 
  curry f a b = f (pair a b)
225
 
  uncurry : {A : Set} -> {B : Set} -> {C : Times A B -> Set}
226
 
           -> ((a : A) -> (b : B) -> C (pair a b)) -> (p : Times A B) -> C p
227
 
  uncurry f (sumI a b) = f a b
228
 
  elimTimes = \{A B : Set}{C : Times A B -> Set} -> uncurry{A}{B}{C}
229
 
  ---------------------------------------------------------------------------
230
 
  -- Natural numbers.
231
 
  ---------------------------------------------------------------------------
232
 
  data Nat : Set where
233
 
    zero : Nat
234
 
    succ : Nat -> Nat
235
 
  elimNat : (C : Nat -> Set)
236
 
           -> (C zero) -> ((m : Nat) -> C m -> C (succ m)) -> (n : Nat) -> C n
237
 
  elimNat C c_z c_s zero = c_z
238
 
  elimNat C c_z c_s (succ m') = c_s m' (elimNat C c_z c_s m')
239
 
 
240
 
  ----------------------------------------------------------------------------
241
 
  -- Linear universe of finite sets.
242
 
  ----------------------------------------------------------------------------
243
 
  Fin : (m : Nat) -> Set
244
 
  Fin zero = Zero
245
 
  Fin (succ n) = Succ (Fin n)
246
 
{-
247
 
  Fin 0 = {}
248
 
  Fin 1 = { zerS }
249
 
  Fin 2 = { zerS (sucS zerS) }
250
 
  Fin 3 = { zerS (sucS zerS) (sucS (sucS zerS)) }
251
 
-}
252
 
  valFin : (n' : Nat) -> Fin n' -> Nat
253
 
  valFin zero     ()
254
 
  valFin (succ n) zerS = zero
255
 
  valFin (succ n) (sucS x) = succ (valFin n x)
256
 
  zeroFin : (n : Nat) -> Fin (succ n)
257
 
  zeroFin n = zerS
258
 
  succFin : (n : Nat) -> Fin n -> Fin (succ n)
259
 
  succFin n N = sucS N
260
 
  ----------------------------------------------------------------------------
261
 
  -- Do these really belong here?
262
 
  ----------------------------------------------------------------------------
263
 
  HEAD : {A : Set} -> (n : Nat) -> (Fin (succ n) -> A) -> A
264
 
  HEAD n f = f (zeroFin n)
265
 
  TAIL : {A : Set} -> (n : Nat) -> (Fin (succ n) -> A) -> Fin n -> A
266
 
  TAIL n f N = f (succFin n N)
267
 
  ----------------------------------------------------------------------------
268
 
  -- Lists.
269
 
  ----------------------------------------------------------------------------
270
 
  data List (A : Set) : Set where
271
 
    nil : List A
272
 
    con : A -> List A -> List A
273
 
  elimList : {A : Set} ->
274
 
            (C : List A -> Set) ->
275
 
            (C nil) ->
276
 
            ((a : A) -> (as : List A) -> C as -> C (con a as)) ->
277
 
            (as : List A) ->
278
 
            C as
279
 
  elimList _ c_nil _ nil = c_nil
280
 
  elimList C c_nil c_con (con a as) = c_con a as (elimList C c_nil c_con as)
281
 
  ----------------------------------------------------------------------------
282
 
  -- Tuples are "dependently typed vectors".
283
 
  ----------------------------------------------------------------------------
284
 
  data Nill : Set where
285
 
    nill : Nill
286
 
  data Cons (A B : Set) : Set where
287
 
    cons : A -> B -> Cons A B
288
 
  Tuple : (n : Nat) -> (C : Fin n -> Set) -> Set
289
 
  Tuple zero = \ C -> Nill
290
 
  Tuple (succ n) = \ C -> Cons (C zerS) (Tuple n (\(N : Fin n) -> C (sucS N)))
291
 
  ----------------------------------------------------------------------------
292
 
  -- Vectors homogeneously typed tuples.
293
 
  ----------------------------------------------------------------------------
294
 
  Vec : Set -> Nat -> Set
295
 
  Vec A m = Tuple m (\(n : Fin m) -> A)
296
 
  ----------------------------------------------------------------------------
297
 
  -- Monoidal expressions.
298
 
  ----------------------------------------------------------------------------
299
 
  data Mon (A : Set) : Set where
300
 
    unit : Mon A
301
 
    at : A -> Mon A
302
 
    mul : Mon A -> Mon A -> Mon A
303
 
{-
304
 
-}
305
 
 
306
 
----------------------------------------------------------------------------
307
 
----------------------------------------------------------------------------
308
 
  data Implies (A B : Set) : Set where
309
 
    impliesI : (A -> B) -> Implies A B
310
 
  data Absurd : Set where
311
 
  data Taut : Set where
312
 
    tt : Taut
313
 
  data Not (P : Set) : Set where
314
 
    notI : (P -> Absurd) -> Not P
315
 
  -- encoding of Exists is unsatisfactory!  Its type should be Set.
316
 
  data Exists (A : Set) (P : A -> Set) : Set where
317
 
    existsI : (evidence : A) -> P evidence -> Exists A P
318
 
  data Forall (A : Set) (P : A -> Set) : Set where
319
 
    forallI : ((a : A) -> P a) -> Forall A P
320
 
  data And (A B : Set) : Set where
321
 
    andI : A -> B -> And A B
322
 
  Iff : Set -> Set -> Set
323
 
  Iff A B = And (Implies A B) (Implies B A)
324
 
  data Or (A B : Set) : Set where
325
 
    orIl : (a : A) -> Or A B
326
 
    orIr : (b : B) -> Or A B
327
 
  Decidable : Set -> Set
328
 
  Decidable P = Or P (Implies P Absurd)
329
 
  data DecidablePred {A : Set} (P : A -> Set) : Set where
330
 
   decidablepredIl : (a : A) -> (P a) -> DecidablePred P
331
 
   decidablepredIr : (a : A) -> (Implies (P a) Absurd) -> DecidablePred P
332
 
  data DecidableRel {A : Set} (R : A -> A -> Set) : Set where
333
 
   decidablerelIl : (a b : A) -> (R a b) -> DecidableRel R
334
 
   decidablerelIr : (a b : A) -> (Implies (R a b) Absurd) -> DecidableRel R
335
 
  data Least {A : Set} (_<=_ : A -> A -> Set) (P : A -> Set) (a : A) : Set where
336
 
    leastI : (P a) -> ((aa : A) -> P aa -> (a <= aa)) -> Least _<=_ P a
337
 
  data Greatest {A : Set} (_<=_ : A -> A -> Set) (P : A -> Set) (a : A) : Set where
338
 
    greatestI : (P a) -> ((aa : A) -> P aa -> (aa <= a)) -> Greatest _<=_ P a
339
 
 
340
 
----------------------------------------------------------------------------
341
 
----------------------------------------------------------------------------
342
 
  data Bool : Set where
343
 
    true : Bool
344
 
    false : Bool
345
 
  elimBool : (C : Bool -> Set) -> C true -> C false -> (b : Bool) -> C b
346
 
  elimBool C c_t c_f true = c_t
347
 
  elimBool C c_t c_f false = c_f
348
 
  whenBool : (C : Set) -> C -> C -> Bool -> C
349
 
  whenBool C c_t c_f b = elimBool (\(_ : Bool) -> C) c_t c_f b
350
 
  data pred (A : Set) : Set where
351
 
    predI : (A -> Bool) -> pred A
352
 
  data rel (A : Set) : Set where
353
 
    relI : (A -> A -> Bool) -> rel A
354
 
  True : Bool -> Set
355
 
  True true = Taut
356
 
  True false = Absurd
357
 
  bool2set = True
358
 
  pred2Pred : {A : Set} -> pred A -> Pred A
359
 
  pred2Pred (predI p) = PredI (\a -> True (p a))
360
 
  rel2Rel : {A : Set} -> rel A -> Rel A
361
 
  rel2Rel (relI r) = RelI (\a -> \b -> True (r a b))
362
 
{-
363
 
  abstract dec_lem (|P :: Set)(decP :: Decidable P)
364
 
    :: Exist |_ (\(b :: Bool) -> Iff (True b) P)
365
 
    = case decP of {
366
 
        (inl trueP) ->
367
 
          struct {
368
 
            fst = true@_;
369
 
            snd =
370
 
              struct {
371
 
                fst = const |_  |_ trueP;  -- (True true@_)
372
 
                snd = const |_ |_  tt;};};
373
 
        (inr notP) ->
374
 
          struct {
375
 
            fst = false@_;
376
 
            snd =
377
 
              struct {
378
 
                fst = whenZero P;
379
 
                snd = notP;};};}
380
 
  dec2bool :: (P :: Set) |-> (decP :: Decidable P) -> Bool
381
 
    = \(P :: Set) |-> \(decP :: Decidable P) -> (dec_lem |_ decP).fst
382
 
  dec2bool_spec (|P :: Set)(decP :: Decidable P)
383
 
    :: Iff (True (dec2bool |_ decP)) P
384
 
    = (dec_lem |_ decP).snd
385
 
 
386
 
  abstract collTrue :: (b :: Bool) -> Collapsed (True b)
387
 
    = let aux (X :: Set)(C :: X -> Set)
388
 
            :: (b :: Bool) ->
389
 
               (f :: True b -> X) ->
390
 
               (t1 :: True b) |->
391
 
               (t2 :: True b) |->
392
 
               C (f t1) -> C (f t2)
393
 
            = \(b :: Bool) ->
394
 
              case b of {
395
 
                (true) ->
396
 
                  \(f :: (x :: True true@_) -> X) ->
397
 
                  \(t1 t2 :: True true@_) |->
398
 
                  \(c :: C (f t1)) ->
399
 
                  case t1 of { (tt) -> case t2 of { (tt) -> c;};};
400
 
                (false) ->
401
 
                  \(f :: (x :: True false@_) -> X) ->
402
 
                  \(t1 t2 :: True false@_) |->
403
 
                  \(c :: C (f t1)) ->
404
 
                  case t1 of { };}
405
 
      in   \(b :: Bool) ->  \(P :: True b -> Set) -> aux (True b) P b id
406
 
 
407
 
  bool2nat (p :: Bool) :: Nat
408
 
    = case p of {
409
 
        (true) -> succ zero;
410
 
        (false) -> zero;}
411
 
-}
412