Numbers in Coq

Overview

Type	Module	Notation scope, key
`nat`	`Nat`	`nat`
`positive`	ZArith	`positive_scope`, `positive`
`N`	ZArith	`N`
`Z`	ZArith	`Z`
`R`	`Reals`	`R`
`Q`	`QArith`	`Q`

`nat`

Peano numbers.

Print nat.
(*
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
*)

`positive`

Only positive integers in a binary form.
That means zero is not included.

Require Import ZArith.
Print positive.
(*
Inductive positive : Set :=
| xI : positive -> positive
| xO : positive -> positive
| xH : positive.
*)

xI: insert 1 as LSB
xO: insert 0 as LSB
xH: 1

Compute xH.
(*
= 1%positive
     : positive
*)

Compute xO xH.
(*
= 2%positive
     : positive
*)

Compute xI xH.
(*
= 3%positive
     : positive
*)

We can sort of think of this as the number in binary with the bits in the reverse order.

For example, consider 10%positive, which is xO (xI (xO xH)).

xO (xI (xO xH)).
 |   |   |  |
 v   v   v  v
 0   1   0  1

which is

1010₂ = 10₁₀

All have to end with xH.

Because if xO was allowed as the end, a lone xO would mean zero, which isn't part of positive.

Compute xO (xI (xO xO)).
(*
The term "xO" has type "positive -> positive"
while it is expected to have type "positive".
*)

`N`

Natural numbers in a more 'concise form' than the nat type.

https://coq.inria.fr/doc/v8.19/stdlib/Coq.Numbers.BinNums.html

Require Import ZArith.
Print N.
(*
Inductive N : Set :=
| N0 : N
| Npos : positive -> N.
*)

Constructor	Meaning	`nat` analogue
`N0`	zero	`O`
`Npos`	positive numbers	`S`

Compute N0.
(*
= 0%N
     : N
*)

Compute Npos 1%positive.
(*
= 1%N
     : N
*)

Compute Npos 45%positive.
(*
= 45%N
     : N
*)

So basically, N is positive along with zero.

`Z`

Require Import ZArith.
Print Z.
(*
Inductive Z : Set :=
| Z0 : Z
| Zpos : positive -> Z
| Zneg : positive -> Z.
*)

Z is like N but with an extra constructor to represent negative numbers.

Compute Z0.
(*
= 0%Z
     : Z
*)
Compute Zpos 8%positive.
(*
= 8%Z
     : Z
*)
Compute Zneg 53%positive.
(*
= (-53)%Z
     : Z
*)

`Q`

Rational numbers

Require Import QArith.
Print Q.
(*
Record Q : Set := Qmake {
   Qnum : Z;
   Qden : positive
}.
*)

Rational numbers are numbers which can be represented in p/q form. Qnum and Qden corresponds to p (numerator) and q (denominator) respectively.

Require Import ZArith.
Require Import QArith.

Compute Qmake 2 3.
(*
= 2 # 3
     : Q
*)

Note that we can't make infinity out of Q's Qmake since Qden has to be a value of type positive, which cannot be zero.

Compute Qmake 1 0.
(*
Cannot interpret this number as a value of type positive
*)

Some operations:

Definition a:Q := Qmake 10 5.
Definition b:Q := Qmake 5 10.
Compute a*b.
(*
= 50 # 50
     : Q
*)

Function	Description
`Qred: Q -> Q`	Reduce fraction
`Qopp: Q -> Q`	Negate fraction
`Qinv: Q -> Q`	Inverse of fraction
`Qplus: Q -> Q -> Q`	Add fractions
`Qplus': Q -> Q -> Q`	Add and reduce
`Qminus: Q -> Q -> Q`	Subtract fractions
`Qminus': Q -> Q -> Q`	Subtract and reduce
`Qmult: Q -> Q -> Q`	Multiply fractions
`Qmult': Q -> Q -> Q`	Multiply and reduce
`Qle: Q -> Q -> Prop`
`Qdiv: Q -> Q -> Q`
`Qlt: Q -> Q -> Prop`
`Qeq: Q -> Q -> Prop`
`Qden: Q -> positive`
`Qnum: Q -> Z`
`Qle_bool: Q -> Q -> bool`
`Qpower: Q -> Z -> Q`
`Qpower_positive: Q -> positive -> Q`
`Qeq_bool: Q -> Q -> bool`

`R`

Require Import Reals.

Compute 12%R.                                   
(*
= ((R1 + R1) * ((R1 + R1) * (R1 + (R1 + R1))))%R
     : R
*)

This is like:

((R1 + R1) * ((R1 + R1) * (R1 + (R1 + R1))))
  |    |       |    |      |     |    |
  v    v       v    v      v     v    v
((1  + 1 ) * ((1  + 1 ) * (1  + (1  + 1 ))))
  |    |       |    |      |     |    |
  +--+-+       +--+-+      |     +-+--+
     |            |        |       |      
     v            v        v       v      
     2     *      2   *   (1  +    2)   
     |            |        |       |      
     +-----+------+        +---+---+
           |                   |
           v                   v
           4          *        3
           |                   |
           +----------+--------+
                      |
                      v
                     12

INR can be used to make an R out of a nat.

Check INR.      
(*
INR
     : nat -> R
*)

Compute INR 5.                                  
(*
= (R1 + R1 + R1 + R1 + R1)%R
     : R
*)

CoRN has a different representation of real numbers.

Coq's built-in R is an axiomatic representation.