From cf7a6b5c56a6e780c73a554e09e34bbc14e86c5c Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Tue, 9 Jan 2018 14:45:11 -0200
Subject: [PATCH] added trial of Reasoning

---
 src/Logic.lagda          | 14 +++----
 src/Properties.lagda     | 26 ++++++------
 src/Relations.lagda      | 12 +++---
 src/RelationsEx.lagda    | 22 +++++++++--
 src/extra/EvenOdd.agda   |  6 +--
 src/extra/Reasoning.agda | 85 ++++++++++++++++++++++++++++++++++++++++
 6 files changed, 133 insertions(+), 32 deletions(-)
 create mode 100644 src/extra/Reasoning.agda

diff --git a/src/Logic.lagda b/src/Logic.lagda
index 38b38661..804df96a 100644
--- a/src/Logic.lagda
+++ b/src/Logic.lagda
@@ -68,11 +68,11 @@ and `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
 Distribution of `×` over `⊎` is an isomorphism.
 \begin{code}
 data _≃_ : Set → Set → Set where
-  iso : ∀ {A B : Set} → (f : A → B) → (g : B → A) →
+  mk-≃ : ∀ {A B : Set} → (f : A → B) → (g : B → A) →
           (∀ (x : A) → g (f x) ≡ x) → (∀ (y : B) → f (g y) ≡ y) → A ≃ B
 
 ×-distributes-+ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C))
-×-distributes-+ = iso f g gf fg
+×-distributes-+ = mk-≃ f g gf fg
   where
 
   f : ∀ {A B C : Set} → (A ⊎ B) × C → (A × C) ⊎ (B × C)
@@ -94,12 +94,12 @@ data _≃_ : Set → Set → Set where
 
 Distribution of `⊎` over `×` is half an isomorphism.
 \begin{code}
-data _≃ʳ_ : Set → Set → Set where
-  isoʳ : ∀ {A B : Set} → (f : A → B) → (g : B → A) →
-          (∀ (x : A) → g (f x) ≡ x) → A ≃ʳ B
+data _≲_ : Set → Set → Set where
+  mk-≲ : ∀ {A B : Set} → (f : A → B) → (g : B → A) →
+          (∀ (x : A) → g (f x) ≡ x) → A ≲ B
 
-+-distributes-× : ∀ {A B C : Set} → ((A × B) ⊎ C) ≃ʳ ((A ⊎ C) × (B ⊎ C))
-+-distributes-× =  isoʳ f g gf
++-distributes-× : ∀ {A B C : Set} → ((A × B) ⊎ C) ≲ ((A ⊎ C) × (B ⊎ C))
++-distributes-× =  mk-≲ f g gf
   where
 
   f : ∀ {A B C : Set} → (A × B) ⊎ C → (A ⊎ C) × (B ⊎ C)
diff --git a/src/Properties.lagda b/src/Properties.lagda
index 3bf164a6..33b03933 100644
--- a/src/Properties.lagda
+++ b/src/Properties.lagda
@@ -518,27 +518,27 @@ QED.
 
 Lemma (xi).
 
-    n + suc m ≡ suc (n + m)
+    m + suc n ≡ suc (m + n)
 
-Proof. By induction on `n`.
+Proof. By induction on `m`.
 
 Base case.
 
-       zero + suc m
+       zero + suc n
     ≡    (i)
-       suc m
+       suc n
     ≡    (i)
-       suc (zero + m)
+       suc (zero + n)
 
 Inductive case.
 
-       suc n + suc m
+       suc m + suc n
     ≡    (ii)
-       suc (n + suc m)
+       suc (m + suc n)
     ≡    (inductive hypothesis)
-       suc (suc (n + m))
+       suc (suc (m + n))
     ≡    (ii)
-       suc (suc n + m)
+       suc (suc m + n)
 
 QED.
 
@@ -550,13 +550,13 @@ These proofs can be encoded concisely in Agda.
 +-identity zero = refl
 +-identity (suc n) rewrite +-identity n = refl
 
-+-suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m)
-+-suc m zero = refl
-+-suc m (suc n) rewrite +-suc m n = refl
++-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
++-suc zero n = refl
++-suc (suc m) n rewrite +-suc m n = refl
 
 +-comm : ∀ (m n : ℕ) → m + n ≡ n + m
 +-comm zero n rewrite +-identity n = refl
-+-comm (suc m) n rewrite +-suc m n | +-comm m n = refl
++-comm (suc m) n rewrite +-suc n m | +-comm m n = refl
 \end{code}
 Here we have renamed Lemma (x) and (xi) to `+-identity` and `+-suc`,
 respectively.  In the final line, rewriting with two equations is
diff --git a/src/Relations.lagda b/src/Relations.lagda
index 1d06910d..7d0efb16 100644
--- a/src/Relations.lagda
+++ b/src/Relations.lagda
@@ -457,17 +457,17 @@ data Trichotomy : ℕ → ℕ → Set where
 
 + *Even and odd* Another example of a useful relation is to define
   even and odd numbers, as done below.  Using these definitions, show
-  that if `n` is even then there exists an `m` such that `n ≡ 2 * m`,
-  and if `n` is odd then there exists an `m` such that `n ≡ 2 * m + 1`.
-  (This exercise requires existentials from the chapter on Logic.)
+  - the sum of two even numbers is even
+  - the sum of an even and an odd number is odd
+  - the sum of two odd numbers is even
 
 \begin{code}
 mutual
   data even : ℕ → Set where
-    zero : even zero
-    suc : ∀ {n : ℕ} → odd n → even (suc n)
+    ev-zero : even zero
+    ev-suc : ∀ {n : ℕ} → odd n → even (suc n)
   data odd : ℕ → Set where
-    suc : ∀ {n : ℕ} → even n → odd (suc n)
+    od-suc : ∀ {n : ℕ} → even n → odd (suc n)
 \end{code}
 The keyword `mutual` indicates that the nested definitions
 are mutually recursive.
diff --git a/src/RelationsEx.lagda b/src/RelationsEx.lagda
index fab5c79a..51cdf08d 100644
--- a/src/RelationsEx.lagda
+++ b/src/RelationsEx.lagda
@@ -46,6 +46,22 @@ trichotomy (suc m) (suc n) with trichotomy m n
 
 *Even and odd*
 
+\begin{code}
++-evev : ∀ {m n : ℕ} → even m → even n → even (m + n)
++-evev ev-zero evn = evn
++-evev (ev-suc (od-suc evm)) evn = ev-suc (od-suc (+-evev evm evn))
+
++-evod : ∀ {m n : ℕ} → even m → odd n → odd (m + n)
++-evod ev-zero odn = odn
++-evod (ev-suc (od-suc evm)) odn = od-suc (ev-suc (+-evod evm odn))
+
++-odev : ∀ {m n : ℕ} → odd m → even n → odd (m + n)
++-odev (od-suc evm) evn = od-suc (+-evev evm evn)
+
++-odod : ∀ {m n : ℕ} → odd m → odd n → even (m + n)
++-odod (od-suc evm) odn = ev-suc (+-evod evm odn)
+\end{code}
+
 \begin{code}
 +-lemma : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + (suc m + 0)
 +-lemma m rewrite +-identity m | +-suc m m = refl
@@ -55,12 +71,12 @@ trichotomy (suc m) (suc n) with trichotomy m n
 
 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
+  is-even zero ev-zero =  zero , refl
+  is-even (suc n) (ev-suc odn) with is-odd n odn
   ... | 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
+  is-odd (suc n) (od-suc evn) with is-even n evn
   ... | m , n≡2*m rewrite n≡2*m = m , refl
 \end{code}
 
diff --git a/src/extra/EvenOdd.agda b/src/extra/EvenOdd.agda
index 9fdf2e0f..a36e33cd 100644
--- a/src/extra/EvenOdd.agda
+++ b/src/extra/EvenOdd.agda
@@ -2,9 +2,9 @@ open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Data.Product using (∃; _,_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
 
-+-identity : ∀ (n : ℕ) → n + zero ≡ n
++-identity : ∀ (m : ℕ) → m + zero ≡ m
 +-identity zero = refl
-+-identity (suc n) rewrite +-identity n = refl
++-identity (suc m) rewrite +-identity m = refl
 
 +-suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m)
 +-suc m zero = refl
@@ -35,7 +35,7 @@ mutual
   ... | m , n≡2*m rewrite n≡2*m = m , refl
 
 +-lemma′ : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0)
-+-lemma′ m rewrite +-suc m (m + 0) = {!!}
++-lemma′ m rewrite +-suc (m + 0) m = refl
 
 is-even′ : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m)
 is-even′ zero zero =  zero , refl
diff --git a/src/extra/Reasoning.agda b/src/extra/Reasoning.agda
new file mode 100644
index 00000000..fc1fece7
--- /dev/null
+++ b/src/extra/Reasoning.agda
@@ -0,0 +1,85 @@
+open import Data.Nat using (ℕ; zero; suc; _+_)
+
+import Relation.Binary.PropositionalEquality as Eq
+import Relation.Binary.PreorderReasoning as Re
+
+module ReEq = Re (Eq.preorder ℕ)
+open ReEq using (begin_; _∎) renaming (_≈⟨⟩_ to _≡⟨⟩_; _∼⟨_⟩_ to _≡⟨_⟩_)
+open Eq using (_≡_; refl; sym; trans)
+
+lift : ∀ {m n : ℕ} → m ≡ n → suc m ≡ suc n
+lift refl = refl
+
++-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
++-assoc zero n p =
+  begin
+    (zero + n) + p
+  ≡⟨⟩
+    zero + (n + p)
+  ∎
++-assoc (suc m) n p =
+  begin
+    (suc m + n) + p
+  ≡⟨⟩
+    suc ((m + n) + p)
+  ≡⟨ lift (+-assoc m n p) ⟩
+    suc (m + (n + p))
+  ≡⟨⟩
+    suc m + (n + p)
+  ∎
+
++-identity : ∀ (m : ℕ) → m + zero ≡ m
++-identity zero =
+  begin
+    zero + zero
+  ≡⟨⟩
+    zero
+  ∎
++-identity (suc m) =
+  begin
+    suc m + zero
+  ≡⟨⟩
+    suc (m + zero)
+  ≡⟨ lift (+-identity m) ⟩
+    suc m
+  ∎
+
++-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
++-suc zero n =
+  begin
+    zero + suc n
+  ≡⟨⟩
+    suc n
+  ≡⟨⟩
+    suc (zero + n)
+  ∎
++-suc (suc m) n =
+  begin
+    suc m + suc n
+  ≡⟨⟩
+    suc (m + suc n)
+  ≡⟨ lift (+-suc m n) ⟩
+    suc (suc (m + n))
+  ≡⟨⟩
+    suc (suc m + n)
+  ∎
+
++-comm : ∀ (m n : ℕ) → m + n ≡ n + m
++-comm m zero =
+  begin
+    m + zero
+  ≡⟨ +-identity m ⟩
+    m
+  ≡⟨⟩
+    zero + m
+  ∎
++-comm m (suc n) =
+  begin
+    m + suc n
+  ≡⟨ +-suc m n ⟩
+    suc (m + n)
+  ≡⟨ lift (+-comm m n) ⟩
+    suc (n + m)
+  ≡⟨⟩
+    suc n + m
+  ∎