module X1 where

----------------------------------------------------------------------
-- Exercise 1 : Boolean conditions                                  --
----------------------------------------------------------------------

-- LIBRARY

{- We'll need some datatypes to start. -}

data Bool : Set where
  true  : Bool
  false : Bool

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

data List (X : Set) : Set where
  [] : List X
  _::_ : X -> List X -> List X

data One : Set where
  void : One

data Zero : Set where

data _*_ (S T : Set) : Set where
  _,_ : S -> T -> S * T

{- We can express knowledge of a Bool. -}

Know : Bool -> Set
Know true  = One
Know false = Zero

-- EXERCISES (those marked * are a bit more difficult)
-- Hint: you may need to split some of the definitions into
-- finer cases. (I had to write something to satisfy the parser!)
-- Hint: use of early solutions to construct later solutions
-- is often a good idea.
-- Hint: inserting other functions you think might be useful
-- (perhaps from the lectures) is often a good idea.


-- Numerical Equality

{- (1.1) Define an equality test for Nat. -}

_=N=_ : Nat -> Nat -> Bool
m =N= n = {! !}

{- (1.2) Show that your equality is reflexive. -}

reflN : (n : Nat) -> Know (n =N= n)
reflN n = {! !}

{- (1.3*) Show that your equality is substitutive.
   Hint: look at foldl from L2.agda.               -}

substN : (m n : Nat) -> Know (m =N= n) ->
         (P : Nat -> Set) -> P m -> P n
substN m n mqn P pm = {! !} 

{- (1.4) Show that your equality is symmetric. -}

symN : (m n : Nat) -> Know (m =N= n) -> Know (n =N= m)
symN m n mqn = {! !}

{- (1.5) Show that your equality is transitive. -}

transN : (l m n : Nat) ->
         Know (l =N= m) -> Know (m =N= n) -> Know (l =N= n)
transN l m n lqm mqn = {! !}


-- Association Lists

-- Let's take association lists to be lists of key-value pairs,
-- where keys are numbers.

AList : Set -> Set
AList X = List (Nat * X)

{- (1.6) Define a function which tests whether a key is defined by
   a given association list. -}

defined : {X : Set} -> Nat -> AList X -> Bool
defined k kxs = {! !}

{- (1.7*) Complete the type of and define a function to look up a value
   in an association list, given that the key is defined. -}

lookup : {X : Set}(k : Nat)(kvs : AList X) -> {! !}
lookup k kvs = {! !}