michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fixed merge on Lists

Browse source
This commit is contained in:
Philip Wadler 2019-10-14 15:54:59 +01:00
commit d13da5e92c
12 changed files with 737 additions and 94 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
courses/tspl/2019/Assignment1.lagda.md
View file

@ -20,9 +20,13 @@ 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.
```bash
submit tspl cw1 Assignment1.lagda.md
```
Please ensure your files execute correctly under Agda!
## Good Scholarly Practice.
Please remember the University requirement as

3
courses/tspl/2019/Assignment2.lagda.md
View file

@ -20,6 +20,9 @@ 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.
```bash
submit tspl cw2 Assignment2.lagda.md
```
Please ensure your files execute correctly under Agda!

524
courses/tspl/2019/Assignment3.lagda.md Normal file
View file

@ -0,0 +1,524 @@
---
title : "Assignment3: TSPL Assignment 3"
layout : page
permalink : /TSPL/2019/Assignment3/
---
```
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 labelled "(practice)" are included for those who want extra practice.
Submit your homework using the "submit" command.
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](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.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)
```
## Lists
#### Exercise `reverse-++-distrib` (recommended)
Show that the reverse of one list appended to another is the
reverse of the second appended to the reverse of the first:
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:
reverse (reverse xs) ≡ xs
#### Exercise `map-compose` (practice)
Prove that the map of a composition is equal to the composition of two maps:
map (g ∘ f) ≡ map g ∘ map f
The last step of the proof requires extensionality.
#### Exercise `map-++-distribute` (practice)
Prove the following relationship between map and append:
map f (xs ++ ys) ≡ map f xs ++ map f ys
#### Exercise `map-Tree` (practice)
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
```
-- Your code goes here
```
#### 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` (practice)
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` (practice)
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
```
```
-- Your code goes here
```
#### Exercise `map-is-fold-Tree` (practice)
Demonstrate an analogue of `map-is-foldr` for the type of trees.
```
-- Your code goes here
```
#### 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` (practice)
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
```
-- Your code goes here
```
#### Exercise `foldr-monoid-foldl` (practice)
Show that if `_⊗_` and `e` form a monoid, then `foldr _⊗_ e` and
`foldl _⊗_ e` always compute the same result.
```
-- Your code goes here
```
#### 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 `_++_`.
```
-- Your code goes here
```
#### Exercise `All-++-≃` (stretch)
Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
```
-- Your code goes here
```
#### Exercise `¬Any≃All¬` (recommended)
Show that `Any` and `All` satisfy a version of De Morgan's Law:
(¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs
(Can you see why it is important that here `_∘_` is generalised
to arbitrary levels, as described in the section on
[universe polymorphism]({{ site.baseurl }}/Equality/#unipoly)?)
Do we also have the following?
(¬_ ∘ All P) xs ≃ Any (¬_ ∘ P) xs
If so, prove; if not, explain why.
#### Exercise `All-∀` (practice)
Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.
```
-- You code goes here
```
#### Exercise `Any-∃` (practice)
Show that `Any P xs` is isomorphic to `∃[ x ] (x ∈ xs × P x)`.
```
-- You code goes here
```
#### 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 predicate holds
for some element of a list. Give their definitions.
```
-- Your code goes here
```
#### Exercise `filter?` (stretch)
Define the following variant of the traditional `filter` function on lists,
which given a decidable predicate and a list 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. Your definition may use `plus` as
defined earlier.
```
-- Your code goes here
```
#### Exercise `mulᶜ` (practice)
Write out the definition of a lambda term that multiplies
two natural numbers represented as Church numerals. Your
definition may use `plusᶜ` as defined earlier (or may not
— there are nice definitions both ways).
```
-- Your code goes here
```
#### Exercise `primed` (stretch) {#primed}
Some people find it annoying to write `` ` "x" `` instead of `x`.
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 : ⊥
```
We intend to apply the function only when the first term is a variable, which we
indicate by postulating a term `impossible` of the empty type `⊥`. If we use
C-c C-n to normalise the term
ƛ′ two ⇒ two
Agda will return an answer warning us that the impossible has occurred:
⊥-elim (plfa.part2.Lambda.impossible (`` `suc (`suc `zero)) (`suc (`suc `zero)) ``)
While postulating the impossible is a useful technique, it must be
used with care, since such postulation could allow us to provide
evidence of _any_ proposition whatsoever, regardless of its truth.
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.
```
-- Your code goes here
```
#### Exercise `—↠≲—↠′` (practice)
Show that the first notion of reflexive and transitive closure
above embeds into the second. Why are they not isomorphic?
```
-- Your code goes here
```
#### Exercise `plus-example` (practice)
Write out the reduction sequence demonstrating that one plus one is two.
```
-- Your code goes here
```
#### Exercise `Context-≃` (practice)
Show that `Context` is isomorphic to `List (Id × Type)`.
For instance, the isomorphism relates the context
∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ
to the list
[ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ]
```
-- Your code goes here
```
#### Exercise `mul-type` (recommended)
Using the term `mul` you defined earlier, write out the derivation
showing that it is well typed.
```
-- Your code goes here
```
#### Exercise `mulᶜ-type` (practice)
Using the term `mulᶜ` you defined earlier, write out the derivation
showing that it is well typed.
```
-- Your code goes here
```
## Properties
#### Exercise `Progress-≃` (practice)
Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.
```
-- Your code goes here
```
#### Exercise `progress′` (practice)
Write out the proof of `progress′` in full, and compare it to the
proof of `progress` above.
```
-- Your code goes here
```
#### Exercise `value?` (practice)
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.
```
-- Your code goes here
```
#### Exercise `mul-eval` (recommended)
Using the evaluator, confirm that two times two is four.
```
-- Your code goes here
```
#### Exercise: `progress-preservation` (practice)
Without peeking at their statements above, write down the progress
and preservation theorems for the simply typed lambda-calculus.
```
-- Your code goes here
```
#### Exercise `subject_expansion` (practice)
We say that `M` _reduces_ to `N` if `M —→ N`,
but we can also describe the same situation by saying
that `N` _expands_ to `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.
```
-- Your code goes here
```
#### Exercise `stuck` (practice)
Give an example of an ill-typed term that does get stuck.
```
-- Your code goes here
```
#### Exercise `unstuck` (recommended)
Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` above.
```
-- Your code goes here
```

46
courses/tspl/2019/tspl2019.md
View file

@ -13,7 +13,7 @@ permalink : /TSPL/2019/
## Lectures
Lectures take place Monday, Wednesday, and Friday in AT 5.07. (Room provisional.)
Lectures take place Monday, Wednesday, and Friday in AT 5.07.
* **10.00--10.50am** Lecture
* **11.10--12.00noon** Tutorial
@ -47,49 +47,49 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. (Room provisional.
<td>4</td>
<td><b>7 Oct</b> <a href="{{ site.baseurl }}/Quantifiers/">Quantifiers</a></td>
<td><b>9 Oct</b> <a href="{{ site.baseurl }}/Decidable/">Decidable</a></td>
<td><b>11 Oct</b> (tutorial only)</td>
<td><b>11 Oct</b> (tutorial only, 10.00&ndash;10.50)</td>
</tr>
<tr>
<td>5</td>
<td><b>14 Oct</b> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
<td><b>16 Oct</b> <!-- (tutorial only) --></td>
<td><b>18 Oct</b> <!-- <a href="{{ site.baseurl }}/Lists/">Lists</a> --></td>
<td><b>16 Oct</b> <a href="{{ site.baseurl }}/Lambda/">Lambda</a></td>
<td><b>18 Oct</b> <a href="{{ site.baseurl }}/Properties/">Properties</a></td>
</tr>
<tr>
<td>6</td>
<td><b>21 Oct</b> <!-- <a href="{{ site.baseurl }}/Lambda/">Lambda</a> --></td>
<td><b>23 Oct</b> <!-- (no class) --></td>
<td><b>25 Oct</b> <!-- <a href="{{ site.baseurl }}/Properties/">Properties</a> --></td>
<td><b>21 Oct</b> <a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a></td>
<td><b>23 Oct</b> <a href="{{ site.baseurl }}/More/">More</a></td>
<td><b>25 Oct</b> <a href="{{ site.baseurl }}/Inference/">Inference</a></td>
</tr>
<tr>
<td>7</td>
<td><b>28 Oct</b> <!-- <a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a> --></td>
<td><b>30 Oct</b> <!-- <a href="{{ site.baseurl }}/More/">More</a> --></td>
<td><b>1 Nov</b> <!-- <a href="{{ site.baseurl }}/Inference/">Inference</a> --></td>
<td><b>28 Oct</b> <a href="{{ site.baseurl }}/Untyped/">Untyped</a></td>
<td><b>30 Oct</b> (to be decided) </td>
<td><b>1 Nov</b> (no class) </td>
</tr>
<tr>
<td>8</td>
<td><b>4 Nov</b> <!-- (no class) --></td>
<td><b>6 Nov</b> <!-- (tutorial only) --></td>
<td><b>8 Nov</b> <!-- <a href="{{ site.baseurl }}/Untyped/">Untyped</a> --></td>
<td><b>4 Nov</b> (no class) </td>
<td><b>6 Nov</b> (tutorial only) </td>
<td><b>8 Nov</b> (no class) </td>
</tr>
<tr>
<td>9</td>
<td><b>11 Nov</b> <!-- (no class) --></td>
<td><b>13 Nov</b> <!-- (tutorial only) --></td>
<td><b>15 Nov</b> <!-- (no class) --></td>
<td><b>11 Nov</b> (no class) </td>
<td><b>13 Nov</b> (tutorial only) </td>
<td><b>15 Nov</b> (no class) </td>
</tr>
<tr>
<td>10</td>
<td><b>18 Nov</b> <!-- (no class) --></td>
<td><b>20 Nov</b> <!-- Propositions as Types --></td>
<td><b>22 Nov</b> <!-- (no class) --></td>
<td><b>18 Nov</b> (no class) </td>
<td><b>20 Nov</b> Propositions as Types </td>
<td><b>22 Nov</b> (no class) </td>
</tr>
<tr>
<td>11</td>
<td><b>25 Nov</b> <!-- (no class) --></td>
<td><b>27 Nov</b> <!-- Quantitative (Wen)--></td>
<td><b>29 Nov</b> (mock exam)</td>
<td><b>25 Nov</b> (no class) </td>
<td><b>27 Nov</b> Quantitative (Wen) </td>
<td><b>29 Nov</b> (mock exam) </td>
</tr>
</table>
@ -119,7 +119,7 @@ For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.ba
* [Assignment 1]({{ site.baseurl }}/TSPL/2019/Assignment1/) cw1 due 4pm Thursday 3 October (Week 3)
* [Assignment 2]({{ site.baseurl }}/TSPL/2019/Assignment2/) cw2 due 4pm Thursday 17 October (Week 5)
* Assignment 3 <!-- [Assignment 3]({{ site.baseurl }}/TSPL/2019/Assignment3/) --> cw3 due 4pm Thursday 31 October (Week 7)
* [Assignment 3]({{ site.baseurl }}/TSPL/2019/Assignment3/) cw3 due 4pm Thursday 31 October (Week 7)
* Assignment 4 <!-- [Assignment 4]({{ site.baseurl }}/TSPL/2019/Assignment4/) --> cw4 due 4pm Thursday 14 November (Week 9)
* Assignment 5 <!-- [Assignment 5]({{ site.baseurl }}/courses/tspl/2010/Mock1.pdf) --> cw5 due 4pm Thursday 21 November (Week 10)
<!-- <br />

14
exercise.sh
View file

@ -1,14 +0,0 @@
#!/bin/bash
# Script to extract exercises from PLFA chapters, e.g., `src/plfa/part1/Naturals.lagda.md`.
# Usage:
#
# ./exercise.sh [SOURCE] [TARGET]
SRC="$1"
shift
DST="$1"
shift
awk '/^#/{flag=0} /^#### Exercise/{flag=1} flag' "$SRC" > "$DST"

18
extra/extra/Lists.lagda.md Normal file
View file

@ -0,0 +1,18 @@
#### Exercise `Any-∃` (practice)
Show that `Any P xs` is isomorphic to `∃[ x ] (x ∈ xs × P x)`.
```
Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → Any P xs ≃ ∃[ x ] (x ∈ xs × P x)
Any-∃ {A} {P} {xs} = record
{ to = to
; from = {!!}
; from∘to = {!!}
; to∘from = {!!} }
where
to : ∀ {A : Set} {P : A → Set} {xs : List A} → Any P xs → ∃[ x ] (x ∈ xs × P x)
to (here {x = x} px) = ⟨ x , ⟨ here refl , px ⟩ ⟩
to (there anyp) with to anyp
... | ⟨ x , ⟨ x∈xs , px ⟩ ⟩ = ⟨ x , ⟨ there x∈xs , px ⟩ ⟩
```

7
extra/extra/Rec1.agda Normal file
View file

@ -0,0 +1,7 @@
module Rec1 where
import Rec2
y : ℕ
y = x

10
extra/extra/Rec2.agda Normal file
View file

@ -0,0 +1,10 @@
module Rec2 where
open import Data.Nat
open import Rec1
x : ℕ
x = 42
z : ℕ
z = y

91
make_assignment.sh Executable file
View file

@ -0,0 +1,91 @@
#!/bin/bash
# This script can be used to automatically generate assignment files from PLFA source files.
# It takes a course abbreviation, e.g. TSPL, a year, and the number of the assignment.
# At the moment, it outputs the University of Edinburgh guidelines for good scholarly practice,
# making it somewhat specific to courses run there, but the header should be easy to edit.
#
# Usage:
#
# ./make_assignment.sh [COURSE_NAME] [COURSE_YEAR] [ASSIGNMENT_NUMBER] [PLFA_SOURCE_FILE...]
COURSE="$1"
shift
YEAR="$1"
shift
NUM="$1"
shift
## Make assignment header
cat <<-EOF
---
title : "Assignment$NUM: $COURSE Assignment $NUM"
layout : page
permalink : /$COURSE/$YEAR/Assignment$NUM/
---
\`\`\`
module Assignment$NUM 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.
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](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).
EOF
## Make import statements
cat <<-EOF
## Imports
\`\`\`
EOF
for SRC in "$@"; do
AGDA_MODULE=$(eval "echo \"$SRC\" | sed -e \"s|src/||g; s|\\\.lagda\\\.md||g; s|/|\\\.|g;\"")
echo "open import $AGDA_MODULE"
done
cat <<-EOF
\`\`\`
EOF
## Extract exercises
for SRC in "$@"; do
NAME=$(basename "${SRC%.lagda.md}")
cat <<-EOF
## $NAME
EOF
awk '/^#/{flag=0} /^#### Exercise/{flag=1} flag' "$SRC"
done

8
src/plfa/part1/Equality.lagda.md
View file

@ -688,6 +688,14 @@ Before the signature used `Set₁` as the type of a term that includes
`Set`, whereas here the signature uses `Set (lsuc ℓ)` as the type of a
term that includes `Set ℓ`.
Most other functions in the standard library are also generalised to
arbitrary levels. For instance, here is the definition of composition.
```
_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
→ (B → C) → (A → B) → A → C
(g ∘ f) x = g (f x)
```
Further information on levels can be found in the [Agda Wiki][wiki].
[wiki]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism

79
src/plfa/part1/Lists.lagda.md
View file

@ -351,21 +351,15 @@ list, and the sum of the numbers up to `n - 1` is `n * (n - 1) / 2`.
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-++-distrib : ∀ {A : Set} (xs ys : List A)
→ reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
```
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
```
reverse (reverse xs) ≡ xs
## Faster reverse
@ -950,32 +944,41 @@ Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
-- Your code goes here
```
#### Exercise `¬Any≃All¬` (stretch)
First generalise composition to arbitrary levels, using
[universe polymorphism]({{ site.baseurl }}/Equality/#unipoly):
```
_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
→ (B → C) → (A → B) → A → C
(g ∘′ f) x = g (f x)
```
#### Exercise `¬Any≃All¬` (recommended)
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
```
(¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs
(Can you see why it is important that here `_∘_` is generalised
to arbitrary levels, as described in the section on
[universe polymorphism]({{ site.baseurl }}/Equality/#unipoly)?)
Do we also have the following?
```
postulate
¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
→ (¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs
```
(¬_ ∘ All P) xs ≃ Any (¬_ ∘ P) xs
If so, prove; if not, explain why.
#### Exercise `All-∀` (practice)
Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.
```
-- You code goes here
```
#### Exercise `Any-∃` (practice)
Show that `Any P xs` is isomorphic to `∃[ x ] (x ∈ xs × P x)`.
```
-- You code goes here
```
## Decidability of All
If we consider a predicate as a function that yields a boolean,
@ -1026,24 +1029,6 @@ for some element of a list. Give their definitions.
```
#### Exercise `All-∀` (practice)
Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.
```
-- You code goes here
```
#### Exercise `Any-∃` (practice)
Show that `Any P xs` is isomorphic to `∃[ x ∈ xs ] P x`.
```
-- You code goes here
```
#### Exercise `filter?` (stretch)
Define the following variant of the traditional `filter` function on lists,

27
src/plfa/part1/Quantifiers.lagda.md
View file

@ -27,16 +27,23 @@ open import plfa.part1.Isomorphism using (_≃_; extensionality)
## Universals
We formalise universal quantification using the
dependent function type, which has appeared throughout this book.
We formalise universal quantification using the dependent function
type, which has appeared throughout this book. For instance, in
Chapter Induction we showed addition is associative:
Given a variable `x` of type `A` and a proposition `B x` which
contains `x` as a free variable, the universally quantified
proposition `∀ (x : A) → B x` holds if for every term `M` of type
`A` the proposition `B M` holds. Here `B M` stands for
the proposition `B x` with each free occurrence of `x` replaced by
`M`. Variable `x` appears free in `B x` but bound in
`∀ (x : A) → B x`.
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
which asserts for all natural numbers `m`, `n`, and `p`
that `(m + n) + p ≡ m + (n + p)` holds. It is a dependent
function, which given values for `m`, `n`, and `p` returns
evidence for the corresponding equation.
In general, given a variable `x` of type `A` and a proposition `B x`
which contains `x` as a free variable, the universally quantified
proposition `∀ (x : A) → B x` holds if for every term `M` of type `A`
the proposition `B M` holds. Here `B M` stands for the proposition
`B x` with each free occurrence of `x` replaced by `M`. Variable `x`
appears free in `B x` but bound in `∀ (x : A) → B x`.
Evidence that `∀ (x : A) → B x` holds is of the form
@ -371,7 +378,7 @@ restated in this way.
-- Your code goes here
```
#### Exercise `∃-|-≤` (practice)
#### Exercise `∃-+-≤` (practice)
Show that `y ≤ z` holds if and only if there exists a `x` such that
`x + y ≡ z`.