実数の構成について
Coqでの実数は9つの項と17の公理で定義されている。項の型と意味はだいたい次の様な感じ。
Parameter R : Set. (* 実数全体 *) Parameter R0 : R. (* 実数の0 *) Parameter R1 : R. (* 実数の1 *) Parameter Rplus : R -> R -> R. (* 実数上での足し算 *) Parameter Rmult : R -> R -> R. (* 実数上での掛け算 *) Parameter Ropp : R -> R. (* 足し算に関する逆元 *) Parameter Rinv : R -> R. (* 掛け算に関する逆元 *) Parameter Rlt : R -> R -> Prop. (* 実数上の"より大きい"を表す述語 *) Parameter up : R -> Z. (* up x はx以上の最小の整数 *)
17の公理は、大きく見て4つの部分に分けられる。
- 実数Rは非自明な体である
Axiom Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1. Axiom Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3). Axiom Rplus_opp_r : forall r:R, r + - r = 0. Axiom Rplus_0_l : forall r:R, 0 + r = r. Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1. Axiom Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3). Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1. Axiom Rmult_1_l : forall r:R, 1 * r = r. Axiom R1_neq_R0 : 1 <> 0. Axiom Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.
- 実数Rは全順序集合である
Axiom total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}. Axiom Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1. Axiom Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3. Axiom Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2. Axiom Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2.
- アルキメデスの原理(いかなる実数に対してもそれより大きい整数が存在する。)
up xは天井関数、IZRは整数Zからの包含写像
Axiom archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.
- 実数Rの連続性(上に有界な領域 E ⊂ R には常に上限が存在する)。
Axiom completeness : forall E:R -> Prop, bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.