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)


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.