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