module Homework1 where

{-
Problem 1: 
==========
Define boolean disjunction and implication

_||_ : Bool → Bool → Bool
_⊃_ : Bool → Bool → Bool

by pattern matching and refinement, using ^C^C, ^C^R, and ^C^SPC.

Compute some instances using ^C^N!

Show more uses of basic commands.

Problem 2:
==========
(a) Define the functions

equal : Nat → Nat → Bool
iseven : Nat → Bool

with obvious meanings.

Compute the result for some instances by normalizing with ^C^N.

(b) In the lecture we defined the functions

_+_ : Nat → Nat → Nat
_*_ : Nat → Nat → Nat

As we showed in the lecture Agda's normalization ^C^N is more general than the usual evaluator of a functional language. You can do "partial evaluation" or "program specialization" by simplifying functions which are only applied on some of its arguments. Show how the following expressions are simplified by ^C^N:

λ n → n + 0
λ n → n + 1
λ n → 0 + n
λ n → 1 + n
λ n → n * 0
λ n → n * 1
λ n → 0 * n
λ n → 1 * n

Explain your results.

Problem 3: 
==========
Define the Maybe type in Agda and the function

tail : {A : Set} → List A -> Maybe (List A)

So that tail of the empty list returns "Nothing".

Problem 4:
==========
(a) Define Haskell's zipwith which takes a binary function and two lists as inputs and outputs the list obtained by applying the function . The type of this function is

zipwith : {A B C : Set} -> (A -> B -> C) -> List A -> List B -> List C

Hint: zipwith is a generalization of ordinary zip where C = A × B and the function with type (A -> B -> C) is the pairing function.

(b) Then define it instead as a function on vectors expressing that the two input vectors (and also the output vector) should have the same length:

zipwith : {A B C : Set} → {n : Nat} → (A → B → C) → Vect A n → Vect B n → Vect C n

(c) Show how to implement ordinary zip on vectors, which returns a vector of pairs, as an instance of zipwith.

Problem 5
=========
(a) Define the iteratation combinator

iterate : {A : Set} -> Nat -> (A -> A) -> A -> A

such that

iterate n f a = f (f ... (f a) ...)

applies the function f n times on a. 

(b) We call iterate n the Church numeral for n. 
Church numerals are used for representing natural numbers in the untyped lambda calculus, where natural numbers are not primitives.

Your task is now to define a function 

idNat : Nat -> Nat
idNat n = iterate n ? ?

by filling the holes (marked by ?) so that idNat n is equal to n for
every concrete natural number n.
-}