# 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 without a label are optional, and may be done if you want some extra practice.

Please ensure your files execute correctly under Agda!

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

#### Exercise `≤-reasoning`

(stretch)

The proof of monotonicity from
Chapter [Relations][plfa.Relations]
can be written in a more readable form by using an anologue 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 both `+-monoˡ-≤`

and `+-mono-≤`

.

## Isomorphism

#### Exercise `≃-implies-≲`

Show that every isomorphism implies an embedding.

postulate ≃-implies-≲ : ∀ {A B : Set} → A ≃ B ----- → A ≲ B

#### Exercise `_⇔_`

(recommended)

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 open _⇔_

Show that equivalence is reflexive, symmetric, and transitive.

#### Exercise `Bin-embedding`

(stretch)

Recall that Exercises [Bin][plfa.Naturals#Bin] and [Bin-laws][plfa.Induction#Bin-laws] define a datatype of bitstrings representing natural numbers.

data Bin : Set where nil : Bin x0_ : Bin → Bin x1_ : Bin → Bin

And ask you to define the following functions:

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

.
Why is there not an isomorphism?

## Connectives

#### Exercise `⇔≃×`

(recommended)

Show that `A ⇔ B`

as defined [earlier][plfa.Isomorphism#iff]
is isomorphic to `(A → B) × (B → A)`

.

#### Exercise `⊎-comm`

(recommended)

Show sum is commutative up to isomorphism.

#### Exercise `⊎-assoc`

Show sum is associative up to ismorphism.

#### Exercise `⊥-identityˡ`

(recommended)

Show zero is the left identity of addition.

#### Exercise `⊥-identityʳ`

Show zero is the right identity of addition.

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

#### Exercise `⊎×-implies-×⊎`

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.

## Negation

#### Exercise `<-irreflexive`

(recommended)

Using negation, show that
[strict inequality][plfa.Relations#strict-inequality]
is irreflexive, that is, `n < n`

holds for no `n`

.

#### Exercise `trichotomy`

Show that strict inequality satisfies
[trichotomy][plfa.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 one of the three must hold, and each implies the negation of the other two.

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

Do we also have the following?

```
¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
```

If so, prove; if not, give a variant that does hold.

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

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

## 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][plfa.Connectives].

#### Exercise `⊎∀-implies-∀⊎`

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 `∃-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-×∃`

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 `∃-even-odd`

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.

#### Exercise `∃-+-≤`

Show that `y ≤ z`

holds if and only if there exists a `x`

such that
`x + y ≡ z`

.

#### 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][plfa.Naturals#Bin], [Bin-laws][plfa.Induction#Bin-laws], and [Bin-predicates][plfa.Relations#Bin-predicates] define a datatype of bitstrings representing natural numbers.

```
data Bin : Set where
nil : Bin
x0_ : Bin → Bin
x1_ : Bin → Bin
```

And ask 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 x
---------------
to (from x) ≡ x
```

Using the above, establish that there is an isomorphism between `ℕ`

and
`∃[ x ](Can x)`

.

## Decidable

#### Exercise `_<?_`

(recommended)

Analogous to the function above, define a function to decide strict inequality.

postulate _<?_ : ∀ (m n : ℕ) → Dec (m < n)

#### Exercise `_≡ℕ?_`

Define a function to decide whether two naturals are equal.

postulate _≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)

#### Exercise `erasure`

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][plfa.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 ⌋