Added Assignment2

2019-09-30 12:24:25 +01:00 · 2019-09-30 12:24:25 +01:00 · 55ecfb595b
commit 55ecfb595b
parent a79cd54db3
4 changed files with 502 additions and 5 deletions
--- a/courses/tspl/2019/Assignment1.lagda.md
+++ b/courses/tspl/2019/Assignment1.lagda.md
@ -19,9 +19,25 @@ 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. -->
+Submit your homework using the "submit" command.
 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

 ```
--- a/courses/tspl/2019/Assignment2.lagda.md
+++ b/courses/tspl/2019/Assignment2.lagda.md
@ -0,0 +1,481 @@
+---
+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.
+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_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+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 Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+open import Data.Unit using (⊤; tt)
+open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)
+open import Relation.Nullary.Negation using (¬?)
+open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Negation using (contraposition)
+open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
+open import plfa.part1.Relations using (_<_; z<s; s<s)
+open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.part1.Isomorphism.≃-Reasoning
+```
+
+## Equality
+
+
+## Imports
+
+This chapter has no imports.  Every chapter in this book, and nearly
+every module in the Agda standard library, imports equality.
+Since we define equality here, any import would create a conflict.
+
+
+## Equality
+
+#### Exercise `≤-Reasoning` (stretch)
+
+The proof of monotonicity from
+Chapter [Relations]({{ site.baseurl }}/Relations/)
+can be written in a more readable form by using an analogue of our
+notation for `≡-Reasoning`.  Define `≤-Reasoning` analogously, and use
+it to write out an alternative proof that addition is monotonic with
+regard to inequality.  Rewrite all of `+-monoˡ-≤`, `+-monoʳ-≤`, and `+-mono-≤`.
+
+```
+-- Your code goes here
+```
+
+## Isomorphism
+
+#### Exercise `≃-implies-≲` (practice)
+
+Show that every isomorphism implies an embedding.
+```
+postulate
+  ≃-implies-≲ : ∀ {A B : Set}
+    → A ≃ B
+      -----
+    → A ≲ B
+```
+
+```
+-- Your code goes here
+```
+
+#### Exercise `_⇔_` (practice) {#iff}
+
+Define equivalence of propositions (also known as "if and only if") as follows:
+```
+record _⇔_ (A B : Set) : Set where
+  field
+    to   : A → B
+    from : B → A
+```
+Show that equivalence is reflexive, symmetric, and transitive.
+
+```
+-- Your code goes here
+```
+
+#### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
+
+Recall that Exercises
+[Bin]({{ site.baseurl }}/Naturals/#Bin) and
+[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws)
+define a datatype `Bin` of bitstrings representing natural numbers,
+and asks you to define the following functions and predicates:
+
+    to : ℕ → Bin
+    from : Bin → ℕ
+
+which satisfy the following property:
+
+    from (to n) ≡ n
+
+Using the above, establish that there is an embedding of `ℕ` into `Bin`.
+```
+-- Your code goes here
+```
+
+Why do `to` and `from` not form an isomorphism?
+
+## Connectives
+
+#### Exercise `⇔≃×` (recommended)
+
+Show that `A ⇔ B` as defined [earlier]({{ site.baseurl }}/Isomorphism/#iff)
+is isomorphic to `(A → B) × (B → A)`.
+
+```
+-- Your code goes here
+```
+
+#### Exercise `⊎-comm` (recommended)
+
+Show sum is commutative up to isomorphism.
+
+```
+-- Your code goes here
+```
+
+#### Exercise `⊎-assoc` (practice)
+
+Show sum is associative up to isomorphism.
+
+```
+-- Your code goes here
+```
+
+#### Exercise `⊥-identityˡ` (recommended)
+
+Show empty is the left identity of sums up to isomorphism.
+
+```
+-- Your code goes here
+```
+
+#### Exercise `⊥-identityʳ` (practice)
+
+Show empty is the right identity of sums up to isomorphism.
+
+```
+-- Your code goes here
+```
+
+#### Exercise `⊎-weak-×` (recommended)
+
+Show that the following property holds:
+```
+postulate
+  ⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
+```
+This is called a _weak distributive law_. Give the corresponding
+distributive law, and explain how it relates to the weak version.
+
+```
+-- Your code goes here
+```
+
+
+#### Exercise `⊎×-implies-×⊎` (practice)
+
+Show that a disjunct of conjuncts implies a conjunct of disjuncts:
+```
+postulate
+  ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
+```
+Does the converse hold? If so, prove; if not, give a counterexample.
+
+```
+-- Your code goes here
+```
+
+## Negation
+
+#### Exercise `<-irreflexive` (recommended)
+
+Using negation, show that
+[strict inequality]({{ site.baseurl }}/Relations/#strict-inequality)
+is irreflexive, that is, `n < n` holds for no `n`.
+
+```
+-- Your code goes here
+```
+
+
+#### Exercise `trichotomy` (practice)
+
+Show that strict inequality satisfies
+[trichotomy]({{ site.baseurl }}/Relations/#trichotomy),
+that is, for any naturals `m` and `n` exactly one of the following holds:
+
+* `m < n`
+* `m ≡ n`
+* `m > n`
+
+Here "exactly one" means that not only one of the three must hold,
+but that when one holds the negation of the other two must also hold.
+
+```
+-- Your code goes here
+```
+
+#### Exercise `⊎-dual-×` (recommended)
+
+Show that conjunction, disjunction, and negation are related by a
+version of De Morgan's Law.
+
+    ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
+
+This result is an easy consequence of something we've proved previously.
+
+```
+-- Your code goes here
+```
+
+
+Do we also have the following?
+
+    ¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
+
+If so, prove; if not, can you give a relation weaker than
+isomorphism that relates the two sides?
+
+#### Exercise `Classical` (stretch)
+
+Consider the following principles:
+
+  * Excluded Middle: `A ⊎ ¬ A`, for all `A`
+  * Double Negation Elimination: `¬ ¬ A → A`, for all `A`
+  * Peirce's Law: `((A → B) → A) → A`, for all `A` and `B`.
+  * Implication as disjunction: `(A → B) → ¬ A ⊎ B`, for all `A` and `B`.
+  * De Morgan: `¬ (¬ A × ¬ B) → A ⊎ B`, for all `A` and `B`.
+
+Show that each of these implies all the others.
+
+```
+-- Your code goes here
+```
+
+
+#### Exercise `Stable` (stretch)
+
+Say that a formula is _stable_ if double negation elimination holds for it:
+```
+Stable : Set → Set
+Stable A = ¬ ¬ A → A
+```
+Show that any negated formula is stable, and that the conjunction
+of two stable formulas is stable.
+
+```
+-- Your code goes here
+```
+
+## Quantifiers
+
+
+#### Exercise `∀-distrib-×` (recommended)
+
+Show that universals distribute over conjunction:
+```
+postulate
+  ∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
+    (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
+```
+Compare this with the result (`→-distrib-×`) in
+Chapter [Connectives]({{ site.baseurl }}/Connectives/).
+
+
+#### Exercise `⊎∀-implies-∀⊎` (practice)
+
+Show that a disjunction of universals implies a universal of disjunctions:
+```
+postulate
+  ⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} →
+    (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x)  →  ∀ (x : A) → B x ⊎ C x
+```
+Does the converse hold? If so, prove; if not, explain why.
+
+
+#### Exercise `∀-×` (practice)
+
+Consider the following type.
+```
+data Tri : Set where
+  aa : Tri
+  bb : Tri
+  cc : Tri
+```
+Let `B` be a type indexed by `Tri`, that is `B : Tri → Set`.
+Show that `∀ (x : Tri) → B x` is isomorphic to `B aa × B bb × B cc`.
+
+
+#### Exercise `∃-distrib-⊎` (recommended)
+
+Show that existentials distribute over disjunction:
+```
+postulate
+  ∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
+    ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
+```
+
+
+#### Exercise `∃×-implies-×∃` (practice)
+
+Show that an existential of conjunctions implies a conjunction of existentials:
+```
+postulate
+  ∃×-implies-×∃ : ∀ {A : Set} {B C : A → Set} →
+    ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
+```
+Does the converse hold? If so, prove; if not, explain why.
+
+
+#### Exercise `∃-⊎` (practice)
+
+Let `Tri` and `B` be as in Exercise `∀-×`.
+Show that `∃[ x ] B x` is isomorphic to `B aa ⊎ B bb ⊎ B cc`.
+
+
+#### Exercise `∃-even-odd` (practice)
+
+How do the proofs become more difficult if we replace `m * 2` and `1 + m * 2`
+by `2 * m` and `2 * m + 1`?  Rewrite the proofs of `∃-even` and `∃-odd` when
+restated in this way.
+
+```
+-- Your code goes here
+```
+
+#### Exercise `∃-|-≤` (practice)
+
+Show that `y ≤ z` holds if and only if there exists a `x` such that
+`x + y ≡ z`.
+
+```
+-- Your code goes here
+```
+
+
+#### Exercise `∃¬-implies-¬∀` (recommended)
+
+Show that existential of a negation implies negation of a universal:
+```
+postulate
+  ∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
+    → ∃[ x ] (¬ B x)
+      --------------
+    → ¬ (∀ x → B x)
+```
+Does the converse hold? If so, prove; if not, explain why.
+
+
+#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
+
+Recall that Exercises
+[Bin]({{ site.baseurl }}/Naturals/#Bin),
+[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws), and
+[Bin-predicates]({{ site.baseurl }}/Relations/#Bin-predicates)
+define a datatype `Bin` of bitstrings representing natural numbers,
+and asks you to define the following functions and predicates:
+
+    to   : ℕ → Bin
+    from : Bin → ℕ
+    Can  : Bin → Set
+
+And to establish the following properties:
+
+    from (to n) ≡ n
+
+    ----------
+    Can (to n)
+
+    Can b
+    ---------------
+    to (from b) ≡ b
+
+Using the above, establish that there is an isomorphism between `ℕ` and
+`∃[ b ](Can b)`.
+
+```
+-- Your code goes here
+```
+
+## Decidable
+
+
+#### Exercise `_<?_` (recommended)
+
+Analogous to the function above, define a function to decide strict inequality:
+```
+postulate
+  _<?_ : ∀ (m n : ℕ) → Dec (m < n)
+```
+
+```
+-- Your code goes here
+```
+
+#### Exercise `_≡ℕ?_` (practice)
+
+Define a function to decide whether two naturals are equal:
+```
+postulate
+  _≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
+```
+
+```
+-- Your code goes here
+```
+
+
+#### Exercise `erasure` (practice)
+
+Show that erasure relates corresponding boolean and decidable operations:
+```
+postulate
+  ∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
+  ∨-⊎ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
+  not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
+```
+
+#### Exercise `iff-erasure` (recommended)
+
+Give analogues of the `_⇔_` operation from
+Chapter [Isomorphism]({{ site.baseurl }}/Isomorphism/#iff),
+operation on booleans and decidables, and also show the corresponding erasure:
+```
+postulate
+  _iff_ : Bool → Bool → Bool
+  _⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
+  iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
+```
+
+```
+-- Your code goes here
+```
+
--- a/courses/tspl/2019/tspl2019.md
+++ b/courses/tspl/2019/tspl2019.md
@ -118,7 +118,7 @@ courses where there are easier marks to be had.
 For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).

 * [Assignment 1]({{ site.baseurl }}/TSPL/2019/Assignment1/) cw1 due 4pm Thursday 3 October (Week 3)
-* Assignment 2 <!-- [Assignment 2]({{ site.baseurl }}/TSPL/2019/Assignment2/) --> cw2 due 4pm Thursday 17 October (Week 5)
+* [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 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)
@ -128,7 +128,7 @@ For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.ba

 Assignments are submitted by running
 ``` bash
-submit tspl cwN AssignmentN.lagda
+submit tspl cwN AssignmentN.lagda.md
 ```
 where N is the number of the assignment.

--- a/src/plfa/part2/Lambda.lagda.md
+++ b/src/plfa/part2/Lambda.lagda.md
@ -1104,13 +1104,13 @@ infix  4  _⊢_⦂_

 data _⊢_⦂_ : Context → Term → Type → Set where

-  -- Axiom
+  -- Axiom 
  ⊢` : ∀ {Γ x A}
    → Γ ∋ x ⦂ A
      -----------
    → Γ ⊢ ` x ⦂ A

-  -- ⇒-I
+  -- ⇒-I 
  ⊢ƛ : ∀ {Γ x N A B}
    → Γ , x ⦂ A ⊢ N ⦂ B
      -------------------