The Coq mailing list

[Milad Niqui <milad AT cs.ru.nl>]

Hi there,

Sorry for replying to myself, but I would like to point out that in my
previous email this:

> Then, as shown below (missing_axioms.v), both of the removed axioms will
> be derivable using all the remaining axioms (except completeness which
> is not needed). 

is an understatement. In fact the only axioms that were needed to derive
the two removed axioms

> - We remove [R1_neq_R0 : 1<>0];
> - We remove [total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > 
> r2}].

are the following.

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 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 archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.

In other words we don't need multiplication. We only need a constant 1
in our langauge that satisfies the [archimed] axiom.

Regards,

Milad