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).
IdrisIdris uses Peano encoding but can automatically convert for more human readable output and more efficient computation. |
data Nat =
||| Zero.
Z
| ||| Successor.
S Nat |
AgdaAgain 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 |
Inductive nat : Type := | O | S (n : nat). |
ArendFunctions 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 |
data Int : Set where pos : (n : Nat) -> Int negsuc : (n : Nat) -> Int |
Coq |
Inductive Integers : Ensemble nat :=
Integers_defn : forall x:nat, In nat Integers x. |
Arend |
\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
|
plus : (x : Nat) -> (y : Nat) -> Nat
plus Z y = y
plus (S k) y = S (plus k y) |
AgdaA very good introduction on this site. |
_+_ : Nat -> Nat -> Nat
zero + n = n
(suc m) + n = suc (m + n) |
Coq |
Fixpoint add n m := match n with | 0 => m | S p => S (p + m) end |
Arendpart 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:
|
|
Next
Having coded our mathematical structures we can now go on to discuss how to use them to prove equalities (see page here)