# Maths - Proof Assist Code

On this page we look at code from proof assistants and programs such as Idris that involve proofs.

First lets look at how mathematical types can be defined.

## Natural Numbers

The best encoding of mathematical structures depends on whether we are computing the algebra or proofs, for example, proofs about natural numbers can be done using Peano encoding, this makes inductive/recursive proofs much more practical, however this encoding is not very practical for general programming or human readability. Some programs such as Idris get round this by automatically converting between them.

This encoding, with a nullary constructor Z (Zero) and a unary constructor S (Successor) completely defines the natural number type, it is initial (see W-type page).

### Idris

github

Idris uses Peano encoding but can automatically convert for more human readable output and more efficient computation.

```data Nat =
||| Zero.
Z
| ||| Successor.
S Nat```

### Agda

github

Again the Peano encoding is automatically converted for more human readable output.

A very good introduction on this site.

```data Nat : Set where
zero : Nat
suc  : (n : Nat) -> Nat```

### Coq

coq library

```Inductive nat : Type :=
| O
| S (n : nat).```

### Arend

library

Functions are included under data which has advantages.

```\data Nat
| zero
| suc Nat
\where {
\func \infixl 6 + (x y : Nat) : Nat \elim y
| 0 => x
| suc y => suc (x + y)

\func \infixl 7 * (x y : Nat) : Nat \elim y
| 0 => 0
| suc y => x * y + x

\func \infixl 6 - (n m : Nat) : Int
| 0, m => neg m
| n, 0 => pos n
| suc n, suc m => n - m

{- | divMod n m returns the pair (q,r) such
- that n = m * q + r and r < m if 0 < m.
-   If m == 0, then divMod n m returns (n,n).
-}
\func divMod (n m : Nat) : \Sigma Nat Nat

\func \infixl 8 div (n m : Nat) => (divMod n m).1

\func \infixl 8 mod (n m : Nat) => (divMod n m).2

\lemma divModProp (n m : Nat) : m * n div m + n mod m = n
}```

## Integers

We can define an integer in terms of (as an extension to) natural numbers. For instance:

Z = N + N

That is, the positive numbers plus the negative numbers, or alternatively:

Z = 2 * N

That is, the positive numbers with a sign.

Neither of these definitions has the nice properties that the natural number definition (above) had, in that these do not completely define integers.

 ```data Nat = Z ||| Zero. | S Nat ||| Successor. | P Nat ||| Predecessor. | S P = P S = Id | S -1 = Z | P Z = -1 ``` To completely define integers we would need equations like this. This has the additional advantage that S is extended to the negative numbers and P is extended to the positive numbers.

However this makes things more complicated and the proof assistants that I looked at don't fully define integers by using equations.

### Idris

`built in - no code`

### Agda

github

```data Int : Set where
pos    : (n : Nat) -> Int
negsuc : (n : Nat) -> Int```

### Coq

coq library

```Inductive Integers : Ensemble nat :=
Integers_defn : forall x:nat, In nat Integers x.```

### Arend

library

```\data Int
| \coerce pos Nat
| neg Nat \with { zero => pos zero }```

## Function Definition (such as Addition)

Now that we can define types we can go on to define functions on those types, such as addition.

The definition is recursive, it defines addition in terms of addition. As with the inductive definition of the naturals, the apparent circularity is not a problem. It works because addition of larger numbers is defined in terms of addition of smaller numbers. Such a definition is called well founded.

### Idris

github

```plus : (x : Nat) -> (y : Nat) -> Nat
plus Z y = y
plus (S k) y = S (plus k y)```

### Agda

github

A very good introduction on this site.

```_+_ : Nat -> Nat -> Nat
zero + n = n
(suc m) + n = suc (m + n)```

### Coq

coq library

```Fixpoint add n m :=
match n with
| 0 => m
| S p => S (p + m)
end```

### Arend

library

part of data definition above.

```    \func \infixl 6 + (x y : Nat) : Nat \elim y
| 0 => x
| suc y => suc (x + y)```

These definitions of addition in natural numbers (Peano encoding) are all basically the same and rely on two identities:

0 + n == n
(1 + m) + n == 1 + (m + n)

In terms of logic (see propositional logic page) we can show them like this:

 n : Nat zero + n = n
 m + n = p (suc m) + n = suc p

## Next

Having coded our mathematical structures we can now go on to discuss how to use them to prove equalities (see page here)