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 + ∎