How to formalize stuff in Agda
==============================

Preliminaries
-------------

For this presentation, we keep the dependencies to a minimum.

```
open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
```

A `variable` declaration allows us to use variables without binding
them explicitly. This means they are implicitly universally quantified
in the types where they occur.

```
variable
  A B C : Set
  x y z : A
  k l m n : Nat
```

(Unary) natural numbers are defined as the datatype `Nat` with two
constructors `zero : Nat` and `suc : Nat → Nat`.

```
_ : Nat
_ = zero + 7 * (suc 3 - 1)
```

We can define polymorphic types and functions by pattern matching on
them. For example, here is the equivalent of Haskell's `Maybe` type.

```
data Maybe (A : Set) : Set where
  just    : A → Maybe A
  nothing :     Maybe A

mapMaybe : (A → B) → (Maybe A → Maybe B)
mapMaybe f x = {!!}
```

Note how `A` and `B` are implicitly quantified in the type of
`mapMaybe`!




The Curry-Howard correspondence
-------------------------------

Under the Curry-Howard correspondence, we can interpret logical
propositions (A ∧ B, ¬A, A ⇒ B, ...) as the types of all their
possible proofs.

A proof of 'A and B' is a *pair* (x , y) of a proof `x : A` and an
proof `y : B`.

```
record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_
```

A proof of 'A or B' is either `inl x` for a proof `x : A` or `inr y`
for a proof `y : B`.

```
data _⊎_ (A B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B
```

A proof of 'A implies B' is a transformation from proofs `x : A` to
proofs of `B`, i.e. a function of type `A → B`.

'true' has exactly one proof `tt : ⊤`.

```
record ⊤ : Set where
  constructor tt     -- no fields
```

'false' has no proofs.

```
data ⊥ : Set where   -- no constructor
```

'not A' can be defined as 'A implies false'.

```
¬_ : Set → Set
¬ A = A → ⊥
```

### Exercises

```
-- “If A then B implies A”
ex₁ : A → (B → A)
ex₁ = {!!}

-- “If A and true then A or false”
ex₂ : (A × ⊤) → (A ⊎ ⊥)
ex₂ = {!!}

-- “If A implies B and B implies C then A implies C ”
ex₃ : (A → B) → (B → C) → (A → B)
ex₃ = {!!}

-- “Either A or not A”
ex₄ : A ⊎ (¬ A)
ex₄ = {!!}

-- “It is not the case that not (either A or not A)”
ex₅ : ¬ (¬ (A ⊎ (¬ A)))
ex₅ = {!!}

```

Equality
--------

To state many properties of our programs, we need the notion of
equality. In Agda, equality is defined as the datatype `_≡_` with one
constructor `refl : x ≡ x`.

```

_ : x ≡ x
_ = refl

sym : x ≡ y → y ≡ x
sym x≡y = {!!}

trans : x ≡ y → y ≡ z → x ≡ z
trans x≡y y≡z = {!!}

cong : (f : A → B) → x ≡ y → f x ≡ f y
cong f x≡y = {!!}
```


Ordering natural numbers
------------------------


The standard ordering on natural numbers can be defined as an *indexed
datatype* with two indices of type `Nat`:

```
module Nat-≤ where
  data _≤_ : Nat → Nat → Set where
    ≤-zero :         zero  ≤ n
    ≤-suc  : m ≤ n → suc m ≤ suc n

  ≤-refl : n ≤ n
  ≤-refl = {!!}

  ≤-trans : k ≤ l → l ≤ m → k ≤ m
  ≤-trans = {!!}

  ≤-antisym : m ≤ n → n ≤ m → m ≡ n
  ≤-antisym = {!!}
```

We define separate 'instance' versions of the constructors to help us
later on. A definition `inst : A` that is marked as an 'instance' will
be used to automatically construct arguments to functions of type
`{{x : A}} → B`.

```
  instance
    ≤-zero-I : zero ≤ n
    ≤-zero-I = ≤-zero

    ≤-suc-I : {{x ≤ y}} → suc x ≤ suc y
    ≤-suc-I {{x≤y}} = ≤-suc x≤y
```



Partial orders
--------------

We'd like to talk not just about orderings on concrete types like
`Nat`, but also about the general concept of a 'partial order'.

```
record Ord (A : Set) : Set₁ where
  field
    _≤_       : A → A → Set
    ≤-refl    : x ≤ x
    ≤-trans   : x ≤ y → y ≤ z → x ≤ z
    ≤-antisym : x ≤ y → y ≤ x → x ≡ y

  _≥_ : A → A → Set
  x ≥ y = y ≤ x

open Ord {{...}}

instance
  Ord-Nat : Ord Nat
  _≤_       {{Ord-Nat}} = Nat-≤._≤_
  ≤-refl    {{Ord-Nat}} = Nat-≤.≤-refl
  ≤-trans   {{Ord-Nat}} = Nat-≤.≤-trans
  ≤-antisym {{Ord-Nat}} = Nat-≤.≤-antisym

instance
  Ord-⊤ : Ord ⊤
  _≤_       {{Ord-⊤}} = {!!}
  ≤-refl    {{Ord-⊤}} = {!!}
  ≤-trans   {{Ord-⊤}} = {!!}
  ≤-antisym {{Ord-⊤}} = {!!}

module Example (A : Set) {{A-≤ : Ord A}} where

  cycle : {x y z : A} → x ≤ y → y ≤ z → z ≤ x → x ≡ y
  cycle x≤y y≤z z≤x = {!!}
```

For working with binary search trees, we need to be able to decide for
any two elements which is the bigger one, i.e. we need a *total*,
*decidable* order.

```
data Tri {{_ : Ord A}} : A → A → Set where
  less    : x ≤ y → Tri x y
  equal   : x ≡ y → Tri x y
  greater : x ≥ y → Tri x y

record TDO (A : Set) : Set₁ where
  field
    {{Ord-A}} : Ord A
    tri       : (x y : A) → Tri x y

open TDO {{...}} public

triNat : (x y : Nat) → Tri x y
triNat x y = {!!}

instance
  TDO-Nat : TDO Nat
  Ord-A {{TDO-Nat}} = Ord-Nat
  tri   {{TDO-Nat}} = triNat
```



Binary search trees
-------------------

In a dependently typed language, we can encode invariants of our data
structures by using *indexed datatypes*. In this example, we will
implement binary search trees by a lower and upper bound to the
elements they contain.

Since the lower bound may be -∞ and the upper bound may be +∞, we
start by providing a generic way to extend a partially ordered set
with those two elements.

```
data [_]∞ (A : Set) : Set where
  -∞  :     [ A ]∞
  [_] : A → [ A ]∞
  +∞  :     [ A ]∞

variable
  lower upper : [ A ]∞

module Ord-[]∞ {A : Set} {{ A-≤ : Ord A}} where

  data _≤∞_ : [ A ]∞ → [ A ]∞ → Set where
    -∞-≤ :          -∞   ≤∞   y
    []-≤ : x ≤ y → [ x ] ≤∞ [ y ]
    +∞-≤ :           x   ≤∞  +∞

  instance
    Ord-[]∞ : {{_ : Ord A}} → Ord [ A ]∞
    _≤_       {{Ord-[]∞}} = _≤∞_
    ≤-refl    {{Ord-[]∞}} = {!!}
    ≤-trans   {{Ord-[]∞}} = {!!}
    ≤-antisym {{Ord-[]∞}} = {!!}

open Ord-[]∞ public

```

Again we define 'instance' versions of the constructors.

```
module _ {{_ : Ord A}} where

  instance
    -∞-≤-I : {y : [ A ]∞} → -∞ ≤ y
    -∞-≤-I = -∞-≤

    +∞-≤-I : {x : [ A ]∞} → x ≤ +∞
    +∞-≤-I = +∞-≤

    []-≤-I : {x y : A} {{x≤y : x ≤ y}} → [ x ] ≤ [ y ]
    []-≤-I {{x≤y = x≤y}} = []-≤ x≤y
```

Now we are (finally) ready to define binary search trees.

```
data BST (A : Set) {{_ : Ord A}} (lower upper : [ A ]∞) : Set where
  leaf : {{l≤u : lower ≤ upper}} → BST A lower upper
  node : (x : A) → BST A lower [ x ] → BST A [ x ] upper → BST A lower upper

_ : BST Nat -∞ +∞
_ = node 42
      (node 6    leaf leaf)
      (node 9000 leaf leaf)
```

Note how instances help by automatically filling in the proofs!



Next up: defining a lookup function. The result of this function is
not just a boolean true/false, but a *proof* that the element is
indeed in the tree.


```
module Lookup {{_ : TDO A}} where

  data _∈_ {lower} {upper} (x : A) : (t : BST A lower upper) → Set where
    here  : ∀ {t₁ t₂} → x ≡ y  → x ∈ node y t₁ t₂
    left  : ∀ {t₁ t₂} → x ∈ t₁ → x ∈ node y t₁ t₂
    right : ∀ {t₁ t₂} → x ∈ t₂ → x ∈ node y t₁ t₂

  lookup : ∀ {lower} {upper}
         → (x : A) (t : BST A lower upper) → Maybe (x ∈ t)
  lookup x t = {!!}
```


Similarly, we can define an insertion function. Here, we need to
enforce the precondition that the element we want to insert is between
the bounds.

```
module Insert {{_ : TDO A}} where

  insert : (x : A) {{l≤x : lower ≤ [ x ]}} {{x≤u : [ x ] ≤ upper}}
         → (t : BST A lower upper) → BST A lower upper
  insert x t = {!!}
```

To prove correctness of insertion, we have to show that `y ∈ insert x
t` is equivalent to `x ≡ y ⊎ y ∈ t`.

```
  module Insert-Correct (x : A) {{_ : lower ≤ [ x ]}} {{_ : [ x ] ≤ upper}} where

    open Lookup

    insert-sound : (t : BST A lower upper)
                 → (x ≡ y) ⊎ (y ∈ t) → y ∈ insert x t
    insert-sound t = {!t!}

    insert-complete : (t : BST A lower upper)
                    → y ∈ insert x t → (x ≡ y) ⊎ (y ∈ t)
    insert-complete t = {!!}

```