# Assignment1: TSPL Assignment 1

module Assignment1 where

## YOUR NAME AND EMAIL GOES HERE

## Introduction

You must do *all* the exercises labelled “(recommended)”.

Exercises labelled “(stretch)” are there to provide an extra challenge. You don’t need to do all of these, but should attempt at least a few.

Exercises without a label are optional, and may be done if you want some extra practice.

Please ensure your files execute correctly under Agda!

## Imports

import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym) open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎) open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s) open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm; ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤) open import plfa.part1.Relations using (_<_; z<s; s<s; zero; suc; even; odd)

## Naturals

#### Exercise `seven`

Write out `7`

in longhand.

#### Exercise `+-example`

Compute `3 + 4`

, writing out your reasoning as a chain of equations.

#### Exercise `*-example`

Compute `3 * 4`

, writing out your reasoning as a chain of equations.

#### Exercise `_^_`

(recommended)

Define exponentiation, which is given by the following equations.

```
n ^ 0 = 1
n ^ (1 + m) = n * (n ^ m)
```

Check that `3 ^ 4`

is `81`

.

#### Exercise `∸-examples`

(recommended)

Compute `5 ∸ 3`

and `3 ∸ 5`

, writing out your reasoning as a chain of equations.

#### Exercise `Bin`

(stretch)

A more efficient representation of natural numbers uses a binary rather than a unary system. We represent a number as a bitstring.

data Bin : Set where nil : Bin x0_ : Bin → Bin x1_ : Bin → Bin

For instance, the bitstring

```
1011
```

standing for the number eleven is encoded, right to left, as

```
x1 x1 x0 x1 nil
```

Representations are not unique due to leading zeros.
Hence, eleven is also represented by `001011`

, encoded as

```
x1 x1 x0 x1 x0 x0 nil
```

Define a function

```
inc : Bin → Bin
```

that converts a bitstring to the bitstring for the next higher
number. For example, since `1100`

encodes twelve, we should have

```
inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
```

Confirm that this gives the correct answer for the bitstrings encoding zero through four.

Using the above, define a pair of functions to convert between the two representations.

```
to : ℕ → Bin
from : Bin → ℕ
```

For the former, choose the bitstring to have no leading zeros if it
represents a positive natural, and represent zero by `x0 nil`

.
Confirm that these both give the correct answer for zero through four.

## Induction

#### Exercise `operators`

Give another example of a pair of operators that have an identity and are associative, commutative, and distribute over one another.

Give an example of an operator that has an identity and is associative but is not commutative.

#### Exercise `finite-+-assoc`

(stretch)

Write out what is known about associativity of addition on each of the first four days using a finite story of creation, as [earlier][plfa.Naturals#finite-creation]

#### Exercise `+-swap`

(recommended)

Show

```
m + (n + p) ≡ n + (m + p)
```

for all naturals `m`

, `n`

, and `p`

. No induction is needed,
just apply the previous results which show addition
is associative and commutative. You may need to use
the following function from the standard library:

```
sym : ∀ {m n : ℕ} → m ≡ n → n ≡ m
```

#### Exercise `*-distrib-+`

(recommended)

Show multiplication distributes over addition, that is,

```
(m + n) * p ≡ m * p + n * p
```

for all naturals `m`

, `n`

, and `p`

.

#### Exercise `*-assoc`

(recommended)

Show multiplication is associative, that is,

```
(m * n) * p ≡ m * (n * p)
```

for all naturals `m`

, `n`

, and `p`

.

#### Exercise `*-comm`

Show multiplication is commutative, that is,

```
m * n ≡ n * m
```

for all naturals `m`

and `n`

. As with commutativity of addition,
you will need to formulate and prove suitable lemmas.

#### Exercise `0∸n≡0`

Show

```
zero ∸ n ≡ zero
```

for all naturals `n`

. Did your proof require induction?

#### Exercise `∸-+-assoc`

Show that monus associates with addition, that is,

```
m ∸ n ∸ p ≡ m ∸ (n + p)
```

for all naturals `m`

, `n`

, and `p`

.

#### Exercise `Bin-laws`

(stretch)

Recall that
Exercise [Bin][plfa.Naturals#Bin]
defines a datatype `Bin`

of bitstrings representing natural numbers
and asks you to define functions

```
inc : Bin → Bin
to : ℕ → Bin
from : Bin → ℕ
```

Consider the following laws, where `n`

ranges over naturals and `x`

over bitstrings.

```
from (inc x) ≡ suc (from x)
to (from n) ≡ n
from (to x) ≡ x
```

For each law: if it holds, prove; if not, give a counterexample.

## Relations

#### Exercise `orderings`

Give an example of a preorder that is not a partial order.

Give an example of a partial order that is not a preorder.

#### Exercise `≤-antisym-cases`

The above proof omits cases where one argument is `z≤n`

and one
argument is `s≤s`

. Why is it ok to omit them?

#### Exercise `*-mono-≤`

(stretch)

Show that multiplication is monotonic with regard to inequality.

#### Exercise `<-trans`

(recommended)

Show that strict inequality is transitive.

#### Exercise `trichotomy`

Show that strict inequality satisfies a weak version of trichotomy, in
the sense that for any `m`

and `n`

that one of the following holds:

`m < n`

,`m ≡ n`

, or`m > n`

Define`m > n`

to be the same as`n < m`

. You will need a suitable data declaration, similar to that used for totality. (We will show that the three cases are exclusive after we introduce [negation][plfa.Negation].)

#### Exercise `+-mono-<`

Show that addition is monotonic with respect to strict inequality. As with inequality, some additional definitions may be required.

#### Exercise `≤-iff-<`

(recommended)

Show that `suc m ≤ n`

implies `m < n`

, and conversely.

#### Exercise `<-trans-revisited`

Give an alternative proof that strict inequality is transitive, using the relating between strict inequality and inequality and the fact that inequality is transitive.

#### Exercise `o+o≡e`

(stretch)

Show that the sum of two odd numbers is even.

#### Exercise `Bin-predicates`

(stretch)

Recall that
Exercise [Bin][plfa.Naturals#Bin]
defines a datatype `Bin`

of bitstrings representing natural numbers.
Representations are not unique due to leading zeros.
Hence, eleven may be represented by both of the following

```
x1 x1 x0 x1 nil
x1 x1 x0 x1 x0 x0 nil
```

Define a predicate

```
Can : Bin → Set
```

over all bitstrings that holds if the bitstring is canonical, meaning it has no leading zeros; the first representation of eleven above is canonical, and the second is not. To define it, you will need an auxiliary predicate

```
One : Bin → Set
```

that holds only if the bistring has a leading one. A bitstring is canonical if it has a leading one (representing a positive number) or if it consists of a single zero (representing zero).

Show that increment preserves canonical bitstrings.

```
Can x
------------
Can (inc x)
```

Show that converting a natural to a bitstring always yields a canonical bitstring.

```
----------
Can (to n)
```

Show that converting a canonical bitstring to a natural and back is the identity.

```
Can x
---------------
to (from x) ≡ x
```

(Hint: For each of these, you may first need to prove related
properties of `One`

.)