From 85312c0f0083fd7250cd4da341e30a8dad94727a Mon Sep 17 00:00:00 2001 From: wadler Date: Tue, 2 Jan 2018 19:47:04 -0200 Subject: [PATCH] added Exercises --- src/Exercises.lagda | 73 ++++++++++++++++++++++++++++++++++++++++++++ src/Properties.lagda | 10 ++++-- 2 files changed, 80 insertions(+), 3 deletions(-) create mode 100644 src/Exercises.lagda diff --git a/src/Exercises.lagda b/src/Exercises.lagda new file mode 100644 index 00000000..45852c45 --- /dev/null +++ b/src/Exercises.lagda @@ -0,0 +1,73 @@ +--- +title : "Exercises: Exercises" +layout : page +permalink : /Exercises +--- + +## Imports + +\begin{code} +open import Data.Nat using (ℕ; suc; zero; _+_; _*_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym) +\end{code} + +## Exercises + +\begin{code} +_∸_ : ℕ → ℕ → ℕ +m ∸ zero = m -- (vii) +zero ∸ (suc n) = zero -- (viii) +(suc m) ∸ (suc n) = m ∸ n -- (ix) + +infixl 6 _∸_ + +assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p) +assoc+ zero n p = refl +assoc+ (suc m) n p rewrite assoc+ m n p = refl + +com+zero : ∀ (n : ℕ) → n + zero ≡ n +com+zero zero = refl +com+zero (suc n) rewrite com+zero n = refl + +com+suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m) +com+suc m zero = refl +com+suc m (suc n) rewrite com+suc m n = refl + +com+ : ∀ (m n : ℕ) → m + n ≡ n + m +com+ zero n rewrite com+zero n = refl +com+ (suc m) n rewrite com+suc m n | com+ m n = refl + +dist*+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p +dist*+ zero n p = refl +dist*+ (suc m) n p rewrite dist*+ m n p | assoc+ p (m * p) (n * p) = refl + +assoc* : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p) +assoc* zero n p = refl +assoc* (suc m) n p rewrite dist*+ n (m * n) p | assoc* m n p = refl + +com*zero : ∀ (n : ℕ) → n * zero ≡ zero +com*zero zero = refl +com*zero (suc n) rewrite com*zero n = refl + +swap+ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p) +swap+ m n p rewrite sym (assoc+ m n p) | com+ m n | assoc+ n m p = refl + +com*suc : ∀ (m n : ℕ) → n * suc m ≡ n + n * m +com*suc m zero = refl +com*suc m (suc n) rewrite com*suc m n | swap+ m n (n * m) = refl + +com* : ∀ (m n : ℕ) → m * n ≡ n * m +com* zero n rewrite com*zero n = refl +com* (suc m) n rewrite com*suc m n | com* m n = refl + +zero∸ : ∀ (n : ℕ) → zero ∸ n ≡ zero +zero∸ zero = refl +zero∸ (suc n) = refl + +assoc∸ : ∀ (m n p : ℕ) → (m ∸ n) ∸ p ≡ m ∸ (n + p) +assoc∸ m zero p = refl +assoc∸ zero (suc n) p rewrite zero∸ p = refl +assoc∸ (suc m) (suc n) p rewrite assoc∸ m n p = refl +\end{code} + + diff --git a/src/Properties.lagda b/src/Properties.lagda index 4db9e72e..aca3a909 100644 --- a/src/Properties.lagda +++ b/src/Properties.lagda @@ -229,9 +229,9 @@ induction hypothesis. We encode this proof in Agda as follows. \begin{code} --- assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p) --- assoc+ zero n p = refl --- assoc+ (suc m) n p rewrite assoc+ m n p = refl +assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p) +assoc+ zero n p = refl +assoc+ (suc m) n p rewrite assoc+ m n p = refl \end{code} Here we have named the proof `assoc+`. In Agda, identifiers can consist of any sequence of characters not including spaces or the characters `@.(){};_`. @@ -564,6 +564,7 @@ com+suc m (suc n) rewrite com+suc m n = refl com : ∀ (m n : ℕ) → m + n ≡ n + m com zero n rewrite com+zero n = refl com (suc m) n rewrite com+suc m n | com m n = refl + \end{code} Here we have renamed Lemma (x) and (xi) to `com+zero` and `com+suc`, respectively. In the final line, rewriting with two equations @@ -571,6 +572,9 @@ respectively. In the final line, rewriting with two equations separating the two proofs of the relevant equations by a vertical bar; the rewrites on the left is performed before that on the right. +## Exercises + +