-- Functions.Universal_Quantification exercises -- By Xiaoning Bian module Functions.Universal_Quantification where open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; _<_; z≤n; s≤s; _≤′_; ≤′-step; ≤′-refl) open import Data.Fin using (Fin; zero; suc; toℕ) open import Data.Empty using (⊥) open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) open import Function using (flip; _$_; _∘_) ≤-refl : (n : ℕ) → n ≤ n ≤-refl zero = z≤n ≤-refl (suc n) = s≤s (≤-refl n) --Define the following functions (prove these properties): ≤-trans : ∀ {m n o} → m ≤ n → n ≤ o → m ≤ o ≤-trans z≤n s = z≤n ≤-trans (s≤s r) (s≤s s) = s≤s ( ≤-trans r s) total : ∀ m n → m ≤ n ⊎ n ≤ m -- hint: use total zero n = inj₁ z≤n total (suc m) zero = inj₂ z≤n total (suc m) (suc n) = [ inj₁ ∘ s≤s , inj₂ ∘ s≤s ]′ (total m n) --From the 4 (should be 3) above properties follows that _≤_ is a total order on ℕ. (We can look at _≤_ as a relation over ℕ.) ≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n ≤-pred (s≤s r) = r ≤-mono : ∀ {m n k} → n ≤ m → k + n ≤ k + m ≤-mono {k = zero} z≤n = z≤n ≤-mono {k = zero} (s≤s r) = s≤s r ≤-mono {k = suc j} z≤n = s≤s (≤-mono {k = j} z≤n) ≤-mono {k = suc j} (s≤s r) = s≤s (≤-mono {k = j} (s≤s r)) -- Define the following functions: ≤-step : ∀ {m n} → m ≤ n → m ≤ 1 + n ≤-step z≤n = z≤n ≤-step (s≤s r) = s≤s (≤-step r) ≤′⇒≤ : ∀ {a b} → a ≤′ b → a ≤ b ≤′⇒≤ {zero} ≤′-refl = z≤n ≤′⇒≤ {zero} (≤′-step r) = z≤n ≤′⇒≤ {suc a} .{suc a} ≤′-refl = s≤s (≤′⇒≤ ≤′-refl) ≤′⇒≤ {suc a} {suc b'} (≤′-step r) = ≤-step (≤′⇒≤ { suc a} {b'} r) z≤′n : ∀ n → zero ≤′ n z≤′n zero = ≤′-refl z≤′n (suc n) = ≤′-step (z≤′n n) s≤′s : ∀ {m n} → m ≤′ n → suc m ≤′ suc n s≤′s ≤′-refl = ≤′-refl s≤′s (≤′-step r) = ≤′-step (s≤′s r) -- not in the excercise. it is used as an auxillary lemma ≤′-mono1 : ∀ {m n} → n ≤′ m → (suc n) ≤′ (suc m) ≤′-mono1 ≤′-refl = ≤′-refl ≤′-mono1 (≤′-step r) = ≤′-step(≤′-mono1 r) ≤⇒≤′ : ∀ {a b} → a ≤ b → a ≤′ b ≤⇒≤′ {zero} {zero} z≤n = ≤′-refl ≤⇒≤′ {zero} {suc b} z≤n = ≤′-step (≤⇒≤′ z≤n) ≤⇒≤′ {suc a} {zero} () ≤⇒≤′ {suc a} {suc b} (s≤s r) = ≤′-mono1 (≤⇒≤′ r) -- Define fin≤: fin≤ : ∀ {n}(m : Fin n) → toℕ m < n fin≤ zero = s≤s z≤n fin≤ {suc n} (suc x) = s≤s(fin≤ {n} x)