# Exercise (Week 10)

## Table of Contents

**DUE**: 20 May, 2018 23:55

Download the exercise tarball and extract it to a directory in your
home directory at CSE. This tarball contains a file, called `Ex09.hs`

,
wherein you will do all of your programming.

To test your code, run the following shell commands to open a GHCi session:

```
$ 3141
newclass starting new subshell for class COMP3141...
$ cabal repl
Resolving dependencies...
Configuring Ex09-1.0...
Preprocessing executable 'Ex09' for Ex09-1.0..
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Ex09 (Ex09.hs, interpreted)
Ok, one module loaded.
*Ex09> reflexivity SZero
...
```

Note that you will only need to submit `Ex09.hs`

, so only make changes
to that file.

Download the exercise tarball and extract it to a directory on
your local machine. This tarball contains a file, called `Ex09.hs`

,
wherein you will do all of your programming.

To test your code, run the following shell commands to open a GHCi session:

```
$ stack repl
Configuring GHCi with the following packages: Ex09
Using main module: 1. Package 'Ex09' component exe:Ex09 ...
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Ex09 (Ex09.hs, interpreted)
Ok, one module loaded.
*Ex09> reflexivity SZero
...
```

Note that you will only need to submit `Ex09.hs`

, so only make changes
to that file.

Download the Haskell for Mac project and unzip it somewhere on your
local machine. Open the project in Haskell for Mac, and begin
coding in `Ex09.hs`

.

Note that you will only need to submit `Ex09.hs`

, so only make changes
to that file.

## 1 Proofs and Types

Because of the Curry-Howard correspondence, if we write a total, terminating program in Haskell, it constitutes a proof of the proposition encoded by its type.

In this exercise, we'll define natural numbers, which we will use exclusively on the type level:

data Nat = Z | S Nat

We also define some *singleton* natural numbers type `SNat`

to allow us to
examine a type-level `Nat`

on the value level:

data SNat :: Nat -> * where SZero :: SNat Z SSucc :: SNat n -> SNat (S n)

Lastly, we will define a type `LessEq a b`

that is inhabited only
when `a`

is less than or equal to `b`

:

data LessEq :: Nat -> Nat -> * where ZLEN :: LessEq Z n SLES :: LessEq n m -> LessEq (S n) (S m)

Each constructor of the `LessEq`

type corresponds to an axiom about
the standard numerical ordering:

In this exercise, we'll prove some theorems about the \(\leq\) relation by writing total, terminating Haskell programs of the corresponding type.

### 1.1 Proving Reflexivity (Part 1, 3 Marks)

First we will prove *reflexivity*, that for all \(n\), \(n \leq n\).
Normally we would prove this by doing an induction on \(n\) and proving
the obligations that arise using the rules above.
Inductive proofs correspond to (terminating) *recursion* via
the Curry-Howard correspondence. So, to prove reflexivity in Haskell,
we can write a function of the following type:

reflexivity :: SNat n -> LessEq n n

Implement this function, using recursion and by matching on the given number. If the function type-checks and returns a result for all inputs, it is a valid proof of reflexivity.

Any type-correct, total and terminating function will do – thus all our tests do is check that your function returns a result for any input.

### 1.2 Proving Transitivity (Part 2, 3 Marks)

Another theorem about natural number ordering we would like to prove
is that of *transitivity*. Rather than do induction on a number, we
must perform rule induction on the first inequality.

Once again, it suffices to implement a total, terminating function of the following type:

transitivity :: LessEq a b -> LessEq b c -> LessEq a c

### 1.3 Proving Antisymmetry (Part 3, 3 Marks)

We shall introduce a new type that is inhabited only if two indexed natural numbers are equal:

data Equal :: Nat -> Nat -> * where EqRefl :: Equal n n

Note that pattern matching on a value of type `Equal a b`

will
inform the Haskell type checker that `a`

and `b`

are the same type.

Using this definition, prove *antisymmetry* of the \(\leq\) operator.

antisymmetry :: LessEq a b -> LessEq b a -> Equal a b antisymmetry _ _ = error "'antisymmetry' unimplemented"

*Hint*: use a `case`

statement to pattern match on the result of the recursion,
introducing the type equality to the GHC type checker.

## 2 Submission instructions

$ give cs3141 Ex09 Ex09.hs

on a CSE terminal, or by using the `give`

web interface. Your file *must* be named `Ex09.hs`

(case-sensitive!).
A dry-run test will autotest your solution at submission time.