Imports

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; _$_; _∘_)

Universal quantification

We can represent a proof for universal quantification on a set by a dependent function on that set.

Example:

≤-refl : (n : ℕ) → n ≤ n
≤-refl zero    = z≤n
≤-refl (suc n) = s≤s (≤-refl n)

Exercises

Define the following functions (prove these properties):

≤-trans      : ∀ {m n o} → m ≤ n → n ≤ o → m ≤ o

total        : ∀ m n → m ≤ n ⊎ n ≤ m -- hint: use [_,_]′

From the 4 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

≤-mono  : ∀ {m n k} → n ≤ m → k + n ≤ k + m

Exercises

Define the following functions:

≤-step : ∀ {m n} → m ≤ n → m ≤  + 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

Exercises with Fin

Define fin≤:

fin≤ : ∀ {n}(m : Fin n) → toℕ m < n