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; _$_; _∘_)
We can represent a proof for universal quantification on a set by a dependent function on that set. For example:
≤-refl : (n : ℕ) → n ≤ n ≤-refl zero = z≤n ≤-refl (suc n) = s≤s (≤-refl n)
Define the following functions (that is, prove those properties):
≤-trans : ∀ {m n o} → m ≤ n → n ≤ o → m ≤ o
total : ∀ m n → m ≤ n ⊎ n ≤ m
≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
≤-mono : ∀ {m n k} → n ≤ m → k + n ≤ k + m
Hint: For total, use the previously defined [_,_] function.
Note that, from the properties above, it follows that _≤_ is a total order on ℕ. (We can take _≤_ as a relation over ℕ.)
Define the following functions:
≤-step : ∀ {m n} → m ≤ n → m ≤ 1 + n
≤′⇒≤ : ∀ {a b} → a ≤′ b → a ≤ b
z≤′n : ∀ n → zero ≤′ n
s≤′s : ∀ {m n} → m ≤′ n → suc m ≤′ suc n
≤⇒≤′ : ∀ {a b} → a ≤ b → a ≤′ b
fin≤ : ∀ {n}(m : Fin n) → toℕ m < n