We’ve mentioned that Agda is a proof assistant, i.e. a system in which one can write proofs that can be checked for validity much like one writes code whose validity is checked by a compiler. A proof as we know it is a sequence of formulas, each one could either be an axiom or follow from a bunch of previous formulas by applying some rule of inference.

In Agda and other systems based on the Curry-Howard correspondence there is another notion of proof, where proofs are programs, formulas are types, and a proof is a correct proof of a certain theorem provided the corresponding program has the type of the corresponding formula. In simpler terms, if one claims a proposition, one has to show the proposition (which is a type) is valid. A type can be shown to be valid if one can either construct an object of that type or provide a means (function) to do so.

Thinking from the computer science perspective, a proof of a theorem can be modeled with a tree, where the root is the theorem, the leaves are the axioms, and the inner nodes follow from their parents by a rule of inference.

While proving a proposition that involves an equality, one may use one side of the equality (say, the right hand side RHS) to prove the other side. We shall see this method, called “equational reasoning”, in detail later.

```
module Types.proofsAsData where
open import Lang.dataStructures
```

Here we present some examples of how to write simple proofs in Agda.

For example, the `<=`

operator can be defined using induction as consisting of two constructors:

- an identity constructor
`ltz`

which compares any natural number with`zero`

- a successive pattern matcher
`lz`

which tries to reduce comparison of`x <= y`

, to`x-1 <= y-1`

:

After applying `lz`

sufficient number of times, if we end up at `0 <= x`

where `ltz`

is invoked, computation terminates and our theorem is proved.

```
data _<=_ : ℕ → ℕ → Set where
: {n : ℕ} → zero <= n
ltz : {m : ℕ} → {n : ℕ} → m <= n → (succ m) <= (succ n)
lt
infix 4 _<=_
```

Now, we can use that to prove a bunch of propositions:

```
: one <= ten
idLess₁ = lt ltz
idLess₁
-- (lt ltz)(one <= ten)
-- ltz (zero <= nine)
-- true
: two <= ten
idLess₁₊ = lt (lt ltz)
idLess₁₊
-- (lt (lt ltz))(two <= ten)
-- (lt ltz)(one <= nine)
-- ltz (zero <= eight)
-- true
: two <= seven
idLess₂ = lt (lt ltz)
idLess₂
: three <= nine
idLess₃ = lt (lt (lt ltz)) idLess₃
```

If we try to compile something that is not true, the compiler will throw an error:

```
: ten <= three
idLess' = lt lt lt lt lt lt lt lt lt ltz idLess'
```

```
68,14-16
proofsAsData.lagda.md:<= _n_31 → succ _m_30 <= succ _n_31) !=< (nine <= two) of
(_m_30 type Set
```

The odd or even proofs can be defined as in the previous proof. Here we successively decrement `n`

till we:

- reach
`even₀`

to prove`n`

is even - reach
`odd₀`

to prove`n`

is odd

```
data Even : ℕ → Set
data Odd : ℕ → Set
data Even where
: Even zero
zeroIsEven : {n : ℕ} → Even n → Even (succ (succ n))
succ
data Odd where
: Odd one
oneIsOdd : {n : ℕ} → Odd n → Odd (succ (succ n)) succ
```

by which we could prove:

```
: Even two
twoisEven = succ zeroIsEven
twoisEven
: Even four
isFourEven = succ (succ zeroIsEven)
isFourEven
: Odd seven
isSevenOdd = succ (succ (succ oneIsOdd)) isSevenOdd
```

Equality of natural numbers can be proven by successively comparing decrements of them, till we reach `0 = 0`

. Else the computation never terminates:

```
data _≡_ : ℕ → ℕ → Set where
: zero ≡ zero
eq₀ : ∀ {n m} → (succ n) ≡ (succ m) eq
```

Similar for not equals:

```
data _≠_ : ℕ → ℕ → Set where
: ∀ n → n ≠ zero
neq₀ : ∀ m → zero ≠ m
neq₁ : ∀ { n m } → (succ n) ≠ (succ m) neq
```

To prove that a particular element of type `A`

belongs to a list `List'`

of type `A`

, we require:

- a reflexive constructor:
`x`

is always in a list containing`x`

and a bunch of other elements`xs`

- a recursive pattern matcher which reduces
`x ∈ list`

to`x ∈ y + list₁`

, which either reduces to`x ∈ x + list₁`

which terminates the computation or`x ∈ list₁`

where `list₁`

is `list`

without `y`

.

```
data _∈_ {A : Set}(x : A) : List A → Set where
: ∀ {xs} → x ∈ (x :: xs)
refl : ∀ {y xs} → x ∈ xs → x ∈ (y :: xs)
succ∈
infixr 4 _∈_
```

Example:

```
: List ℕ
theList = one :: two :: four :: seven :: three :: []
theList
: three ∈ theList
threeIsInList = succ∈ (succ∈ (succ∈ (succ∈ refl))) threeIsInList
```

The relationship we saw earlier between formal proofs and computer programs is called the **Curry-Howard isomorphism**, also known as the **Curry-Howard correspondence**. This states that a proof is a program and the formula it proves is the type of the program. Broadly, they discovered that logical operations have analogues in types as can be seen below:

Type Theory | Logic |
---|---|

`A` |
proposition |

`x : A` |
proof |

`ϕ` , `1` |
⟂, ⊤ |

`A × B` |
A ∧ B (and / conjunction) |

`A + B` |
A ∨ B (or / disjunction) |

`A → B` |
A ⟹ B (implication) |

`x : A ⊢ B(x)` |
predicate |

`x : A ⊢ b : B(x)` |
conditional proof |

\(\Pi_{x:A} B(x)\) | ∀ x B(x) |

\(\Sigma_{x:A} B(x)\) | ∃ x B(x) |

\(p : x =_A y\) | proof of equality |

\(\Sigma_{x,y:A} x =_A y\) | equality relation |