From 29dc9321d8f809ec6ab7e36782d417d063af79a2 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Tue, 21 Jan 2020 17:03:56 +0000 Subject: [PATCH] Minor clarifications on exercises in Naturals and Induction. --- src/plfa/part1/Induction.lagda.md | 12 +++++------- src/plfa/part1/Naturals.lagda.md | 7 ++++--- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md index d57c5e97..e7466153 100644 --- a/src/plfa/part1/Induction.lagda.md +++ b/src/plfa/part1/Induction.lagda.md @@ -75,13 +75,11 @@ that a newly introduced operator is associative but not commutative. Give another example of a pair of operators that have an identity and are associative, commutative, and distribute over one another. +(You do not have to prove these properties.) Give an example of an operator that has an identity and is associative but is not commutative. - -``` --- Your code goes here -``` +(You do not have to prove these properties.) ## Associativity @@ -944,9 +942,9 @@ for all naturals `m`, `n`, and `p`. Show the following three laws - m ^ (n + p) ≡ (m ^ n) * (m ^ p) - (m * n) ^ p ≡ (m ^ p) * (n ^ p) - m ^ (n * p) ≡ (m ^ n) ^ p + m ^ (n + p) ≡ (m ^ n) * (m ^ p) (^-distribˡ-+-*) + (m * n) ^ p ≡ (m ^ p) * (n ^ p) (^-distribʳ-*) + (m ^ n) ^ p ≡ m ^ (n * p) (^-*-assoc) for all `m`, `n`, and `p`. diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index 73ff4824..694e3f0c 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -428,7 +428,7 @@ other word for evidence, which we will use interchangeably, is _proof_. #### Exercise `+-example` (practice) {#plus-example} -Compute `3 + 4`, writing out your reasoning as a chain of equations. +Compute `3 + 4`, writing out your reasoning as a chain of equations, using the equations for `+`. ``` -- Your code goes here @@ -489,7 +489,8 @@ it can easily be inferred from the corresponding term. #### Exercise `*-example` (practice) {#times-example} -Compute `3 * 4`, writing out your reasoning as a chain of equations. +Compute `3 * 4`, writing out your reasoning as a chain of equations, using the equations for `*`. +(You do not need to step through the evaluation of `+`.) ``` -- Your code goes here @@ -566,7 +567,7 @@ _ = ∎ ``` -#### Exercise `∸-examples` (recommended) {#monus-examples} +#### Exercise `∸-example₁` and `∸-example₂` (recommended) {#monus-examples} Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.