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 = {! !}