From 62f3ccd3bd323b6ab47fc3d07453934d7e402a85 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Fri, 5 Jan 2018 19:30:53 -0200
Subject: [PATCH] PropertiesEx and RelationsEx

---
 src/PropertiesEx.lagda | 72 ++++++++++++++++++++++++++++++++++++++++++
 src/RelationsEx.lagda  | 67 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 139 insertions(+)
 create mode 100644 src/PropertiesEx.lagda
 create mode 100644 src/RelationsEx.lagda

diff --git a/src/PropertiesEx.lagda b/src/PropertiesEx.lagda
new file mode 100644
index 00000000..5e3d321c
--- /dev/null
+++ b/src/PropertiesEx.lagda
@@ -0,0 +1,72 @@
+---
+title     : "Properties Exercises"
+layout    : page
+permalink : /PropertiesEx
+---
+
+\begin{code}
+open import Naturals using (ℕ; suc; zero; _+_; _*_; _∸_)
+open import Properties using (+-assoc; +-comm)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
+
+\end{code}
+
+*Swapping terms*
+
+\begin{code}
++-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
++-swap m n p rewrite sym (+-assoc m n p) | +-comm m n | +-assoc n m p = refl
+\end{code}
+
+*Multiplication distributes over addition*
+
+\begin{code}
+*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
+*-distrib-+ zero n p = refl
+*-distrib-+ (suc m) n p rewrite *-distrib-+ m n p | +-assoc p (m * p) (n * p) = refl
+\end{code}
+
+*Multiplication is associative*
+
+\begin{code}
+*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
+*-assoc zero n p = refl
+*-assoc (suc m) n p rewrite *-distrib-+ n (m * n) p | *-assoc m n p = refl
+\end{code}
+
+*Multiplications is commutative*
+
+\begin{code}
+*-zero : ∀ (n : ℕ) → n * zero ≡ zero
+*-zero zero = refl
+*-zero (suc n) rewrite *-zero n = refl
+
++-*-suc : ∀ (m n : ℕ) → n * suc m ≡ n + n * m
++-*-suc m zero = refl
++-*-suc m (suc n) rewrite +-*-suc m n | +-swap m n (n * m) = refl
+
+*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
+*-comm zero n rewrite *-zero n = refl
+*-comm (suc m) n rewrite +-*-suc m n | *-comm m n = refl
+\end{code}
+
+*Monus from zero*
+
+\begin{code}
+0∸n≡0 : ∀ (n : ℕ) → zero ∸ n ≡ zero
+0∸n≡0 zero = refl
+0∸n≡0 (suc n) = refl
+\end{code}
+
+The proof does not require induction.
+
+*Associativity of monus with addition*
+
+\begin{code}
+∸-+-assoc : ∀ (m n p : ℕ) → (m ∸ n) ∸ p ≡ m ∸ (n + p)
+∸-+-assoc m zero p = refl
+∸-+-assoc zero (suc n) p rewrite 0∸n≡0 p = refl
+∸-+-assoc (suc m) (suc n) p rewrite ∸-+-assoc m n p = refl
+\end{code}
+
+
diff --git a/src/RelationsEx.lagda b/src/RelationsEx.lagda
new file mode 100644
index 00000000..fab5c79a
--- /dev/null
+++ b/src/RelationsEx.lagda
@@ -0,0 +1,67 @@
+---
+title     : "Relations Exercises"
+layout    : page
+permalink : /RelationsEx
+---
+
+## Imports
+
+\begin{code}
+open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_)
+open import Relations using (_≤_; _<_; Trichotomy; even; odd)
+open import Properties using (+-comm; +-identity; +-suc)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
+open import Data.Product using (∃; _,_)
+open Trichotomy
+open _<_
+open _≤_
+open even
+open odd
+\end{code}
+
+*Trichotomy*
+
+\begin{code}
+trichotomy : ∀ (m n : ℕ) → Trichotomy m n
+trichotomy zero zero = same refl
+trichotomy zero (suc n) = less z<s
+trichotomy (suc m) zero = more z<s
+trichotomy (suc m) (suc n) with trichotomy m n
+... | less m<n = less (s<s m<n)
+... | same refl = same refl
+... | more n<m = more (s<s n<m)
+\end{code}
+
+*Relate strict comparison to comparison*
+
+\begin{code}
+<-implies-≤ : ∀ {m n : ℕ} → m < n → suc m ≤ n
+<-implies-≤ z<s = s≤s z≤n
+<-implies-≤ (s<s m<n) = s≤s (<-implies-≤ m<n)
+
+≤-implies-< : ∀ {m n : ℕ} → suc m ≤ n → m < n
+≤-implies-< (s≤s z≤n) = z<s
+≤-implies-< (s≤s (s≤s m≤n)) = s<s (≤-implies-< (s≤s m≤n))
+\end{code}
+
+*Even and odd*
+
+\begin{code}
++-lemma : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + (suc m + 0)
++-lemma m rewrite +-identity m | +-suc m m = refl
+
++-lemma′ : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + (suc m + 0)
++-lemma′ m rewrite +-suc m (m + 0) = {!!}
+
+mutual
+  is-even : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m)
+  is-even zero zero =  zero , refl
+  is-even (suc n) (suc oddn) with is-odd n oddn
+  ... | m , n≡1+2*m rewrite n≡1+2*m | +-lemma m = suc m , refl
+
+  is-odd : ∀ (n : ℕ) → odd n → ∃(λ (m : ℕ) → n ≡ 1 + 2 * m)
+  is-odd (suc n) (suc evenn) with is-even n evenn
+  ... | m , n≡2*m rewrite n≡2*m = m , refl
+\end{code}
+
+