From 3edd665893c2abfa6e687a7276a17273617dcdd5 Mon Sep 17 00:00:00 2001 From: mohring Date: Thu, 11 Jan 2001 11:09:11 +0000 Subject: Mise a jour Rbase git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1241 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Lists/Streams.v | 2 +- theories/Reals/Raxioms.v | 44 +- theories/Reals/Rbase.v | 1727 ++++++++++++++++++++-------------------- theories/Zarith/fast_integer.v | 23 +- theories/Zarith/zarith_aux.v | 4 +- 5 files changed, 890 insertions(+), 910 deletions(-) (limited to 'theories') diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 5962e0ed2..297a888eb 100755 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -61,7 +61,7 @@ CoInductive EqSt : Stream->Stream->Prop := (* A coinduction principle *) -Tactic Definition CoInduction proof := +Meta Definition CoInduction proof := Cofix proof; Intros; Constructor; [Clear proof | Try (Apply proof;Clear proof)]. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 21ab28be8..a9c3f621d 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -1,9 +1,8 @@ -(* $Id$ *) +(*i $Id$ i*) (*********************************************************) -(* Axiomatisation of the classical reals *) -(* *) +(*s {Axiomatisation of the classical reals} *) (*********************************************************) Require Export ZArith. @@ -11,17 +10,19 @@ Require Export Rsyntax. Require Export TypeSyntax. (*********************************************************) -(* Field axioms *) +(* {Field axioms} *) (*********************************************************) (*********************************************************) -(* Addition *) +(*s 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``. @@ -32,7 +33,7 @@ Axiom Rplus_ne:(r:R)``r+0==r``/\``0+r==r``. Hints Resolve Rplus_ne : real v62. (***********************************************************) -(* Multiplication *) +(*s Multiplication *) (***********************************************************) (**********) @@ -45,16 +46,19 @@ Hints Resolve Rmult_assoc : real v62. (**********) Axiom Rinv_l:(r:R)``r<>0``->``(1/r)*r==1``. +Hints Resolve Rinv_l : real. + (**********) Axiom Rmult_ne:(r:R)``r*1==r``/\``1*r==r``. Hints Resolve Rmult_ne : real v62. (**********) -Axiom R1_neq_R0:(~R1==R0). +Axiom R1_neq_R0:``1<>0``. +Hints Resolve R1_neq_R0 : real. (*********************************************************) -(* Distributivity *) +(*s Distributivity *) (*********************************************************) (**********) @@ -65,14 +69,14 @@ Hints Resolve Rmult_Rplus_distr : real v62. (* Order axioms *) (*********************************************************) (*********************************************************) -(* Total Order *) +(*s Total Order *) (*********************************************************) (**********) Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT ``r1r2``). (*********************************************************) -(* Lower *) +(*s Lower *) (*********************************************************) (**********) @@ -88,37 +92,39 @@ Axiom Rlt_compatibility:(r,r1,r2:R)``r1``r+r1``r1``r*r1 R0 - |(S O) => R1 - |(S n) => (Rplus (INR n) R1) + O => ``0`` + |(S O) => ``1`` + |(S n) => ``(INR n)+1`` end). (**********************************************************) -(* Injection from Z to R *) +(*s Injection from Z to R *) (**********************************************************) (**********) Definition IZR:Z->R:=[z:Z](Cases z of - ZERO => R0 + ZERO => ``0`` |(POS n) => (INR (convert n)) - |(NEG n) => (Ropp (INR (convert n))) + |(NEG n) => ``-(INR (convert n))`` end). (**********************************************************) -(* R Archimedian *) +(*s R Archimedian *) (**********************************************************) (**********) Axiom archimed:(r:R)``(IZR (up r)) > r``/\``(IZR (up r))-r <= 1``. (**********************************************************) -(* R Complete *) +(*s R Complete *) (**********************************************************) (**********) diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index 970b18ee4..f2f6cc2d7 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -1,19 +1,17 @@ -(* $Id$ *) +(*i $Id$ i*) -(**************************************************************************) -(* Basic lemmas for the classical reals numbers *) -(**************************************************************************) +(***************************************************************************) +(*s Basic lemmas for the classical reals numbers *) +(***************************************************************************) Require Export Raxioms. Require Export ZArithRing. -Require Classical_Prop. Require Omega. -(**************************************************************************) -(* On commence par instancier la tactique Ring sur les réels *) -(**************************************************************************) - +(***************************************************************************) +(*s Instantiating Ring tactic on reals *) +(***************************************************************************) Lemma RTheory : (Ring_Theory Rplus Rmult R1 R0 Ropp [x,y:R]false). Split. @@ -35,14 +33,41 @@ Defined. Add Abstract Ring R Rplus Rmult R1 R0 Ropp [x,y:R]false RTheory. (**************************************************************************) -(* Basic Lemmas *) +(*s Relation between orders and equality *) (**************************************************************************) (**********) -Lemma Req_EM:(r1,r2:R)(r1==r2)\/(~r1==r2). -Intros;Apply (classic r1==r2). +Lemma Rlt_antirefl:(r:R)~``r``r1<>r2``. + Red; Intros r1 r2 H H0; Apply (Rlt_antirefl r1). + Pattern 2 r1; Rewrite H0; Trivial. +Save. + +Lemma Rgt_not_eq:(r1,r2:R)``r1>r2``->``r1<>r2``. +Intros; Apply sym_not_eqT; Apply Rlt_not_eq; Auto with real. +Save. + +(**********) +Lemma imp_not_Req:(r1,r2:R)(``r1r2``) -> ``r1<>r2``. +Intros r1 r2 [H|H]. +Apply Rlt_not_eq; Auto with real. +Apply Rgt_not_eq; Auto with real. +Save. +Hints Resolve imp_not_Req : real. + +(*s Reasoning by case on equalities and order *) + +(**********) +Lemma Req_EM:(r1,r2:R)(r1==r2)\/``r1<>r2``. +Intros;Elim (total_order_T r1 r2);Intro. +Case y; Auto with real. +Auto with real. Save. -Hints Resolve Req_EM : real v62. +Hints Resolve Req_EM : real. (**********) Lemma total_order:(r1,r2:R)``r1r2``. @@ -51,28 +76,128 @@ Elim y;Intro;Auto. Save. (**********) -Lemma not_Req:(r1,r2:R)(~(r1==r2))->((Rlt r1 r2)\/(Rgt r1 r2)). -Intros; Case (total_order r1 r2); Intros. -Left; Exact H0. +Lemma not_Req:(r1,r2:R)``r1<>r2``->(``r1r2``). +Intros; Case (total_order r1 r2); Intros; Auto with real. Case H0; Intros. -Absurd r1==r2; Auto with zarith real. -Right; Exact H1. +Absurd r1==r2; Auto with real. +Auto with real. Save. + +(*********************************************************************************) +(*s Order Lemma : relating [<], [>], [<=] and [>=] *) +(*********************************************************************************) + (**********) -Lemma imp_not_Req:(r1,r2:R)((Rlt r1 r2)\/(Rgt r1 r2))->(~(r1==r2)). -Intros; Elim H; Intro; Clear H;Red; Intro;Rewrite H in H0. -Generalize (Rlt_antisym r2 r2 H0); Intro; Auto with zarith real. -Unfold Rgt in H0;Generalize (Rlt_antisym r2 r2 H0);Intro; Auto with zarith real. +Lemma Rlt_le:(r1,r2:R)``r1 ``r1<=r2``. +Unfold Rle; Auto. Save. +Hints Resolve Rlt_le : real. (**********) -Lemma Rlt_antirefl:(r:R)~(Rlt r r). - Red; Intros; Apply (Rlt_antisym r r H); Auto with zarith real. +Lemma Rle_ge : (r1,r2:R)``r1<=r2`` -> ``r2>=r1``. +Destruct 1; Red; Auto with real. Save. (**********) -Lemma total_order_Rlt:(r1,r2:R)(sumboolT (Rlt r1 r2) ~(Rlt r1 r2)). +Lemma Rge_le : (r1,r2:R)``r1>=r2`` -> ``r2<=r1``. +Destruct 1; Red; Auto with real. +Save. + +(**********) +Lemma not_Rle:(r1,r2:R)~(``r1<=r2``)->``r1>r2``. +Intros; Unfold Rle in H; Elim (total_order r1 r2); Intro. +Elim H;Left; Assumption. +Elim H0; Intro;Auto. +Elim H;Right; Assumption. +Save. + +Hints Immediate Rle_ge Rge_le not_Rle : real. + +(**********) +Lemma Rlt_le_not:(r1,r2:R)``r2~(``r1<=r2``). +Intros; Red; Intro; Elim H0; Clear H0; Intro. +Exact (Rlt_antisym r1 r2 H0 H). +Case (imp_not_Req r1 r2); Auto with real. +Save. + +Lemma Rle_not:(r1,r2:R)``r1>r2`` -> ~(``r1<=r2``). +Proof Rlt_le_not. + +Hints Immediate Rlt_le_not : real. + +(**********) +Lemma Rlt_ge_not:(r1,r2:R)``r1~(``r1>=r2``). +Unfold Rge; Red; Intros. +Apply (Rlt_le_not r2 r1 H). +Red; Case H0; Auto with real. +Save. + +Hints Immediate Rlt_ge_not : real. + +(**********) +Lemma eq_Rle:(r1,r2:R)r1==r2->``r1<=r2``. +Unfold Rle; Auto. +Save. +Hints Immediate eq_Rle : real. + +Lemma eq_Rge:(r1,r2:R)r1==r2->``r1>=r2``. +Unfold Rge; Auto. +Save. +Hints Immediate eq_Rge : real. + +Lemma eq_Rle_sym:(r1,r2:R)r2==r1->``r1<=r2``. +Unfold Rle; Auto. +Save. +Hints Immediate eq_Rle_sym : real. + +Lemma eq_Rge_sym:(r1,r2:R)r2==r1->``r1>=r2``. +Unfold Rge; Auto. +Save. +Hints Immediate eq_Rge_sym : real. + +Lemma Rle_antisym : (r1,r2:R)``r1<=r2`` -> ``r2<=r1``-> r1==r2. +Unfold Rle; Intros. +Case H; Intro; Auto with real. +Case H0; Intro; Auto with real. +Case (Rlt_antisym r1 r2 H1 H2). +Save. +Hints Resolve Rle_antisym : real. + +(**********) +Lemma Rle_le_eq:(r1,r2:R)(``r1<=r2``/\``r2<=r1``)<->(r1==r2). +Split; Auto with real. +Intros (H1,H2); Auto with real. +Save. + + +(**********) +Lemma Rle_trans:(r1,r2,r3:R) ``r1<=r2``->``r2<=r3``->``r1<=r3``. +Intros r1 r2 r3; Unfold Rle; Intros. +Elim H; Elim H0; Intros. +Left; Apply Rlt_trans with r2; Trivial. +Left; Rewrite <- H1; Trivial. +Left; Rewrite H2; Trivial. +Right; Transitivity r2; Trivial. +Save. + +(**********) +Lemma Rle_lt_trans:(r1,r2,r3:R)``r1<=r2``->``r2``r1 H1; Auto with zarith real. +Save. + +(**********) +Lemma Rlt_le_trans:(r1,r2,r3:R)``r1``r2<=r3``->``r1r2`` ~(``r1>r2``)). Unfold Rgt;Intros;Apply total_order_Rlt. Save. (**********) -Lemma total_order_Rge:(r1,r2:R)(sumboolT (Rge r1 r2) ~(Rge r1 r2)). -Unfold Rge;Unfold Rgt;Intros;Elim (total_order_Rle r2 r1);Intro. -Left;Unfold Rle in y;Elim y;Auto. -Right;Unfold Rle in y;Red;Intro;Elim H;Intro. -Elim y;Left;Assumption. -Elim y;Right;Auto. +Lemma total_order_Rge:(r1,r2:R)(sumboolT (``r1>=r2``) ~(``r1>=r2``)). +Intros;Elim (total_order_Rle r2 r1);Intro. +Left; Auto with real. +Right; Auto with real. Save. +Lemma total_order_Rlt_Rle:(r1,r2:R)(sumboolT ``r1 (sumboolT ``r1 (sumboolT ``n<=m(y==(Ropp x)). - Intros; Replace y with (Rplus (Rplus (Ropp x) x) y); +Lemma Rplus_Ropp:(x,y:R)``x+y==0``->``y== -x``. + Intros; Replace y with ``(-x+x)+y``; [ Rewrite -> Rplus_assoc; Rewrite -> H; Ring | Ring ]. Save. @@ -125,999 +281,867 @@ Save. (* New *) Hint eqT_R_congr : real := Resolve (congr_eqT R). -Lemma Rplus_plus_r:(r,r1,r2:R)(r1==r2)->((Rplus r r1)==(Rplus r r2)). +Lemma Rplus_plus_r:(r,r1,r2:R)(r1==r2)->``r+r1==r+r2``. Auto with real. Save. - -(* Old *) -Hints Resolve Rplus_plus_r : v62. +(* Old *) Hints Resolve Rplus_plus_r : v62. (**********) -Lemma r_Rplus_plus:(r,r1,r2:R)((Rplus r r1)==(Rplus r r2))->(r1==r2). - Intros; - Cut (Rplus (Rplus (Ropp r) r) r1)==(Rplus (Rplus (Ropp r) r) r2). - Ring (Rplus (Rplus (Ropp r) r) r1) (Rplus (Rplus (Ropp r) r) r2); Trivial. +Lemma r_Rplus_plus:(r,r1,r2:R)``r+r1==r+r2``->r1==r2. + Intros; Transitivity ``(-r+r)+r1``. + Ring. + Transitivity ``(-r+r)+r2``. Repeat Rewrite -> Rplus_assoc; Rewrite <- H; Reflexivity. + Ring. Save. - Hints Resolve r_Rplus_plus : real. (**********) -Lemma Rplus_ne_i:(r,b:R)((Rplus r b)==r)->(b==R0). - Intros r b; Replace r with (Rplus r R0). - Rewrite -> Rplus_assoc; Ring (Rplus R0 b); EAuto with real. - Ring. +Lemma Rplus_ne_i:(r,b:R)``r+b==r`` -> ``b==0``. + Intros r b; Pattern 2 r; Replace r with ``r+0``; + EAuto with real. Save. (***********************************************************) -(* Multiplication *) +(*s Multiplication *) (***********************************************************) (**********) -Lemma Rinv_r:(r:R)(~(r==R0))->((Rmult r (Rinv r))==R1). - Intros; Rewrite -> Rmult_sym; Apply (Rinv_l r H); Auto with zarith real. +Lemma Rinv_r:(r:R)``r<>0``->``r* (1/r)==1``. + Intros; Rewrite -> Rmult_sym; Auto with real. Save. +Hints Resolve Rinv_r : real. + +Lemma Rinv_l_sym:(r:R)``r<>0``->``1==(1/r) * r``. + Symmetry; Auto with real. +Save. + +Lemma Rinv_r_sym:(r:R)``r<>0``->``1==r* (1/r)``. + Symmetry; Auto with real. +Save. +Hints Resolve Rinv_l_sym Rinv_r_sym : real. + (**********) -Lemma Rmult_Or:(r:R)((Rmult r R0)==R0). +Lemma Rmult_Or :(r:R) ``r*0==0``. Intro; Ring. Save. Hints Resolve Rmult_Or : real v62. (**********) -Lemma Rmult_Ol:(r:R)((Rmult R0 r)==R0). +Lemma Rmult_Ol:(r:R)(``0*r==0``). Intro; Ring. Save. Hints Resolve Rmult_Ol : real v62. (**********) -Lemma Rmult_mult_r:(r,r1,r2:R)(r1==r2)->((Rmult r r1)==(Rmult r r2)). - Auto with real. +Lemma Rmult_1r:(r:R)(``r*1==r``). +Intro; Ring. Save. -(* OLD *) -Hints Resolve Rmult_mult_r : v62. +Hints Resolve Rmult_1r : real. (**********) -Lemma r_Rmult_mult:(r,r1,r2:R)((Rmult r r1)==(Rmult r r2))-> - (~(r==R0))->(r1==r2). - Intros; - Cut (Rmult (Rmult (Rinv r) r) r1)==(Rmult (Rmult (Rinv r) r) r2). - Rewrite -> Rinv_l with r; Ring (Rmult R1 r1) (Rmult R1 r2); Trivial. - - Repeat Rewrite -> Rmult_assoc. - Rewrite H; Trivial. +Lemma Rmult_1l:(r:R)(``1*r==r``). +Intro; Ring. Save. +Hints Resolve Rmult_1l : real. (**********) -Lemma without_div_Od:(r1,r2:R)(Rmult r1 r2)==R0 -> r1==R0 \/ r2==R0. - Intros; Cut r1==R0\/~r1==R0. - Intros [Hz | Hnotz]. - Left; Auto. - Replace r2 with (Rmult R0 (Rinv r1)); Auto with real. - Apply r_Rmult_mult with r1. - Rewrite H; Ring. - Assumption. +Lemma Rmult_mult_r:(r,r1,r2:R)r1==r2->``r*r1==r*r2``. Auto with real. Save. +(* OLD *) Hints Resolve Rmult_mult_r : v62. + +(**********) +Lemma r_Rmult_mult:(r,r1,r2:R)(``r*r1==r*r2``)->``r<>0``->(r1==r2). + Intros; Transitivity ``(1/r * r)*r1``. + Rewrite Rinv_l; Auto with real. + Transitivity ``(1/r * r)*r2``. + Repeat Rewrite Rmult_assoc; Rewrite H; Trivial. + Rewrite Rinv_l; Auto with real. +Save. (**********) -Lemma without_div_Oi1:(r1,r2:R) r1==R0 -> (Rmult r1 r2)==R0. - Intros; Rewrite -> H; Ring. +Lemma without_div_Od:(r1,r2:R)``r1*r2==0`` -> ``r1==0`` \/ ``r2==0``. + Intros; Case (Req_EM r1 ``0``); [Intro Hz | Intro Hnotz]. + Auto. + Right; Apply r_Rmult_mult with r1; Trivial. + Rewrite H; Auto with real. Save. (**********) -Lemma without_div_Oi2:(r1,r2:R) r2==R0 -> (Rmult r1 r2)==R0. - Intros; Rewrite -> H; Ring. +Lemma without_div_Oi:(r1,r2:R) ``r1==0``\/``r2==0`` -> ``r1*r2==0``. + Intros r1 r2 [H | H]; Rewrite H; Auto with real. Save. +Hints Resolve without_div_Oi : real. + (**********) -Lemma without_div_Oi:(r1,r2:R) (r1==R0)\/(r2==R0) -> (Rmult r1 r2)==R0. - Intros r1 r2 [H | H]; Rewrite H; Ring. +Lemma without_div_Oi1:(r1,r2:R) ``r1==0`` -> ``r1*r2==0``. + Auto with real. Save. +(**********) +Lemma without_div_Oi2:(r1,r2:R) ``r2==0`` -> ``r1*r2==0``. + Auto with real. +Save. + + (**********) -Lemma without_div_O_contr:(r1,r2:R) - ~(Rmult r1 r2)==R0 -> ~r1==R0 /\ ~r2==R0. -Intros; Cut (P,Q,R:Prop)(P\/Q->R)->~R->~P/\~Q. -Intro;Generalize (H0 r1==R0 r2==R0 (Rmult r1 r2)==R0 - (without_div_Oi r1 r2));Intro;Apply (H1 H). -Tauto. +Lemma without_div_O_contr:(r1,r2:R)``r1*r2<>0`` -> ``r1<>0`` /\ ``r2<>0``. +Intros r1 r2 H; Split; Red; Intro; Apply H; Auto with real. Save. +(**********) +Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. +Red; Intros r1 r2 (H1,H2) H. +Case (without_div_Od r1 r2); Auto with real. +Save. +Hints Resolve mult_non_zero : real. + (**********) Lemma Rmult_Rplus_distrl: - (r1,r2,r3:R) ((Rmult (Rplus r1 r2) r3)== - (Rplus (Rmult r1 r3) (Rmult r2 r3))). + (r1,r2,r3:R) ``(r1+r2)*r3 == (r1*r3)+(r2*r3)``. Intros; Ring. Save. +(*s Square function *) + (***********) -Definition Rsqr:R->R:=[r:R](Rmult r r). +Definition Rsqr:R->R:=[r:R]``r*r``. (***********) -Lemma Rsqr_O:((Rsqr R0)==R0). - Unfold Rsqr; Ring. +Lemma Rsqr_O:(Rsqr ``0``)==``0``. + Unfold Rsqr; Auto with real. Save. (***********) -Lemma Rsqr_r_R0:(r:R)(Rsqr r)==R0->r==R0. +Lemma Rsqr_r_R0:(r:R)(Rsqr r)==``0``->``r==0``. Unfold Rsqr;Intros;Elim (without_div_Od r r H);Trivial. Save. (*********************************************************) -(* Opposite *) +(*s Opposite *) (*********************************************************) (**********) -Lemma Ropp_Ropp:(r:R)((Ropp (Ropp r))==r). - Intro; Ring. +Lemma eq_Ropp:(r1,r2:R)(r1==r2)->``-r1 == -r2``. + Auto with real. Save. +Hints Resolve eq_Ropp : real. (**********) -Lemma Ropp_O:((Ropp R0)==R0). +Lemma Ropp_O:``-0==0``. Ring. Save. Hints Resolve Ropp_O : real v62. (**********) -Lemma Ropp_distr1:(r1,r2:R) - ((Ropp (Rplus r1 r2))==(Rplus (Ropp r1) (Ropp r2))). - Intros; Ring. +Lemma eq_RoppO:(r:R)``r==0``-> ``-r==0``. + Intros; Rewrite -> H; Auto with real. Save. +Hints Resolve eq_RoppO : real. (**********) -Lemma Ropp_distr2:(r1,r2:R)((Ropp (Rminus r1 r2))==(Rminus r2 r1)). - Intros; Ring. +Lemma Ropp_Ropp:(r:R)``-(-r)==r``. + Intro; Ring. Save. +Hints Resolve Ropp_Ropp : real. -(**********) -Lemma eq_Rminus:(r1,r2:R)(r1==r2)->((Rminus r1 r2)==R0). - Intros; Rewrite H; Ring. +(*********) +Lemma Ropp_neq:(r:R)``r<>0``->``-r<>0``. +Red;Intros r H H0. +Apply H. +Transitivity ``-(-r)``; Auto with real. Save. +Hints Resolve Ropp_neq : real. (**********) -Lemma Rminus_eq:(r1,r2:R)(Rminus r1 r2)==R0 -> r1==r2. - Intros r1 r2; Unfold Rminus; Rewrite -> Rplus_sym; Intro. - Rewrite <- (Ropp_Ropp r2); Apply (Rplus_Ropp (Ropp r2) r1 H). +Lemma Ropp_distr1:(r1,r2:R)``-(r1+r2)==(-r1 + -r2)``. + Intros; Ring. Save. +Hints Resolve Ropp_distr1 : real. -(**********) -Lemma Rminus_eq_contra:(r1,r2:R)~r1==r2->~(Rminus r1 r2)==R0. -Intros;Cut (P,Q:Prop)(P->Q)->(~Q->~P). -Intro cla;Apply (cla (Rminus r1 r2)==R0 r1==r2 (Rminus_eq r1 r2));Assumption. -Tauto. +(*s Opposite and multiplication *) + +Lemma Ropp_mul1:(r1,r2:R)``(-r1)*r2 == -(r1*r2)``. + Intros; Ring. Save. +Hints Resolve Ropp_mul1 : real. (**********) -Lemma Rminus_distr: - (x,y,z:R) (Rmult x (Rminus y z))== - (Rminus (Rmult x y) (Rmult x z)). -Intros; Ring. +Lemma Ropp_mul2:(r1,r2:R)``(-r1)*(-r2)==r1*r2``. + Intros; Ring. Save. +Hints Resolve Ropp_mul2 : real. + +(*s Substraction *) + +Lemma minus_R0:(r:R)``r-0==r``. +Intro;Ring. +Save. +Hints Resolve minus_R0 : real. (**********) -Lemma eq_Ropp:(r1,r2:R)(r1==r2)->((Ropp r1)==(Ropp r2)). - Auto with real. +Lemma Ropp_distr2:(r1,r2:R)``-(r1-r2)==r2-r1``. + Intros; Ring. Save. +Hints Resolve Ropp_distr2 : real. (**********) -Lemma eq_RoppO:(r:R)(r==R0)->((Ropp r)==R0). - Intros; Rewrite -> H; Ring. +Lemma eq_Rminus:(r1,r2:R)(r1==r2)->``r1-r2==0``. + Intros; Rewrite H; Ring. Save. +Hints Resolve eq_Rminus : real. (**********) -Lemma minus_R0:(r:R)(Rminus r R0)==r. -Intro;Unfold Rminus;Rewrite (eq_RoppO R0 (refl_eqT R R0)); - Elim(Rplus_ne r);Intros a b;Rewrite a;Clear a b;Auto with zarith real. +Lemma Rminus_eq:(r1,r2:R)``r1-r2==0`` -> r1==r2. + Intros r1 r2; Unfold Rminus; Rewrite -> Rplus_sym; Intro. + Rewrite <- (Ropp_Ropp r2); Apply (Rplus_Ropp (Ropp r2) r1 H). Save. +Hints Immediate Rminus_eq : real. (**********) -Lemma Ropp_mul1:(r1,r2:R)(Rmult (Ropp r1) r2)==(Ropp (Rmult r1 r2)). - Intros; Ring. +Lemma Rminus_eq_contra:(r1,r2:R)``r1<>r2``->``r1-r2<>0``. +Red; Intros r1 r2 H H0. +Apply H; Auto with real. Save. +Hints Resolve Rminus_eq_contra : real. (**********) -Lemma Ropp_mul2:(r1,r2:R)(Rmult (Ropp r1) (Ropp r2))==(Rmult r1 r2). - Intros; Ring. +Lemma Rminus_distr: (x,y,z:R) ``x*(y-z)==(x*y) - (x*z)``. +Intros; Ring. Save. -(*********) -Lemma Ropp_neq:(r:R)~r==R0->~(Ropp r)==R0. -Intros;Red;Intro;Generalize (Rplus_plus_r r (Ropp r) R0 H0);Intro; - Rewrite (Rplus_Ropp_r r) in H1; - Rewrite (let (H1,H2)=(Rplus_ne r) in H1) in H1; - Generalize (sym_eqT R R0 r H1);Intro;Auto. +(*s Inverse *) +Lemma Rinv_R1:``1/1==1``. +Apply (r_Rmult_mult ``1`` ``1/1`` ``1``); Auto with real. +Rewrite (Rinv_r R1 R1_neq_R0);Auto with real. Save. +Hints Resolve Rinv_R1 : real. (*********) -Lemma Rinv_R1:(Rinv R1)==R1. -Apply (r_Rmult_mult R1 (Rinv R1) R1); - [Rewrite (Rinv_r R1 R1_neq_R0); - Rewrite (let (H1,H2)=(Rmult_ne R1) in H1);Trivial| - Red;Intro;Apply R1_neq_R0;Assumption]. +Lemma Rinv_neq_R0:(r:R)``r<>0``->``(1/r)<>0``. +Red; Intros; Apply R1_neq_R0. +Replace ``1`` with ``(1/r) * r``; Auto with real. Save. +Hints Resolve Rinv_neq_R0 : real. (*********) -Lemma Rinv_neq_R0:(r:R)(~r==R0)->~(Rinv r)==R0. -Intros;Red;Intro;Generalize (Rmult_mult_r r (Rinv r) R0 H0); - Clear H0;Intro;Rewrite (Rinv_r r H) in H0;Rewrite (Rmult_Or r) in H0; - Generalize R1_neq_R0;Intro;Auto. +Lemma Rinv_Rinv:(r:R)``r<>0``->``1/(1/r)==r``. +Intros;Apply (r_Rmult_mult ``1/r``); Auto with real. +Transitivity ``1``; Auto with real. Save. +Hints Resolve Rinv_Rinv : real. (*********) -Lemma Rinv_Rinv:(r:R)(~r==R0)->(Rinv (Rinv r))==r. -Intros;Apply (r_Rmult_mult (Rinv r) (Rinv (Rinv r)) r); - [Rewrite (Rinv_r (Rinv r) (Rinv_neq_R0 r H)); - Rewrite (Rinv_l r H);Trivial |Apply Rinv_neq_R0;Assumption]. +Lemma Rinv_Rmult:(r1,r2:R)``r1<>0``->``r2<>0``->``1/(r1*r2)==(1/r1)*(1/r2)``. +Intros; Apply (r_Rmult_mult ``r1*r2``);Auto with real. +Transitivity ``1``; Auto with real. +Transitivity ``(r1*1/r1)*(r2*(1/r2))``; Auto with real. +Rewrite Rinv_r; Trivial. +Rewrite Rinv_r; Auto with real. +Ring. Save. (*********) -Lemma Rinv_Rmult:(r1,r2:R)(~r1==R0)->(~r2==R0)-> - (Rinv (Rmult r1 r2))==(Rmult (Rinv r1) (Rinv r2)). -Intros;Cut ~(Rmult r1 r2)==R0. -Intro;Apply (r_Rmult_mult (Rmult r1 r2));Auto. -Rewrite (Rinv_r (Rmult r1 r2) H1); - Rewrite (Rmult_sym (Rinv r1) (Rinv r2)); - Rewrite (Rmult_assoc r1 r2 (Rmult (Rinv r2) (Rinv r1))); - Rewrite <-(Rmult_assoc r2 (Rinv r2) (Rinv r1)); - Rewrite (Rinv_r r2 H0); - Rewrite (let (H1,H2)=(Rmult_ne (Rinv r1)) in H2); - Rewrite (Rinv_r r1 H);Trivial. -Red;Intro;Generalize (without_div_Od r1 r2 H1);Intro;Elim H2;Intro;Auto. +Lemma Ropp_Rinv:(r:R)``r<>0``->``-(1/r)==1/(-r)``. +Intros; Apply (r_Rmult_mult ``-r``);Auto with real. +Transitivity ``1``; Auto with real. +Rewrite (Ropp_mul2 r ``1/r``); Auto with real. Save. -(*********) -Lemma Ropp_Rinv:(r:R)~r==R0->(Ropp (Rinv r))==(Rinv (Ropp r)). -Intros;Generalize (refl_eqT R R1);Pattern 1 R1; - Rewrite <-(Rinv_l r H);Rewrite <-(Rinv_l (Ropp r) (Ropp_neq r H)); - Intro;Rewrite <-(Ropp_mul2 (Rinv r) r) in H0; - Rewrite (Rmult_sym (Ropp (Rinv r)) (Ropp r)) in H0; - Rewrite (Rmult_sym (Rinv (Ropp r)) (Ropp r)) in H0; - Apply (r_Rmult_mult (Ropp r) (Ropp (Rinv r)) (Rinv (Ropp r)) - H0 (Ropp_neq r H)). +Lemma Rinv_r_simpl_r : (r1,r2:R)``r1<>0``->``r1*(1/r1)*r2==r2``. +Intros; Transitivity ``1*r2``; Auto with real. +Rewrite Rinv_r; Auto with real. Save. +Lemma Rinv_r_simpl_l : (r1,r2:R)``r1<>0``->``r2*r1*(1/r1)==r2``. +Intros; Transitivity ``r2*1``; Auto with real. +Transitivity ``r2*(r1*1/r1)``; Auto with real. +Save. + +Lemma Rinv_r_simpl_m : (r1,r2:R)``r1<>0``->``r1*r2*(1/r1)==r2``. +Intros; Transitivity ``r2*1``; Auto with real. +Transitivity ``r2*(r1*1/r1)``; Auto with real. +Ring. +Save. +Hints Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m : real. + (*********) -Lemma Rinv_Rmult_simpl:(a,b,c:R)(~a==R0)-> - (Rmult (Rmult a (Rinv b))(Rmult c (Rinv a)))== - (Rmult c (Rinv b)). -Intros; Rewrite (Rmult_sym (Rmult a (Rinv b)) (Rmult c (Rinv a))); - Rewrite (Rmult_assoc c (Rinv a) (Rmult a (Rinv b))); - Rewrite <-(Rmult_assoc (Rinv a) a (Rinv b)); - Rewrite (Rinv_l a H);Rewrite (let (H1,H2)=(Rmult_ne (Rinv b)) in H2); - Reflexivity. +Lemma Rinv_Rmult_simpl:(a,b,c:R)``a<>0``->``(a*(1/b))*(c*(1/a))==c*(1/b)``. +Intros. +Transitivity ``(a*1/a)*(c*(1/b))``; Auto with real. +Ring. Save. -(*********************************************************) -(* Order Lemma *) -(*********************************************************) -(*********************************************************) -(* Lower *) -(*********************************************************) +(*s Order and addition *) -(**********) -Lemma not_Rle:(r1,r2:R)~(Rle r1 r2)->(Rgt r1 r2). -Intros; Unfold Rle in H; Elim (total_order r1 r2); Intro. -Elim H;Left; Assumption. -Elim H0; Intro;Auto with zarith real. -Elim H;Right; Assumption. +Lemma Rlt_compatibility_r:(r,r1,r2:R)``r1``r1+r~(Rle r1 r2). -Intros; Red; Intro;Unfold Rle in H0;Elim H0; Intro. -Generalize (Rlt_antisym r1 r2 H1); Intro; Auto with zarith real. -Elim (imp_not_Req r2 r1);Auto with zarith real. +Lemma Rlt_anti_compatibility: (r,r1,r2:R)``r+r1 < r+r2`` -> ``r1 Rplus_Ropp_l. +Elim (Rplus_ne r1); Elim (Rplus_ne r2); Intros; Rewrite <- H3; + Rewrite <- H1; Auto with zarith real. +Rewrite -> Rplus_assoc; Rewrite -> Rplus_assoc; + Apply (Rlt_compatibility ``-r`` ``r+r1`` ``r+r2`` H). Save. (**********) -Lemma Rlt_ge_not:(r1,r2:R)(Rlt r1 r2)->~(Rge r1 r2). -Intros;Red;Intro;Unfold Rge in H0;Unfold Rgt in H0;Elim H0;Intro. -Apply (Rlt_antisym r1 r2 H H1). -Rewrite H1 in H;Exact (Rlt_antisym r2 r2 H H). +Lemma Rle_compatibility:(r,r1,r2:R)``r1<=r2`` -> ``r+r1 <= r+r2 ``. +Unfold Rle; Intros; Elim H; Intro. +Left; Apply (Rlt_compatibility r r1 r2 H0). +Right; Rewrite <- H0; Auto with zarith real. Save. (**********) -Lemma Rle_le_eq:(r1,r2:R)(Rle r1 r2)/\(Rle r2 r1)<->(r1==r2). -Intros; Split; Intro. -Elim H; Unfold Rle; Intros. -Elim H0; Elim H1; Intros. -Absurd (Rlt r2 r1). -Red; Intro. -Apply (Rlt_antisym r1 r2 H3 H4). -Auto with zarith real. -Auto with zarith real. -Auto with zarith real. -Auto with zarith real. -Rewrite <- H; Split; Unfold Rle; Right; Auto with zarith real. +Lemma Rle_compatibility_r:(r,r1,r2:R)``r1<=r2`` -> ``r1+r<=r2+r``. +Unfold Rle; Intros; Elim H; Intro. +Left; Apply (Rlt_compatibility_r r r1 r2 H0). +Right; Rewrite <- H0; Auto with real. Save. +Hints Resolve Rle_compatibility Rle_compatibility_r : real. + (**********) -Lemma Rlt_le:(r1,r2:R)(Rlt r1 r2)->(Rle r1 r2). -Intros; Unfold Rle; Left; Auto with zarith real. +Lemma Rle_anti_compatibility: (r,r1,r2:R)``r+r1<=r+r2`` -> ``r1<=r2``. +Unfold Rle; Intros; Elim H; Intro. +Left; Apply (Rlt_anti_compatibility r r1 r2 H0). +Right; Apply (r_Rplus_plus r r1 r2 H0). Save. (**********) -Lemma eq_Rle:(r1,r2:R)(r1==r2)->(Rle r1 r2). -Intros; Unfold Rle; Right; Auto with zarith real. +Lemma sum_inequa_Rle_lt:(a,x,b,c,y,d:R)``a<=x`` -> ``x + ``c ``y<=d`` -> ``a+c < x+y < b+d``. +Intros;Split. +Apply Rlt_le_trans with ``a+y``; Auto with real. +Apply Rlt_le_trans with ``b+y``; Auto with real. Save. -(**********) -Lemma Rle_trans:(r1,r2,r3:R) - (Rle r1 r2)->(Rle r2 r3)->(Rle r1 r3). -Intros r1 r2 r3; Unfold Rle; Intros. -Elim H; Elim H0; Intros. -Cut (Rlt r1 r3). -Intro. -Apply (Rlt_le r1 r3); Auto with zarith real. -Apply (Rlt_trans r1 r2 r3); Auto with zarith real. -Rewrite <- H1; Auto with zarith real. -Rewrite -> H2; Auto with zarith real. -Rewrite -> H2; Auto with zarith real. +(*********) +Lemma Rplus_lt:(r1,r2,r3,r4:R)``r1 ``r3 ``r1+r3 < r2+r4``. +Intros; Apply Rlt_trans with ``r2+r3``; Auto with real. Save. -(**********) -Lemma Rle_lt_trans:(r1,r2,r3:R) - (Rle r1 r2)->(Rlt r2 r3)->(Rlt r1 r3). -Intros; Unfold Rle in H; Elim H; Intro. -Apply (Rlt_trans r1 r2 r3 H1 H0). -Rewrite -> H1; Auto with zarith real. +(*********) +Lemma Rplus_lt_le_lt:(r1,r2,r3,r4:R)``r1 ``r3<=r4`` -> ``r1+r3 < r2+r4``. +Intros; Apply Rlt_le_trans with ``r2+r3``; Auto with real. Save. -(**********) -Lemma Rlt_le_trans:(r1,r2,r3:R) - (Rlt r1 r2)->(Rle r2 r3)->(Rlt r1 r3). -Intros; Unfold Rle in H0; Elim H0; Intro. -Apply (Rlt_trans r1 r2 r3 H H1). -Rewrite <- H1; Auto with zarith real. +(*********) +Lemma Rplus_le_lt_lt:(r1,r2,r3,r4:R)``r1<=r2`` -> ``r3 ``r1+r3 < r2+r4``. +Intros; Apply Rle_lt_trans with ``r2+r3``; Auto with real. Save. +Hints Immediate Rplus_lt Rplus_lt_le_lt Rplus_le_lt_lt : real. + +(*s Order and Opposite *) + (**********) -Lemma Rlt_anti_compatibility: - (r,r1,r2:R)(Rlt (Rplus r r1) (Rplus r r2))->(Rlt r1 r2). -Intros; - Cut (Rlt (Rplus (Rplus (Ropp r) r) r1) - (Rplus (Rplus (Ropp r) r) r2)). -Rewrite -> Rplus_Ropp_l. -Elim (Rplus_ne r1); Elim (Rplus_ne r2); Intros; Rewrite <- H3; - Rewrite <- H1; Auto with zarith real. -Rewrite -> Rplus_assoc; Rewrite -> Rplus_assoc; - Apply (Rlt_compatibility (Ropp r) (Rplus r r1) (Rplus r r2) H). +Lemma Rgt_Ropp:(r1,r2:R) ``r1 > r2`` -> ``-r1 < -r2``. +Unfold Rgt; Intros. +Apply (Rlt_anti_compatibility ``r2+r1``). +Replace ``r2+r1+(-r1)`` with r2. +Replace ``r2+r1+(-r2)`` with r1. +Trivial. +Ring. +Ring. Save. +Hints Resolve Rgt_Ropp. (**********) -Lemma Rle_compatibility:(r,r1,r2:R)(Rle r1 r2)-> - (Rle (Rplus r r1) (Rplus r r2)). -Unfold Rle; Intros; Elim H; Intro. -Left; Apply (Rlt_compatibility r r1 r2 H0). -Right; Rewrite <- H0; Auto with zarith real. +Lemma Rlt_Ropp:(r1,r2:R) ``r1 < r2`` -> ``-r1 > -r2``. +Unfold Rgt; Auto with real. Save. +Hints Resolve Rlt_Ropp : real. (**********) -Lemma Rle_anti_compatibility: - (r,r1,r2:R)(Rle (Rplus r r1) (Rplus r r2))->(Rle r1 r2). -Unfold Rle; Intros; Elim H; Intro. -Left; Apply (Rlt_anti_compatibility r r1 r2 H0). -Right; Apply (r_Rplus_plus r r1 r2 H0). +Lemma Rle_Ropp:(r1,r2:R) ``r1 <= r2`` -> ``-r1 >= -r2``. +Unfold Rge; Intros r1 r2 [H|H]; Auto with real. Save. +Hints Resolve Rle_Ropp : real. (**********) -Lemma Rgt_Ropp:(r1,r2:R) - (Rgt r1 r2)->(Rlt (Ropp r1) (Ropp r2)). -Intros;Unfold Rgt in H; - Generalize (Rlt_compatibility (Ropp r2) r2 r1 H);Intro; - Generalize (Rlt_compatibility (Ropp r1) (Rplus (Ropp r2) r2) - (Rplus (Ropp r2) r1) H0); - Rewrite (Rplus_Ropp_l r2);Rewrite (Rplus_sym (Ropp r2) r1); - Rewrite <-(Rplus_assoc (Ropp r1) r1 (Ropp r2)); - Rewrite (Rplus_Ropp_l r1);Elim (Rplus_ne (Ropp r1));Intros a b; - Rewrite a;Clear a b;Elim (Rplus_ne (Ropp r2));Intros a b; - Rewrite b;Clear a b;Auto with zarith real. +Lemma Rge_Ropp:(r1,r2:R) ``r1 >= r2`` -> ``-r1 <= -r2``. +Unfold Rge; Intros r1 r2 [H|H]; Auto with real. +Red; Auto with real. Save. +Hints Resolve Rge_Ropp : real. (**********) -Lemma Rlt_Ropp:(r1,r2:R) - (Rlt r1 r2)->(Rgt (Ropp r1) (Ropp r2)). -Intros; Cut (Rgt r2 r1). -Intro; Cut (Rlt (Ropp r2) (Ropp r1)); Auto with zarith real. -Apply (Rgt_Ropp r2 r1 H0). -Auto with zarith real. +Lemma Rlt_RO_Ropp:(r:R) ``0 < r`` -> ``0 > -r``. +Intros; Replace ``0`` with ``-0``; Auto with real. Save. +Hints Resolve Rlt_RO_Ropp : real. (**********) -Lemma Rlt_anti_monotony:(r,r1,r2:R)(Rlt r R0)->(Rlt r1 r2)-> - (Rgt (Rmult r r1) (Rmult r r2)). -Intros;Generalize (Rlt_Ropp r1 r2 H0);Intro;Unfold Rgt; - Rewrite <-(Ropp_mul2 r r2);Rewrite <-(Ropp_mul2 r r1); - Apply (Rlt_monotony (Ropp r) (Ropp r2) (Ropp r1));Auto with zarith real. -Apply (Rlt_anti_compatibility r R0 (Ropp r)); - Elim (Rplus_ne r);Intros a b;Rewrite a;Clear a b; - Rewrite (Rplus_Ropp_r r);Assumption. +Lemma Rgt_RO_Ropp:(r:R) ``0 > r`` -> ``0 < -r``. +Intros; Replace ``0`` with ``-0``; Auto with real. Save. +Hints Resolve Rgt_RO_Ropp : real. (**********) -Lemma Rle_monotony: - (r,r1,r2:R) - (Rle R0 r) - ->(Rle r1 r2)->(Rle (Rmult r r1) (Rmult r r2)). -Intros r r1 r2;Unfold Rle;Intros;Elim H;Elim H0;Intros. -Left;Apply Rlt_monotony;Assumption. -Right;Rewrite H1;Reflexivity. -Right;Rewrite <- H2;Rewrite Rmult_Ol;Rewrite Rmult_Ol;Reflexivity. -Right;Rewrite H1;Reflexivity. +Lemma Rle_RO_Ropp:(r:R) ``0 <= r`` -> ``0 >= -r``. +Intros; Replace ``0`` with ``-0``; Auto with real. Save. +Hints Resolve Rle_RO_Ropp : real. (**********) -Lemma Rlt_minus:(r1,r2:R)(Rlt r1 r2)->(Rlt (Rminus r1 r2) R0). -Intros; Cut (Rlt (Rminus r1 r2) (Rminus r2 r2)). -Rewrite -> (eq_Rminus r2); Auto with zarith real. -Unfold Rminus; Rewrite -> (Rplus_sym r1 (Ropp r2)); - Rewrite -> (Rplus_sym r2 (Ropp r2)); - Apply (Rlt_compatibility (Ropp r2) r1 r2 H). +Lemma Rge_RO_Ropp:(r:R) ``0 >= r`` -> ``0 <= -r``. +Intros; Replace ``0`` with ``-0``; Auto with real. Save. +Hints Resolve Rge_RO_Ropp : real. -(**********) -Lemma Rle_minus:(r1,r2:R)(Rle r1 r2)->(Rle (Rminus r1 r2) R0). -Unfold Rle; Intros; Elim H; Intro. -Left; Apply (Rlt_minus r1 r2 H0). -Right; Apply (eq_Rminus r1 r2 H0). +(*s Order and multiplication *) + +Lemma Rlt_monotony_r:(r,r1,r2:R)``0 ``r1 < r2`` -> ``r1*r < r2*r``. +Intros; Rewrite (Rmult_sym r1 r); Rewrite (Rmult_sym r2 r); Auto with real. Save. +Hints Resolve Rlt_monotony_r. -(**********) -Lemma Rminus_lt:(r1,r2:R)(Rlt (Rminus r1 r2) R0)->(Rlt r1 r2). -Intros;Unfold Rminus in H; - Generalize (Rlt_compatibility r2 (Rplus r1 (Ropp r2)) R0 H); - Intro;Clear H; - Rewrite (Rplus_sym r1 (Ropp r2)) in H0; - Rewrite <- (Rplus_assoc r2 (Ropp r2) r1) in H0; - Rewrite (Rplus_Ropp_r r2) in H0;Elim (Rplus_ne r1); Elim (Rplus_ne r2); - Intros; - Rewrite H3 in H0; Rewrite H in H0; Auto with zarith real. +Lemma Rlt_anti_monotony:(r,r1,r2:R)``r < 0`` -> ``r1 < r2`` -> ``r*r1 > r*r2``. +Intros; Replace r with ``-(-r)``; Auto with real. +Rewrite (Ropp_mul1 ``-r``); Rewrite (Ropp_mul1 ``-r``). +Apply Rlt_Ropp; Auto with real. Save. (**********) -Lemma Rminus_le:(r1,r2:R)(Rle (Rminus r1 r2) R0)->(Rle r1 r2). -Unfold Rle;Intros;Elim H; Intro;Clear H. -Left;Apply Rminus_lt;Auto with zarith real. -Right;Apply Rminus_eq;Auto with zarith real. +Lemma Rle_monotony: + (r,r1,r2:R)``0 <= r`` -> ``r1 <= r2`` -> ``r*r1 <= r*r2``. +Intros r r1 r2;Unfold Rle;Intros H H0;Elim H;Elim H0;Intros; Auto with real. +Right;Rewrite <- H2;Ring. Save. +Hints Resolve Rle_monotony : real. -(**********) -Lemma sum_inequa_Rle_lt:(a,x,b,c,y,d:R)(Rle a x)->(Rlt x b)-> - (Rlt c y)->(Rle y d)-> - (Rlt (Rplus a c) (Rplus x y))/\(Rlt (Rplus x y) (Rplus b d)). -Intros;Split. -Apply (Rlt_le_trans (Rplus a c) (Rplus a y) (Rplus x y)). -Apply (Rlt_compatibility a c y H1). -Rewrite (Rplus_sym a y);Rewrite (Rplus_sym x y); - Apply (Rle_compatibility y a x H). -Apply (Rle_lt_trans (Rplus x y) (Rplus d x) (Rplus b d)). -Rewrite (Rplus_sym d x);Apply (Rle_compatibility x y d H2). -Rewrite (Rplus_sym b d);Apply (Rlt_compatibility d x b H0). +Lemma Rle_monotony_r: + (r,r1,r2:R)``0 <= r`` -> ``r1 <= r2`` -> ``r1*r <= r2*r``. +Intros r r1 r2 H; +Rewrite (Rmult_sym r1 r); Rewrite (Rmult_sym r2 r); Auto with real. Save. +Hints Resolve Rle_monotony_r : real. -(*********) -Lemma Rplus_lt:(r1,r2,r3,r4:R)(Rlt r1 r2)->(Rlt r3 r4)-> - (Rlt (Rplus r1 r3) (Rplus r2 r4)). -Intros; Generalize (Rlt_compatibility r3 r1 r2 H); - Generalize (Rlt_compatibility r2 r3 r4 H0);Intros; - Rewrite (Rplus_sym r3 r2) in H2;Rewrite (Rplus_sym r3 r1) in H2; - Apply (Rlt_trans (Rplus r1 r3) (Rplus r2 r3) (Rplus r2 r4) H2 H1). +Lemma Rle_anti_monotony + :(r,r1,r2:R)``r <= 0`` -> ``r1 <= r2`` -> ``r*r1 >= r*r2``. +Intros; Replace r with ``-(-r)``; Auto with real. +Rewrite (Ropp_mul1 ``-r``); Rewrite (Ropp_mul1 ``-r``). +Apply Rle_Ropp; Auto with real. Save. +Hints Resolve Rle_anti_monotony : real. -(*********) -Lemma Rplus_lt_le_lt:(r1,r2,r3,r4:R)(Rlt r1 r2)->(Rle r3 r4)-> - (Rlt (Rplus r1 r3) (Rplus r2 r4)). -Intros;Unfold Rle in H0; Elim H0. -Exact (Rplus_lt r1 r2 r3 r4 H). -Intro;Rewrite H1;Rewrite (Rplus_sym r1 r4);Rewrite (Rplus_sym r2 r4); - Exact (Rlt_compatibility r4 r1 r2 H). + + +Lemma Rmult_lt:(r1,r2,r3,r4:R)``r3>0`` -> ``r2>0`` -> + `` r1 < r2`` -> ``r3 < r4`` -> ``r1*r3 < r2*r4``. +Intros; Apply Rlt_trans with ``r2*r3``; Auto with real. Save. -(*********) -Lemma Rmult_lt:(r1,r2,r3,r4:R)(Rgt r3 R0)->(Rgt r2 R0)-> - (Rlt r1 r2)->(Rlt r3 r4)->(Rlt (Rmult r1 r3) (Rmult r2 r4)). -Intros;Unfold Rgt in H H0;Generalize (Rlt_monotony r3 r1 r2 H H1);Intro; - Generalize (Rlt_monotony r2 r3 r4 H0 H2);Intro; - Rewrite (Rmult_sym r3 r1) in H3;Rewrite (Rmult_sym r3 r2) in H3; - Apply (Rlt_trans (Rmult r1 r3) (Rmult r2 r3) (Rmult r2 r4) H3 H4). + +(*s Order and Substractions *) +Lemma Rlt_minus:(r1,r2:R)``r1 < r2`` -> ``r1-r2 < 0``. +Intros; Apply (Rlt_anti_compatibility ``r2``). +Replace ``r2+(r1-r2)`` with r1. +Replace ``r2+0`` with r2; Auto with real. +Ring. Save. +Hints Resolve Rlt_minus : real. (**********) -Lemma inser_trans_R:(n,m,p,q:R)(Rle n m)/\(Rlt m p)-> - (sumboolT ((Rle n m)/\(Rlt m q)) ((Rle q m)/\(Rlt m p))). -Intros; Cut (sumboolT (Rle q m) (Rlt m q)). -Intro;Cut (Rle n m);[Intro;Cut (Rlt m p)|Elim H;Auto with zarith real]. -Intro;Elim X;Intro. -Right; Auto with zarith real. -Left; Auto with zarith real. -Elim H;Auto with zarith real. -Generalize (total_order_Rle q m); Intro; Elim X; Intro. -Left;Auto with zarith real. -Right; Generalize (not_Rle q m y); Auto with zarith real. +Lemma Rle_minus:(r1,r2:R)``r1 <= r2`` -> ``r1-r2 <= 0``. +Unfold Rle; Intros; Elim H; Auto with real. Save. (**********) -Lemma tech_Rplus:(r,s:R)(Rle R0 r)->(Rlt R0 s)->~(Rplus r s)==R0. -Red;Intros;Cut (Rlt R0 (Rplus r s)). -Intro;Elim (imp_not_Req R0 (Rplus r s));Auto with zarith real. -Clear H1;Generalize (Rlt_compatibility r R0 s H0);Intro; - Elim (Rplus_ne r);Intros a b;Rewrite a in H1;Clear a b; - Apply (Rle_lt_trans R0 r (Rplus r s) H H1). +Lemma Rminus_lt:(r1,r2:R)``r1-r2 < 0`` -> ``r1 < r2``. +Intros; Replace r1 with ``r1-r2+r2``. +Pattern 3 r2; Replace r2 with ``0+r2``; Auto with real. +Ring. Save. -(***********) -Lemma pos_Rsqr:(r:R)(Rle R0 (Rsqr r)). -Intro; Cut (Rlt r R0)\/r==R0\/(Rgt r R0). -Intro; Elim H; Intro; Unfold Rle. -Left; Replace R0 with (Rmult r R0). -Unfold Rsqr; Apply (Rlt_anti_monotony r r R0 H0 H0). -Auto with zarith real. -Elim H0; Intro. -Right; Rewrite -> H1; Apply sym_eqT; Apply Rsqr_O. -Left; Unfold Rgt in H1; Replace R0 with (Rmult r R0). -Unfold Rsqr; Apply (Rlt_monotony r R0 r H1 H1). -Auto with zarith real. -Apply (total_order r R0). +(**********) +Lemma Rminus_le:(r1,r2:R)``r1-r2 <= 0`` -> ``r1 <= r2``. +Intros; Replace r1 with ``r1-r2+r2``. +Pattern 3 r2; Replace r2 with ``0+r2``; Auto with real. +Ring. Save. -(***********) -Lemma pos_Rsqr1:(r:R)(~(r==R0))->(Rlt R0 (Rsqr r)). -Intros; Cut (Rlt r R0)\/(Rgt r R0). -Intro; Elim H0; Intro. -Replace R0 with (Rmult r R0); Unfold Rsqr. -Apply (Rlt_anti_monotony r r R0 H1 H1). -Auto with zarith real. -Unfold Rgt in H1; Replace R0 with (Rmult r R0). -Unfold Rsqr; Apply (Rlt_monotony r R0 r H1 H1). -Auto with zarith real. -Apply (not_Req r R0 H). -Save. (**********) -Lemma Rlt_R0_R1:(Rlt R0 R1). -Cut ~R1==R0->(Rlt R0 (Rsqr R1)). -Intro; Replace R1 with (Rsqr R1); Cut ~R1==R0; Auto with zarith real. -Red; Intro; Apply (R1_neq_R0 H0). -Unfold Rsqr; Elim (Rmult_ne R1); Auto with zarith real. -Red; Intro; Apply (R1_neq_R0 H0). -Intro; Apply (pos_Rsqr1 R1 H). +Lemma tech_Rplus:(r,s:R)``0<=r`` -> ``0 ``r+s<>0``. +Intros; Apply sym_not_eqT; Apply Rlt_not_eq. +Rewrite Rplus_sym; Replace ``0`` with ``0+0``; Auto with real. Save. +Hints Immediate tech_Rplus : real. -(*********) -Lemma Rlt_Rinv:(r:R)(Rlt R0 r)->(Rlt R0 (Rinv r)). -Intros; Fold (Rgt (Rinv r) R0); Apply (not_Rle (Rinv r) R0);Red; - Intro;Unfold Rle in H0;Elim H0; Intro;Clear H0. -Generalize (Rlt_monotony r (Rinv r) R0 H H1);Rewrite (Rinv_r r). -Rewrite (Rmult_Or r);Intro;Generalize (Rle_not R0 R1 H0); - Generalize (Rlt_le R0 R1 Rlt_R0_R1);Intros;Auto. -Apply (sym_not_eqT R R0 r);Apply (imp_not_Req R0 r);Left;Assumption. -Generalize (Rmult_mult_r r (Rinv r) R0 H1);Rewrite (Rinv_r r). -Rewrite (Rmult_Or r);Intro;Generalize R1_neq_R0;Auto. -Apply (sym_not_eqT R R0 r);Apply (imp_not_Req R0 r);Left;Assumption. +(*s Order and the square function *) +Lemma pos_Rsqr:(r:R)``0<=(Rsqr r)``. +Intro; Case (total_order_Rlt_Rle r ``0``); Unfold Rsqr; Intro. +Replace ``r*r`` with ``(-r)*(-r)``; Auto with real. +Replace ``0`` with ``-r*0``; Auto with real. +Replace ``0`` with ``0*r``; Auto with real. Save. -(*********) -Lemma Rlt_Rinv2:(r:R)(Rlt r R0)->(Rlt (Rinv r) R0). -Intros;Fold (Rgt R0 (Rinv r)); Apply (not_Rle R0 (Rinv r));Red; - Intro;Unfold Rle in H0;Elim H0; Intro;Clear H0. -Generalize (Rlt_monotony (Rinv r) r R0 H1 H);Rewrite (Rinv_l r). -Rewrite (Rmult_Or (Rinv r));Intro;Generalize (Rle_not R0 R1 H0); - Generalize (Rlt_le R0 R1 Rlt_R0_R1);Intros;Auto. -Apply (imp_not_Req r R0);Left;Assumption. -Generalize (Rmult_mult_r r R0 (Rinv r) H1);Rewrite (Rinv_r r). -Rewrite (Rmult_Or r);Intro;Generalize R1_neq_R0;Auto. -Apply (imp_not_Req r R0);Left;Assumption. +(***********) +Lemma pos_Rsqr1:(r:R)``r<>0``->``0<(Rsqr r)``. +Intros; Case (not_Req r ``0``); Trivial; Unfold Rsqr; Intro. +Replace ``r*r`` with ``(-r)*(-r)``; Auto with real. +Replace ``0`` with ``-r*0``; Auto with real. +Replace ``0`` with ``0*r``; Auto with real. Save. +Hints Resolve pos_Rsqr pos_Rsqr1 : real. + +(*s Zero is less than one *) +Lemma Rlt_R0_R1:``0<1``. +Replace ``1`` with ``(Rsqr 1)``; Auto with real. +Unfold Rsqr; Auto with real. +Save. +Hints Resolve Rlt_R0_R1 : real. + +(*s Order and inverse *) +Lemma Rlt_Rinv:(r:R)``0``0<1/r``. +Intros; Change ``1/r>0``; Apply not_Rle; Red; Intros. +Absurd ``1<=0``; Auto with real. +Replace ``1`` with ``r*(1/r)``; Auto with real. +Replace ``0`` with ``r*0``; Auto with real. +Save. +Hints Resolve Rlt_Rinv : real. (*********) -Lemma Rinv_lt:(r1,r2:R)(Rlt R0 (Rmult r1 r2))->(Rlt r1 r2)-> - (Rlt (Rinv r2) (Rinv r1)). -Intros;Generalize (Rlt_monotony (Rinv (Rmult r1 r2)) r1 r2 - (Rlt_Rinv (Rmult r1 r2) H) H0);Intro; - Elim (without_div_O_contr r1 r2 - (sym_not_eqT R R0 (Rmult r1 r2) (imp_not_Req R0 (Rmult r1 r2) - (or_introl (Rlt R0 (Rmult r1 r2)) (Rgt R0 (Rmult r1 r2)) H)))); - Intros;Rewrite Rinv_Rmult in H1;Auto; - Rewrite (Rmult_assoc (Rinv r1) (Rinv r2) r2) in H1; - Rewrite (Rinv_l r2 H3) in H1; - Rewrite (let (H1,H2)=(Rmult_ne (Rinv r1)) in H1) in H1; - Rewrite (Rmult_sym (Rinv r1) (Rinv r2)) in H1; - Rewrite (Rmult_assoc (Rinv r2) (Rinv r1) r1 ) in H1; - Rewrite (Rinv_l r1 H2) in H1; - Rewrite (let (H1,H2)=(Rmult_ne (Rinv r2)) in H1) in H1;Assumption. +Lemma Rlt_Rinv2:(r:R)``r < 0``->``1/r < 0``. +Intros; Change ``0>1/r``; Apply not_Rle; Red; Intros. +Absurd ``1<=0``; Auto with real. +Replace ``1`` with ``r*(1/r)``; Auto with real. +Replace ``0`` with ``r*0``; Auto with real. +Apply Rge_le; Auto with real. Save. +Hints Resolve Rlt_Rinv2 : real. (**********) Lemma Rlt_monotony_rev: - (r,r1,r2:R)(Rlt R0 r)->(Rlt (Rmult r r1) (Rmult r r2)) - ->(Rlt r1 r2). -Intros;Cut (s:R) (Rmult (Rinv r) (Rmult r s))==s. -Intros; Rewrite <- (H1 r1); Rewrite <- (H1 r2);Apply Rlt_monotony. -Apply Rlt_Rinv; Assumption. -Assumption. -Intro;Rewrite <- Rmult_assoc;Rewrite Rinv_l. + (r,r1,r2:R)``0 ``r*r1 < r*r2`` -> ``r1 < r2``. +Intros; Replace r1 with ``1/r*(r*r1)``. +Replace r2 with ``1/r*(r*r2)``; Auto with real. +Transitivity ``r*1/r*r2``; Auto with real. +Ring. +Transitivity ``r*1/r*r1``; Auto with real. Ring. -Apply imp_not_Req; Right; Unfold Rgt; Assumption. Save. +(*********) +Lemma Rinv_lt:(r1,r2:R)``0 < r1*r2`` -> ``r1 < r2`` -> ``1/r2 < 1/r1``. +Intros; Apply Rlt_monotony_rev with ``r1*r2``; Auto with real. +Case (without_div_O_contr r1 r2 ); Intros; Auto with real. +Replace ``r1*r2*1/r2`` with r1. +Replace ``r1*r2*1/r1`` with r2; Trivial. +Symmetry; Auto with real. +Symmetry; Auto with real. +Save. + + (*********************************************************) -(* Greater *) +(*s Greater *) (*********************************************************) (**********) -Lemma Rge_ge_eq:(r1,r2:R)(Rge r1 r2)->(Rge r2 r1)->r1==r2. -Unfold Rge; Intros; Elim H; Intro; Auto with zarith real. -Elim H0; Intro; Auto with zarith real. -Absurd (Rgt r1 r2); Auto with zarith real. -Unfold Rgt; Unfold Rgt in H2; Apply Rlt_antisym; Auto with zarith real. +Lemma Rge_ge_eq:(r1,r2:R)``r1 >= r2`` -> ``r2 >= r1`` -> r1==r2. +Intros; Apply Rle_antisym; Auto with real. Save. (**********) -Lemma Rlt_not_ge:(r1,r2:R)~(Rlt r1 r2)->(Rge r1 r2). +Lemma Rlt_not_ge:(r1,r2:R)~(``r1``r1>=r2``. Intros; Unfold Rge; Elim (total_order r1 r2); Intro. -ElimType False; Auto with zarith real. -Elim H0; Auto with zarith real. +Absurd ``r1(Rle r1 r2). -Intros; Unfold Rgt in H; Unfold Rle; Elim (total_order r1 r2); Intro. -Left ; Auto with zarith real. -Elim H0; Intro; Auto with zarith real. -Unfold Rgt in H1; ElimType False; Auto with zarith real. +Lemma Rgt_not_le:(r1,r2:R)~(``r1>r2``)->``r1<=r2``. +Intros r1 r2 H; Apply Rge_le. +Exact (Rlt_not_ge r2 r1 H). Save. (**********) -Lemma Rgt_ge:(r1,r2:R)(Rgt r1 r2)->(Rge r1 r2). -Intros; Unfold Rge; Left; Auto with zarith real. +Lemma Rgt_ge:(r1,r2:R)``r1>r2`` -> ``r1 >= r2``. +Red; Auto with real. Save. (**********) -Lemma Rlt_sym:(r1,r2:R) - (((Rlt r1 r2)->(Rgt r2 r1))/\((Rgt r2 r1)->(Rlt r1 r2))). -Intros; Split; Intro; Unfold Rgt; Auto with zarith real. +Lemma Rlt_sym:(r1,r2:R)``r1 ``r2>r1``. +Split; Unfold Rgt; Auto with real. Save. (**********) -Lemma Rle_sym1:(r1,r2:R)(Rle r1 r2)->(Rge r2 r1). -Intros r1 r2; Unfold Rge; Unfold Rle; Intro; Elim H; Intro. -Left; Unfold Rgt; Auto with zarith real. -Right; Auto with zarith real. -Save. +Lemma Rle_sym1:(r1,r2:R)``r1<=r2``->``r2>=r1``. +Proof Rle_ge. (**********) -Lemma Rle_sym2:(r1,r2:R)(Rge r2 r1)->(Rle r1 r2). -Intros r1 r2; Unfold Rge; Unfold Rle; Intro; Elim H; Intro. -Left; Unfold Rgt in H0; Auto with zarith real. -Right; Auto with zarith real. -Save. +Lemma Rle_sym2:(r1,r2:R)``r2>=r1`` -> ``r1<=r2``. +Proof [r1,r2](Rge_le r2 r1). (**********) -Lemma Rle_sym:(r1,r2:R) - (((Rle r1 r2)->(Rge r2 r1))/\((Rge r2 r1)->(Rle r1 r2))). -Intros; Split; Intro. -Apply Rle_sym1; Auto with zarith real. -Apply Rle_sym2; Auto with zarith real. +Lemma Rle_sym:(r1,r2:R)``r1<=r2``<->``r2>=r1``. +Split; Auto with real. Save. (**********) -Lemma Rge_gt_trans:(r1,r2,r3:R) - (Rge r1 r2)->(Rgt r2 r3)->(Rgt r1 r3). -Intros r1 r2 r3; Unfold Rgt; Unfold Rge; Intros; Elim H; Intros. -Unfold Rgt in H1; Apply (Rlt_trans r3 r2 r1 H0 H1). -Rewrite -> H1; Auto with zarith real. +Lemma Rge_gt_trans:(r1,r2,r3:R)``r1>=r2``->``r2>r3``->``r1>r3``. +Unfold Rgt; Intros; Apply Rlt_le_trans with r2; Auto with real. Save. (**********) -Lemma Rgt_ge_trans:(r1,r2,r3:R) - (Rgt r1 r2)->(Rge r2 r3)->(Rgt r1 r3). -Intros r1 r2 r3; Unfold Rgt; Unfold Rge; Intros; Elim H0; Intros. -Apply (Rlt_trans r3 r2 r1 H1 H). -Rewrite <- H1; Auto with zarith real. +Lemma Rgt_ge_trans:(r1,r2,r3:R)``r1>r2`` -> ``r2>=r3`` -> ``r1>r3``. +Unfold Rgt; Intros; Apply Rle_lt_trans with r2; Auto with real. Save. (**********) -Lemma Rgt_trans:(r1,r2,r3:R) - (Rgt r1 r2)->(Rgt r2 r3)->(Rgt r1 r3). -Intros; Cut (Rge r1 r2). -Intro; Apply (Rge_gt_trans r1 r2 r3 H1 H0). -Apply (Rgt_ge r1 r2 H). +Lemma Rgt_trans:(r1,r2,r3:R)``r1>r2`` -> ``r2>r3`` -> ``r1>r3``. +Unfold Rgt; Intros; Apply Rlt_trans with r2; Auto with real. Save. (**********) -Lemma Rge_trans:(r1,r2,r3:R) - (Rge r1 r2)->(Rge r2 r3)->(Rge r1 r3). -Intros; Cut (Rle r2 r1). -Cut (Rle r3 r2); Intros. -Cut (Rle r3 r1). -Intro; Apply (Rle_sym1 r3 r1 H3). -Apply (Rle_trans r3 r2 r1 H1 H2). -Apply (Rle_sym2 r3 r2 H0). -Apply (Rle_sym2 r2 r1 H). +Lemma Rge_trans:(r1,r2,r3:R)``r1>=r2`` -> ``r2>=r3`` -> ``r1>=r3``. +Intros; Apply Rle_ge. +Apply Rle_trans with r2; Auto with real. Save. (**********) -Lemma eq_Rge:(r1,r2:R)(r1==r2)->(Rge r1 r2). -Intros; Unfold Rge; Right; Auto with zarith real. +Lemma Rgt_RoppO:(r:R)``r>0``->``(-r)<0``. +Intros; Rewrite <- Ropp_O; Auto with real. Save. (**********) -Lemma Rle_Ropp:(r1,r2:R) - (Rle r1 r2)->(Rge (Ropp r1) (Ropp r2)). -Unfold Rle; Intros; Unfold Rge; Elim H; Intro. -Left; Apply (Rlt_Ropp r1 r2 H0). -Right; Apply (eq_Ropp r1 r2 H0). +Lemma Rlt_RoppO:(r:R)``r<0``->``-r>0``. +Intros; Rewrite <- Ropp_O; Auto with real. Save. +Hints Resolve Rgt_RoppO Rlt_RoppO: real. (**********) -Lemma Rgt_RoppO:(r:R)(Rgt r R0)->(Rlt (Ropp r) R0). -Intros; Rewrite <- Ropp_O; Apply (Rgt_Ropp r R0); Auto with zarith real. +Lemma Rlt_r_plus_R1:(r:R)``0<=r`` -> ``0(Rgt (Ropp r) R0). -Intros; Rewrite <- Ropp_O; Apply (Rlt_Ropp r R0); Auto with zarith real. +Lemma Rlt_r_r_plus_R1:(r:R)``r(Rlt R0 (Rplus r R1)). -Unfold Rle; Intros; Elim H; Intro; Clear H. -Apply (Rlt_anti_compatibility (Ropp r) R0 (Rplus r R1)); - Elim (Rplus_ne (Ropp r)); Intros; Rewrite H; Clear H H1; - Rewrite <- (Rplus_assoc (Ropp r) r R1); Rewrite Rplus_Ropp_l; - Elim (Rplus_ne R1); Intros; Rewrite H1; Clear H H1; - Fold (Rgt r R0) in H0; Generalize (Rgt_RoppO r H0); Intro; - Generalize Rlt_R0_R1; Intro; Apply (Rlt_trans (Ropp r) R0 R1 H H1). -Rewrite <- H0; Elim (Rplus_ne R1); Intros; Rewrite H1; Clear H H1; - Apply Rlt_R0_R1. -Save. (**********) -Lemma tech_Rgt_minus:(r1,r2:R)(Rlt R0 r2)->(Rgt r1 (Rminus r1 r2)). -Intros;Fold (Rgt r2 R0) in H;Generalize (Rgt_RoppO r2 H); Intro; - Generalize (Rlt_compatibility r1 (Ropp r2) R0 H0); Intro; - Elim (Rplus_ne r1); Intros a b; Rewrite a in H1; Clear a b; - Unfold Rgt;Unfold Rminus;Assumption. +Lemma tech_Rgt_minus:(r1,r2:R)``0``r1>r1-r2``. +Red; Unfold Rminus; Intros. +Pattern 2 r1; Replace r1 with ``r1+0``; Auto with real. Save. (***********) -Lemma Rgt_plus_plus_r:(r,r1,r2:R)(Rgt r1 r2)-> - (Rgt (Rplus r r1) (Rplus r r2)). -Unfold Rgt; Intros; Apply (Rlt_compatibility r r2 r1 H). +Lemma Rgt_plus_plus_r:(r,r1,r2:R)``r1>r2``->``r+r1 > r+r2``. +Unfold Rgt; Auto with real. Save. +Hints Resolve Rgt_plus_plus_r : real. (***********) -Lemma Rgt_r_plus_plus:(r,r1,r2:R)(Rgt (Rplus r r1) (Rplus r r2))-> - (Rgt r1 r2). +Lemma Rgt_r_plus_plus:(r,r1,r2:R)``r+r1 > r+r2`` -> ``r1 > r2``. Unfold Rgt; Intros; Apply (Rlt_anti_compatibility r r2 r1 H). Save. (***********) -Lemma Rge_plus_plus_r:(r,r1,r2:R)(Rge r1 r2)-> - (Rge (Rplus r r1) (Rplus r r2)). -Unfold Rge; Intros; Elim H; Intro. -Left; Apply (Rgt_plus_plus_r r r1 r2 H0). -Right; Apply (Rplus_plus_r r r1 r2 H0). +Lemma Rge_plus_plus_r:(r,r1,r2:R)``r1>=r2`` -> ``r+r1 >= r+r2``. +Intros; Apply Rle_ge; Auto with real. Save. +Hints Resolve Rge_plus_plus_r : real. (***********) -Lemma Rge_r_plus_plus:(r,r1,r2:R)(Rge (Rplus r r1) (Rplus r r2))-> - (Rge r1 r2). -Unfold Rge; Intros; Elim H; Intro. -Left; Apply (Rgt_r_plus_plus r r1 r2 H0). -Right; Apply (r_Rplus_plus r r1 r2 H0). +Lemma Rge_r_plus_plus:(r,r1,r2:R)``r+r1 >= r+r2`` -> ``r1>=r2``. +Intros; Apply Rle_ge; Apply Rle_anti_compatibility with r; Auto with real. Save. (***********) Lemma Rge_monotony: - (x,y,z:R) (Rge z R0) -> (Rge x y) -> (Rge (Rmult x z) (Rmult y z)). -Intros;Apply Rle_sym1; - Rewrite (Rmult_sym y z); Rewrite (Rmult_sym x z); - Apply Rle_monotony;Apply Rle_sym2; Assumption. + (x,y,z:R) ``z>=0`` -> ``x>=y`` -> ``x*z >= y*z``. +Intros; Apply Rle_ge; Auto with real. Save. (***********) -Lemma Rgt_minus:(r1,r2:R)(Rgt r1 r2)->(Rgt (Rminus r1 r2) R0). -Intros; Cut (Rgt (Rminus r1 r2) (Rminus r2 r2)). -Rewrite -> (eq_Rminus r2 r2); Auto with zarith real. -Unfold Rminus; Rewrite -> (Rplus_sym r1 (Ropp r2)); - Rewrite -> (Rplus_sym r2 (Ropp r2)); - Apply (Rgt_plus_plus_r (Ropp r2) r1 r2 H). +Lemma Rgt_minus:(r1,r2:R)``r1>r2`` -> ``r1-r2 > 0``. +Intros; Replace ``0`` with ``r2-r2``; Auto with real. +Unfold Rgt Rminus; Auto with real. Save. (*********) -Lemma minus_Rgt:(r1,r2:R)(Rgt (Rminus r1 r2) R0)->(Rgt r1 r2). -Intros;Generalize (Rgt_plus_plus_r r2 (Rminus r1 r2) R0 H); Intro; - Rewrite (Rplus_sym r2 (Rminus r1 r2)) in H0;Unfold Rminus in H0; - Rewrite (Rplus_assoc r1 (Ropp r2) r2) in H0; - Rewrite (Rplus_Ropp_l r2) in H0; - Elim (Rplus_ne r1); Intros a b; Rewrite a in H0; Clear a b; - Elim (Rplus_ne r2); Intros a b; Rewrite a in H0; Clear a b;Exact H0. +Lemma minus_Rgt:(r1,r2:R)``r1-r2 > 0`` -> ``r1>r2``. +Intros; Replace r2 with ``r2+0``; Auto with real. +Intros; Replace r1 with ``r2+(r1-r2)``; Auto with real. +Ring. Save. (**********) -Lemma Rge_minus:(r1,r2:R)(Rge r1 r2)->(Rge (Rminus r1 r2) R0). +Lemma Rge_minus:(r1,r2:R)``r1>=r2`` -> ``r1-r2 >= 0``. Unfold Rge; Intros; Elim H; Intro. Left; Apply (Rgt_minus r1 r2 H0). Right; Apply (eq_Rminus r1 r2 H0). Save. (*********) -Lemma minus_Rge:(r1,r2:R)(Rge (Rminus r1 r2) R0)->(Rge r1 r2). -Intros;Generalize (Rge_plus_plus_r r2 (Rminus r1 r2) R0 H); Intro; - Rewrite (Rplus_sym r2 (Rminus r1 r2)) in H0;Unfold Rminus in H0; - Rewrite (Rplus_assoc r1 (Ropp r2) r2) in H0; - Rewrite (Rplus_Ropp_l r2) in H0; - Elim (Rplus_ne r1); Intros a b; Rewrite a in H0; Clear a b; - Elim (Rplus_ne r2); Intros a b; Rewrite a in H0; Clear a b;Exact H0. +Lemma minus_Rge:(r1,r2:R)``r1-r2 >= 0`` -> ``r1>=r2``. +Intros; Replace r2 with ``r2+0``; Auto with real. +Intros; Replace r1 with ``r2+(r1-r2)``; Auto with real. +Ring. Save. + (*********) -Lemma Rmult_gt:(r1,r2:R)(Rgt r1 R0)->(Rgt r2 R0)->(Rgt (Rmult r1 r2) R0). -Unfold Rgt;Intros;Generalize (Rlt_monotony r1 R0 r2 H H0);Intro; - Rewrite (Rmult_Or r1) in H1;Assumption. +Lemma Rmult_gt:(r1,r2:R)``r1>0`` -> ``r2>0`` -> ``r1*r2>0``. +Unfold Rgt;Intros. +Replace ``0`` with ``0*r2``; Auto with real. Save. (*********) -Lemma Rmult_lt_0:(r1,r2,r3,r4:R)(Rge r3 R0)->(Rgt r2 R0)-> - (Rlt r1 r2)->(Rlt r3 r4)->(Rlt (Rmult r1 r3) (Rmult r2 r4)). -Intros;Elim H. -Intro;Exact (Rmult_lt r1 r2 r3 r4 H3 H0 H1 H2). -Intro;Rewrite H3;Rewrite (Rmult_Or r1); - Cut (Rgt r4 R0). -Intro;Exact (Rmult_gt r2 r4 H0 H4). -Cut (Rle R0 r3). -Intro;Exact (Rle_lt_trans R0 r3 r4 H4 H2). -Exact (Rle_sym2 R0 r3 H). +Lemma Rmult_lt_0 + :(r1,r2,r3,r4:R)``r3>=0``->``r2>0``->``r1``r3``r1*r3(Rlt R0 y)->(Rlt R0 (Rmult x y)). -Generalize Rmult_gt;Unfold Rgt;Auto. +Lemma Rmult_lt_pos:(x,y:R)``0 ``0 ``0 ``0<=b`` -> ``a+b==0`` -> ``a==0``. +Intros a b [H|H] H0 H1; Auto with real. +Absurd ``0(Rle R0 b)->(Rplus a b)==R0-> - (a==R0)/\(b==R0). -Intros;Generalize (Rle_Ropp R0 b H0);Intro;Rewrite Ropp_O in H2; - Generalize (Rle_Ropp R0 a H);Intro;Rewrite Ropp_O in H3; - Generalize (Rplus_Ropp a b H1);Intro;Rewrite Rplus_sym in H1; - Generalize (Rplus_Ropp b a H1);Intro;Clear H1;Rewrite <- H4 in H3; - Rewrite <-H5 in H2;Clear H4 H5; Generalize (Rle_sym1 R0 a H);Clear H; - Intro;Generalize (Rle_sym1 R0 b H0);Clear H0;Intro;Split;Apply Rge_ge_eq; - Assumption. +Lemma Rplus_eq_R0 + :(a,b:R)``0<=a`` -> ``0<=b`` -> ``a+b==0`` -> ``a==0``/\``b==0``. +Split. +Apply Rplus_eq_R0_l with b; Auto with real. +Apply Rplus_eq_R0_l with a; Auto with real. +Rewrite Rplus_sym; Auto with real. Save. + (***********) -Lemma Rplus_Rsr_eq_R0:(a,b:R)(Rplus (Rsqr a) (Rsqr b))==R0-> - (a==R0)/\(b==R0). -Intros;Elim (Rplus_eq_R0 (Rsqr a) (Rsqr b) (pos_Rsqr a) (pos_Rsqr b) H); - Intros;Clear H;Split;Apply Rsqr_r_R0;Assumption. +Lemma Rplus_Rsr_eq_R0_l:(a,b:R)``(Rsqr a)+(Rsqr b)==0``->``a==0``. +Intros; Apply Rsqr_r_R0; Apply Rplus_eq_R0_l with (Rsqr b); Auto with real. +Save. + +Lemma Rplus_Rsr_eq_R0:(a,b:R)``(Rsqr a)+(Rsqr b)==0``->``a==0``/\``b==0``. +Split. +Apply Rplus_Rsr_eq_R0_l with b; Auto with real. +Apply Rplus_Rsr_eq_R0_l with a; Auto with real. +Rewrite Rplus_sym; Auto with real. Save. + (**********************************************************) -(* Injection from N to R *) +(*s Injection from N to R *) (**********************************************************) (**********) -Lemma S_INR:(n:nat)(INR (S n))==(Rplus (INR n) R1). -Intro; Simpl; Case n. -Simpl; Elim (Rplus_ne R1); Auto with zarith real. -Auto with zarith real. +Lemma S_INR:(n:nat)(INR (S n))==``(INR n)+1``. +Intro; Case n; Auto with real. Save. (**********) Lemma S_O_plus_INR:(n:nat) - (INR (plus (S O) n))==(Rplus (INR (S O)) (INR n)). -Intro; Replace (plus (S O) n) with (S (plus O n)). -Replace (INR (S (plus O n))) with (Rplus (INR (plus O n)) R1). -Replace (INR (S O)) with (Rplus (INR O) R1). -Replace (INR (S O)) with (Rplus (INR O) R1); Simpl; Elim (Rplus_ne R1); - Intros; Rewrite -> H0; Auto with zarith real; Rewrite -> Rplus_sym; - Auto with zarith real. -Simpl. -Elim (Rplus_ne R1); Auto with zarith real. -Apply sym_eqT; Apply (S_INR (plus O n)). -Auto with zarith real. -Save. - -(**********) -Lemma plus_INR:(n,m:nat)(INR (plus n m))==(Rplus (INR n) (INR m)). -Induction n. -Simpl; Intro; Elim (Rplus_ne (INR m)); Auto with zarith real. -Intros; Rewrite -> plus_Snm_nSm; - Replace (INR (S n0)) with (Rplus (INR n0) R1). -Rewrite -> Rplus_assoc; Rewrite -> (Rplus_sym R1 (INR m)); - Replace (Rplus (INR m) R1) with (INR (S m)). -Apply (H (S m)). -Apply (S_INR m). -Apply sym_eqT; Apply (S_INR n0). -Save. - -(**********) -Lemma minus_INR:(n,m:nat)(le m n)-> - (INR (minus n m))==(Rminus (INR n) (INR m)). -Intros; - Cut (Rplus (INR m) (INR (minus n m))) - ==(Rplus (INR m) (Rminus (INR n) (INR m))). -Intro; - Apply (r_Rplus_plus (INR m) (INR (minus n m)) - (Rminus (INR n) (INR m)) H0). -Rewrite <- plus_INR; Rewrite -> le_plus_minus_r. -Unfold Rminus; Rewrite -> Rplus_sym; Rewrite -> Rplus_assoc; - Rewrite -> Rplus_Ropp_l; Elim (Rplus_ne (INR n)); Auto with zarith real. -Auto with zarith real. + (INR (plus (S O) n))==``(INR (S O))+(INR n)``. +Intro; Simpl; Case n; Intros; Auto with real. +Save. + +(**********) +Lemma plus_INR:(n,m:nat)(INR (plus n m))==``(INR n)+(INR m)``. +Intros n m; Induction n. +Simpl; Auto with real. +Replace (plus (S n) m) with (S (plus n m)); Auto with arith. +Repeat Rewrite S_INR. +Rewrite Hrecn; Ring. +Save. + + +(**********) +Lemma minus_INR:(n,m:nat)(le m n)->(INR (minus n m))==``(INR n)-(INR m)``. +Intros n m le; Pattern m n; Apply le_elim_rel; Auto with real. +Intros; Rewrite <- minus_n_O; Auto with real. +Intros; Repeat Rewrite S_INR; Simpl. +Rewrite H0; Ring. Save. (*********) Lemma mult_INR:(n,m:nat)(INR (mult n m))==(Rmult (INR n) (INR m)). -Induction n. -Simpl; Intro;Apply sym_eqT;Apply Rmult_Ol. -Intros;Unfold 1 mult;Cbv Beta Iota;Fold mult; - Rewrite (plus_INR m (mult n0 m));Rewrite (H m); - Pattern 1 (INR m); - Rewrite <-(let (H1,H2)=(Rmult_ne (INR m)) in H1); - Rewrite (Rmult_sym (INR n0) (INR m)); - Rewrite <-(Rmult_Rplus_distr (INR m) R1 (INR n0)); - Rewrite (Rplus_sym R1 (INR n0));Rewrite <-(S_INR n0); - Apply Rmult_sym. -Save. +Intros n m; Induction n. +Simpl; Auto with real. +Intros; Repeat Rewrite S_INR; Simpl. +Rewrite plus_INR; Rewrite Hrecn; Ring. +Save. +Hints Resolve plus_INR minus_INR mult_INR : real. (*********) -Lemma INR_lt_0:(n:nat)(lt O n)->(Rlt R0 (INR n)). -Induction n;Intros. -Absurd (lt (0) (0));[Apply lt_n_n|Assumption]. -Elim (le_lt_or_eq (0) n0 (lt_n_Sm_le (0) n0 H0));Intro. -Generalize (H H1);Clear H H1;Intro;Rewrite (S_INR n0); - Generalize (Rlt_compatibility R1 R0 (INR n0) H);Intro; - Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H1; - Rewrite (Rplus_sym (INR n0) R1); - Apply (Rlt_trans R0 R1 (Rplus R1 (INR n0)) (Rlt_R0_R1) H1). -Rewrite <-H1;Simpl;Apply Rlt_R0_R1. +Lemma INR_lt_0:(n:nat)(lt O n)->``0 < (INR n)``. +Induction 1; Intros; Auto with real. +Rewrite S_INR; Auto with real. Save. +Hints Resolve INR_lt_0: real. (**********) -Lemma INR_le:(n:nat)(Rle R0 (INR n)). -Induction n. -Simpl; Apply (eq_Rle R0 R0 (refl_eqT R R0)). -Intros;Rewrite (S_INR n0);Apply (Rlt_le R0 (Rplus (INR n0) R1)); - Apply (Rlt_r_plus_R1 (INR n0) H). +Lemma INR_pos : (p:positive)``0<(INR (convert p))``. +Intro; Apply INR_lt_0. +Simpl; Auto with real. +Apply compare_convert_O. Save. +Hints Resolve INR_pos : real. + +(**********) +Lemma INR_le:(n:nat)``0 <= (INR n)``. +Intro n; Case n. +Simpl; Auto with real. +Auto with arith real. +Save. +Hints Resolve INR_le: real. (*********) -Lemma INR_le_nm:(n,m:nat)(le n m)->(Rle (INR n) (INR m)). -Intros;Elim (le_lt_or_eq n m H);Intro. -Cut (lt (0) (minus m n)). -Intro;Generalize (INR_lt_0 (minus m n) H1); - Intro;Rewrite minus_INR in H2;Auto; - Apply (Rlt_le (INR n) (INR m));Fold (Rgt (INR m) (INR n)); - Apply (minus_Rgt (INR m) (INR n));Unfold Rgt;Assumption. -Omega. -Rewrite H0;Unfold Rle;Right;Trivial. +Lemma INR_le_nm:(n,m:nat)(le n m)->``(INR n)<=(INR m)``. +Induction 1; Intros; Auto with real. +Rewrite S_INR. +Apply Rle_trans with (INR m0); Auto with real. Save. +Hints Resolve INR_le_nm: real. (**********) -Lemma not_INR_O:(n:nat)~(INR n)==R0->~n=O. -Intros;Cut n=(0)->(INR n)==R0. -Tauto. -Intro;Rewrite H0;Auto with zarith real. +Lemma not_INR_O:(n:nat)``(INR n)<>0``->~n=O. +Red; Intros n H H1. +Apply H. +Rewrite H1; Trivial. Save. +Hints Immediate not_INR_O : real. + (**********) -Lemma not_O_INR:(n:nat)~n=O->~(INR n)==R0. -Intros;Cut (INR n)==R0->n=O. -Tauto. -Elim n;Intros;Auto with zarith real. -Rewrite (S_INR n0) in H1;Generalize (Rplus_Ropp (INR n0) R1 H1);Intro; - Generalize (tech_Rplus (INR n0) R1 (INR_le n0) Rlt_R0_R1);Intro; - ElimType False;Auto with zarith real. -Save. +Lemma not_O_INR:(n:nat)~n=O->``(INR n)<>0``. +Intro n; Case n. +Intro; Absurd (0)=(0); Trivial. +Intros; Rewrite S_INR. +Apply Rgt_not_eq; Red; Auto with real. +Save. +Hints Resolve not_O_INR : real. + + (**********************************************************) -(* Injection from Z to R *) +(*s Injection from Z to R *) (**********************************************************) (**********) @@ -1130,121 +1154,71 @@ Save. (**********) Lemma INR_IZR_INZ:(n:nat)(INR n)==(IZR (INZ n)). -Induction n;Auto with zarith real. -Intros;Rewrite S_INR;Simpl;Rewrite bij1;Rewrite <-S_INR;Auto with zarith real. -Save. - -(**********) -Lemma plus_IZR:(z,t:Z)(IZR (Zplus z t))==(Rplus (IZR z) (IZR t)). -Destruct z; - [Simpl;Intro; Elim (Rplus_ne (IZR t)); Intros a b; Rewrite b; Auto with zarith real| - Destruct t|Destruct t]. -Simpl;Elim (Rplus_ne (INR (convert p))); Intros a b; Rewrite a; Auto with zarith real. -Simpl;Intro;Rewrite <- (plus_INR (convert p) (convert p0)); - Rewrite (convert_add p p0);Trivial with zarith real. -Unfold Zplus;Intro;Simpl; - Generalize (refl_equal relation (compare p p0 EGAL)); - Pattern 2 3 (compare p p0 EGAL);Case (compare p p0 EGAL);Intro. -Rewrite (compare_convert_EGAL p p0 H); - Rewrite (Rplus_Ropp_r (INR (convert p0)));Auto with zarith real. -Simpl;Rewrite (true_sub_convert p0 p (ZC2 p p0 H)); - Rewrite (minus_INR (convert p0) (convert p) - (lt_le_weak (convert p) (convert p0) - (compare_convert_INFERIEUR p p0 H))); - Rewrite (Ropp_distr2 (INR (convert p0)) (INR (convert p))); - Unfold Rminus;Trivial with zarith real. -Simpl;Rewrite (true_sub_convert p p0 H); - Rewrite (minus_INR (convert p) (convert p0));[Unfold Rminus;Trivial with zarith real| - Generalize (compare_convert_SUPERIEUR p p0 H);Intro;Unfold gt in H0; - Apply (lt_le_weak (convert p0) (convert p) H0)]. -Simpl;Elim (Rplus_ne (Ropp (INR (convert p)))); Intros a b; - Rewrite a; Auto with zarith real. -Intro;Rewrite (Zplus_sym (NEG p) (POS p0)); - Rewrite (Rplus_sym (IZR (NEG p)) (IZR (POS p0))); - Unfold Zplus;Simpl; - Generalize (refl_equal relation (compare p0 p EGAL)); - Pattern 2 3 (compare p0 p EGAL);Case (compare p0 p EGAL);Intro. -Rewrite (compare_convert_EGAL p0 p H); - Rewrite (Rplus_Ropp_r (INR (convert p)));Auto with zarith real. -Simpl;Rewrite (true_sub_convert p p0 (ZC2 p0 p H)); - Rewrite (minus_INR (convert p) (convert p0) - (lt_le_weak (convert p0) (convert p) - (compare_convert_INFERIEUR p0 p H))); - Rewrite (Ropp_distr2 (INR (convert p)) (INR (convert p0))); - Unfold Rminus;Trivial with zarith real. -Simpl;Rewrite (true_sub_convert p0 p H); - Rewrite (minus_INR (convert p0) (convert p));[Unfold Rminus;Trivial with zarith real| - Generalize (compare_convert_SUPERIEUR p0 p H);Intro;Unfold gt in H0; - Apply (lt_le_weak (convert p) (convert p0) H0)]. -Simpl;Intro; - Rewrite <-(Ropp_distr1 (INR (convert p)) (INR (convert p0))); - Rewrite <- (plus_INR (convert p) (convert p0)); - Rewrite (convert_add p p0);Trivial with zarith real. -Save. - -(**********) -Lemma Ropp_Ropp_IZR:(z:Z)(IZR (`-z`))==(Ropp (IZR z)). -Induction z; Simpl. -Apply sym_eqT; Apply Ropp_O. -Trivial with zarith real. -Intro;Rewrite (Ropp_Ropp (INR (convert p)));Trivial with zarith real. -Save. - -(**********) -Lemma Z_R_minus:(z1,z2:Z) - (Rminus (IZR z1) (IZR z2))==(IZR (Zminus z1 z2)). -Unfold Rminus; Unfold Zminus; Intros; Apply sym_eqT; - Rewrite <-(Ropp_Ropp_IZR z2);Apply plus_IZR. +Induction n; Auto with real. +Intros; Simpl; Rewrite bij1; Auto with real. +Save. + +Lemma plus_IZR_NEG_POS : + (p,q:positive)(IZR `(POS p)+(NEG q)`)==``(IZR (POS p))+(IZR (NEG q))``. +Intros. +Case (lt_eq_lt_dec (convert p) (convert q)). +Intros [H | H]; Simpl. +Rewrite convert_compare_INFERIEUR; Simpl; Trivial. +Rewrite (true_sub_convert q p). +Rewrite minus_INR; Auto with arith; Ring. +Apply ZC2; Apply convert_compare_INFERIEUR; Trivial. +Rewrite (convert_intro p q); Trivial. +Rewrite convert_compare_EGAL; Simpl; Auto with real. +Intro H; Simpl. +Rewrite convert_compare_SUPERIEUR; Simpl; Auto with arith. +Rewrite (true_sub_convert p q). +Rewrite minus_INR; Auto with arith; Ring. +Apply ZC2; Apply convert_compare_INFERIEUR; Trivial. +Save. + +(**********) +Lemma plus_IZR:(z,t:Z)(IZR `z+t`)==``(IZR z)+(IZR t)``. +Destruct z; Destruct t; Intros; Auto with real. +Simpl; Intros; Rewrite convert_add; Auto with real. +Apply plus_IZR_NEG_POS. +Rewrite Zplus_sym; Rewrite Rplus_sym; Apply plus_IZR_NEG_POS. +Simpl; Intros; Rewrite convert_add; Rewrite plus_INR; Auto with real. +Save. + +(**********) +Lemma Ropp_Ropp_IZR:(z:Z)(IZR (`-z`))==``-(IZR z)``. +Intro z; Case z; Simpl; Auto with real. +Save. + +(**********) +Lemma Z_R_minus:(z1,z2:Z)``(IZR z1)-(IZR z2)``==(IZR `z1-z2`). +Intros; Unfold Rminus; Unfold Zminus. +Rewrite <-(Ropp_Ropp_IZR z2); Symmetry; Apply plus_IZR. Save. (**********) -Lemma lt_O_IZR:(z:Z)(Rlt R0 (IZR z))->(Zlt ZERO z). -Induction z; Simpl; Intros. -Generalize (Rlt_antirefl R0);Intro;ElimType False;Auto with zarith real. -Unfold Zlt;Simpl;Trivial with zarith real. -Absurd (Rlt R0 (Ropp (INR (convert p))));Auto with zarith real. -Apply (Rlt_antisym (Ropp (INR (convert p)))); - Apply (Rgt_RoppO (INR (convert p)));Unfold Rgt; - Cut (~(INR (convert p))==R0). -Intro;Generalize (not_INR_O (convert p) H0);Elim (convert p). -Intro;Absurd O=O;Auto with zarith real. -Intros;Rewrite (S_INR n);Apply (Rlt_r_plus_R1 (INR n) (INR_le n)). -Apply (imp_not_Req (INR (convert p)) R0); - Fold (Rgt (Ropp (INR (convert p))) R0) in H; - Generalize (Rgt_RoppO (Ropp (INR (convert p))) H);Intro; - Rewrite (Ropp_Ropp (INR (convert p))) in H0;Left;Assumption. -Save. - -(**********) -Lemma lt_IZR:(z1,z2:Z)(Rlt (IZR z1) (IZR z2))->(`z1`z=0`. -Destruct z; Auto with zarith real; - [ Simpl; Intros; ElimType False | Simpl; Intros; ElimType False ]. -Absurd (INR (convert p))==R0; Auto with zarith real. -Apply (not_O_INR (convert p));Red; Intro;Clear H;Unfold convert in H0; - Generalize H0; Elim p;Intros. -Simpl in H1;Absurd (S (positive_to_nat p0 (2)))=(0); Auto with zarith real. -Simpl in H1;Cut (2)=(plus (1) (1)); Auto with zarith real. -Intro; Rewrite H2 in H1;Rewrite (ZL2 p0 (1)) in H1;Clear H2; - Cut (positive_to_nat p0 (1))=(0);Auto with zarith real. -Simpl in H1;Absurd (1)=(0); Auto with zarith real. -Generalize (eq_Ropp (Ropp (INR (convert p))) R0 H);Intro;Clear H; - Rewrite (Ropp_Ropp (INR (convert p))) in H0;Rewrite Ropp_O in H0; - Absurd (INR (convert p))==R0; Auto with zarith real. -Apply (not_O_INR (convert p));Red; Intro;Clear H0; - Unfold convert in H;Generalize H; Elim p;Intros. -Simpl in H1;Absurd (S (positive_to_nat p0 (2)))=(0); Auto with zarith real. -Simpl in H1;Cut (2)=(plus (1) (1)); Auto with zarith real. -Intro; Rewrite H2 in H1;Rewrite (ZL2 p0 (1)) in H1;Clear H2; - Cut (positive_to_nat p0 (1))=(0);Auto with zarith real. -Simpl in H0;Absurd (1)=(0); Auto with zarith real. +Lemma lt_O_IZR:(z:Z)``0 < (IZR z)``->`0`z1`z=0`. +Destruct z; Simpl; Intros; Auto with zarith. +Case (Rlt_not_eq ``0`` (INR (convert p))); Auto with real. +Case (Rlt_not_eq ``-(INR (convert p))`` ``0`` ); Auto with real. +Apply Rgt_RoppO; Red; Auto with real. Save. (**********) @@ -1255,79 +1229,66 @@ Intros;Generalize (eq_Rminus (IZR z1) (IZR z2) H); Save. (*********) -Lemma le_O_IZR:(z:Z)(Rle R0 (IZR z))->(Zle ZERO z). -Unfold Rle;Intros;Elim H;Clear H;Intro. -Unfold Zle;Red;Intro;Apply (Zlt_le_weak `0` z (lt_O_IZR z H)); - Assumption. -Generalize (eq_IZR_R0 z (sym_eqT R R0 (IZR z) H));Intro;Omega. -Save. - -(**********) -Lemma le_IZR_R1:(z:Z)(Rle (IZR z) R1)->(Zle z `1`). -Induction z; Intros. -Omega. -Unfold Rle in H;Cut `(POS p) < 1`\/`(POS p) = 1`. -Omega. -Elim H;Intro. -Left;Apply (Zlt_O_minus_lt `1` (POS p));Apply (lt_O_IZR `1-(POS p)`); - Cut (R1==(IZR `1`));Auto with zarith real. -Intro;Rewrite H1 in H0;Clear H1;Fold (Rgt (IZR `1`) (IZR (POS p))) in H0; - Generalize (Rgt_minus (IZR `1`) (IZR (POS p)) H0);Intro; - Unfold Rgt in H1;Rewrite (Z_R_minus `1` (POS p)) in H1; - Assumption. -Right;Cut (R1==(IZR `1`));Auto with zarith real. -Intro;Rewrite H1 in H0;Clear H1 H;Apply (eq_IZR (POS p) `1` H0). -Unfold Rle in H;Cut `(NEG p) < 1`\/`(NEG p) = 1`. -Omega. -Elim H;Intro. -Left;Apply (Zlt_O_minus_lt `1` (NEG p));Apply (lt_O_IZR `1-(NEG p)`); - Cut (R1==(IZR `1`));Auto with zarith real. -Intro;Rewrite H1 in H0;Clear H1;Fold (Rgt (IZR `1`) (IZR (NEG p))) in H0; - Generalize (Rgt_minus (IZR `1`) (IZR (NEG p)) H0);Intro; - Unfold Rgt in H1;Rewrite (Z_R_minus `1` (NEG p)) in H1; - Assumption. -Right;Cut (R1==(IZR `1`));Auto with zarith real. -Intro;Rewrite H1 in H0;Clear H1 H;Apply (eq_IZR (NEG p) `1` H0). -Save. - -(**********) -Lemma IZR_ge: - (m,n:Z) `m>= n` ->(Rge (IZR m) (IZR n)). -Intros;Apply Rlt_not_ge;Red;Intro;Generalize (lt_IZR m n H0);Intro; Omega. -Save. - -(**********) -Lemma single_z_r_R1:(r:R)(z,x:Z)(Rlt r (IZR z))->(Rle (IZR z) (Rplus r R1)) - ->(Rlt r (IZR x))->(Rle (IZR x) (Rplus r R1))->z=x. -Intros;Generalize (Rlt_Ropp r (IZR x) H1);Intro; - Generalize (Rle_Ropp (IZR x) (Rplus r R1) H2);Intro;Clear H1 H2; - Unfold Rgt in H3; - Generalize (Rle_sym2 (Ropp (Rplus r R1)) (Ropp (IZR x)) H4); - Intro;Clear H4; - Generalize (sum_inequa_Rle_lt (Ropp (Rplus r R1)) (Ropp (IZR x)) - (Ropp r) r (IZR z) (Rplus r R1) H1 H3 H H0);Intro;Elim H2;Intros; - Clear H2 H H0 H3 H1;Rewrite (Rplus_sym (Ropp (IZR x)) (IZR z)) in - H4;Rewrite (Rplus_sym (Ropp (IZR x)) (IZR z)) in H5; - Fold (Rminus (IZR z) (IZR x)) in H4; - Fold (Rminus (IZR z) (IZR x)) in H5; - Rewrite <-(Rplus_assoc (Ropp r) r R1) in H5; - Rewrite (Rplus_Ropp_l r) in H5;Rewrite (Ropp_distr1 r R1) in H4; - Rewrite (Rplus_sym (Ropp r) (Ropp R1)) in H4; - Rewrite (Rplus_assoc (Ropp R1) (Ropp r) r) in H4; - Rewrite (Rplus_Ropp_l r) in H4;Elim (Rplus_ne R1);Intros a b;Rewrite b in H5; - Clear a b;Elim (Rplus_ne (Ropp R1));Intros a b;Rewrite a in H4; - Clear a b;Rewrite (Z_R_minus z x) in H4;Rewrite (Z_R_minus z x) in H5; - Cut (R1==(IZR `1`));Auto with zarith real. -Cut (Ropp R1)==(IZR `-1`);Auto with zarith real. -Intros;Rewrite H0 in H5;Rewrite H in H4;Clear H H0; - Generalize (lt_IZR `-1` `z-x` H4);Intro; - Generalize (lt_IZR `z-x` `1` H5);Intro;Clear H4 H5;Omega. -Save. - -(**********) -Lemma tech_single_z_r_R1:(r:R)(z:Z)(Rlt r (IZR z))-> - (Rle (IZR z) (Rplus r R1))-> - (Ex [s:Z] (~s=z/\(Rlt r (IZR s))/\(Rle (IZR s) (Rplus r R1))))->False. -Intros;Elim H1;Intros;Elim H2;Intros;Elim H4;Intros;Clear H1 H2 H4; - Generalize (single_z_r_R1 r z x H H0 H5 H6);Intro;Auto with zarith real. +Lemma le_O_IZR:(z:Z)``0<= (IZR z)``->`0<=z`. +Unfold Rle; Intros z [H|H]. +Red;Intro;Apply (Zlt_le_weak `0` z (lt_O_IZR z H)); Assumption. +Rewrite (eq_IZR_R0 z); Auto with zarith real. Save. + +(**********) +Lemma le_IZR:(z1,z2:Z)``(IZR z1)<=(IZR z2)``->`z1<=z2`. +Unfold Rle; Intros z1 z2 [H|H]. +Apply (Zlt_le_weak z1 z2); Auto with real. +Apply lt_IZR; Trivial. +Rewrite (eq_IZR z1 z2); Auto with zarith real. +Save. + +(**********) +Lemma le_IZR_R1:(z:Z)``(IZR z)<=1``-> `z<=1`. +Pattern 1 ``1``; Replace ``1`` with (IZR `1`); Intros; Auto. +Apply le_IZR; Trivial. +Save. + +(**********) +Lemma IZR_ge: (m,n:Z) `m>= n` -> ``(IZR m)>=(IZR n)``. +Intros;Apply Rlt_not_ge;Red;Intro. +Generalize (lt_IZR m n H0); Intro; Omega. +Save. + +Lemma one_IZR_lt1 : (z:Z)``-1<(IZR z)<1``->`z=0`. +Intros z (H1,H2). +Apply Zle_antisym. +Apply Zlt_n_Sm_le; Apply lt_IZR; Trivial. +Replace `0` with (Zs `-1`); Trivial. +Apply Zlt_le_S; Apply lt_IZR; Trivial. +Save. + +Lemma one_IZR_r_R1 + : (r:R)(z,x:Z)``r<(IZR z)<=r+1``->``r<(IZR x)<=r+1``->z=x. +Intros r z x (H1,H2) (H3,H4). +Cut `z-x=0`; Auto with zarith. +Apply one_IZR_lt1. +Rewrite <- Z_R_minus; Split. +Replace ``-1`` with ``r-(r+1)``. +Unfold Rminus; Apply Rplus_lt_le_lt; Auto with real. +Ring. +Replace ``1`` with ``(r+1)-r``. +Unfold Rminus; Apply Rplus_le_lt_lt; Auto with real. +Ring. +Save. + + +(**********) +Lemma single_z_r_R1 + : (r:R)(z,x:Z)``r<(IZR z)``->``(IZR z)<=r+1``->``r<(IZR x)``->``(IZR x)<=r+1``->z=x. +Intros; Apply one_IZR_r_R1 with r; Auto. +Save. + +(**********) +Lemma tech_single_z_r_R1 + :(r:R)(z:Z)``r<(IZR z)``->``(IZR z)<=r+1`` + -> (Ex [s:Z] (~s=z/\``r<(IZR s)``/\``(IZR s)<=r+1``))->False. +Intros r z H1 H2 (s, (H3,(H4,H5))). +Apply H3; Apply single_z_r_R1 with r; Trivial. +Save. + diff --git a/theories/Zarith/fast_integer.v b/theories/Zarith/fast_integer.v index 9b6e661fb..e77011114 100644 --- a/theories/Zarith/fast_integer.v +++ b/theories/Zarith/fast_integer.v @@ -1,12 +1,12 @@ (**************************************************************************) (* *) -(* Binary Integers *) +(*s Binary Integers *) (* *) (* Pierre Crégut (CNET, Lannion, France) *) (* *) (**************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Le. Require Lt. @@ -14,7 +14,8 @@ Require Plus. Require Mult. Require Minus. -Section fast_integer. +(*s Definition of fast binary integers *) +Section fast_integers. Inductive positive : Set := xI : positive -> positive @@ -139,6 +140,19 @@ Induction m; [ | Unfold convert; Intros n H; Simpl; Rewrite convert_add_un; Rewrite H; Auto with arith]. Save. +Theorem compare_positive_to_nat_O : + (p:positive)(m:nat)(le m (positive_to_nat p m)). +Induction p; Simpl; Auto with arith. +Intros; Apply le_trans with (plus m m); Auto with arith. +Save. + +Theorem compare_convert_O : (p:positive)(lt O (convert p)). +Intro; Unfold convert; Apply lt_le_trans with (S O); Auto with arith. +Apply compare_positive_to_nat_O. +Save. + +Hints Resolve compare_convert_O. + Fixpoint double_moins_un [x:positive]:positive := Cases x of (xI x') => (xI (xO x')) @@ -1441,5 +1455,4 @@ Intros x y;Case x;Case y; [ | Unfold Zcompare; Intros q p; Rewrite <- ZC4; Intros H; Exists (true_sub q p); Simpl; Rewrite (ZC1 q p H); Trivial with arith]. Save. - -End fast_integer. \ No newline at end of file +End fast_integers. \ No newline at end of file diff --git a/theories/Zarith/zarith_aux.v b/theories/Zarith/zarith_aux.v index 113a59347..4309d2970 100644 --- a/theories/Zarith/zarith_aux.v +++ b/theories/Zarith/zarith_aux.v @@ -11,11 +11,11 @@ Require Arith. Require Export fast_integer. -Tactic Definition ElimCompare com1 com2:= +Meta Definition ElimCompare com1 com2:= Elim (Dcompare (Zcompare com1 com2)); [ Idtac | Intro hidden_auxiliary; Elim hidden_auxiliary; - Clear hidden_auxiliary ]. + Clear hidden_auxiliary ] . Definition Zlt := [x,y:Z](Zcompare x y) = INFERIEUR. Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR. -- cgit v1.2.3