[Coq] Arithmetic in Coq : N

Nは二進数で表現された自然数の型です。

Require Import NArith.すると使用出来ます。型の定義は下記の様です。

Inductive N : Set :=  N0 : N | Npos : positive -> N

positiveは下記の様に定義されています。

Inductive positive : Set :=
    xI : positive -> positive | xO : positive -> positive | xH : positive

こんな感じで正の数を表現しています。xHが最上位ビットで、xIが x -> 2x+1, xOが x -> 2x ということです。

Coq < Check (xO (xI (xO xH))).
10%positive : positive

これは(1~0~1~0)%positive.とも書けます。

natとの変換は下記で可能。

nat_of_N : N -> nat
N_of_nat : nat -> N

演算子は

Ndouble_plus_one, Ndouble : N -> N
Nsucc, Npred : N -> N
Nplus, Nminus, Nmult : N -> N -> N　。+, -, * もあり。
Ncompare : N -> N -> comparison 。Infixで ?=
  comparisonは、
  Inductive comparison : Set :=
    Eq : comparison | Lt : comparison | Gt : comparison
Nlt, Ngt, Nle, Nge : N -> N -> Prop　。Infix で <, <=, >, >=
Nmin, Nmax : N -> N -> N
Ndiv2 : N -> N

Nに関する帰納法は次の２つの好きな方を使える。Nrectを用いてNindもある。

N_ind_double
     : forall (a : N) (P : N -> Prop),
       P 0%N ->
       (forall a0 : N, P a0 -> P (Ndouble a0)) ->
       (forall a0 : N, P a0 -> P (Ndouble_plus_one a0)) -> P a
Nrect
     : forall P : N -> Type,
       P 0%N -> (forall n : N, P n -> P (Nsucc n)) -> forall n : N, P n

Require Import ZArith.ZOdiv.すれば、

Ndiv_eucl : N -> N -> N * N
Ndiv : N -> N -> N
Nmod : N -> N -> N
Theorem Ndiv_eucl_correct: forall a b,
  let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N.

と除算も使える。

---
追記
ZArith.ZOdivと、ZArithの中でImportしてるZArith.Zdivとは互換性無いのだな。
ZArithを使わないことはまず無いので、ZOdivは使わないほうがよさそう。