import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym; _≢_) open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎) open import Data.Nat using (ℕ; zero; suc; _+_; _*_) open import Data.Nat.Properties using (+-comm; *-comm) -- Context infix 4 _≤_ data _≤_ : ℕ → ℕ → Set where z≤n : ∀ {n} → zero ≤ n s≤s : ∀ {m n} → m ≤ n → suc m ≤ suc n ≤-refl : ∀ {n} → n ≤ n ≤-refl {zero} = z≤n ≤-refl {suc n} = s≤s ≤-refl ≤-trans : ∀ {m n p} → m ≤ n → n ≤ p → m ≤ p ≤-trans z≤n n≤p = z≤n ≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p) +-monoʳ-≤ : ∀ {n p q} → p ≤ q → n + p ≤ n + q +-monoʳ-≤ {zero} p≤q = p≤q +-monoʳ-≤ {suc n} p≤q = s≤s (+-monoʳ-≤ p≤q) +-monoˡ-≤ : ∀ {m n p} → m ≤ n → m + p ≤ n + p +-monoˡ-≤ {m} {n} {p} m≤n rewrite +-comm m p | +-comm n p = +-monoʳ-≤ m≤n +-mono-≤ : ∀ {m n p q} → m ≤ n → p ≤ q → m + p ≤ n + q +-mono-≤ m≤n p≤q = ≤-trans (+-monoˡ-≤ m≤n) (+-monoʳ-≤ p≤q) infix 4 _<_ data _<_ : ℕ → ℕ → Set where z_ _>_ : ℕ → ℕ → Set m > n = n < m module Variant1 where data <-Trichotomy : ℕ → ℕ → Set where tri-< : ∀ {m n : ℕ} → m < n → <-Trichotomy m n tri-≡ : ∀ {m n : ℕ} → m ≡ n → <-Trichotomy m n tri-> : ∀ {m n : ℕ} → m > n → <-Trichotomy m n <-trichotomy : ∀ (m n : ℕ) → <-Trichotomy m n <-trichotomy zero zero = tri-≡ refl <-trichotomy zero (suc n) = tri-< z z m>n = tri-> (sn) module Variant2 where -- This type describes the disjunction of two propositions A ∨ B, and will -- be covered in Chapter 'Connectives'. A proof of A ∨ B is either a proof -- of A (via constructor inₗ) or a proof of B (via constructor inᵣ). infixr 1 _∨_ data _∨_ : Set → Set → Set where inₗ : ∀ {A B : Set} → A → A ∨ B inᵣ : ∀ {A B : Set} → B → A ∨ B -- This type describes the trichotomy property for an arbitrary binary -- relation R. -- `Trichotomy _<_` is equivalent to -- `∀ (m n : ℕ) → <-Trichotomy m n` from `Variant1`. Trichotomy : ∀ {A : Set} → (A → A → Set) → Set Trichotomy {A} R = ∀ (x y : A) → R x y ∨ x ≡ y ∨ R y x -- The actual proof is the same as in `Variant1`, except that we now -- use combinations of `inₗ` and `inᵣ` instead of `tri-<`, `tri-≡`, and `tri->`, -- which makes it less readable on first sight. <-trichotomy : Trichotomy _>_ <-trichotomy zero zero = inᵣ (inₗ refl) <-trichotomy zero (suc n) = inᵣ (inᵣ zm) = inᵣ (inᵣ (sm)) -- Exercise +-mono-< (practice) ------------------------------------------------ +-mono-<ʳ : ∀ {m p q : ℕ} → p < q → m + p < m + q +-mono-<ʳ {zero} p