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 the “submit” command.

submit tspl cw2 Assignment2.lagda.md

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

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

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)

Recall that Exercises Bin and 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 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 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

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.

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)

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

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

YOUR NAME AND EMAIL GOES HERE

Introduction

Good Scholarly Practice.

Imports

Equality

Imports

Equality

Exercise ≤-Reasoning (stretch)

Isomorphism

Exercise ≃-implies-≲ (practice)

Exercise _⇔_ (practice)

Exercise Bin-embedding (stretch)

Connectives

Exercise ⇔≃× (recommended)

Exercise ⊎-comm (recommended)

Exercise ⊎-assoc (practice)

Exercise ⊥-identityˡ (recommended)

Exercise ⊥-identityʳ (practice)

Exercise ⊎-weak-× (recommended)

Exercise ⊎×-implies-×⊎ (practice)

Negation

Exercise <-irreflexive (recommended)

Exercise trichotomy (practice)

Exercise ⊎-dual-× (recommended)

Exercise Classical (stretch)

Exercise Stable (stretch)

Quantifiers

Exercise ∀-distrib-× (recommended)

Exercise ⊎∀-implies-∀⊎ (practice)

Exercise ∀-× (practice)

Exercise ∃-distrib-⊎ (recommended)

Exercise ∃×-implies-×∃ (practice)

Exercise ∃-⊎ (practice)

Exercise ∃-even-odd (practice)

Exercise ∃-|-≤ (practice)

Exercise ∃¬-implies-¬∀ (recommended)

Exercise Bin-isomorphism (stretch)

Decidable

Exercise _<?_ (recommended)

Exercise _≡ℕ?_ (practice)

Exercise erasure (practice)

Exercise iff-erasure (recommended)

Exercise `≤-Reasoning` (stretch)

Exercise `≃-implies-≲` (practice)

Exercise `_⇔_` (practice)

Exercise `Bin-embedding` (stretch)

Exercise `⇔≃×` (recommended)

Exercise `⊎-comm` (recommended)

Exercise `⊎-assoc` (practice)

Exercise `⊥-identityˡ` (recommended)

Exercise `⊥-identityʳ` (practice)

Exercise `⊎-weak-×` (recommended)

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

Exercise `<-irreflexive` (recommended)

Exercise `trichotomy` (practice)

Exercise `⊎-dual-×` (recommended)

Exercise `Classical` (stretch)

Exercise `Stable` (stretch)

Exercise `∀-distrib-×` (recommended)

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

Exercise `∀-×` (practice)

Exercise `∃-distrib-⊎` (recommended)

Exercise `∃×-implies-×∃` (practice)

Exercise `∃-⊎` (practice)

Exercise `∃-even-odd` (practice)

Exercise `∃-|-≤` (practice)

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

Exercise `Bin-isomorphism` (stretch)

Exercise `_<?_` (recommended)

Exercise `_≡ℕ?_` (practice)

Exercise `erasure` (practice)

Exercise `iff-erasure` (recommended)