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