coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Milad Niqui <milad AT cs.ru.nl>
- To: coq-club AT pauillac.inria.fr
- Cc: hurkens AT sci.kun.nl
- Subject: [Coq-Club] Removing two axioms from Raxioms.v
- Date: Wed, 09 May 2007 12:19:31 +0200
- Organization: Radboud University Nijmegen
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.
- [Coq-Club] Removing two axioms from Raxioms.v, Milad Niqui
- Re: [Coq-Club] Removing two axioms from Raxioms.v, Milad Niqui
- Re: [Coq-Club] Removing two axioms from Raxioms.v, Roland Zumkeller
Archive powered by MhonArc 2.6.16.