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

Updated exercise in Lists and Assignment3

Browse source
This commit is contained in:
wadler 2019-10-28 16:29:01 +00:00
parent 9f0ae6e4b6
commit c0d9e7851e
1 changed files with 20 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
courses/tspl/2019/Assignment3.lagda.md
View file

@ -220,6 +220,7 @@ replacement for `_×_`. As a consequence, demonstrate an equivalence relating
-- Your code goes here -- Your code goes here
``` ```
#### Exercise `All-++-≃` (stretch) #### Exercise `All-++-≃` (stretch)
Show that the equivalence `All-++-⇔` can be extended to an isomorphism. Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
@ -228,11 +229,12 @@ Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
-- Your code goes here -- Your code goes here
``` ```
#### Exercise `¬Any≃All¬` (recommended)
#### Exercise `¬Any⇔All¬` (recommended)
Show that `Any` and `All` satisfy a version of De Morgan's Law: Show that `Any` and `All` satisfy a version of De Morgan's Law:
(¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs (¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs
(Can you see why it is important that here `_∘_` is generalised (Can you see why it is important that here `_∘_` is generalised
to arbitrary levels, as described in the section on to arbitrary levels, as described in the section on
@ -240,11 +242,26 @@ to arbitrary levels, as described in the section on
Do we also have the following? Do we also have the following?
(¬_ ∘ All P) xs ≃ Any (¬_ ∘ P) xs (¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs
If so, prove; if not, explain why. If so, prove; if not, explain why.
```
-- Your code goes here
```
#### Exercise `¬Any≃All¬` (stretch)
Show that the equivalence `¬Any⇔All¬` can be extended to an isomorphism.
You will need to use extensionality.
```
-- Your code goes here
```
#### Exercise `All-∀` (practice) #### Exercise `All-∀` (practice)
Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`. Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.