From 1b3b6f7cf189f843da3e1e5d5c7c280d6a2f397e Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Sun, 15 Sep 2019 17:36:16 +0100
Subject: [PATCH] minor fixes to assignments
---
courses/tspl/2018/Assignment1.lagda.md | 4 ++--
courses/tspl/2019/Assignment1.lagda.md | 31 ++++++++++++--------------
src/plfa/part1/Induction.lagda.md | 4 ++--
3 files changed, 18 insertions(+), 21 deletions(-)
diff --git a/courses/tspl/2018/Assignment1.lagda.md b/courses/tspl/2018/Assignment1.lagda.md
index 2b48c6a5..0252aff1 100644
--- a/courses/tspl/2018/Assignment1.lagda.md
+++ b/courses/tspl/2018/Assignment1.lagda.md
@@ -125,7 +125,7 @@ Give an example of an operator that has an identity and is
associative but is not commutative.
-#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
+#### 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
@@ -179,7 +179,7 @@ Show
for all naturals `n`. Did your proof require induction?
-#### Exercise `∸-|-assoc` {#monus-plus-assoc}
+#### Exercise `∸-+-assoc` {#monus-plus-assoc}
Show that monus associates with addition, that is,
diff --git a/courses/tspl/2019/Assignment1.lagda.md b/courses/tspl/2019/Assignment1.lagda.md
index 2b48c6a5..56888514 100644
--- a/courses/tspl/2019/Assignment1.lagda.md
+++ b/courses/tspl/2019/Assignment1.lagda.md
@@ -1,7 +1,7 @@
---
title : "Assignment1: TSPL Assignment 1"
layout : page
-permalink : /TSPL/2018/Assignment1/
+permalink : /TSPL/2019/Assignment1/
---
```
@@ -12,15 +12,12 @@ module Assignment1 where
## Introduction
-<!-- This assignment is due **1pm Friday 26 April**. -->
-
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.
+Exercises labelled "(practice)" are included for those who want extra practice.
<!-- Submit your homework using the "submit" command. -->
Please ensure your files execute correctly under Agda!
@@ -39,17 +36,17 @@ open import plfa.part1.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
## Naturals
-#### Exercise `seven` {#seven}
+#### Exercise `seven` (practice) {#seven}
Write out `7` in longhand.
-#### Exercise `+-example` {#plus-example}
+#### Exercise `+-example` (practice) {#plus-example}
Compute `3 + 4`, writing out your reasoning as a chain of equations.
-#### Exercise `*-example` {#times-example}
+#### Exercise `*-example` (practice) {#times-example}
Compute `3 * 4`, writing out your reasoning as a chain of equations.
@@ -116,7 +113,7 @@ Confirm that these both give the correct answer for zero through four.
## Induction
-#### Exercise `operators` {#operators}
+#### 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.
@@ -125,7 +122,7 @@ Give an example of an operator that has an identity and is
associative but is not commutative.
-#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
+#### 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
@@ -162,7 +159,7 @@ Show multiplication is associative, that is,
for all naturals `m`, `n`, and `p`.
-#### Exercise `*-comm` {#times-comm}
+#### Exercise `*-comm` (practice) {#times-comm}
Show multiplication is commutative, that is,
@@ -171,7 +168,7 @@ Show multiplication is commutative, that is,
for all naturals `m` and `n`. As with commutativity of addition,
you will need to formulate and prove suitable lemmas.
-#### Exercise `0∸n≡0` {#zero-monus}
+#### Exercise `0∸n≡0` (practice) {#zero-monus}
Show
@@ -179,7 +176,7 @@ Show
for all naturals `n`. Did your proof require induction?
-#### Exercise `∸-|-assoc` {#monus-plus-assoc}
+#### Exercise `∸-+-assoc` (practice) {#monus-plus-assoc}
Show that monus associates with addition, that is,
@@ -211,14 +208,14 @@ For each law: if it holds, prove; if not, give a counterexample.
## Relations
-#### Exercise `orderings` {#orderings}
+#### 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` {#leq-antisym-cases}
+#### 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?
@@ -233,7 +230,7 @@ Show that multiplication is monotonic with regard to inequality.
Show that strict inequality is transitive.
-#### Exercise `trichotomy` {#trichotomy}
+#### 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:
@@ -255,7 +252,7 @@ As with inequality, some additional definitions may be required.
Show that `suc m ≤ n` implies `m < n`, and conversely.
-#### Exercise `<-trans-revisited` {#less-trans-revisited}
+#### 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
diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md
index 565ec395..e7b96f88 100644
--- a/src/plfa/part1/Induction.lagda.md
+++ b/src/plfa/part1/Induction.lagda.md
@@ -697,7 +697,7 @@ judgments where the first number is less than _m_.
There is also a completely finite approach to generating the same equations,
which is left as an exercise for the reader.
-#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
+#### 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
@@ -927,7 +927,7 @@ for all naturals `n`. Did your proof require induction?
```
-#### Exercise `∸-|-assoc` (practice) {#monus-plus-assoc}
+#### Exercise `∸-+-assoc` (practice) {#monus-plus-assoc}
Show that monus associates with addition, that is,