InterimReport.agda

   1 module InterimReport where
   2
   3 import Level
   4
   5 module Core where
   6   data Exists (A : Set) (B : A -> Set) : Set where
   7     _,_ : (x : A) -> B x -> Exists A B
   8
   9   fst : forall {A B} -> Exists A B -> A
  10   fst (x , _) = x
  11
  12   snd : forall {A B} -> (s : Exists A B) -> B (fst s)
  13   snd (_ , x) = x
  14
  15   data Bot : Set where
  16
  17   absurd : {A : Set} -> Bot -> A
  18   absurd ()
  19
  20   data Top : Set where
  21     <> : Top
  22
  23   data Bool : Set where
  24     true  : Bool
  25     false : Bool
  26
  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
  31
  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
  36
  37   data W (A : Set) (B : A -> Set) : Set where
  38     _<!_ : (a : A) -> (B a -> W A B) -> W A B
  39
  40   -- Ugh!  Comments and definiton stolen from
  41   -- <http://www.e-pig.org/epilogue/?p=324>
  42   rec : forall {S P}
  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))
  51
  52   _\/_ : (A B : Set) -> Set
  53   A \/ B = Exists Bool (\ b -> if b then A else B)
  54
  55   inl : forall {A B} -> A -> A \/ B
  56   inl x = true , x
  57
  58   inr : forall {A B} -> B -> A \/ B
  59   inr x = false , x
  60
  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)
  64     (snd x)
  65
  66   Tr : Bool -> Set
  67   Tr b = if b then Top else Bot
  68
  69   Nat : Set
  70   Nat = W Bool Tr
  71
  72   zero : Nat
  73   zero = false <! absurd
  74
  75   suc : Nat -> Nat
  76   suc n = true <! \ _ -> n
  77
  78   plus : Nat -> Nat -> Nat
  79   plus x y =
  80     rec (\ _ -> Nat)
  81         (\ b -> if b / (\ b -> (Tr b -> Nat) -> (Tr b -> Nat) -> Nat)
  82                 then (\ _ f -> suc (f <>)) else (\ _ _ -> y)) x
  83
  84   data _==_ {A : Set} : A -> A -> Set where
  85     refl : {x : A} -> x == x
  86
  87   subst : forall {A x y} -> (x == y) -> (T : A -> Set) -> T x -> T y
  88   subst refl T t = t
  89
  90   _/==_ : forall {A} -> A -> A -> Set
  91   x /== y = x == y -> Bot
  92
  93 module Ext where
  94   data List (A : Set) : Set where
  95     nil  : List A
  96     _::_ : A -> List A -> List A
  97
  98   data Nat : Set where
  99     zero : Nat
 100     suc  : Nat -> Nat
 101
 102   data Vec (A : Set) : Nat -> Set where
 103     nil  : Vec A zero
 104     _::_ : forall {n} -> A -> Vec A n -> Vec A (suc n)
 105
 106   head : forall {A n} -> Vec A (suc n) -> A
 107   head (x :: _) = x
 108
 109   data Fin : Nat -> Set where
 110     fzero : forall {n} -> Fin (suc n)
 111     fsuc  : forall {n} -> Fin n -> Fin (suc n)
 112
 113   _!!_ : forall {A n} -> Vec A n -> Fin n -> A
 114   (x :: _)  !! fzero  = x
 115   (x :: xs) !! fsuc i = xs !! i
 116
 117   open Core using (_==_; refl; subst)
 118
 119   id : {A : Set} -> A -> A
 120   id x = x
 121
 122   map : forall {A B} -> (A -> B) -> List A -> List B
 123   map _ nil       = nil
 124   map f (x :: xs) = f x :: map f xs
 125
 126   cong : forall {A B} {x y : A} (f : A -> B) -> x == y -> f x == f y
 127   cong f refl = refl
 128
 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)
 132
 133   _#_ : {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C)
 134   f # g = \ x -> f (g x)
 135
 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)
 140
 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
 144
 145   map-id==id' : forall {A} -> map {A} id == id
 146   map-id==id' = ext map-id==id
 147
 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)