blob: 15e04d7d73b99b9e30e30b42a0a15c737b756a56 (
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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
module background where
import Level
module Core where
data Exists (A : Set) (B : A -> Set) : Set where
_,_ : (x : A) -> B x -> Exists A B
fst : forall {A B} -> Exists A B -> A
fst (x , _) = x
snd : forall {A B} -> (s : Exists A B) -> B (fst s)
snd (_ , x) = x
data Bot : Set where
absurd : {A : Set} -> Bot -> A
absurd ()
data Top : Set where
<> : Top
data Bool : Set where
true : Bool
false : Bool
if_/_then_else_ : forall {a} (x : Bool) ->
(P : Bool -> Set a) -> P true -> P false -> P x
if true / _ then x else _ = x
if false / _ then _ else x = x
if_then_else_ : forall {a} {P : Bool -> Set a} ->
(x : Bool) -> P true -> P false -> P x
if true then x else _ = x
if false then _ else y = y
data W (A : Set) (B : A -> Set) : Set where
_<!_ : (a : A) -> (B a -> W A B) -> W A B
-- Ugh! Comments and definiton stolen from
-- <http://www.e-pig.org/epilogue/?p=324>
rec : forall {S P}
(C : W S P -> Set) -> -- some conclusion we hope holds
((s : S) -> -- given a shape...
(f : P s -> W S P) -> -- ...and a bunch of kids…
((p : P s) -> C (f p)) -> -- ...and C for each kid in the bunch…
C (s <! f)) -> -- ...does C hold for the node?
(x : W S P) -> -- If so, ...
C x -- ...C always holds.
rec C c (s <! f) = c s f (\ p -> rec C c (f p))
_\/_ : (A B : Set) -> Set
A \/ B = Exists Bool (\ b -> if b then A else B)
inl : forall {A B} -> A -> A \/ B
inl x = true , x
inr : forall {A B} -> B -> A \/ B
inr x = false , x
case : {A B C : Set} -> A \/ B -> (A -> C) -> (B -> C) -> C
case {A} {B} {C} x f g =
(if (fst x) / (\ b -> (if b then A else B) -> C) then f else g)
(snd x)
Tr : Bool -> Set
Tr b = if b then Top else Bot
Nat : Set
Nat = W Bool Tr
zero : Nat
zero = false <! absurd
suc : Nat -> Nat
suc n = true <! \ _ -> n
plus : Nat -> Nat -> Nat
plus x y =
rec (\ _ -> Nat)
(\ b -> if b / (\ b -> (Tr b -> Nat) -> (Tr b -> Nat) -> Nat)
then (\ _ f -> suc (f <>)) else (\ _ _ -> y)) x
data _==_ {A : Set} : A -> A -> Set where
refl : {x : A} -> x == x
subst : forall {A x y} -> (x == y) -> (T : A -> Set) -> T x -> T y
subst refl T t = t
_/==_ : forall {A} -> A -> A -> Set
x /== y = x == y -> Bot
module Ext where
data List (A : Set) : Set where
nil : List A
_::_ : A -> List A -> List A
data Nat : Set where
zero : Nat
suc : Nat -> Nat
data Vec (A : Set) : Nat -> Set where
nil : Vec A zero
_::_ : forall {n} -> A -> Vec A n -> Vec A (suc n)
head : forall {A n} -> Vec A (suc n) -> A
head (x :: _) = x
data Fin : Nat -> Set where
fzero : forall {n} -> Fin (suc n)
fsuc : forall {n} -> Fin n -> Fin (suc n)
_!!_ : forall {A n} -> Vec A n -> Fin n -> A
(x :: _) !! fzero = x
(x :: xs) !! fsuc i = xs !! i
open Core using (_==_; refl; subst)
id : {A : Set} -> A -> A
id x = x
map : forall {A B} -> (A -> B) -> List A -> List B
map _ nil = nil
map f (x :: xs) = f x :: map f xs
cong : forall {A B} {x y : A} -> (f : A -> B) -> x == y -> f x == f y
cong f refl = refl
map-id==id : {A : Set} (xs : List A) -> map id xs == id xs
map-id==id nil = refl
map-id==id (x :: xs) = cong (_::_ x) (map-id==id xs)
_#_ : forall {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C)
f # g = \ x -> f (g x)
map-#==#-map : forall {A B C} (f : B -> C) (g : A -> B) (xs : List A) ->
map (f # g) xs == (map f # map g) xs
map-#==#-map f g nil = refl
map-#==#-map f g (x :: xs) = cong (_::_ (f (g x))) (map-#==#-map f g xs)
-- If we could have this...
postulate ext : forall {A B} {f g : A -> B} ->
((x : A) -> f x == g x) -> f == g
map-id==id' : {A : Set} -> map {A} id == id
map-id==id' = ext map-id==id
map-#==#-map' : forall {A B C} (f : B -> C) (g : A -> B) ->
map (f # g) == (map f # map g)
map-#==#-map' f g = ext (map-#==#-map f g)
|
