Added (practice) label to unlabeled exercises

src/plfa/part1/Connectives.lagda.md

@@ -431,7 +431,7 @@ Show sum is commutative up to isomorphism.
 -- Your code goes here
 ```
 
-#### Exercise `⊎-assoc`
+#### Exercise `⊎-assoc` (practice)
 
 Show sum is associative up to isomorphism.
 
@@ -502,7 +502,7 @@ Show empty is the left identity of sums up to isomorphism.
 -- Your code goes here
 ```
 
-#### Exercise `⊥-identityʳ`
+#### Exercise `⊥-identityʳ` (practice)
 
 Show empty is the right identity of sums up to isomorphism.
 
@@ -742,7 +742,7 @@ distributive law, and explain how it relates to the weak version.
 ```
 
 
-#### Exercise `⊎×-implies-×⊎`
+#### Exercise `⊎×-implies-×⊎` (practice)
 
 Show that a disjunct of conjuncts implies a conjunct of disjuncts:
 ```

src/plfa/part1/Decidable.lagda.md

@@ -303,7 +303,7 @@ postulate
 -- Your code goes here
 ```
 
-#### Exercise `_≡ℕ?_`
+#### Exercise `_≡ℕ?_` (practice)
 
 Define a function to decide whether two naturals are equal:
 ```
@@ -535,7 +535,7 @@ indicating that the order of the equations determines which of the
 first or the second can match.  This time the answer is different depending
 on which matches; but either is equally valid.
 
-#### Exercise `erasure`
+#### Exercise `erasure` (practice)
 
 Show that erasure relates corresponding boolean and decidable operations:
 ```

src/plfa/part1/Induction.lagda.md

@@ -71,7 +71,7 @@ distributes over another operator.  A careful author will often call
 out these properties---or their lack---for instance by pointing out
 that a newly introduced operator is associative but not commutative.
 
-#### Exercise `operators` {#operators}
+#### Exercise `operators` (practice) {#operators}
 
 Give another example of a pair of operators that have an identity
 and are associative, commutative, and distribute over one another.
@@ -900,7 +900,7 @@ for all naturals `m`, `n`, and `p`.
 ```
 
 
-#### Exercise `*-comm` {#times-comm}
+#### Exercise `*-comm` (practice) {#times-comm}
 
 Show multiplication is commutative, that is,
 
@@ -914,7 +914,7 @@ you will need to formulate and prove suitable lemmas.
 ```
 
 
-#### Exercise `0∸n≡0` {#zero-monus}
+#### Exercise `0∸n≡0` (practice) {#zero-monus}
 
 Show
 
@@ -927,7 +927,7 @@ for all naturals `n`. Did your proof require induction?
 ```
 
 
-#### Exercise `∸-|-assoc` {#monus-plus-assoc}
+#### Exercise `∸-|-assoc` (practice) {#monus-plus-assoc}
 
 Show that monus associates with addition, that is,
 

src/plfa/part1/Isomorphism.lagda.md

@@ -436,7 +436,7 @@ module ≲-Reasoning where
 open ≲-Reasoning
 ```
 
-#### Exercise `≃-implies-≲`
+#### Exercise `≃-implies-≲` (practice)
 
 Show that every isomorphism implies an embedding.
 ```
@@ -451,7 +451,7 @@ postulate
 -- Your code goes here
 ```
 
-#### Exercise `_⇔_` {#iff}
+#### Exercise `_⇔_` (practice) {#iff}
 
 Define equivalence of propositions (also known as "if and only if") as follows:
 ```

src/plfa/part1/Lists.lagda.md

@@ -525,7 +525,7 @@ parameterised on _n_ types will have a map that is parameterised on
 _n_ functions.
 
 
-#### Exercise `map-compose`
+#### Exercise `map-compose` (practice)
 
 Prove that the map of a composition is equal to the composition of two maps:
 ```
@@ -535,7 +535,7 @@ postulate
 ```
 The last step of the proof requires extensionality.
 
-#### Exercise `map-++-commute`
+#### Exercise `map-++-commute` (practice)
 
 Prove the following relationship between map and append:
 ```
@@ -544,7 +544,7 @@ postulate
    →  map f (xs ++ ys) ≡ map f xs ++ map f ys
 ```
 
-#### Exercise `map-Tree`
+#### Exercise `map-Tree` (practice)
 
 Define a type of trees with leaves of type `A` and internal
 nodes of type `B`:
@@ -640,7 +640,7 @@ postulate
 ```
 
 
-#### Exercise `map-is-foldr`
+#### Exercise `map-is-foldr` (practice)
 
 Show that map can be defined using fold:
 ```
@@ -650,7 +650,7 @@ postulate
 ```
 This requires extensionality.
 
-#### Exercise `fold-Tree`
+#### Exercise `fold-Tree` (practice)
 
 Define a suitable fold function for the type of trees given earlier:
 ```
@@ -663,7 +663,7 @@ postulate
 -- Your code goes here
 ```
 
-#### Exercise `map-is-fold-Tree`
+#### Exercise `map-is-fold-Tree` (practice)
 
 Demonstrate an analogue of `map-is-foldr` for the type of trees.
 
@@ -781,7 +781,7 @@ foldr-monoid-++ _⊗_ e monoid-⊗ xs ys =
   ∎
 ```
 
-#### Exercise `foldl`
+#### 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:
@@ -794,7 +794,7 @@ operations associate to the left rather than the right.  For example:
 ```
 
 
-#### Exercise `foldr-monoid-foldl`
+#### Exercise `foldr-monoid-foldl` (practice)
 
 Show that if `_⊗_` and `e` form a monoid, then `foldr _⊗_ e` and
 `foldl _⊗_ e` always compute the same result.
@@ -1005,7 +1005,7 @@ for some element of a list.  Give their definitions.
 ```
 
 
-#### Exercise `All-∀`
+#### Exercise `All-∀` (practice)
 
 Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.
 
@@ -1014,7 +1014,7 @@ Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.
 ```
 
 
-#### Exercise `Any-∃`
+#### Exercise `Any-∃` (practice)
 
 Show that `Any P xs` is isomorphic to `∃[ x ∈ xs ] P x`.
 

src/plfa/part1/Naturals.lagda.md

@@ -76,7 +76,7 @@ after zero; and `2` is shorthand for `suc (suc zero)`, which is the
 same as `suc 1`, the successor of one; and `3` is shorthand for the
 successor of two; and so on.
 
-#### Exercise `seven` {#seven}
+#### Exercise `seven` (practice) {#seven}
 
 Write out `7` in longhand.
 
@@ -426,7 +426,7 @@ is not like testimony in a court which must be weighed to determine
 whether the witness is trustworthy.  Rather, it is ironclad.  The
 other word for evidence, which we will use interchangeably, is _proof_.
 
-#### Exercise `+-example` {#plus-example}
+#### Exercise `+-example` (practice) {#plus-example}
 
 Compute `3 + 4`, writing out your reasoning as a chain of equations.
 
@@ -487,7 +487,7 @@ Here we have omitted the signature declaring `_ : 2 * 3 ≡ 6`, since
 it can easily be inferred from the corresponding term.
 
 
-#### Exercise `*-example` {#times-example}
+#### Exercise `*-example` (practice) {#times-example}
 
 Compute `3 * 4`, writing out your reasoning as a chain of equations.
 

src/plfa/part1/Negation.lagda.md

@@ -197,7 +197,7 @@ is irreflexive, that is, `n < n` holds for no `n`.
 ```
 
 
-#### Exercise `trichotomy`
+#### Exercise `trichotomy` (practice)
 
 Show that strict inequality satisfies
 [trichotomy]({{ site.baseurl }}/Relations/#trichotomy),

src/plfa/part1/Quantifiers.lagda.md

@@ -92,7 +92,7 @@ postulate
 Compare this with the result (`→-distrib-×`) in
 Chapter [Connectives]({{ site.baseurl }}/Connectives/).
 
-#### Exercise `⊎∀-implies-∀⊎`
+#### Exercise `⊎∀-implies-∀⊎` (practice)
 
 Show that a disjunction of universals implies a universal of disjunctions:
 ```
@@ -103,7 +103,7 @@ postulate
 Does the converse hold? If so, prove; if not, explain why.
 
 
-#### Exercise `∀-×`
+#### Exercise `∀-×` (practice)
 
 Consider the following type.
 ```
@@ -244,7 +244,7 @@ postulate
     ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
 ```
 
-#### Exercise `∃×-implies-×∃`
+#### Exercise `∃×-implies-×∃` (practice)
 
 Show that an existential of conjunctions implies a conjunction of existentials:
 ```
@@ -254,7 +254,7 @@ postulate
 ```
 Does the converse hold? If so, prove; if not, explain why.
 
-#### Exercise `∃-⊎`
+#### Exercise `∃-⊎` (practice)
 
 Let `Tri` and `B` be as in Exercise `∀-×`.
 Show that `∃[ x ] B x` is isomorphic to `B aa ⊎ B bb ⊎ B cc`.
@@ -361,7 +361,7 @@ follows by `odd-suc`.
 
 This completes the proof in the backward direction.
 
-#### Exercise `∃-even-odd`
+#### Exercise `∃-even-odd` (practice)
 
 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
@@ -371,7 +371,7 @@ restated in this way.
 -- Your code goes here
 ```
 
-#### Exercise `∃-|-≤`
+#### Exercise `∃-|-≤` (practice)
 
 Show that `y ≤ z` holds if and only if there exists a `x` such that
 `x + y ≡ z`.

src/plfa/part1/Relations.lagda.md

@@ -229,7 +229,7 @@ lack---for instance by saying that a newly introduced relation is a
 partial order but not a total order.
 
 
-#### Exercise `orderings` {#orderings}
+#### Exercise `orderings` (practice) {#orderings}
 
 Give an example of a preorder that is not a partial order.
 
@@ -347,7 +347,7 @@ and `suc n ≤ suc m` and must show `suc m ≡ suc n`.  The inductive
 hypothesis `≤-antisym m≤n n≤m` establishes that `m ≡ n`, and our goal
 follows by congruence.
 
-#### Exercise `≤-antisym-cases` {#leq-antisym-cases}
+#### Exercise `≤-antisym-cases` (practice) {#leq-antisym-cases}
 
 The above proof omits cases where one argument is `z≤n` and one
 argument is `s≤s`.  Why is it ok to omit them?
@@ -593,7 +593,7 @@ Show that strict inequality is transitive.
 -- Your code goes here
 ```
 
-#### Exercise `trichotomy` {#trichotomy}
+#### Exercise `trichotomy` (practice) {#trichotomy}
 
 Show that strict inequality satisfies a weak version of trichotomy, in
 the sense that for any `m` and `n` that one of the following holds:
@@ -611,7 +611,7 @@ similar to that used for totality.
 -- Your code goes here
 ```
 
-#### Exercise `+-mono-<` {#plus-mono-less}
+#### Exercise `+-mono-<` (practice) {#plus-mono-less}
 
 Show that addition is monotonic with respect to strict inequality.
 As with inequality, some additional definitions may be required.
@@ -628,7 +628,7 @@ Show that `suc m ≤ n` implies `m < n`, and conversely.
 -- Your code goes here
 ```
 
-#### Exercise `<-trans-revisited` {#less-trans-revisited}
+#### Exercise `<-trans-revisited` (practice) {#less-trans-revisited}
 
 Give an alternative proof that strict inequality is transitive,
 using the relation between strict inequality and inequality and

src/plfa/part2/BigStep.lagda.md

@@ -120,7 +120,7 @@ data _⊢_⇓_ : ∀{Γ} → ClosEnv Γ → (Γ ⊢ ★) → Clos → Set where
   call-by-value.
 
 
-#### Exercise `big-step-eg`
+#### Exercise `big-step-eg` (practice)
 
 Show that `(ƛ ƛ # 1) · ((ƛ # 0 · # 0) · (ƛ # 0 · # 0))`
 terminates under big-step call-by-name evaluation.
@@ -374,7 +374,7 @@ cbn→reduce {M}{Δ}{δ}{N′} M⇓c
     ⟨ subst (exts σ) N′ , rs ⟩
 ```
 
-#### Exercise `big-alt-implies-multi`
+#### Exercise `big-alt-implies-multi` (practice)
 
 Formulate an alternative big-step semantics, of the form `M ↓ N`,
 for call-by-name that uses substitution instead of environments.

src/plfa/part2/Bisimulation.lagda.md

@@ -169,7 +169,7 @@ However, leaving the simulation small let's us focus on the essence.
 It's a handy technical trick that we can have a large source language,
 but only bother to include in the simulation the terms of interest.
 
-#### Exercise `_†`
+#### Exercise `_†` (practice)
 
 Formalise the translation from source to target given in the introduction.
 Show that `M † ≡ N` implies `M ~ N`, and conversely.
@@ -198,7 +198,7 @@ commutes with values.  That is, if `M ~ M†` and `M` is a value then
 It is a straightforward case analysis, where here the only value
 of interest is a lambda abstraction.
 
-#### Exercise `~val⁻¹`
+#### Exercise `~val⁻¹` (practice)
 
 Show that this also holds in the reverse direction: if `M ~ M†`
 and `Value M†` then `Value M`.
@@ -456,7 +456,7 @@ In its structure, it looks a little bit like a proof of progress:
     we have `N [ x := V ] ~ N† [ x := V† ]`.
 
 
-#### Exercise `sim⁻¹`
+#### Exercise `sim⁻¹` (practice)
 
 Show that we also have a simulation in the other direction, and hence that we have
 a bisimulation.
@@ -465,7 +465,7 @@ a bisimulation.
 -- Your code goes here
 ```
 
-#### Exercise `products`
+#### Exercise `products` (practice)
 
 Show that the two formulations of products in
 Chapter [More]({{ site.baseurl }}/More/)

src/plfa/part2/Confluence.lagda.md

@@ -141,7 +141,7 @@ data _⇛*_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
 ```
 
 
-#### Exercise `par-diamond-eg`
+#### Exercise `par-diamond-eg` (practice)
 
 Revisit the counter example to the diamond property for reduction by
 showing that the diamond property holds for parallel reduction in that

src/plfa/part2/DeBruijn.lagda.md

@@ -966,7 +966,7 @@ Substitution preserves types, and Preservation.
 We now turn to proving the remaining results from the
 previous development.
 
-#### Exercise `V¬—→`
+#### Exercise `V¬—→` (practice)
 
 Following the previous development, show values do
 not reduce, and its corollary, terms that reduce are not

src/plfa/part2/Lambda.lagda.md

@@ -196,7 +196,7 @@ defined earlier.
 ```
 
 
-#### Exercise `mulᶜ`
+#### Exercise `mulᶜ` (practice)
 
 Write out the definition of a lambda term that multiplies
 two natural numbers represented as Church numerals. Your
@@ -740,7 +740,7 @@ The three constructors specify, respectively, that `—↠′` includes `—→`
 and is reflexive and transitive.  A good exercise is to show that
 the two definitions are equivalent (indeed, one embeds in the other).
 
-#### Exercise `—↠≲—↠′`
+#### Exercise `—↠≲—↠′` (practice)
 
 Show that the first notion of reflexive and transitive closure
 above embeds into the second. Why are they not isomorphic?
@@ -901,7 +901,7 @@ _ =
 In the next chapter, we will see how to compute such reduction sequences.
 
 
-#### Exercise `plus-example`
+#### Exercise `plus-example` (practice)
 
 Write out the reduction sequence demonstrating that one plus one is two.
 
@@ -1002,7 +1002,7 @@ data Context : Set where
 ```
 
 
-#### Exercise `Context-≃`
+#### Exercise `Context-≃` (practice)
 
 Show that `Context` is isomorphic to `List (Id × Type)`.
 For instance, the isomorphism relates the context
@@ -1381,7 +1381,7 @@ showing that it is well typed.
 ```
 
 
-#### Exercise `mulᶜ-type`
+#### Exercise `mulᶜ-type` (practice)
 
 Using the term `mulᶜ` you defined earlier, write out the derivation
 showing that it is well typed.

src/plfa/part2/More.lagda.md

@@ -1199,7 +1199,7 @@ _ =
    ∎
 ```
 
-#### Exercise `More`
+#### Exercise `More` (practice)
 
 Formalise the remaining constructs defined in this chapter.
 Make your changes in this file.

src/plfa/part2/Properties.lagda.md

@@ -332,7 +332,7 @@ this requires that we match against the lambda expression `L` to
 determine its bound variable and body, `ƛ x ⇒ N`, so we can show that
 `L · M` reduces to `N [ x := M ]`.
 
-#### Exercise `Progress-≃`
+#### Exercise `Progress-≃` (practice)
 
 Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.
 
@@ -340,7 +340,7 @@ Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.
 -- Your code goes here
 ```
 
-#### Exercise `progress′`
+#### Exercise `progress′` (practice)
 
 Write out the proof of `progress′` in full, and compare it to the
 proof of `progress` above.
@@ -349,7 +349,7 @@ proof of `progress` above.
 -- Your code goes here
 ```
 
-#### Exercise `value?`
+#### Exercise `value?` (practice)
 
 Combine `progress` and `—→¬V` to write a program that decides
 whether a well-typed term is a value:
@@ -1276,7 +1276,7 @@ Using the evaluator, confirm that two times two is four.
 ```
 
 
-#### Exercise: `progress-preservation`
+#### Exercise: `progress-preservation` (practice)
 
 Without peeking at their statements above, write down the progress
 and preservation theorems for the simply typed lambda-calculus.
@@ -1286,7 +1286,7 @@ and preservation theorems for the simply typed lambda-calculus.
 ```
 
 
-#### Exercise `subject_expansion`
+#### Exercise `subject_expansion` (practice)
 
 We say that `M` _reduces_ to `N` if `M —→ N`,
 but we can also describe the same situation by saying
@@ -1353,7 +1353,7 @@ Milner, who used denotational rather than operational semantics. He
 introduced `wrong` as the denotation of a term with a type error, and
 showed _well-typed terms don't go wrong_.)
 
-#### Exercise `stuck`
+#### Exercise `stuck` (practice)
 
 Give an example of an ill-typed term that does get stuck.
 

src/plfa/part2/Untyped.lagda.md

@@ -99,7 +99,7 @@ data Type : Set where
   ★ : Type
 ```
 
-#### Exercise (`Type≃⊤`)
+#### Exercise (`Type≃⊤`) (practice)
 
 Show that `Type` is isomorphic to `⊤`, the unit type.
 
@@ -118,7 +118,7 @@ data Context : Set where
 ```
 We let `Γ` and `Δ` range over contexts.
 
-#### Exercise (`Context≃ℕ`)
+#### Exercise (`Context≃ℕ`) (practice)
 
 Show that `Context` is isomorphic to `ℕ`.
 
@@ -402,7 +402,7 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
     → ƛ N —→ ƛ N′
 ```
 
-#### Exercise (`variant-1`)
+#### Exercise (`variant-1`) (practice)
 
 How would the rules change if we want call-by-value where terms
 normalise completely?  Assume that `β` should not permit reduction
@@ -412,7 +412,7 @@ unless both terms are in normal form.
 -- Your code goes here
 ```
 
-#### Exercise (`variant-2`)
+#### Exercise (`variant-2`) (practice)
 
 How would the rules change if we want call-by-value where terms
 do not reduce underneath lambda?  Assume that `β`
@@ -738,7 +738,7 @@ Because `` `suc `` is now a defined term rather than primitive,
 it is no longer the case that `plus · two · two` reduces to `four`,
 but they do both reduce to the same normal term.
 
-#### Exercise `plus-eval`
+#### Exercise `plus-eval` (practice)
 
 Use the evaluator to confirm that `plus · two · two` and `four`
 normalise to the same term.

src/plfa/part3/Denotational.lagda.md

@@ -500,7 +500,7 @@ arguments.
 ↦-elim2 d₁ d₂ lt = ↦-elim d₁ (sub d₂ lt)
 ```
 
-#### Exercise `denot-plusᶜ`
+#### Exercise `denot-plusᶜ` (practice)
 
 What is a denotation for `plusᶜ`? That is, find a value `v` (other than `⊥`)
 such that `∅ ⊢ plusᶜ ↓ v`. Also, give the proof of `∅ ⊢ plusᶜ ↓ v`