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.Product using (Σ; ∃; Σ-syntax; ∃-syntax)
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 Relation.Unary using (Decidable)
open import Function using (_∘_)
open import Level using (Level)
open import plfa.part1.Relations using (_<_; z<s; s<s)
open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
open plfa.part1.Isomorphism.≃-Reasoning
open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
  _++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)

Equality

Exercise ≤-reasoning (stretch)

The proof of monotonicity from Chapter [Relations][plfa.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 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 isomorphism.

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 ⌋

Lists

Exercise reverse-++-commute (recommended)

Show that the reverse of one list appended to another is the reverse of the second appended to the reverse of the first.

postulate
  reverse-++-commute : ∀ {A : Set} {xs ys : List A}
    → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

A function is an involution if when applied twice it acts as the identity function. Show that reverse is an involution.

postulate
  reverse-involutive : ∀ {A : Set} {xs : List A}
    → reverse (reverse xs) ≡ xs

Exercise map-compose

Prove that the map of a composition is equal to the composition of two maps.

postulate
  map-compose : ∀ {A B C : Set} {f : A → B} {g : B → C}
    → map (g ∘ f) ≡ map g ∘ map f

The last step of the proof requires extensionality.

Exercise map-++-commute

Prove the following relationship between map and append.

postulate
  map-++-commute : ∀ {A B : Set} {f : A → B} {xs ys : List A}
   →  map f (xs ++ ys) ≡ map f xs ++ map f ys

Exercise map-Tree

Define a type of trees with leaves of type A and internal nodes of type B.

data Tree (A B : Set) : Set where
  leaf : A → Tree A B
  node : Tree A B → B → Tree A B → Tree A B

Define a suitable map operator over trees.

postulate
  map-Tree : ∀ {A B C D : Set}
    → (A → C) → (B → D) → Tree A B → Tree C D

Use fold to define a function to find the product of a list of numbers. For example,

product [ 1 , 2 , 3 , 4 ] ≡ 24

Exercise foldr-++ (recommended)

Show that fold and append are related as follows.

postulate
  foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
    foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs

Exercise map-is-foldr

Show that map can be defined using fold.

postulate
  map-is-foldr : ∀ {A B : Set} {f : A → B} →
    map f ≡ foldr (λ x xs → f x ∷ xs) []

This requires extensionality.

Exercise fold-Tree

Define a suitable fold function for the type of trees given earlier.

postulate
  fold-Tree : ∀ {A B C : Set}
    → (A → C) → (C → B → C → C) → Tree A B → C

Exercise map-is-fold-Tree

Demonstrate an analogue of map-is-foldr for the type of trees.

Exercise sum-downFrom (stretch)

Define a function that counts down as follows.

downFrom : ℕ → List ℕ
downFrom zero     =  []
downFrom (suc n)  =  n ∷ downFrom n

For example,

_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
_ = refl

Prove that the sum of the numbers (n - 1) + ⋯ + 0 is equal to n * (n ∸ 1) / 2.

postulate
  sum-downFrom : ∀ (n : ℕ)
    → sum (downFrom n) * 2 ≡ n * (n ∸ 1)

Exercise foldl

Define a function foldl which is analogous to foldr, but where operations associate to the left rather than the right. For example,

foldr _⊗_ e [ x , y , z ]  =  x ⊗ (y ⊗ (z ⊗ e))
foldl _⊗_ e [ x , y , z ]  =  ((e ⊗ x) ⊗ y) ⊗ z

Exercise foldr-monoid-foldl

Show that if _⊕_ and e form a monoid, then foldr _⊗_ e and foldl _⊗_ e always compute the same result.

Exercise Any-++-⇔ (recommended)

Prove a result similar to All-++-⇔, but with Any in place of All, and a suitable replacement for _×_. As a consequence, demonstrate an equivalence relating _∈_ and _++_.

Exercise All-++-≃ (stretch)

Show that the equivalence All-++-⇔ can be extended to an isomorphism.

Exercise ¬Any≃All¬ (stretch)

First generalise composition to arbitrary levels, using [universe polymorphism][plfa.Equality#unipoly].

_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
  → (B → C) → (A → B) → A → C
(g ∘′ f) x  =  g (f x)

Show that Any and All satisfy a version of De Morgan’s Law.

postulate
  ¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
    → (¬_ ∘′ Any P) xs ≃ All (¬_ ∘′ P) xs

Do we also have the following?

postulate
  ¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
    → (¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs

If so, prove; if not, explain why.

Exercise any? (stretch)

Just as All has analogues all and all? which determine whether a predicate holds for every element of a list, so does Any have analogues any and any? which determine whether a predicates holds for some element of a list. Give their definitions.

Exercise filter? (stretch)

Define the following variant of the traditional filter function on lists, which given a list and a decidable predicate returns all elements of the list satisfying the predicate.

postulate
  filter? : ∀ {A : Set} {P : A → Set}
    → (P? : Decidable P) → List A → ∃[ ys ]( All P ys )