module Homework2 where

{-
Problem 1: Define logical or and logical equivalence

_||_ : 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!

Problem 2:
(a) Define the factorial function

factorial : Nat → Nat

Compute the result of factorial for some instances by normalizing with ^C^N. How large factorials can Agda compute?

(b) Define the power function

power : Nat → Nat → Nat

such that power m n = n^m. Compute the result of power for some instances of m by normalizing with ^C^N.

Agda's normalization is more general than the usual evaluator of a functional language. You can do "partial evaluation" or "program specialization" by running power only on its first argument. Compute in this way power zero, power one, power two, etc! What are the results? Could you achieve the same effect if you swapped the order of arguments to power?

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

head : {A : Set} → List A -> Maybe A

Problem 4:
(a) Define the Haskell zip function which takes two lists as inputs and outputs the corresponding lists of pairs. The type of this function is

zip : {A B : Set} -> List A -> List B -> List (A × B)

where you get access to the product type A × B by writing

open import Product

Alternatively, if you have installed the standard library you can import products from there by writing

open import Data.Product

Note that you need to decide what to do when you zip lists of unequal length. (What does Haskell do?)

(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:

zip : {A B : Set} → {n : Nat} → Vect A n → Vect B n → Vect (A × B) n

Problem 5: Define

next : BoolExpr → Maybe BoolExpr

such that next t = Just t' iff there is proof p : t ⇒ t'
-}