# Assignment2: TSPL Assignment 2

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

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).

## Connectives

module Connectives where

## Imports

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 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

module Negation where

## Imports

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 is irreflexive, that is, `n < n`

holds for no `n`

.

-- Your code goes here

#### Exercise `trichotomy`

(practice)

Show that strict inequality satisfies 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

module Quantifiers where

## Imports

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 plfa.part1.Connectives hiding (Tri) open import plfa.part1.Quantifiers hiding (∀-distrib-×; ⊎∀-implies-∀⊎; ∃-distrib-⊎; ∃×-implies-×∃; ∃¬-implies-¬∀; Tri)

#### 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.

Hint: you will need to use `∀-extensionality`

.

#### 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`

.

Hint: you will need to use `∀-extensionality`

.

#### 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)

Recall that Exercises Bin, Bin-laws, and 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′`

-- Your code goes here

## Decidable

module Decidable where

## Imports

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: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, 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

#### 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, Bin-laws, and 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)
```