The Coq mailing list

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

Hi,

Tonny Hurkens and I suggest that the file Raxioms.v in the standard
library be modified as follows.

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

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). In particular they are both a consequence of the very
strong [archimed] axiom (strong in the sense that it assumes the
extractable existence of a function from R->Z that behaves similar to
the ceiling functions).

Milad Niqui

--8<-----------------------------------------------------------------
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: Raxioms.v 9245 2006-10-17 12:53:34Z notin $ i*)

(************************************************************************)
(* Modified by Tonny Hurkens and Milad Niqui                            *)
(** Modification as follows:
 - We remove [R1_neq_R0 : 1<>0];
 - We remove [total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > 
r2}].

The two removed axioms will then follow from the remaining axioms
except [completeness].  *)


(*********************************************************)
(**    Axiomatisation of the classical reals             *)
(*********************************************************)

Require Export ZArith_base.
Require Export Rdefinitions.
Open Local Scope R_scope.

(*********************************************************)
(** *            Field axioms                            *)
(*********************************************************)

(*********************************************************)
(** **   Addition                                        *)
(*********************************************************)

(**********)
Axiom Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1.
Hint Resolve Rplus_comm: real.

(**********)
Axiom Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3).
Hint Resolve Rplus_assoc: real.

(**********)
Axiom Rplus_opp_r : forall r:R, r + - r = 0.
Hint Resolve Rplus_opp_r: real v62.

(**********)
Axiom Rplus_0_l : forall r:R, 0 + r = r.
Hint Resolve Rplus_0_l: real.

(***********************************************************)       
(** **    Multiplication                                   *)
(***********************************************************)

(**********)
Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
Hint Resolve Rmult_comm: real v62. 

(**********)
Axiom Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
Hint Resolve Rmult_assoc: real v62.

(**********)
Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
Hint Resolve Rinv_l: real.

(**********)
Axiom Rmult_1_l : forall r:R, 1 * r = r.
Hint Resolve Rmult_1_l: real.

(**********)
(* Axiom R1_neq_R0 : 1 <> 0. *)
(* Hint Resolve R1_neq_R0: real. *)

(*********************************************************)
(** **   Distributivity                                  *)
(*********************************************************)

(**********)
Axiom
  Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.
Hint Resolve Rmult_plus_distr_l: real v62.

(*********************************************************)
(** *    Order axioms                                    *)
(*********************************************************)

(* Axiom total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}. *)

(*********************************************************)
(** **   Lower                                           *)
(*********************************************************)

(**********)
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.

Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.

(**********************************************************) 
(** *    Injection from N to R                            *)
(**********************************************************)

(**********)
Boxed Fixpoint INR (n:nat) : R :=
  match n with
  | O => 0
  | S O => 1
  | S n => INR n + 1
  end.  
Arguments Scope INR [nat_scope].


(**********************************************************) 
(** *    Injection from [Z] to [R]                        *)
(**********************************************************)

(**********)
Definition IZR (z:Z) : R :=
  match z with
  | Z0 => 0
  | Zpos n => INR (nat_of_P n)
  | Zneg n => - INR (nat_of_P n)
  end.  
Arguments Scope IZR [Z_scope].

(**********************************************************)
(** *    [R] Archimedian                                  *)
(**********************************************************)

(**********)
Axiom archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.

(**********************************************************)
(** *    [R] Complete                                     *)
(**********************************************************)

(**********)
Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m.

(**********)
Definition bound (E:R -> Prop) :=  exists m : R, is_upper_bound E m.

(**********)
Definition is_lub (E:R -> Prop) (m:R) :=
  is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).

(**********)
Axiom
  completeness :
    forall E:R -> Prop,
      bound E -> (exists x : R, E x) -> sigT (fun m:R => is_lub E m).

--8<-----------------------------------------------------------------
(************************************************************************)
(* Copyright 2007 Milad Niqui and Tonny Hurkens                         *)
(* This file is distributed under the terms of the                      *)
(* GNU Lesser General Public License Version 2.1                        *)
(* A copy of the license can be found at                                *)
(*                  <http://www.gnu.org/licenses/lgpl.txt>              *)
(************************************************************************)

Require Import Raxioms_modified.
Open Local Scope R_scope.


Lemma Rlt_stepl:forall x y z, Rlt x y -> x=z -> Rlt z y.
Proof.
 intros x y z H_lt H_eq; subst; assumption.
Defined.

Lemma Rlt_stepr:forall x y z, Rlt x y -> y=z -> Rlt x z.
Proof.
 intros x y z H_lt H_eq; subst; assumption.
Defined.

Declare Left Step Rlt_stepl.
Declare Right Step Rlt_stepr.

Lemma Rle_stepl:forall x y z, Rle x y -> x=z -> Rle z y.
Proof.
 intros x y z H_lt H_eq; subst; assumption.
Defined.

Lemma Rle_stepr:forall x y z, Rle x y -> y=z -> Rle x z.
Proof.
 intros x y z H_lt H_eq; subst; assumption.
Defined.

Declare Left Step Rle_stepl.
Declare Right Step Rle_stepr.


(** First we derive [R1_neq_R0:0<>1] from some simple ordered-field
properties and [archimed 0]: *)

Lemma Rplus_0_r: forall r: R, r + 0 = r.  Proof.
 intros r; rewrite Rplus_comm; rewrite Rplus_0_l; reflexivity.
Qed.

Lemma Rplus_opp_r_uniq: forall r1 r2 : R, r1 + r2 = 0 -> r2 = - r1.
Proof.
 intros r1 r2 H.
 transitivity (0+r2).
  rewrite Rplus_0_l; trivial.
  rewrite <- (Rplus_opp_r r1).
  rewrite (Rplus_comm r1 (-r1)).
  rewrite Rplus_assoc.
  rewrite H.
  rewrite Rplus_0_r.
  trivial.
Qed.

Lemma Ropp_0: - 0 = 0.
Proof.
 symmetry; apply Rplus_opp_r_uniq; rewrite Rplus_0_l; trivial.
Qed.

Lemma Rlt_le_trans: forall r1 r2 r3 : R, r1 < r2 -> r2 <= r3 -> r1 < r3.
Proof.
 intros r1 r2 r3 H1 [H2|H2].
  apply Rlt_trans with r2; trivial.
  subst r2; trivial.
Qed.

Lemma Rlt_0_1:0<1.
Proof.
 destruct (archimed 0) as [H1 H2].
 apply Rlt_le_trans with (IZR (up 0)).
 unfold Rgt in H1; trivial.
 stepl (IZR (up 0) - 0); trivial.
 unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; trivial.
Qed.

(** The first removed axiom: *)
Theorem R1_neq_R0:1<>0.
Proof.
 intro H.
 contradiction (Rlt_asym 0 1 Rlt_0_1).
  stepl 0.
   stepr 1; trivial; apply Rlt_0_1.
  symmetry; trivial.
Qed.
Hint Resolve R1_neq_R0: real.


(** In the rest of the file we prove [total_order_T] using all the
remaining axioms (including [archimed]) in Raxioms_modified.v, except
[completeness] *)

Lemma Ropp_plus_distr: forall r1 r2 : R, - (r1 + r2) = - r1 + - r2.
Proof.
 intros r1 r2.
 rewrite (Rplus_comm (-r1)).
 symmetry.
 apply Rplus_opp_r_uniq.
 rewrite Rplus_assoc. 
 rewrite <- (Rplus_assoc r2).  
 rewrite Rplus_opp_r.
 rewrite Rplus_0_l.
 rewrite Rplus_opp_r; trivial.
Qed.

Lemma Ropp_involutive: forall r : R, - - r = r.
Proof.
 intro r.
 rewrite <- (Rplus_0_l (- -r)).
 rewrite <- (Rplus_opp_r r).
 rewrite Rplus_assoc.
 rewrite Rplus_opp_r.
 rewrite Rplus_0_r.
 reflexivity.
Qed.

Lemma Rplus_eq_reg_l: forall r r1 r2 : R, r + r1 = r + r2 -> r1 = r2.
Proof.
 intros r r1 r2 H.
 rewrite <- (Rplus_0_l r1).
 rewrite <- (Rplus_0_l r2).
 rewrite Rplus_comm.
 rewrite (Rplus_comm 0).
 rewrite <- (Rplus_opp_r r).
 repeat rewrite <- Rplus_assoc.
 rewrite Rplus_comm.  
 rewrite (Rplus_comm (r2+r)).
 apply (f_equal2 Rplus); trivial.
 rewrite Rplus_comm.
 rewrite (Rplus_comm r2).
 trivial.
Qed.

Lemma Rle_antisym: forall r1 r2 : R, r1 <= r2 -> r2 <= r1 -> r1 = r2.
Proof.
 intros r1 r2 [H1|H1] [H2|H2]; 
 (subst r2; trivial) ||  contradiction (Rlt_asym r1 r1); apply Rlt_trans with 
r2; trivial.
Qed.

Lemma Rminus_lt: forall r1 r2 : R, r1 - r2 < 0 -> r1 < r2.
Proof.
 intros r1 r2 H.
 rewrite <- (Rplus_0_l r1).
 rewrite <- (Rplus_opp_r r2).
 rewrite Rplus_assoc.
 rewrite <- Rplus_0_l.
 rewrite (Rplus_comm 0).
 apply Rplus_lt_compat_l.
 rewrite Rplus_comm.
 trivial.
Qed.

Lemma Rlt_zero_Rminus: forall r1 r2 : R, 0 < r1 - r2 -> r2 < r1.
Proof.
 intros r1 r2 H.
 rewrite <- (Rplus_0_l r1).
 rewrite <- (Rplus_opp_r r2).
 rewrite Rplus_assoc.
 stepl (r2+0).
  apply Rplus_lt_compat_l; rewrite Rplus_comm; unfold Rminus in H; trivial.
  rewrite Rplus_0_r; trivial.
Qed.

Lemma Rplus_le_compat_l : forall r r1 r2:R, r1 <= r2 -> r + r1 <= r + r2.
Proof.
 intros r r1 r2 [H|H].
  left; apply Rplus_lt_compat_l; trivial.
  right; subst r1; trivial.
Qed.

Lemma Rminus_le: forall r1 r2 : R, r1 - r2 <= 0 -> r1 <= r2.
Proof.
 intros r1 r2 H.
 rewrite <- (Rplus_0_l r1).
 rewrite <- (Rplus_opp_r r2).
 rewrite Rplus_assoc.
 rewrite <- Rplus_0_l.
 rewrite (Rplus_comm 0).
 apply Rplus_le_compat_l.
 rewrite Rplus_comm.
 trivial.
Qed.

Lemma Rle_trans: forall r1 r2 r3 : R, r1 <= r2 -> r2 <= r3 -> r1 <= r3.
Proof.
 intros r1 r2 r3 [H1|H1] [H2|H2].
  left; apply Rlt_trans with r2; trivial.
  left; subst r2; trivial.
  left; subst r2; trivial.
  right; subst r2; trivial.
Qed.

Lemma Rplus_lt_reg_l: forall r r1 r2 : R, r + r1 < r + r2 -> r1 < r2.
Proof.
 intros r r1 r2 H.
 rewrite <- (Rplus_0_l r1).
 rewrite <- (Rplus_0_l r2).
 rewrite Rplus_comm.
 rewrite (Rplus_comm 0).
 rewrite <- (Rplus_opp_r r).
 repeat rewrite <- Rplus_assoc.
 rewrite Rplus_comm.  
 rewrite (Rplus_comm (r2+r)).
 apply Rplus_lt_compat_l.
 rewrite Rplus_comm.
 rewrite (Rplus_comm r2).
 trivial.
Qed.

Lemma Rplus_le_reg_l: forall r r1 r2 : R, r + r1 <= r + r2 -> r1 <= r2.
Proof.
 intros r r1 r2 [H|H].
  left; apply Rplus_lt_reg_l with r; trivial.
  right; apply Rplus_eq_reg_l with r; trivial.
Qed.

Lemma Rplus_le_compat_r: forall r r1 r2 : R, r1 <= r2 -> r1 + r <= r2 + r.
Proof.
 intros r r1 r2 H.
 rewrite Rplus_comm.
 rewrite (Rplus_comm r2).
 apply Rplus_le_compat_l; trivial.
Qed.

Lemma S_INR : forall n:nat, INR (S n) = INR n + 1.
Proof.
 intros n; simpl; destruct n; trivial; simpl; rewrite Rplus_0_l; trivial.
Qed.

Lemma lt_INR_0 : forall n:nat, (0 < n)%nat -> 0 < INR n.
Proof.
 simple induction 1; intros.
  simpl; apply Rlt_0_1.
  rewrite S_INR.  
  apply Rlt_trans with (INR m); trivial.
  apply Rlt_zero_Rminus.
  stepr 1.
   apply Rlt_0_1.
   rewrite Rplus_comm.
   unfold Rminus.
   rewrite Rplus_assoc.
   rewrite Rplus_opp_r.
   rewrite Rplus_0_r; trivial.
Qed.

Lemma INR_pos : forall p:positive, 0 < INR (nat_of_P p).
Proof.
  intro p; apply lt_INR_0; apply lt_O_nat_of_P.
Qed.

Lemma plus_INR : forall n m:nat, INR (n + m) = INR n + INR m.
Proof.
 intros n m; induction n as [| n Hrecn].
  simpl; rewrite Rplus_0_l; trivial.
  replace (S n + m)%nat with (S (n + m)); trivial; repeat rewrite S_INR.
  rewrite Hrecn. 
  rewrite <- (Rplus_comm 1).
  rewrite (Rplus_comm (INR n) 1).
  rewrite Rplus_assoc; trivial.
Qed.

Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) = INR n - INR m.
Proof.
 intros n m le; pattern m, n; apply le_elim_rel; trivial.
 intros p; rewrite <- minus_n_O; simpl; unfold Rminus; rewrite Ropp_0; 
rewrite Rplus_0_r; reflexivity.
 intros p q H H0; repeat rewrite S_INR; simpl; rewrite H0.
  unfold Rminus at 2.
  rewrite Ropp_plus_distr.
  rewrite Rplus_assoc.
  rewrite <- (Rplus_comm (-1)).
  rewrite <- (Rplus_assoc 1).
  rewrite Rplus_opp_r.
  rewrite Rplus_0_l; trivial.
Qed.

Lemma plus_IZR_NEG_POS : forall p q:positive, IZR (Zpos p + Zneg q) = IZR 
(Zpos p) + IZR (Zneg q).
Proof.
 intros.
 case (lt_eq_lt_dec (nat_of_P p) (nat_of_P q)).
  intros [H| H]; simpl.
   rewrite nat_of_P_lt_Lt_compare_complement_morphism; simpl in |- *; trivial.
   rewrite (nat_of_P_minus_morphism q p).
    rewrite minus_INR.
     unfold Rminus; rewrite Ropp_plus_distr; rewrite Ropp_involutive; rewrite 
Rplus_comm; trivial.
     apply lt_le_weak; trivial.
    apply ZC2; apply nat_of_P_lt_Lt_compare_complement_morphism; trivial.
  
   rewrite (nat_of_P_inj p q); trivial.
   rewrite Pcompare_refl; simpl; rewrite Rplus_opp_r; trivial.

  intro H; simpl.
  rewrite nat_of_P_gt_Gt_compare_complement_morphism; simpl; trivial.
  rewrite (nat_of_P_minus_morphism p q).
   rewrite minus_INR.
    unfold Rminus; trivial. 
    apply lt_le_weak; trivial.
   apply ZC2; apply nat_of_P_lt_Lt_compare_complement_morphism; trivial.
Qed.

Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m.
Proof.
 intros [|z|z] [|t|t]; repeat rewrite Rplus_0_l; repeat rewrite Rplus_0_r; 
try solve[simpl; trivial].
  simpl; rewrite nat_of_P_plus_morphism; apply plus_INR.
  apply plus_IZR_NEG_POS.
  rewrite Zplus_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS.
  simpl; rewrite nat_of_P_plus_morphism; rewrite plus_INR; apply 
Ropp_plus_distr.
Qed.

Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n.
Proof.
 intros [|p|p]; simpl; trivial.
  rewrite Ropp_0; trivial.
  rewrite Ropp_involutive; trivial.
Qed.

Lemma Z_R_minus : forall n m:Z, IZR n - IZR m = IZR (n - m).
Proof.
 intros n m; unfold Rminus; unfold Zminus; rewrite plus_IZR; rewrite 
Ropp_Ropp_IZR; trivial.
Qed.

Lemma lt_IZR_0:forall m : Z, (0 < m)%Z -> 0 < IZR m.
Proof.
 intros [|p|p] H; try discriminate H; simpl; apply INR_pos.
Qed.

Lemma Zlt_minus: forall a b : Z, (b < a)%Z -> (0 < a - b)%Z.
Proof.
 intros a b H; apply Zplus_lt_reg_l with b; unfold Zminus; 
 rewrite (Zplus_comm a); rewrite (Zplus_assoc b (- b)); rewrite Zplus_opp_r; 
rewrite <- Zplus_0_r_reverse; assumption.
Qed.

Lemma IZR_lt: forall n m : Z, (n < m)%Z -> IZR n < IZR m.
Proof.
 intros n m H.
 apply Rlt_zero_Rminus.
 rewrite Z_R_minus.
 apply lt_IZR_0.
 apply Zlt_minus; trivial.
Qed.

Lemma IZR_le: forall n m : Z, (n <= m)%Z -> IZR n <= IZR m.
Proof.
 intros n m H.
 destruct (Z_le_lt_eq_dec n m H) as [H1|H1].
  left; apply IZR_lt; trivial.
  right; apply (f_equal IZR); trivial.
Qed.

Lemma total_Rle: forall r1 r2:R, {r1 < r2} + {r2 <= r1}.
Proof.
 intros r1 r2.
 destruct (archimed (r1-r2)) as [H1 H2].
 destruct (Zlt_cotrans 0 1 Zlt_0_1 (up (r1 - r2))) as [H3|H3].
  right.
  apply Rminus_le.
  stepl (- (r1 -r2)).
   apply Rplus_le_reg_l with 1.
   stepr 1.
    apply Rle_trans with (IZR (up (r1 - r2)) - (r1 - r2)); trivial.
    unfold Rminus.
    apply Rplus_le_compat_r.
    stepl (IZR (Zsucc 0%Z)); trivial.
    apply IZR_le.
    apply Zlt_le_succ; trivial.

    rewrite Rplus_0_r; trivial.
    unfold Rminus.
    rewrite Ropp_plus_distr.
    rewrite Rplus_comm.
    rewrite Ropp_involutive; trivial.
 
  left.
  apply Rminus_lt.
  unfold Rgt in H1.
  apply Rlt_le_trans with (IZR (up (r1 - r2))); trivial.
  stepr (IZR 0%Z); trivial.
  apply IZR_le.
  apply Zlt_succ_le; trivial.
Qed.

(* The second removed axioms: *)
Theorem total_order_T: forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}.
Proof.
 intros r1 r2.
 destruct (total_Rle r1 r2).
  repeat left; trivial.
  destruct (total_Rle r2 r1).
   right; trivial.
   left; right.
   apply Rle_antisym; trivial.
Qed.