# Constructive and Non-Constructive Proofs in Agda (Part 2): Agda in a Nutshell

Last week, we started a new blog series to introduce you to creating constructive and non-constructive proofs in Agda.

In our previous post, we took a look on logic in itself, we considered classical and intuitionistic logical calculi. It will come in handy today when we start tackling theorem proving in Agda based on a constructive logical framework.

In this article, we will introduce the reader to dependently typed programming and theorem proving in Agda. We will compare our examples of Agda code with their Haskell counterparts. After that, we will consider an example use of Agda in the formalisation of algebra.

## General words on Agda

Agda is a dependently typed functional programming language based on a variant of Martin-Löf type theory. This type theory is a constructive proof-theoretic formal system, so Agda doesn’t have the default features for writing classical logic based proofs in contrast to HOL or Isabelle.

Agda has a Haskell-like syntax and a much richer type system (but we’re working on bringing Haskell to the same level), so we may use Agda as a proof-assistant based on the propositions-as-types paradigm. In other words, Agda is a programming language that allows providing formal proofs within constructive mathematics.

In this section, we will make a brief introduction to the syntax and possibilities of Agda.

See here for a more detailed introduction.

## Basic stuff

### Types in Agda

##### Datatypes

Datatypes in Agda are introduced as generalized algebraic datatypes (GADT):

Trivial example: a datatype of writers and a datatype of their works.

```
data Writers : Set where
Wilde Shelley Byron Sartre Camus : Writers
```

```
data Literature : Set where
DorianGrey Alastor ChildeHarold LaNausée L’Étranger : Literature
```

The typical example is a datatype of unary natural numbers:

```
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
```

In Haskell we define these types as follows:

```
data Writers =
Wilde
| Shelley
| Byron
| Sartre
| Camus
data Literature =
DorianGrey
| Alastor
| ChildeHarold
| LaNausée
| L’Étranger
data ℕ = Zero | Suc ℕ
```

These datatypes are so-called simple datatypes.

##### Parameterized and indexed datatypes

See to read about parameterized and indexed datatypes in more detail.

A parameterized datatype is a datatype that depends on some parameter that should remain the same in the types of constructors. For instance, `List`

is a datatype parameterized over a type `A`

.

```
data List (A : Set) : Set where
Nil : List A
Cons : A → List A → List A
```

Datatypes also can have indexes that could differ from constructor to constructor in contrast to parameters. These datatypes are so-called datatype families. Example:

```
data Vec (A : Set) : ℕ → Set where
Nil : Vec A zero
Cons : {n : ℕ} → A → Vec A n → Vec A (suc n)
```

`Vec`

(vector) is a datatype that is applied to another type `A`

and a natural number `n`

. We also say that `Vec`

is parameterized by `A`

and indexed by `ℕ`

. `Nil`

is an empty vector. `Cons`

is a constructor adding a new element to a given vector increasing the length counter. Here `n`

is an implicit argument of the constructor. `Cons`

is also an example of a dependent function, as will be seen below.

In Haskell, we would have the following GADT via `DataKinds`

, `PolyKinds`

and `GADTs`

extensions:

```
{-# LANGUAGE DataKinds, PolyKinds, GADTs #-}
import Data.Kind (Type)
data Vec :: Type -> ℕ -> Type where
Nil :: Vec a 'Zero
Cons :: a -> Vec a n -> Vec a ('Succ n)
```

Another example: `Fin`

is a type that describes finite types, in other words, types of finite cardinality. Informally, `Fin`

is a type of finite sets:

```
data Fin : ℕ → Set where
zero : {n : ℕ} → Fin (suc n)
suc : {n : ℕ} → Fin n → Fin (suc n)
```

`Fin`

is a datatype indexed by a natural number. `zero`

reflects an empty set which is an element of any finite set. `suc`

is a constructor that applies the finite set `i`

and yields a new finite set, which is a larger than `i`

on one element.

In Haskell, we define `Fin`

using `DataKinds`

and `KindSignatures`

extensions as with vectors above:

```
{-# LANGUAGE DataKinds, PolyKinds, GADTs #-}
import Data.Kind (Type)
data Fin :: Nat -> Type where
Fzero :: forall (n :: ℕ). Fin ('Succ n)
Fsucc :: forall n. Fin n -> Fin ('Succ n)
```

Note that, datatypes `Vec`

and `Fin`

implemented in Agda are also examples of dependent types, these types depend on values (in particular, on natural numbers), not only on types.

On the other hand, their counterparts in Haskell are not dependent types in a strict sense, because `forall (n :: ℕ)`

in Haskell does not introduce a value, therefore `Fin`

does not depend on any values.

See here for an introduction to type level programming in Haskell.

### Functions

Functions in Agda are arranged similarly to Haskell, using pattern matching:

```
bookToWriter : Literature → Writers
bookToWriter DorianGrey = Wilde
bookToWriter Alastor = Shelley
bookToWriter ChildeHarold = Byron
bookToWriter LaNausée = Sartre
bookToWriter L’Étranger = Camus
```

We will discuss dependent functions in more detail. A dependent function is a function that takes a term `a`

of type `A`

and returns some result of type `B`

, where `a`

may appear in `B`

. We consider a simple example, where `a`

is a type itself.

```
const₁ : (A B : Set) → A → B → A
const₁ A B x y = x
```

Here types `A`

and `B`

are explicit arguments. If we don’t need to mention these types explicitly, we may take them implicitly:

```
const₂ : {A B : Set} → A → B → A
const₂ x y = x
```

We may compare this function in Agda with a similar function implemented in Haskell with the help of the `RankNTypes`

extension that allows writing the universal quantifier on types explicitly:

```
{-# LANGUAGE RankNTypes #-}
const₁ :: forall a b. a -> b -> a
const₁ x y = x
```

We introduce the following datatypes to consider the next example:

```
data Ireland : Set where
Dublin : Ireland
```

```
data England : Set where
London : England
```

```
data France : Set where
Paris : France
```

After that, we construct a function that returns some country datatype for a given writer.

```
WriterToCountry : Writers → Set
WriterToCountry Wilde = Ireland
WriterToCountry Shelley = England
WriterToCountry Byron = England
WriterToCountry Sartre = France
WriterToCountry Camus = France
```

```
WriterToCity : (w : Writers) → WriterToCountry w
WriterToCity Wilde = Dublin
WriterToCity Shelley = London
WriterToCity Byron = London
WriterToCity Sartre = Paris
WriterToCity Camus = Paris
```

`WriterToCity`

is an example of a dependent function, because the type of the result depends on the argument. The type of a dependent function is the so-called $\Pi$-type. More generally, suppose we have some function `P: A → Set`

, then $\Pi$-type is a type of the function that assigns to every term `t : A`

some object of type `P t`

. In Agda notation, we write this type as ` (t : A) → P t`

for some `{A : Set} {P : A → Set}`

in context.
Logically $\Pi$-type encodes intuitionistic universal quantifier. In other words, `P`

is a predicate and some function of a type ` (t : A) → P t`

is a proof that for each `t : A`

the property `P`

has established.

In Haskell, we don’t have dependent quantification at term level, but we have it at type level. Therefore, we implement comparable functions as closed type families. Similarly, we promote values of type `Writers`

into the type level via `DataKinds`

in both cases:

```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
data Ireland = Dublin
data France = Paris
data England = London
type family WriterToCountry (a :: Writers) :: Type where
WriterToCountry 'Wilde = Ireland
WriterToCountry 'Shelley = England
WriterToCountry 'Byron = England
WriterToCountry 'Sartre = France
WriterToCountry 'Camus = France
```

Also, we declare `WriterToCity`

type family that is similar to `WriterToCity`

function implemented in Agda. In contrast to Agda, we should enable the language extension called `TypeInType`

. You may implement this function via `PolyKinds`

since GHC 8.6.

```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
type family WriterToCity (a :: Writers) :: WriterToCountry a where
WriterToCity 'Wilde = 'Dublin
WriterToCity 'Shelley = 'London
WriterToCity 'Byron = 'London
WriterToCity 'Camus = 'Paris
WriterToCity 'Sartre = 'Paris
```

### Dependent pairs

We introduce the dependent pair type ($\Sigma$-type) through a simple example.

Let us consider the following inductive predicate on two lists as a GADT:

```
data IsReverse {A : Set} : (xs ys : List A) → Set where
ReverseNil : IsReverse [] []
ReverseCons : (x : A) (xs ys : List A)
→ IsReverse xs ys
→ IsReverse (x ∷ xs) (ys ++ [ x ])
```

`IsReverse xs ys`

denotes that the list `ys`

is equal to reversed `xs`

. `IsReverse`

is a datatype parameterized over a type `A`

and indexed over two lists of elements of type `A`

.

We prove the theorem that for all list `xs`

there exists list `ys`

such that `ys`

is a reversed list `xs`

. In other words, we should produce a dependent pair, where the first projection of this pair is some list `ys`

and the second one is a proof that `ys`

is reversed list `xs`

.
We use the dependent pair type to prove existence:

```
theoremReverse₁ : {A : Set} (xs : List A) → Σ (List A) (λ ys → IsReverse xs ys)
theoremReverse₁ [] = [] , ReverseNil
theoremReverse₁ (z ∷ zs) =
let ys = proj₁ (theoremReverse₁ zs) in
let ysProof = proj₂ (theoremReverse₁ zs) in
ys ++ [ x ] , ReverseCons z zs ys ysProof
```

We should read the signature ` {A : Set} (xs : List A) → Σ (List A) (λ ys → IsReverse xs ys)`

as “let `A`

be type and `xs`

be a list with elements of the type A, then there exists list `ys`

, such that `ys`

is the reversed list `xs`

”.

We prove this theorem by induction on `xs`

and build `ys`

for every case. If `xs`

is empty, then we present an empty list as the desired list `ys`

and `ReverseNil`

is a proof that `ys`

is equal to reversed list `xs`

, because both of them are empty. Thus, we have proved the base case.
The inductive step is a case when `xs`

is a non-empty list, i.e. `xs = z :: zs`

. List `zs`

is smaller than `z :: zs`

, so we can apply induction hypothesis to `zs`

and show that `::`

preserves the desired property using the `ReverseCons`

constructor.

Generally, $\Sigma$-type is defined in Agda as follows:

```
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
constructor _,_
field
fst : A
snd : B fst
```

This record is defined for arbitrary universes, and we consider below what universes are in more detail. The given record has two fields. The first field called `fst`

is an object of a type A. The second one is an application `B`

to the argument from the first field.
From a logical point of view, we read `Σ A B`

as “there exists some element of a type `A`

, such that this element satisfies property `B`

”, i.e. $\Sigma$-type encodes constructive existential quantifier. As we have told before, to prove the existence of some object with desired property constructively, then we should present the particular object and prove this object satisfies this considered property.

### Universes

A hierarchy of types is a quite old idea that initially belongs to the logician and philosopher Bertrand Russell. The basic types such as `Nat`

or `Bool`

have a type called `Set`

, but `Set`

is not `Set`

itself. `Set`

has a type `Set₁`

, etc. Otherwise, we could infer Russell’s paradox, so our system would be inconsistent in that case.

Universe polymorphism also allows defining functions that can be called on types of arbitrary levels. Let us show how universe polymorphism works on the following example. Suppose we have this function called `s`

:

```
s : {A B C : Set} → (A → B → C) → (A → B) → A → C
s f g x = f x (g x)
```

We implement a similar function in Haskell via `RankNTypes`

:

```
{-# LANGUAGE RankNTypes #-}
s :: forall a b c. (a -> b -> c) -> (a -> b) -> a -> c
s f g x = f x (g x)
```

We can indicate that types `A`

, `B`

, `C`

are types of arbitrary level `a`

:

```
s₁ : {a : Level} {A B C : Set a} → (A → B → C) → (A → B) → A → C
s₁ f g x = f x (g x)
```

We generalize `s`

further, because `A`

, `B`

and `C`

in `s₁`

belong to the same level, but these types may generally belong to different levels :

```
s₂ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c}
→ (A → B → C) → (A → B) → A → C
s₂ f g x = f x (g x)
```

We would implement something similar as closed type family in Haskell:

```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
type family S₂ (f :: a -> b -> c) (g :: a -> b) (x :: a) :: c where
S₂ f g x = f x (g x)
```

By the way, the most general version of `s`

in Agda is an universe polymorphic dependent function:

```
S : {a b c : Level} {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c}
→ (f : (x : A) → (y : B x) → C x y) → (g : (x : A) → B x)
→ (x : A) → C x (g x)
S f g x = f x (g x)
```

### Records

Records in Agda are arranged similarly to Haskell. This record implemented in Haskell

```
data Person = Person {
name :: String
, country :: String
, age :: Int
}
```

may be translated to Agda as follows via keyword `record`

:

```
record Person : Set where
field
name : String
country : String
age : Int
```

Typeclasses are introduced in Agda as records. For example, we implement typeclass called `Functor`

:

```
record Functor {a} (F : Set a → Set a) : Set (suc a) where
field
fmap : ∀ {A B} → (A → B) → F A → F B
```

Instances may be declared either by constructing a record explicitly or by using copatterns:

```
instance
ListFunctor₁ : Functor List
ListFunctor₁ = record { fmap = map }
```

```
instance
ListFunctor₂ : Functor List
fmap {{ListFunctor₂}} = map
```

### Propositional equality

The identity type is a datatype that reflects equality of terms in predicate logic. This type is defined as follows:

```
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
```

We consider a few examples where propositional equality is used. The first one is a proof of distributivity of natural number multiplication over addition.

```
*-+-distr : ∀ a b c → (b + c) * a ≡ b * a + c * a
*-+-distr a zero c = refl
*-+-distr a (suc b) c =
begin
(suc b + c) * a ≡⟨ refl ⟩
a + (b + c) * a ≡⟨ cong (_+_ a) (*-+-distr a b c) ⟩
a + (b * a + c * a) ≡⟨ sym (+-assoc a (b * a) (c * a)) ⟩
suc b * a + c * a
∎
```

This property is proved by induction on `b`

. When `b`

equals zero, the equality holds trivially. Otherwise, if `b`

is a non-zero number, then equality is proved using the induction hypothesis.

##### Propositional equality in Haskell

See the relevant part of the Haskell Prelude documentation.

We have propositional equality in Haskell as well:

```
data a :~: b where
Refl :: a :~: a
```

Unlike in Agda, this datatype is defined on types of arbitrary kinds, not on terms. In other words, `(:~:) :: k -> k -> *`

, where `k`

is an arbitrary kind.

## Algebraic example

We consider a few more examples in Agda to better understand its possibilities. Remember the abstract algebra, especially ring theory. We provide some algebraic definitions below:

**Definition 3***A ring is an algebraic system $\langle R, +, \cdot, -, 0 \rangle$, where $R$ is a non-empty set, $0 \in R$,
$+$, $\cdot$ are binary operations on $R$ and $-$ is a unary operation on $R$ such that:*

- $\forall a, b, c \in R, (a + b) + c = a + (b + c)$;
- $\forall a, b \in R, a + b = b + a$;
- $\forall a \in R, - a + a = 0$;
- $\forall a \in R, a + 0 = a$;
- $\forall a, b, c \in R, (a + b) \cdot c = (a \cdot c) + (b \cdot c)$;
- $\forall a, b, c \in R, a \cdot (b + c) = (a \cdot b) + (a \cdot c)$.

We define a ring in Agda similarly by declaring a record called `Ring`

. `Ring`

is a type `R`

with additional operations:

```
record Ring (R : Set) : Set₁ where
constructor mkRing
infixr 7 _·_
infixr 6 _+_
field
θ : R
-_ : R → R
_+_ : R → R → R
_·_ : R → R → R
```

After that, we formulate the axioms of a ring having declared operations above:

```
+-assoc : (a b c : R) → (a + b) + c ≡ a + (b + c)
+-commute : (a b : R) → a + b ≡ b + a
+-inv₁ : (a : R) → - a + a ≡ θ
+-θ : (a : R) → a + θ ≡ a
·-distr-right : (a b c : R) → (a + b) · c ≡ (a · c) + (b · c)
·-distr-left : (a b c : R) → a · (b + c) ≡ (a · b) + (a · c)
open Ring {{...}} public
```

It is easy to see that the definition of a ring in Agda is similar to the informal definition of a ring proposed above.

Suppose we need to extend a ring with additional axioms. Consider a Lie ring that generalizes Lie algebra, which is a well-known construction in linear algebra widely applied in mathematical physics and quantum mechanics. Initially, we suggest the following informal definition:

**Definition 4***A Lie ring is a ring $\langle R, +, \cdot, -, 0 \rangle$ with two additional axioms:*

- (Alternation) $\forall a \in R, a \cdot a = 0$;
- (Jacobi identity) $\forall a, b, c \in R, (a \cdot b) \cdot c + b \cdot (c \cdot a) + c \cdot (a \cdot b) = 0$.

We extend a ring to a Lie ring in Agda by declaring a new record, but we need to tell somehow that a given type `R`

is already a ring. We pass an additional instance argument in a signature of a record called `LieRing`

for this purpose:

```
record LieRing (R : Set){{ring : Ring R}} : Set₁ where
```

Then we add the special axioms of a Lie ring as usual:

```
constructor mkLeeRing
field
alternation : (a : R) → a · a ≡ θ
jacobiIdentity : (a b c : R) → (a · b) · c + b · (c · a) + c · (a · b) ≡ θ
```

Lie ring is anticommutative, in other words:

**Lemma 1***Let $R$ be Lie ring, then forall $a, b \in R$, $a \cdot b + b \cdot a = 0$.*

* Proof*
Firstly, we prove this fact informally. For convenience, we prove this useful proposition.

**Proposition 1***If $R$ is a Lie ring, then forall $a, b \in R$, $(a + b) \cdot (a + b) = (a \cdot b) + (b \cdot a)$.*

$\begin{array}{lll} & (a + b) \cdot (a + b) = & \\ & \quad\quad\quad\quad\quad\quad\quad \text{Right distribution} & \\ & a \cdot (a + b) + b \cdot (a + b) = & \\ & \quad\quad\quad\quad\quad\quad\quad \text{Left distribution} & \\ & (a \cdot a + a \cdot b) + (b \cdot a + b \cdot b) = & \\ & \quad\quad\quad\quad\quad\quad\quad \text{Alternation}& \\ & (a \cdot a + a \cdot b) + (b \cdot a + 0) = & \\ & \quad\quad\quad\quad\quad\quad\quad \text{Identity axiom}& \\ & (a \cdot a + a \cdot b) + b \cdot a = & \\ & \quad\quad\quad\quad\quad\quad\quad \text{Alternation}& \\ & (0 + a \cdot b) + b \cdot a = & \\ & \quad\quad\quad\quad\quad\quad\quad \text{Identity axiom}& \\ & a \cdot b + b \cdot a& \end{array}$ $\Box$

Thus $a \cdot b + b \cdot a = (a + b) \cdot (a + b) = 0$ by proposition above and alternation.

$\Box$

Formalisation of this proof completely preserves the reasoning above. The first lemma is the sequence of equalities applied sequentially via transitivity of propositional equality:

```
lemma : (a b : R) → (a + b) · (a + b) ≡ (a · b) + (b · a)
lemma a b =
begin
((a + b) · (a + b)
≡⟨ ·-distr-right a b (a + b) ⟩
a · (a + b) + b · (a + b)
≡⟨ cong₂ _+_ (·-distr-left a a b) (·-distr-left b a b) ⟩
(a · a + a · b) + (b · a + b · b)
≡⟨ cong (_+_ (a · a + a · b)) (cong₂ _+_ refl (alternation b)) ⟩
(a · a + a · b) + (b · a + θ)
≡⟨ cong (_+_ (a · a + a · b)) (+-θ (b · a)) ⟩
(a · a + a · b) + (b · a)
≡⟨ cong₂ _+_
(cong₂ _+_ (alternation a) refl)
refl ⟩
(θ + a · b) + (b · a)
≡⟨ cong₂ _+_ (trans (+-commute θ (a · b)) (+-θ (a · b))) refl ⟩
(a · b + b · a)
∎)
```

Anticommutativity is proved in the same way using the obtained lemma:

```
anticommutativity : (a b : R) → (a · b + b · a) ≡ θ
anticommutativity a b = (a · b + b · a) ≡⟨ sym $ lemma a b ⟩ (alternation (a + b))
```

## Conclusion

In this post, we have briefly described basic concepts of dependently typed programming and theorem proving in Agda via examples. In the next post, we will introduce negation with classical postulates and play with non-constructive proofs in Agda.