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  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

Exercises with Fin

Define fin≤:


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