module chap04_equality where import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym) open import Data.Nat using (ℕ; zero; suc; _+_) open import Data.Nat.Properties using (+-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) -- Exercise ≤-Reasoning (stretch) ---------------------------------------------- infixr 2 _≤⟨_⟩_ _≤⟨⟩_ infix 3 _≤∎ _≤⟨_⟩_ : ∀ m {n p} → m ≤ n → n ≤ p → m ≤ p m ≤⟨ m≤n ⟩ n≤p = ≤-trans m≤n n≤p _≤⟨⟩_ : ∀ m {n} → m ≤ n → m ≤ n m ≤⟨⟩ m≤n = m≤n _≤∎ : ∀ n → n ≤ n _≤∎ e = ≤-refl -- Allows using ≡-proofs in ≤-chains, used in +-monoˡ-≤. ≡→≤ : ∀ {m n} → m ≡ n → m ≤ n ≡→≤ refl = ≤-refl module NewProofs where +-monoʳ-≤ : ∀ {n p q} → p ≤ q → n + p ≤ n + q +-monoʳ-≤ {zero} {p} {q} p≤q = 0 + p ≤⟨⟩ p ≤⟨ p≤q ⟩ q ≤⟨⟩ 0 + q ≤∎ +-monoʳ-≤ {suc n} {p} {q} p≤q = suc n + p ≤⟨⟩ suc (n + p) ≤⟨ s≤s (+-monoʳ-≤ p≤q) ⟩ suc (n + q) ≤⟨⟩ suc n + q ≤∎ +-monoˡ-≤ : ∀ {m n p} → m ≤ n → m + p ≤ n + p +-monoˡ-≤ {m} {n} {p} m≤n = m + p ≤⟨ ≡→≤ (+-comm m p) ⟩ p + m ≤⟨ +-monoʳ-≤ m≤n ⟩ p + n ≤⟨ ≡→≤ (+-comm p n) ⟩ n + p ≤∎ +-mono-≤ : ∀ {m n p q} → m ≤ n → p ≤ q → m + p ≤ n + q +-mono-≤ {m} {n} {p} {q} m≤n p≤q = m + p ≤⟨ +-monoˡ-≤ m≤n ⟩ n + p ≤⟨ +-monoʳ-≤ p≤q ⟩ n + q ≤∎ module OldProofs where +-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)