[Coq] Arithmetic in Coq : nat

Coqで大きな自然数あるいは整数を使いたくなったので調べてみました。

★nat

　Coqで自然数というと基本はnatです。natというと自分で作る物であるかの様な気すらしますが勿論標準で備わっています。
　natを使う場合Require Import Arith.すると標準ライブラリが使えます。

●基本
Init.Peanoの中で、pred, plus, mult, le, lt, ge, gtが定義されていてImport不要で使える。

●大小比較関係

- eq_nat : nat -> nat -> Prop
-- heorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}. が使える
- lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. こんな感じで使う
Definition nat_compare (n m:nat) :=
  match lt_eq_lt_dec n m with 
    | inleft (left _) => Lt
    | inleft (right _) => Eq
    | inright _ => Gt
  end.
-- le_lt_dec n m : {n <= m} + {m < n}. など

●四則演算

- 末尾再帰なtail_plusというのもある
- minus : nat -> nat -> nat. n - m とかも書ける。結果が負になる場合もOを返す。
- min, max : nat -> nat -> nat.
- div2, double : nat -> nat.
- 除算は無いが、Require Import Arith.Euclid. すれば商と剰余には下記がある
-- quotient : forall n, n > 0 ->
    forall m:nat, {q : nat | exists r : nat, m = q * n + r /\ n > r}.
-- modulo : forall n, n > 0 ->
    forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}.