# Assignment3: TSPL Assignment 3

module Assignment3 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.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not) open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n) open import Data.Nat.Properties using (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ) open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩) open import Data.Empty using (⊥; ⊥-elim) open import Function using (_∘_) open import Algebra.Structures using (IsMonoid) open import Level using (Level) open import Relation.Unary using (Decidable) 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; _∈_) open import plfa.part2.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′) open import plfa.part2.Properties hiding (value?; unstuck; preserves; wttdgs)

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

#### Exercise `reverse-involutive`

(recommended)

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

#### Exercise `product`

(recommended)

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 )

## Lambda

#### Exercise `mul`

(recommended)

Write out the definition of a lambda term that multiplies two natural numbers.

#### Exercise `primed`

(stretch)

We can make examples with lambda terms slightly easier to write by adding the following definitions.

ƛ′_⇒_ : Term → Term → Term ƛ′ (` x) ⇒ N = ƛ x ⇒ N ƛ′ _ ⇒ _ = ⊥-elim impossible where postulate impossible : ⊥ case′_[zero⇒_|suc_⇒_] : Term → Term → Term → Term → Term case′ L [zero⇒ M |suc (` x) ⇒ N ] = case L [zero⇒ M |suc x ⇒ N ] case′ _ [zero⇒ _ |suc _ ⇒ _ ] = ⊥-elim impossible where postulate impossible : ⊥ μ′_⇒_ : Term → Term → Term μ′ (` x) ⇒ N = μ x ⇒ N μ′ _ ⇒ _ = ⊥-elim impossible where postulate impossible : ⊥

The definition of `plus`

can now be written as follows.

plus′ : Term plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒ case′ m [zero⇒ n |suc m ⇒ `suc (+ · m · n) ] where + = ` "+" m = ` "m" n = ` "n"

Write out the definition of multiplication in the same style.

#### Exercise `_[_:=_]′`

(stretch)

The definition of substitution above has three clauses (`ƛ`

, `case`

, and `μ`

) that invoke a with clause to deal with bound variables. Rewrite the definition to factor the common part of these three clauses into a single function, defined by mutual recursion with substitution.

#### Exercise `—↠≃—↠′`

Show that the two notions of reflexive and transitive closure above are isomorphic.

#### Exercise `plus-example`

Write out the reduction sequence demonstrating that one plus one is two.

#### Exercise `mul-type`

(recommended)

Using the term `mul`

you defined earlier, write out the derivation showing that it is well-typed.

## Properties

#### Exercise `Progress-≃`

Show that `Progress M`

is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`

.

#### Exercise `progress′`

Write out the proof of `progress′`

in full, and compare it to the proof of `progress`

above.

#### Exercise `value?`

Combine `progress`

and `—→¬V`

to write a program that decides whether a well-typed term is a value.

postulate value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)

#### Exercise `subst′`

(stretch)

Rewrite `subst`

to work with the modified definition `_[_:=_]′`

from the exercise in the previous chapter. As before, this should factor dealing with bound variables into a single function, defined by mutual recursion with the proof that substitution preserves types.

#### Exercise `mul-eval`

(recommended)

Using the evaluator, confirm that two times two is four.

#### Exercise: `progress-preservation`

Without peeking at their statements above, write down the progress and preservation theorems for the simply typed lambda-calculus.

#### Exercise `subject-expansion`

We say that `M`

*reduces* to `N`

if `M —→ N`

, and conversely that `M`

*expands* to `N`

if `N —→ M`

. The preservation property is sometimes called *subject reduction*. Its opposite is *subject expansion*, which holds if `M —→ N`

and `∅ ⊢ N ⦂ A`

imply `∅ ⊢ M ⦂ A`

. Find two counter-examples to subject expansion, one with case expressions and one not involving case expressions.

#### Exercise `stuck`

Give an example of an ill-typed term that does get stuck.

#### Exercise `unstuck`

(recommended)

Provide proofs of the three postulates, `unstuck`

, `preserves`

, and `wttdgs`

above.