Assignment 3

courses/tspl/2019/tspl2019.md

@@ -13,7 +13,7 @@ permalink : /TSPL/2019/
 
 ## Lectures
 
-Lectures take place Monday, Wednesday, and Friday in AT 5.07. (Room provisional.)
+Lectures take place Monday, Wednesday, and Friday in AT 5.07.
 * **10.00--10.50am** Lecture
 * **11.10--12.00noon** Tutorial
 
@@ -47,49 +47,49 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. (Room provisional.
   <td>4</td>
   <td><b>7 Oct</b> <a href="{{ site.baseurl }}/Quantifiers/">Quantifiers</a></td>
   <td><b>9 Oct</b> <a href="{{ site.baseurl }}/Decidable/">Decidable</a></td>
-  <td><b>11 Oct</b> (tutorial only)</td>
+  <td><b>11 Oct</b> (tutorial only, 10.00&ndash;10.50)</td>
  </tr>
  <tr>
   <td>5</td>
   <td><b>14 Oct</b> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
-  <td><b>16 Oct</b> <a href="{{ site.baseurl }}/Lambda/">Lambda</a>
+  <td><b>16 Oct</b> <a href="{{ site.baseurl }}/Lambda/">Lambda</a></td>
-  <td><b>18 Oct</b> <a href="{{ site.baseurl }}/Properties/">Properties</a>
+  <td><b>18 Oct</b> <a href="{{ site.baseurl }}/Properties/">Properties</a></td>
  </tr>
  <tr>
   <td>6</td>
-  <td><b>21 Oct</b> <a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a>
+  <td><b>21 Oct</b> <a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a></td>
-  <td><b>23 Oct</b> <a href="{{ site.baseurl }}/More/">More</a>
+  <td><b>23 Oct</b> <a href="{{ site.baseurl }}/More/">More</a></td>
-  <td><b>25 Oct</b> <a href="{{ site.baseurl }}/Inference/">Inference</a>
+  <td><b>25 Oct</b> <a href="{{ site.baseurl }}/Inference/">Inference</a></td>
  </tr>
  <tr>
   <td>7</td>
-  <td><b>28 Oct</b> <a href="{{ site.baseurl }}/Untyped/">Untyped</a>
+  <td><b>28 Oct</b> <a href="{{ site.baseurl }}/Untyped/">Untyped</a></td>
-  <td><b>30 Oct</b> (to be decided)
+  <td><b>30 Oct</b> (to be decided) </td>
-  <td><b>1 Nov</b>  (no class)
+  <td><b>1 Nov</b>  (no class) </td>
  </tr>
  <tr>
   <td>8</td>
-  <td><b>4 Nov</b> (no class)
+  <td><b>4 Nov</b> (no class) </td>
-  <td><b>6 Nov</b> (tutorial only)
+  <td><b>6 Nov</b> (tutorial only) </td>
-  <td><b>8 Nov</b> (no class)
+  <td><b>8 Nov</b> (no class) </td>
  </tr>
  <tr>
   <td>9</td>
-  <td><b>11 Nov</b> (no class)
+  <td><b>11 Nov</b> (no class) </td>
-  <td><b>13 Nov</b> (tutorial only)
+  <td><b>13 Nov</b> (tutorial only) </td>
-  <td><b>15 Nov</b> (no class)
+  <td><b>15 Nov</b> (no class) </td>
  </tr>
  <tr>
   <td>10</td>
-  <td><b>18 Nov</b> (no class)
+  <td><b>18 Nov</b> (no class) </td>
-  <td><b>20 Nov</b> Propositions as Types
+  <td><b>20 Nov</b> Propositions as Types </td>
-  <td><b>22 Nov</b> (no class)
+  <td><b>22 Nov</b> (no class) </td>
  </tr>
  <tr>
   <td>11</td>
-  <td><b>25 Nov</b> (no class)
+  <td><b>25 Nov</b> (no class) </td>
-  <td><b>27 Nov</b> Quantitative (Wen)
+  <td><b>27 Nov</b> Quantitative (Wen) </td>
-  <td><b>29 Nov</b> (mock exam)</td>
+  <td><b>29 Nov</b> (mock exam) </td> 
  </tr>
 </table>
 
@@ -119,7 +119,7 @@ For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.ba
 
 * [Assignment 1]({{ site.baseurl }}/TSPL/2019/Assignment1/) cw1 due 4pm Thursday 3 October (Week 3)
 * [Assignment 2]({{ site.baseurl }}/TSPL/2019/Assignment2/) cw2 due 4pm Thursday 17 October (Week 5)
-* Assignment 3 <!-- [Assignment 3]({{ site.baseurl }}/TSPL/2019/Assignment3/) --> cw3 due 4pm Thursday 31 October (Week 7)
+* [Assignment 3]({{ site.baseurl }}/TSPL/2019/Assignment3/) cw3 due 4pm Thursday 31 October (Week 7)
 * Assignment 4 <!-- [Assignment 4]({{ site.baseurl }}/TSPL/2019/Assignment4/) --> cw4 due 4pm Thursday 14 November (Week 9)
 * Assignment 5 <!-- [Assignment 5]({{ site.baseurl }}/courses/tspl/2010/Mock1.pdf) --> cw5 due 4pm Thursday 21 November (Week 10)
   <!-- <br />

src/plfa/part1/Equality.lagda.md

@@ -688,6 +688,14 @@ Before the signature used `Set₁` as the type of a term that includes
 `Set`, whereas here the signature uses `Set (lsuc ℓ)` as the type of a
 term that includes `Set ℓ`.
 
+Most other functions in the standard library are also generalised to
+arbitrary levels. For instance, here is the definition of composition.
+```
+_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
+  → (B → C) → (A → B) → A → C
+(g ∘ f) x  =  g (f x)
+```
+
 Further information on levels can be found in the [Agda Wiki][wiki].
 
 [wiki]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism

src/plfa/part1/Lists.lagda.md

@@ -351,21 +351,15 @@ list, and the sum of the numbers up to `n - 1` is `n * (n - 1) / 2`.
 
 Show that the reverse of one list appended to another is the
 reverse of the second appended to the reverse of the first:
-```
+
-postulate
+    reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
-  reverse-++-distrib : ∀ {A : Set} (xs ys : List A)
-    → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
-```
 
 #### Exercise `reverse-involutive` (recommended)
 
 A function is an _involution_ if when applied twice it acts
 as the identity function.  Show that reverse is an involution:
-```
+
-postulate
+    reverse (reverse xs) ≡ xs
-  reverse-involutive : ∀ {A : Set} {xs : List A}
-    → reverse (reverse xs) ≡ xs
-```
 
 
 ## Faster reverse
@@ -528,21 +522,17 @@ _n_ functions.
 #### Exercise `map-compose` (practice)
 
 Prove that the map of a composition is equal to the composition of two maps:
-```
+
-postulate
+    map (g ∘ f) ≡ map g ∘ map f
-  map-compose : ∀ {A B C : Set} {f : A → B} {g : B → C}
+
-    → map (g ∘ f) ≡ map g ∘ map f
-```
 The last step of the proof requires extensionality.
 
-#### Exercise `map-++-commute` (practice)
+#### Exercise `map-++-distribute` (practice)
 
 Prove the following relationship between map and append:
-```
+
-postulate
+    map f (xs ++ ys) ≡ map f xs ++ map f ys
-  map-++-commute : ∀ {A B : Set} {f : A → B} {xs ys : List A}
+
-   →  map f (xs ++ ys) ≡ map f xs ++ map f ys
-```
 
 #### Exercise `map-Tree` (practice)
 
@@ -929,32 +919,41 @@ Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
 -- Your code goes here
 ```
 
-#### Exercise `¬Any≃All¬` (stretch)
+#### Exercise `¬Any≃All¬` (recommended)
-
-First generalise composition to arbitrary levels, using
-[universe polymorphism]({{ site.baseurl }}/Equality/#unipoly):
-```
-_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
-  → (B → C) → (A → B) → A → C
-(g ∘′ f) x  =  g (f x)
-```
 
 Show that `Any` and `All` satisfy a version of De Morgan's Law:
-```
+
-postulate
+    (¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs
-  ¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
+
-    → (¬_ ∘′ Any P) xs ≃ All (¬_ ∘′ P) xs
+(Can you see why it is important that here `_∘_` is generalised
-```
+to arbitrary levels, as described in the section on
+[universe polymorphism]({{ site.baseurl }}/Equality/#unipoly)?)
 
 Do we also have the following?
-```
+
-postulate
+    (¬_ ∘ All P) xs ≃ Any (¬_ ∘ P) xs
-  ¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
+
-    → (¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs
-```
 If so, prove; if not, explain why.
 
 
+#### Exercise `All-∀` (practice)
+
+Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.
+
+```
+-- You code goes here
+```
+
+
+#### Exercise `Any-∃` (practice)
+
+Show that `Any P xs` is isomorphic to `∃[ x ] (x ∈ xs × P x)`.
+
+```
+-- You code goes here
+```
+
+
 ## Decidability of All
 
 If we consider a predicate as a function that yields a boolean,
@@ -1005,24 +1004,6 @@ for some element of a list.  Give their definitions.
 ```
 
 
-#### Exercise `All-∀` (practice)
-
-Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.
-
-```
--- You code goes here
-```
-
-
-#### Exercise `Any-∃` (practice)
-
-Show that `Any P xs` is isomorphic to `∃[ x ∈ xs ] P x`.
-
-```
--- You code goes here
-```
-
-
 #### Exercise `filter?` (stretch)
 
 Define the following variant of the traditional `filter` function on lists,