diff options
Diffstat (limited to 'theories7/Reals/Raxioms.v')
| -rw-r--r-- | theories7/Reals/Raxioms.v | 172 |
1 files changed, 0 insertions, 172 deletions
diff --git a/theories7/Reals/Raxioms.v b/theories7/Reals/Raxioms.v deleted file mode 100644 index caf8524c..00000000 --- a/theories7/Reals/Raxioms.v +++ /dev/null @@ -1,172 +0,0 @@ -(************************************************************************) -(* 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,v 1.2.2.1 2004/07/16 19:31:33 herbelin Exp $ i*) - -(*********************************************************) -(** Axiomatisation of the classical reals *) -(*********************************************************) - -Require Export ZArith_base. -V7only [ -Require Export Rsyntax. -Import R_scope. -]. -Open Local Scope R_scope. - -V7only [ -(*********************************************************) -(* Compatibility *) -(*********************************************************) -Notation sumboolT := Specif.sumbool. -Notation leftT := Specif.left. -Notation rightT := Specif.right. -Notation sumorT := Specif.sumor. -Notation inleftT := Specif.inleft. -Notation inrightT := Specif.inright. -Notation sigTT := Specif.sigT. -Notation existTT := Specif.existT. -Notation SigT := Specif.sigT. -]. - -(*********************************************************) -(* Field axioms *) -(*********************************************************) - -(*********************************************************) -(** Addition *) -(*********************************************************) - -(**********) -Axiom Rplus_sym:(r1,r2:R)``r1+r2==r2+r1``. -Hints Resolve Rplus_sym : real. - -(**********) -Axiom Rplus_assoc:(r1,r2,r3:R)``(r1+r2)+r3==r1+(r2+r3)``. -Hints Resolve Rplus_assoc : real. - -(**********) -Axiom Rplus_Ropp_r:(r:R)``r+(-r)==0``. -Hints Resolve Rplus_Ropp_r : real v62. - -(**********) -Axiom Rplus_Ol:(r:R)``0+r==r``. -Hints Resolve Rplus_Ol : real. - -(***********************************************************) -(** Multiplication *) -(***********************************************************) - -(**********) -Axiom Rmult_sym:(r1,r2:R)``r1*r2==r2*r1``. -Hints Resolve Rmult_sym : real v62. - -(**********) -Axiom Rmult_assoc:(r1,r2,r3:R)``(r1*r2)*r3==r1*(r2*r3)``. -Hints Resolve Rmult_assoc : real v62. - -(**********) -Axiom Rinv_l:(r:R)``r<>0``->``(/r)*r==1``. -Hints Resolve Rinv_l : real. - -(**********) -Axiom Rmult_1l:(r:R)``1*r==r``. -Hints Resolve Rmult_1l : real. - -(**********) -Axiom R1_neq_R0:``1<>0``. -Hints Resolve R1_neq_R0 : real. - -(*********************************************************) -(** Distributivity *) -(*********************************************************) - -(**********) -Axiom Rmult_Rplus_distr:(r1,r2,r3:R)``r1*(r2+r3)==(r1*r2)+(r1*r3)``. -Hints Resolve Rmult_Rplus_distr : real v62. - -(*********************************************************) -(** Order axioms *) -(*********************************************************) -(*********************************************************) -(** Total Order *) -(*********************************************************) - -(**********) -Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT ``r1<r2`` r1==r2) ``r1>r2``). - -(*********************************************************) -(** Lower *) -(*********************************************************) - -(**********) -Axiom Rlt_antisym:(r1,r2:R)``r1<r2`` -> ~ ``r2<r1``. - -(**********) -Axiom Rlt_trans:(r1,r2,r3:R) - ``r1<r2``->``r2<r3``->``r1<r3``. - -(**********) -Axiom Rlt_compatibility:(r,r1,r2:R)``r1<r2``->``r+r1<r+r2``. - -(**********) -Axiom Rlt_monotony:(r,r1,r2:R)``0<r``->``r1<r2``->``r*r1<r*r2``. - -Hints Resolve Rlt_antisym Rlt_compatibility Rlt_monotony : real. - -(**********************************************************) -(** Injection from N to R *) -(**********************************************************) - -(**********) -Fixpoint INR [n:nat]:R:=(Cases n of - O => ``0`` - |(S O) => ``1`` - |(S n) => ``(INR n)+1`` - end). -Arguments Scope INR [nat_scope]. - - -(**********************************************************) -(** Injection from [Z] to [R] *) -(**********************************************************) - -(**********) -Definition IZR:Z->R:=[z:Z](Cases z of - ZERO => ``0`` - |(POS n) => (INR (convert n)) - |(NEG n) => ``-(INR (convert n))`` - end). -Arguments Scope IZR [Z_scope]. - -(**********************************************************) -(** [R] Archimedian *) -(**********************************************************) - -(**********) -Axiom archimed:(r:R)``(IZR (up r)) > r``/\``(IZR (up r))-r <= 1``. - -(**********************************************************) -(** [R] Complete *) -(**********************************************************) - -(**********) -Definition is_upper_bound:=[E:R->Prop][m:R](x:R)(E x)->``x <= m``. - -(**********) -Definition bound:=[E:R->Prop](ExT [m:R](is_upper_bound E m)). - -(**********) -Definition is_lub:=[E:R->Prop][m:R] - (is_upper_bound E m)/\(b:R)(is_upper_bound E b)->``m <= b``. - -(**********) -Axiom complet:(E:R->Prop)(bound E)-> - (ExT [x:R] (E x))-> - (sigTT R [m:R](is_lub E m)). - |