1 module InterimReport where
6 data Exists (A : Set) (B : A -> Set) : Set where
7 _,_ : (x : A) -> B x -> Exists A B
9 fst : forall {A B} -> Exists A B -> A
12 snd : forall {A B} -> (s : Exists A B) -> B (fst s)
17 absurd : {A : Set} -> Bot -> A
27 if_/_then_else_ : forall {a} (x : Bool) ->
28 (P : Bool -> Set a) -> P true -> P false -> P x
29 if true / _ then x else _ = x
30 if false / _ then _ else x = x
32 if_then_else_ : forall {a} {P : Bool -> Set a}
33 (x : Bool) -> P true -> P false -> P x
34 if true then x else _ = x
35 if false then _ else y = y
37 data W (A : Set) (B : A -> Set) : Set where
38 _<!_ : (a : A) -> (B a -> W A B) -> W A B
40 -- Ugh! Comments and definiton stolen from
41 -- <http://www.e-pig.org/epilogue/?p=324>
43 (C : W S P -> Set) -> -- some conclusion we hope holds
44 ((s : S) -> -- given a shape...
45 (f : P s -> W S P) -> -- ...and a bunch of kids…
46 ((p : P s) -> C (f p)) -> -- ...and C for each kid in the bunch…
47 C (s <! f)) -> -- ...does C hold for the node?
48 (x : W S P) -> -- If so, ...
49 C x -- ...C always holds.
50 rec C c (s <! f) = c s f (\ p -> rec C c (f p))
52 _\/_ : (A B : Set) -> Set
53 A \/ B = Exists Bool (\ b -> if b then A else B)
55 inl : forall {A B} -> A -> A \/ B
58 inr : forall {A B} -> B -> A \/ B
61 case : {A B C : Set} -> A \/ B -> (A -> C) -> (B -> C) -> C
62 case {A} {B} {C} x f g =
63 (if (fst x) / (\ b -> (if b then A else B) -> C) then f else g)
67 Tr b = if b then Top else Bot
73 zero = false <! absurd
76 suc n = true <! \ _ -> n
78 plus : Nat -> Nat -> Nat
81 (\ b -> if b / (\ b -> (Tr b -> Nat) -> (Tr b -> Nat) -> Nat)
82 then (\ _ f -> suc (f <>)) else (\ _ _ -> y)) x
84 data _==_ {A : Set} : A -> A -> Set where
85 refl : {x : A} -> x == x
87 subst : forall {A x y} -> (x == y) -> (T : A -> Set) -> T x -> T y
90 _/==_ : forall {A} -> A -> A -> Set
91 x /== y = x == y -> Bot
94 data List (A : Set) : Set where
96 _::_ : A -> List A -> List A
102 data Vec (A : Set) : Nat -> Set where
104 _::_ : forall {n} -> A -> Vec A n -> Vec A (suc n)
106 head : forall {A n} -> Vec A (suc n) -> A
109 data Fin : Nat -> Set where
110 fzero : forall {n} -> Fin (suc n)
111 fsuc : forall {n} -> Fin n -> Fin (suc n)
113 _!!_ : forall {A n} -> Vec A n -> Fin n -> A
114 (x :: _) !! fzero = x
115 (x :: xs) !! fsuc i = xs !! i
117 open Core using (_==_; refl; subst)
119 id : {A : Set} -> A -> A
122 map : forall {A B} -> (A -> B) -> List A -> List B
124 map f (x :: xs) = f x :: map f xs
126 cong : forall {A B} {x y : A} (f : A -> B) -> x == y -> f x == f y
129 map-id==id : {A : Set} (xs : List A) -> map id xs == id xs
130 map-id==id nil = refl
131 map-id==id (x :: xs) = cong (_::_ x) (map-id==id xs)
133 _#_ : {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C)
134 f # g = \ x -> f (g x)
136 map-#==#-map : forall {A B C} (f : B -> C) (g : A -> B) (xs : List A) ->
137 map (f # g) xs == (map f # map g) xs
138 map-#==#-map f g nil = refl
139 map-#==#-map f g (x :: xs) = cong (_::_ (f (g x))) (map-#==#-map f g xs)
141 -- If we could have this...
142 postulate ext : forall {A B} {f g : A -> B} ->
143 ((x : A) -> f x == g x) -> f == g
145 map-id==id' : forall {A} -> map {A} id == id
146 map-id==id' = ext map-id==id
148 map-#==#-map' : forall {A B C} (f : B -> C) (g : A -> B) ->
149 map (f # g) == (map f # map g)
150 map-#==#-map' f g = ext (map-#==#-map f g)