Theorems about the natural numbers

Many of these definitions and proofs have been ported from the coq stdlib. Some results are prefixed with nat_ and some are not. Should we be more consistent? We want to close the trunc_scope so that notations from there don't conflict here.

Basic operations on naturals

It is common to call S succ so we add it as a parsing only notation.

The predecessor of a natural number.

Addition of natural numbers

Truncated subtraction: n - m is 0 if n ≤ m

Minimum, maximum

Power

Euclidean division

This division is linear and tail-recursive. In divmod, y is the predecessor of the actual divisor, and u is y sub the real remainder.

Greatest common divisor

We use Euclid algorithm, which is normally not structural, but Coq is now clever enough to accept this (behind modulo there is a subtraction, which now preserves being a subterm)

Square

Square root

The following square root function is linear (and tail-recursive). With Peano representation, we can't do better. For faster algorithm, see Psqrt/Zsqrt/Nsqrt... We search the square root of n = k + p^2 + (q - r) with q = 2p and 0<=r<=q. We start with p=q=r=0, hence looking for the square root of n = k. Then we progressively decrease k and r. When k = S k' and r=0, it means we can use (S p) as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2. When k reaches 0, we have found the biggest p^2 square contained in n, hence the square root of n is p.

Log2

This base-2 logarithm is linear and tail-recursive. In log2_iter, we maintain the logarithm p of the counter q, while r is the distance between q and the next power of 2, more precisely q + S r = 2^(S p) and r<2^p. At each recursive call, q goes up while r goes down. When r is 0, we know that q has almost reached a power of 2, and we increase p at the next call, while resetting r to q. Graphically (numbers are q, stars are r) :

                    10
                  9
                8
              7   *
            6       *
          5           ...
        4
      3   *
    2       *
  1   *       *
0   *   *       *

We stop when k, the global downward counter reaches 0. At that moment, q is the number we're considering (since k+q is invariant), and p its logarithm.

Injectivity of successor

TODO: keep or remove?

Zero is not the successor of a number

Multiplication

Standard associated names

Equality of natural numbers

Boolean equality and its properties

nat has decidable paths

And is therefore a HSet

Inequality of natural numbers

A general form for injectivity of this constructor

Which we specialise to this lemma

We define the less-than relation lt in terms of leq

We declare it as an existing class so typeclass search is performed on its goals.

We add a typeclass instance for unfolding the definition so lemmas about leq can be used.

We should also give them their various typeclass instances

Principle of double induction

Maximum and minimum : definitions and specifications

nth iteration of the function f : A → A. We have definitional equalities nat_iter 0 f x = x and nat_iter n.+1 f x = f (nat_iter n f x). We make this a notation, so it doesn't add a universe variable for the universe containing A.

Preservation of invariants : if f : A → A preserves the invariant P, then the iterates of f also preserve it.

Arithmetic

Exponentiation

Factorials

Natural number ordering

Theorems about natural number ordering

Arithmetic relations between trunc_index and nat.