---
title     : "Assignment2: TSPL Assignment 2"
permalink : /TSPL/2024/Assignment2/
---

```
module Assignment2 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 Gradescope. Go to the course page under Learn.
Select `Assessment`, then select `Assignment Submission`.
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:

> [https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct](https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct)

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). Do not publish solutions to the coursework.

## Deadline and late policy

The deadline and late policy for this assignment are specified on
Learn in the "Coursework Planner". There are no extensions and
no ETAs. Coursework is marked best three out of four. Guidance
on late submissions is at

> [https://web.inf.ed.ac.uk/node/4533](https://web.inf.ed.ac.uk/node/4533)


## Connectives

```
module Connectives where
```

## Imports

```agda
  import Relation.Binary.PropositionalEquality as Eq
  open Eq using (_≡_; refl)
  open Eq.≡-Reasoning
  open import Data.Nat using (ℕ)
  open import Function using (_∘_)
  open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality; _⇔_)
  open plfa.part1.Isomorphism.≃-Reasoning
  open import plfa.part1.Connectives
    hiding (⊎-weak-×; ⊎×-implies-×⊎)
```

#### Exercise `⇔≃×` (practice)

Show that `A ⇔ B` as defined [earlier](/Isomorphism/#iff)
is isomorphic to `(A → B) × (B → A)`.

```agda
  -- Your code goes here
```


#### Exercise `⊎-comm` (recommended)

Show sum is commutative up to isomorphism.

```agda
  -- Your code goes here
```

#### Exercise `⊎-assoc` (practice)

Show sum is associative up to isomorphism.

```agda
  -- Your code goes here
```

#### Exercise `⊥-identityˡ` (recommended)

Show empty is the left identity of sums up to isomorphism.

```agda
  -- Your code goes here
```

#### Exercise `⊥-identityʳ` (practice)

Show empty is the right identity of sums up to isomorphism.

```agda
  -- Your code goes here
```

#### Exercise `⊎-weak-×` (recommended)

Show that the following property holds:
```agda
  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.

```agda
  -- Your code goes here
```


#### Exercise `⊎×-implies-×⊎` (practice)

Show that a disjunct of conjuncts implies a conjunct of disjuncts:
```agda
  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.

```agda
  -- Your code goes here
```



## Negation

```
module Negation where
```

## Imports

```agda
  open import Relation.Binary.PropositionalEquality using (_≡_; refl)
  open import Data.Nat using (ℕ; zero; suc)
  open import plfa.part1.Isomorphism using (_≃_; extensionality)
  open import plfa.part1.Connectives
  open import plfa.part1.Negation
    hiding (Stable)
```

#### Exercise `<-irreflexive` (recommended)

Using negation, show that
[strict inequality](/Relations/#strict-inequality)
is irreflexive, that is, `n < n` holds for no `n`.

```agda
  -- Your code goes here
```


#### Exercise `trichotomy` (practice)

Show that strict inequality satisfies
[trichotomy](/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.

```agda
  -- 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.

```agda
  -- 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.

```agda
  -- Your code goes here
```


#### Exercise `Stable` (stretch)

Say that a formula is _stable_ if double negation elimination holds for it:
```agda
  Stable : Set → Set
  Stable A = ¬ ¬ A → A
```
Show that any negated formula is stable, and that the conjunction
of two stable formulas is stable.

```agda
  -- Your code goes here
```


## Quantifiers

```
module Quantifiers where
```

## Imports

```agda
  import Relation.Binary.PropositionalEquality as Eq
  open Eq using (_≡_; refl)
  open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
  open import Relation.Nullary using (¬_)
  open import Function using (_∘_)
  open import plfa.part1.Isomorphism using (_≃_; extensionality; ∀-extensionality)
  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 Function.Bundles using (_⇔_)
  open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
```

#### Exercise `∀-distrib-×` (recommended)

Show that universals distribute over conjunction:
```agda
  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](/Connectives/).

Hint: you will need to use [`∀-extensionality`](/Isomorphism/#extensionality).

#### Exercise `⊎∀-implies-∀⊎` (practice)

Show that a disjunction of universals implies a universal of disjunctions:
```agda
  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.
```agda
  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`.

Hint: you will need to use [`∀-extensionality`](/Isomorphism/#extensionality).


#### Exercise `∃-distrib-⊎` (recommended)

Show that existentials distribute over disjunction:
```agda
  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:
```agda
  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.

```agda
  -- Your code goes here
```

#### Exercise `∃-+-≤` (practice)

Show that `y ≤ z` holds if and only if there exists a `x` such that
`x + y ≡ z`.

```agda
  -- Your code goes here
```


#### Exercise `∃¬-implies-¬∀` (recommended)

Show that existential of a negation implies negation of a universal:
```agda
  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](/Naturals/#Bin),
[Bin-laws](/Induction/#Bin-laws), and
[Bin-predicates](/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`.

We recommend proving the following lemmas which show that, for a given
binary number `b`, there is only one proof of `One b` and similarly
for `Can b`.

    ≡One : ∀ {b : Bin} (o o′ : One b) → o ≡ o′

    ≡Can : ∀ {b : Bin} (cb cb′ : Can b) → cb ≡ cb′

Many of the alternatives for proving `to∘from` turn out to be tricky.
However, the proof can be straightforward if you use the following lemma,
which is a corollary of `≡Can`.

    proj₁≡→Can≡ : {cb cb′ : ∃[ b ] Can b} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′

```agda
  -- Your code goes here
```



## Decidable

```
module Decidable where
```

## Imports

```agda
  import Relation.Binary.PropositionalEquality as Eq
  open Eq using (_≡_; refl)
  open Eq.≡-Reasoning
  open import Data.Nat using (ℕ; zero; suc)
  open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
  open import Data.Sum using (_⊎_; inj₁; inj₂)
  open import Relation.Nullary using (¬_)
  open import Relation.Nullary.Negation using ()
    renaming (contradiction to ¬¬-intro)
  open import Data.Unit using (⊤; tt)
  open import Data.Empty using (⊥; ⊥-elim)
  open import plfa.part1.Relations using (_<_; z<s; s<s)
  open import plfa.part1.Isomorphism using (_⇔_)
  open import plfa.part1.Decidable
    hiding (_<?_; _≡ℕ?_; ∧-×; ∨-⊎; not-¬; _iff_; _⇔-dec_; iff-⇔)
```

#### Exercise `_<?_` (recommended)

Analogous to the function above, define a function to decide strict inequality:
```agda
  postulate
    _<?_ : ∀ (m n : ℕ) → Dec (m < n)
```

```agda
  -- Your code goes here
```

#### Exercise `_≡ℕ?_` (practice)

Define a function to decide whether two naturals are equal:
```agda
  postulate
    _≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
```

```agda
  -- Your code goes here
```


#### Exercise `erasure` (practice)

Show that erasure relates corresponding boolean and decidable operations:
```agda
  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](/Isomorphism/#iff),
operation on booleans and decidables, and also show the corresponding erasure:
```agda
  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 ⌋
```

```agda
  -- Your code goes here
```

#### Exercise `False` (practice)

Give analogues of `True`, `toWitness`, and `fromWitness` which work
with *negated* properties. Call these `False`, `toWitnessFalse`, and
`fromWitnessFalse`.


#### Exercise `Bin-decidable` (stretch)

Recall that Exercises
[Bin](/Naturals/#Bin),
[Bin-laws](/Induction/#Bin-laws), and
[Bin-predicates](/Relations/#Bin-predicates)
define a datatype `Bin` of bitstrings representing natural numbers,
and asks you to define the following predicates:

    One  : Bin → Set
    Can  : Bin → Set

Show that both of the above are decidable.

    One? : ∀ (b : Bin) → Dec (One b)
    Can? : ∀ (b : Bin) → Dec (Can b)