Journal Part I

theuibcoworkes.plfa Keybase team

The following is intended to be a guide to read the PLFA book and some related materials. It's a very simplified version of the original material presented in the book. It may also contain excerpts from other sources without any reference. So we don't claim any authorship of the following unless stated otherwise.

Recurrent participants on Zoom meetings (Keybase's team):

• Elisabeth Bonnevier

• Ragnhild Bratli

• Jonathan Cubides

• David Grellscheid

• Knut Anders Stokke

• Tam Thanh Truong

• Farhad Vadiee

• Michal Walicki

Agda

Agda is a dependently typed programming language. It is an extension of Martin-Löf’s type theory... Because of strong typing and dependent types, Agda can be used as a proof assistant, allowing to prove mathematical theorems (in a constructive setting) and to run such proofs as algorithms. See this on https://agda.readthedocs.io/

You can remix this notebook to play with the code above, or you better install Agda on your computer.

$ brew install agda

$ pip3 install agda-pkg

$ apkg install --github plfa/plfa.github.io --branch dev --name plfa

Agda works smoothly on Emacs. However, you can try it on VS Code with extension "agda-mode", and similarly on Atom.

Unicode symbols

We love math symbols and we can type them in Agda as well. This works well in Emacs, and in VS Code. On your browser you can try to remix this notebook.

This chapter uses the following unicode:

ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)

→  U+2192  RIGHTWARDS ARROW (\to, \r, \->)

∸  U+2238  DOT MINUS (\.-)

≡  U+2261  IDENTICAL TO (\==)

⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)

⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)

∎  U+220E  END OF PROOF (\qed) 

ls

module part1 where

Agda files

Agda files can have multiple extensions:

• ".agda" stands for plain agda

• ".lagda" stands for literate agda i.e. one can mix text and code.

  • use "\begin{code} ...\end{code}"

  • deviations are depending on the markup language you wan to use:

    • ".lagda.md" stands for Markdown. It uses "```agda" blocks

    • ".lagda.rst" stands for ReStructured Text. It uses ":: blocks". Read the documentation for more details.

Once you have ready Agda to play with. You can type-check compile your code file using the agda command and the filename as follows:

echo "-- Hello" > Test.agda 

cat Test.agda 

agda Test.agda

Agda comments

Comments can be:

• inline using "-- " or

• multiline using "{- -}"

-- One can always introduce (not recommended) alias

-- for any data type in Agda.

-- This is Knut Anders typing Tam here

{- 

This is a comment 

This too

And this

-}

Another cool thing about agda is its interaction capabilities for which you need to use a supported text editor. Some keystrokes for interaction we use in the meetings are:

-- C-c C-c to split the variable by pattern matching

-- C-c C-a calls the solver "auto" 

-- C-c C-r "refine" the goal with the hint you provide in

Type of types

The most basic type is inline_formula not implementedthe type of types living in the level inline_formula not implemented. This states that a type lives in a specific level but it could be lifted to a higher universe. For now, we leave out that discussion, and we will come back later. We will only need types of type Set or zero level types.

Aliases of a type is possible as follows.

Type = Set

Aliases of a term is possible as follows.

The basic judgement in type theory is inline_formula not implemented. This tells us inline_formula not implemented is of type inline_formula not implemented. We also say inline_formula not implemented is a term of the type inline_formula not implemented. Unlike set theory, a term like inline_formula not implemented can not be of another type inline_formula not implemented , unless they are equal. We will address that issue later.

X : Set

X = _

a : X

b : X

Empty type

data

  𝟘 : Set  

  where

EmptyType = 𝟘 -- alias for your type

⊥ = 𝟘

-- The empty type

-- It has not constructor

Unit type

data

  𝟙    -- \b1

    : Set

  where

  unit : 𝟙

Unit = 𝟙

⊤ = 𝟙

Nat type

The naturals are an inductive data type

• Natural numbers is a type denoted by ℕ, i.e., ℕ : Set.

• Two inference rules express the two only possible ways to construct terms of this type.

  • Base case: zero is a natural number, i.e., zero : ℕ.

  • Inductive case: if m is a natural number, then suc m is also a natural number, i.e., suc : ℕ → ℕ.

data

  ℕ : Set 

  where

  zero : ℕ

  suc  : ℕ -> ℕ

Nat  = ℕ

num3 : ℕ 

num3 = suc (suc (suc zero))

"While the natural numbers have been understood for as long as people can count, the inductive definition of the natural numbers is relatively recent. It can be traced back to Richard Dedekind's paper "Was sind und was sollen die Zahlen?" (What are and what should be the numbers?), published in 1888, and Giuseppe Peano's book "Arithmetices principia, nova methodo exposita" (The principles of arithmetic presented by a new method), published the following year."

One can introduce alias for the data constructors by means of the keyword "pattern".

pattern succ n = suc n

pattern zr    = zero

NATURAL pragma

{-# BUILTIN NATURAL ℕ #-}

The pragma also enables a more efficient internal representation of naturals using the Haskell type for arbitrary-precision integers. Representing the natural n with zero and suc requires space proportional to n, whereas representing it as an arbitrary-precision integer in Haskell only requires space proportional to the logarithm of n.

n3 : ℕ 

n3 = 3

• Pragma documentation: https://agda.readthedocs.io/en/latest/language/built-ins.html#natural-numbers

Operations on naturals

Given a type inline_formula not implemented, we want to define functions of type inline_formula not implemented. One can define such functions by specifying how the function behaves on each of the inline_formula not implemented-constructors. Such approach is called pattern matching.

We use pattern matching in Agda when constructors appear on the left-hand side of an equation.

Addition

• The definition is recursive, in that the last line defines addition in terms of addition.

• Such a definition is called well founded, because addition of larger numbers is defined in terms of addition of smaller numbers.

_+_ : ℕ → ℕ → ℕ

zero    + n = n

(suc m) + n = suc (m + n)

-- sized types...

One can also define summation by pattern match on the second parameter. We can expect these two definitions to be equivalent, equal pointwise.

_+2_ : ℕ → ℕ → ℕ

n +2 zero    = n

n +2 (suc m) = suc (m +2 n)

Read more on this andt function extensionality https://ncatlab.org/nlab/show/function+extensionality.

Multiplication

_*_ : ℕ → ℕ → ℕ

zero    * n =  zero

(suc m) * n =  n + (m * n)

Monus

We can also define subtraction. Since there are no negative natural numbers, if we subtract a larger number from a smaller number we will take the result to be zero. This adaption of subtraction to naturals is called monus (a twist on minus).

_∸_ : ℕ → ℕ → ℕ

m     ∸ zero   =  m

zero  ∸ suc n  =  zero

suc m ∸ suc n  =  m ∸ n

Exponentiation

_^_ : ℕ → ℕ → ℕ

m ^ 0 = 1 

m ^ (suc n)  =  m * (m ^ n)

-- 0 ^ 0  = 1

More NATURAL pragmas

{-# BUILTIN NATPLUS  _+_ #-}

{-# BUILTIN NATTIMES _*_ #-}

{-# BUILTIN NATMINUS _∸_ #-}

Equality type

import Relation.Binary.PropositionalEquality as Eq

open Eq using (_≡_; refl)

• Because we can interpret types as "sets" in our context, it makes sense to call terms as elements of a type.

• Above we imported the equality type from the standard library but its definition follows the same principle below:

data

  _≡_ {i} {A : Set i} (x : A) 

  	: A → Set i

  where

  refl : x ≡ x

X : Set i 

X = ...

X -- is a type

a : X 

b : X

p : a ≡ b

p = ?

The declaration above uses curly braces { } rather than parentheses. This means that the arguments are implicit and need not be written explicitly; instead, they are inferred by Agda's type-checker.

Say we have a a' : A, we can construct the type a == a'. What is p : a == a'?

zeroequalsitself : 0 ≡ 0

zeroequalsitself = refl

Properties of the identity type

sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x

sym refl = refl

trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z

trans refl = λ p → p

Discussion:

_ : 2 + 3 ≡ 5

_ = refl

• One can think of each term as evidence for the assertion 2 + 3 ≡ 5.

• This duality of interpretation of a type as a proposition, and of a term as evidence is central point to the way math is formalised using type theory, we formalise concepts in Agda, and will be a running theme throughout this book.

• The other word for evidence, which we will use interchangeably, is proof.

Now, let see prove some lemmas about natural numbers. We will handy to define the congruence relation on the equality type (NB the general version is not given below) :

ap : ∀ {A B : Set}

  → (f : A → B)

  → ∀ {x y : A} → x ≡ y

  → f x ≡ f y

ap f refl = refl

cong = ap 

In Agda we can avoid some trivial terms by using underscore as follows:

Lemmas

Lemma. +-r

+-r : (n m k : ℕ) → m ≡ n → m + k ≡ n + k

+-r _ _ k refl = ap (_+ k) refl 

For clarity, one might want to specify the implicit argument hidden above in the usage of refl, we do that using curly brace notation for explicit arguments as follows:

Lemma. +-l

+-l : (n m k : ℕ) → m ≡ n → k + m ≡ k + n

+-l _ m k refl = ap (k +_) (refl {x = m})

Implicit arguments

Those arguments given implicit in the type definition can be pulled out. We can use that for defining functions that give the domain or codomain of the input function. NB the subindex to denote types below.

domain

  : ∀ {A : Set₀} {B : Set₁}

  → (A → B)

  → Set₀

domain {A} f = A

codomain

  : ∀ {A : Set₀} {B : Set₁}

  → (A → B)

  → Set₁

codomain {B = B} f = B

Anonymous functions (lambdas)

-- _ = λ x → x

-- _ = λ x y → x + y

-- Pattern match on the right-hand side, by using λ{... → ...}

mock

  : ∀ {A : Set} {x y : A}

  → x ≡ y

  → y ≡ x

mock = λ {refl → refl}

Equational reasoning

Copy from the Agda standard library, we add below function and stuff to have equational reasoning.

module _ {A : Set} where

  infix  3 _∎

  infixr 2 _≡⟨⟩_ step-≡ step-≡˘

  infix  1 begin_

  begin_ : ∀{x y : A} → x ≡ y → x ≡ y

  begin_ x≡y = x≡y

  _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y

  _ ≡⟨⟩ x≡y = x≡y

  step-≡ : ∀ (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z

  step-≡ _ y≡z x≡y = trans x≡y y≡z

  step-≡˘ : ∀ (x {y z} : A) → y ≡ z → y ≡ x → x ≡ z

  step-≡˘ _ y≡z y≡x = trans (sym y≡x) y≡z

  _∎ : ∀ (x : A) → x ≡ x

  _∎ _ = refl

  syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z

  syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z

Now, try using equational reasoning to prove the following lemma cong-app2.

cong-app2

  : ∀ { A B C : Set}

  → (f : A → B → C)

  → {a a' : A} → a  ≡ a'

  → {b b' : B} → b ≡ b'

  → f a b  ≡ f a' b'

cong-app2 f refl refl = refl

cong-app2'

  : ∀ { A B C : Set}

  → (f : A → B → C)

  → {a a' : A} → a  ≡ a'

  → {b b' : B} → b ≡ b'

  → f a b  ≡ f a' b'

cong-app2' f {a}{a'} p {b}{b'} q = 

  begin

    f a b

      ≡⟨ ap (f a) q ⟩

    f a b'

      ≡⟨ ap (λ x → f x b') p ⟩

    f a' b'

    ∎

Lemmas for natural numbers

Properties for addition

+zero : (m : ℕ) → (m + zero ≡ m)

+zero zero     = refl

+zero (suc m) = ap (λ z → suc z) (+zero m)

+-rightSucc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

+-rightSucc zero n = refl

+-rightSucc (suc m) n = ap suc (+-rightSucc m n)

Lemma. Addition is commutative.

+-comm : (n m :  ℕ)

  → n + m ≡ m + n

+-comm zero     m    = sym (+zero m)

+-comm (suc n) zero = ap suc (+zero n)

+-comm nn@(suc n) mm@(suc m)

-- Calculation

   = begin

   ((suc n) + (suc m))

    ≡⟨⟩ -- by definition (above and below are equal)

   (suc (n  + suc m))

    ≡⟨ ap suc (+-comm n (suc m)) ⟩

   (suc (suc (m + n)))

    ≡˘⟨ ap suc (+-rightSucc _ _) ⟩

      (suc ( m + suc n))

    ≡⟨⟩

   ((suc m) + (suc n))

    ∎    

In the definition above we use the symbol @ as the prefix for some variables. This symbols adds another way to refer to that argument. That's is convenient in some cases when you have split your definition in very complicate inductive cases and you want to use them somewhere else inside the proof.

-- --Commutativity Tam's proof

-- +-comm' : ∀ (n m : ℕ) → (n + m ≡ m + n)

-- +-comm  zero m   = sym (+-zero m)

-- +-comm (suc n) m = trans (ap suc (+-comm n m)) (sym (+-rightSucc m n))

-- Original:

--   (succ n + succ m) ≡ (succ m + succ n)

--   succ (n + succ m) ≡ succ (m + succ n)

-- After rewrite 1:

--   succ (succ (m + n)) ≡ succ (m + succ n)

--   succ (succ (m + n)) ≡ succ (m + succ n)

-- After rewrite 2:

-- succ (succ (m + n)) ≡ succ (succ (n + m))

-- Using rewrite 1: +-comm (n, succ m) :  (n + succ m) ≡ (succ m) + n

-- Using rewrite 2: +-comm (m , succ n) : (m + succ n) ≡ succ (n + m)

-- Using rewrite 3: +-comm m n : (m + n) ≡ (n + m)

+-comm-rw

  : (n m : ℕ)

  → n + m ≡ m + n

+-comm-rw zero     m    = sym (+zero m)

+-comm-rw (suc n) zero = ap suc (+zero n)

+-comm-rw (suc n) (suc m)

   rewrite

    +-comm-rw n (suc m)

  | +-comm-rw m (suc n)

  | +-comm-rw m n

  = refl

Lemma. Addition is associative.

+-assoc : (n m k : ℕ) → ((n + m) + k ≡ n + (m + k))

+-assoc zero m k = refl

+-assoc (suc n) m k = ap suc (+-assoc n m k)

Lemma. 2+3 is 5.

Let's prove this proposition by given a calculation.

_ : 2 + 3 ≡ 5

_ =

  begin

    2 + 3

  ≡⟨⟩    -- is shorthand for

    (suc (suc zero)) + (suc (suc (suc zero)))

  ≡⟨⟩    -- inductive case

    suc ((suc zero) + (suc (suc (suc zero))))

  ≡⟨⟩    -- inductive case

    suc (suc (zero + (suc (suc (suc zero)))))

  ≡⟨⟩    -- base case

    suc (suc (suc (suc (suc zero))))

  ≡⟨⟩    -- is longhand for

    5

  ∎

Properties of multiplication

Lemma. Multiplication by zero on the right is zero.

*-zero : ∀ (n : ℕ) → (n * zero ≡ zero)

*-zero zero    = refl

*-zero (suc n) =  *-zero n

Lemma. Multiplication is commutative.

*-comm : (a b : ℕ) → a * b ≡ b * a

*-comm zero zero = refl

*-comm zero (suc b) = *-comm zero b

*-comm (suc a) zero = *-comm a zero

*-comm (suc a) (suc b) =

  begin 

    (suc a * suc b)

  ≡⟨⟩

    (suc b + (a * suc b))

  ≡⟨⟩

    (suc (b + (a * suc b)))

  ≡⟨ ap (λ x → suc (b + x)) (*-comm a (suc b)) ⟩

    suc (b + (suc b * a))

  ≡⟨⟩

    (suc (b + (a + (b * a))))

  ≡⟨ ap suc (sym (+-assoc b a (b * a))) ⟩

    (suc ((b + a) + (b * a)))

  ≡⟨ ap (λ x → suc (x + (b * a))) (+-comm b a) ⟩

    (suc ((a + b) + (b * a)))

  ≡⟨ ap (λ x → suc ((a + b) + x)) (*-comm b a) ⟩

    (suc ((a + b) + (a * b)))

  ≡⟨ ap suc (+-assoc a b (a * b)) ⟩

    (suc (a + (b + (a * b))))

  ≡⟨⟩

    (suc (a + ((suc a) * b)))

  ≡⟨ ap (λ x → suc (a + x)) (*-comm (suc a) b) ⟩ 

    (suc (a + (b * (suc a))))

  ≡⟨⟩

    (suc a + (b * suc a))

  ≡⟨⟩

    (suc b * suc a)

  ∎

*-comm2 : ∀ (n m : ℕ) → (n * m ≡ m * n)

*-comm2 zero m = sym (*-zero m)

*-comm2 (suc n) m =

    begin

    ((suc n) * m)

      ≡⟨⟩

    (m + (n * m))

      ≡⟨ ap (m +_) (*-comm2 n m) ⟩

    (m + (m * n))

      ≡⟨ sym (*-rightSucc m n) ⟩

    (m * (suc n))

    ∎

    where

    *-rightSucc : ∀ (n m : ℕ) → n * suc m ≡ n + (n * m)

    *-rightSucc zero m = refl

    *-rightSucc (suc n) m =

      begin

      (suc n * suc m)

        ≡⟨⟩

      (suc m + (n * suc m))

        ≡⟨ ap ((suc m) +_) (*-rightSucc n m) ⟩

      (suc m + (n + (n * m)))

        ≡⟨⟩

      (suc (m + (n + (n * m))))

        ≡⟨ ap suc (sym (+-assoc m n (n * m))) ⟩

      (suc ((m + n) + (n * m)))

        ≡⟨ ap suc (ap (_+ (n * m)) (+-comm m n)) ⟩

      (suc ((n + m) + (n * m)))

        ≡⟨ ap suc (+-assoc n m (n * m)) ⟩

      (suc (n + (m + (n * m))))

        ≡⟨⟩

      (suc n + (m + (n * m)))

        ≡⟨⟩

      (suc n + ((suc n) * m))

      ∎

Lemma. Distributivity of multiplication over addition.

+*-dist : ∀ (n m k : ℕ) → (n + m) * k ≡ (n * k) + (m * k)

+*-dist zero m k = refl

+*-dist (suc n) m k = 

    begin

    (((suc n) + m) * k)

      ≡⟨⟩

    ((suc (n + m) * k))

      ≡⟨⟩

    (k + ((n + m) * k))  

      ≡⟨ ap (k +_) (+*-dist n m k) ⟩

    (k + ((n * k) + (m * k)))

      ≡⟨ sym (+-assoc k (n * k) (m * k)) ⟩

    ((k + (n * k)) + (m * k))

      ≡⟨⟩

    (((suc n) * k) + (m * k))

    ∎

Lemma. Associativity of multiplication.

*-assoc : ∀ (n m k : ℕ) → (n * m) * k ≡ n * (m * k)

*-assoc zero m k = refl

*-assoc (suc n) m k =

    begin

    ((suc n * m) * k)

    ≡⟨⟩

    ((m + (n * m)) * k)

    ≡⟨ +*-dist m (n * m) k ⟩

    ((m * k) + ((n * m) * k))

    ≡⟨ (ap ((m * k) +_) (*-assoc n m k)) ⟩

    ((m * k) + (n * (m * k)))

    ≡⟨⟩

    (suc n * (m * k))

    ∎

Operators precedence

• We often use precedence to avoid writing too many parentheses.

• Application binds more tightly than (or has precedence over) any operator, and so we may write suc m + n to mean (suc m) + n. As another example, we say that multiplication binds more tightly than addition, and so write n + m * n to mean n + (m * n).

• We also sometimes say that addition associates to the left, and so write m + n + p to mean (m + n) + p.

In Agda the precedence and associativity of infix operators needs to be declared:

infixl 6  _+_ 

infixl 6 _∸_

infixl 7  _*_

• infixl indicates that the operators associate to the left, or

• infixr to indicate that an operator associates to the right, or

• infix to indicate that parentheses are always required to disambiguate.

More about this on https://agda.readthedocs.io/en/v2.5.2/language/mixfix-operators.html

Currying

We have chosen to represent a function of two arguments in terms of a function of the first argument that returns a function of the second argument. This trick goes by the name currying and it is about the following correspondence:

• Currying is named for Haskell Curry, after whom the programming language Haskell is also named. Curry's work dates to the 1930's.

• The idea actually appears in the Begriffschrift of Gottlob Frege, published in 1879.

Binary encoding of naturals

A more efficient representation of natural numbers uses a binary rather than a unary system. We represent a number as a bit-string:

data Bin : Set where

  ⟨⟩ : Bin

  _O : Bin → Bin

  _I : Bin → Bin

print (bin(11))

For instance, the standing for the number eleven is encoded as

eleven1 : Bin

eleven1 = ⟨⟩ I O I I

• Representations are not unique due to leading zeros. Hence, eleven is also represented by 001011, encoded as:

For instance, the standing for the number eleven is encoded as

eleven2 : Bin

eleven2 = ⟨⟩ O I O I I

Using the above, one would be able to define a pair of functions to convert between the two representations.

to   : ℕ → Bin

from : Bin → ℕ

Agda standard library

The definition above are available in the Agda standard library by using the following imports.

{-

import Relation.Binary.PropositionalEquality as Eq

open Eq using (_≡_; refl; cong)

open import Data.Nat using (ℕ; zero; suc; _+_)

import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

open import Data.Nat.Properties using (+-comm)

-}

Relations

Unicode symbols used in this part of the book.

≤  U+2264  LESS-THAN OR EQUAL TO (\<=, \le)

≥  U+2265  GREATER-THAN OR EQUAL TO (\>=, \ge)

ˡ  U+02E1  MODIFIER LETTER SMALL L (\^l)

ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)

After having defined operations such as addition and multiplication, the next step is to define relations, such as less than or equal.

The relation less than or equal has an infinite number of instances and can be defined in Agda as follows. Notice the usage of implicit arguments, curly braces notation.

Less than or equal relation

data 

  _≤_ 

   : ℕ → ℕ → Set 

  where

  z≤n 

   : ∀ {n : ℕ}

   ----------- (zero-initial)

   → zero ≤ n

  s≤s 

    : ∀ {m n : ℕ}

    → m ≤ n

    --------------- (monotonicity)

    → suc m ≤ suc n

Strict inequality

We can define strict inequality similarly to inequality:

infix 4 _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}

      ------------

    → zero < suc n

  s<s : ∀ {m n : ℕ}

    → m < n

      -------------

    → suc m < suc n

Precedence of ≤

We declare the precedence for comparison as follows:

infix 4 _≤_

We set the precedence of _≤_ at level 4, so it binds less tightly than _+_ at level 6 and hence 1 + 2 ≤ 3 parses as (1 + 2) ≤ 3. We write infix to indicate that the operator does not associate to either the left or right, as it makes no sense to parse 1 ≤ 2 ≤ 3 as either (1 ≤ 2) ≤ 3 or 1 ≤ (2 ≤ 3).

Examples

-- _ : 2 ≤ 4

_ : 2 ≤ 4

_ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))

One may also identify implicit arguments by name:

_ : 2 ≤ 4

_ = s≤s {m = 1} {n = 3} (s≤s {m = 0} {n = 2} (z≤n {n = 2}))

In the latter format, you may only supply some implicit arguments:

_ : 2 ≤ 4

_ = s≤s {n = 3} (s≤s {n = 2} z≤n)

It is not permitted to swap implicit arguments, even when named.

Inversion Lemmas

Lemma. There is only one way to prove that suc m ≤ suc n, for any inline_formula not implemented and inline_formula not implemented.

inv-s≤s 

  : ∀ {m n : ℕ}

  → suc m ≤ suc n

    -------------

  → m ≤ n

inv-s≤s (s≤s m≤n) = m≤n

Lemma. There is only one way a number can be less than or equal to zero.

inv-z≤n : ∀ {m : ℕ}

  → m ≤ zero

    --------

  → m ≡ zero

inv-z≤n z≤n = refl

Properties of ordering relations

Definition. A binary relation inline_formula not implemented on a set inline_formula not implemented is a subset of inline_formula not implemented. A relation inline_formula not implemented can have following properties. Consider variables inline_formula not implemented.

• Reflexive. inline_formula not implemented for all x.

• Transitive. inline_formula not implemented and inline_formula not implemented then inline_formula not implemented.

• Anti-symmetric. If inline_formula not implemented and inline_formula not implemented then inline_formula not implemented.

• Total. inline_formula not implemented inline_formula not implemented or inline_formula not implemented. "all elements are comparable."

Lemma. The relation _≤_ satisfies all four of these properties.

Definition.

• Preorder = reflexive + transitive.

• Partial order = preorder + anti-symmetric.

• Total order = partial-order + total.

Exercise orderings

• Give examples of a preorder that is not a partial order.

  • Example in real life: Let inline_formula not implemented be the set of all employees at UiB and define the relation inline_formula not implemented such that for any two persons inline_formula not implemented we have inline_formula not implemented if inline_formula not implemented's shoe size is less than or equal to inline_formula not implemented's shoe size. This is a preorder, but not a partial order as shoe size is not a unique identifier and inline_formula not implemented is therefore not anti-symmetric.

-- A := {0,1}

R1 : ℕ → ℕ → Set

R1 0 0 = 𝟙

R1 1 1 = 𝟙

R1 0 1 = 𝟙

R1 1 0 = 𝟙

R1 _ _ = 𝟘

-- A := {0,1,2}

R2 : ℕ → ℕ → Set

R2 0 0 = 𝟙

R2 1 1 = 𝟙

R2 2 2 = 𝟙

R2 0 1 = 𝟙

R2 0 2 = 𝟙

R2 1 0 = 𝟙

R2 1 2 = 𝟙

R2 _ _ = 𝟘

• Give an example of a partial order that is not a total order.

Lemma. (Reflexivity)

≤-refl 

  : ∀ {n : ℕ}

   -----

  → n ≤ n

≤-refl {zero}  = z≤n

≤-refl {suc n} = s≤s ≤-refl

Lemma. (Transitivity)

≤-trans : ∀ {m n p : ℕ}

  → m ≤ n

  → n ≤ p

    -----

  → m ≤ p

≤-trans z≤n       _          =  z≤n

≤-trans (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans m≤n n≤p)

Compare above with the version below that uses explicit arguments.

≤-trans′ : ∀ (m n p : ℕ)

  → m ≤ n

  → n ≤ p

    -----

  → m ≤ p

≤-trans′ zero    _       _       z≤n       _         = z≤n

≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans′ m n p m≤n n≤p)

NB the distinction between two techniques: induction on evidence and induction on values. But we've already seen some examples before when we pattern match on the identity type.

Lemma. (Anti-symmetry)

≤-antisym 

  : ∀ {m n : ℕ}

  → m ≤ n

  → n ≤ m

    -----

  → m ≡ n

≤-antisym z≤n       z≤n        =  refl

≤-antisym (s≤s m≤n) (s≤s n≤m)  =  cong suc (≤-antisym m≤n n≤m)

Lemma. +-mono-r-≤

+-mono-r-≤

    : (l m n : ℕ)

    → (p : l ≤ m)

    ---------------

    → n + l ≤ n + m

+-mono-r-≤ l m zero p = p

+-mono-r-≤ l m (suc n) p = s≤s (+-mono-r-≤ l m n p)

Lemma. +-mono-l

+-mono-l-≤

  : (l m n : ℕ)

  → l ≤ m

  ---------------

  → l + n ≤ m + n

+-mono-l-≤ l m n p

  rewrite

  +-comm l n

  | +-comm m n

  = +-mono-r-≤ l m n p

Lemma. +-mono-≤

+-mono-≤ : (k l m n : ℕ) → k ≤ l → m ≤ n → k + m ≤ l + n

+-mono-≤ k l m n p q = ≤-trans (+-mono-r-≤ m n k q)

                               (+-mono-l-≤ k l n p)

Lemma. *-mono-≤

*-mono-≤ : (k l m n : ℕ)

    → k ≤ l

    → m ≤ n

    ---------------

    → k * m ≤ l * n

*-mono-≤ zr zr m n p q = p

*-mono-≤ zr (suc l) m n p q = z≤n

*-mono-≤ (suc k) (suc l) m n (s≤s p) q

  = +-mono-≤ m n (k * m) (l * n) q (*-mono-≤ k l m n p q)

Type families and Unification

Views

data

  Case

    (n : ℕ)

    : Set

  where

  c1 : Case n

  c2 : Case n

  c3 : Case n

  otherwise :  Case n

f : (n : ℕ) → Case n

f 0 = c2

f 1 = c3

f 2 = c1

f 4 = c2

f (suc n) = otherwise

g : ℕ →  ℕ

g n with f n --- fn ≡ w

... | c1 = 2

... | c2 = 0

... | c3 = 1

... | otherwise = _

Comparable numbers view

data

  Comparable

    (m n : ℕ)

      : Set

  where

    less-than    : m ≤ n → Comparable m n

    greater-than : n ≤ m → Comparable m n

≤-total : (m n : ℕ) → Comparable m n

≤-total zero n = less-than z≤n

≤-total (suc m) zero = greater-than z≤n

≤-total (suc m) (suc n) with ≤-total m n -- ≤-total m n ≡ w

... | less-than m≤n   = less-than (s≤s m≤n)

... | greater-than x = greater-than (s≤s x)

Even description

More on Views

data

  Tri

    (n m : ℕ)

    : Set

  where

  c< : n < m → Tri n m

  c> : m < n → Tri n m

  c= : m ≡ n → Tri n m

tri : (n m : ℕ) → Tri n m

tri zr zr      = c= refl

tri zr (suc m) = c< z<s

tri (suc n) zr = c> z<s

tri (suc n) (suc m)

  with tri n m

... | c< x = c< (s<s x)

... | c> x = c> (s<s x)

... | c= x = c= (ap suc x)