331 lines
8.6 KiB
Markdown
331 lines
8.6 KiB
Markdown
---
|
||
title : "Assignment1: TSPL Assignment 1"
|
||
layout : page
|
||
permalink : /TSPL/2019/Assignment1/
|
||
---
|
||
|
||
```
|
||
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 labelled "(practice)" are included for those who want extra practice.
|
||
|
||
Submit your homework using the "submit" command.
|
||
```bash
|
||
submit tspl cw1 Assignment1.lagda.md
|
||
```
|
||
Please ensure your files execute correctly under Agda!
|
||
|
||
|
||
|
||
## Good Scholarly Practice.
|
||
|
||
Please remember the University requirement as
|
||
regards all assessed work. Details about this can be found at:
|
||
|
||
> [http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct](http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct)
|
||
|
||
Furthermore, you are required to take reasonable measures to protect
|
||
your assessed work from unauthorised access. For example, if you put
|
||
any such work on a public repository then you must set access
|
||
permissions appropriately (generally permitting access only to
|
||
yourself, or your group in the case of group practicals).
|
||
|
||
|
||
|
||
## Imports
|
||
|
||
```
|
||
import Relation.Binary.PropositionalEquality as Eq
|
||
open Eq using (_≡_; refl; cong; sym)
|
||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
|
||
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` (practice) {#seven}
|
||
|
||
Write out `7` in longhand.
|
||
|
||
|
||
#### Exercise `+-example` (practice) {#plus-example}
|
||
|
||
Compute `3 + 4`, writing out your reasoning as a chain of equations.
|
||
|
||
|
||
#### Exercise `*-example` (practice) {#times-example}
|
||
|
||
Compute `3 * 4`, writing out your reasoning as a chain of equations.
|
||
|
||
|
||
#### Exercise `_^_` (recommended) {#power}
|
||
|
||
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) {#monus-examples}
|
||
|
||
Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.
|
||
|
||
|
||
#### Exercise `Bin` (stretch) {#Bin}
|
||
|
||
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` (practice) {#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) {#finite-plus-assoc}
|
||
|
||
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) {#plus-swap}
|
||
|
||
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) {#times-distrib-plus}
|
||
|
||
Show multiplication distributes over addition, that is,
|
||
|
||
(m + n) * p ≡ m * p + n * p
|
||
|
||
for all naturals `m`, `n`, and `p`.
|
||
|
||
#### Exercise `*-assoc` (recommended) {#times-assoc}
|
||
|
||
Show multiplication is associative, that is,
|
||
|
||
(m * n) * p ≡ m * (n * p)
|
||
|
||
for all naturals `m`, `n`, and `p`.
|
||
|
||
#### Exercise `*-comm` (practice) {#times-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` (practice) {#zero-monus}
|
||
|
||
Show
|
||
|
||
zero ∸ n ≡ zero
|
||
|
||
for all naturals `n`. Did your proof require induction?
|
||
|
||
#### Exercise `∸-|-assoc` (practice) {#monus-plus-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) {#Bin-laws}
|
||
|
||
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` (practice) {#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` (practice) {#leq-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) {#less-trans}
|
||
|
||
Show that strict inequality is transitive.
|
||
|
||
#### Exercise `trichotomy` (practice) {#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-<` {#plus-mono-less}
|
||
|
||
Show that addition is monotonic with respect to strict inequality.
|
||
As with inequality, some additional definitions may be required.
|
||
|
||
#### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
|
||
|
||
Show that `suc m ≤ n` implies `m < n`, and conversely.
|
||
|
||
#### Exercise `<-trans-revisited` (practice) {#less-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) {#odd-plus-odd}
|
||
|
||
Show that the sum of two odd numbers is even.
|
||
|
||
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
|
||
|
||
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`.)
|