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 ⌋

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 ⌋