diff options
| author | herbelin | 2002-04-17 11:30:23 +0000 |
|---|---|---|
| committer | herbelin | 2002-04-17 11:30:23 +0000 |
| commit | cc1be0bf512b421336e81099aa6906ca47e4257a (patch) | |
| tree | c25fa8ed965729d7a85efa3b3292fdf7f442963d /theories/Reals | |
| parent | ebf9aa9f97ef0d49ed1b799c9213f78efad4fec7 (diff) | |
Uniformisation (Qed/Save et Implicits Arguments)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/R_Ifp.v | 34 | ||||
| -rw-r--r-- | theories/Reals/R_sqr.v | 114 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis.v | 170 | ||||
| -rw-r--r-- | theories/Reals/Rbase.v | 424 | ||||
| -rw-r--r-- | theories/Reals/Rbasic_fun.v | 68 | ||||
| -rw-r--r-- | theories/Reals/Rderiv.v | 22 | ||||
| -rw-r--r-- | theories/Reals/Rfunctions.v | 66 | ||||
| -rw-r--r-- | theories/Reals/Rgeom.v | 24 | ||||
| -rw-r--r-- | theories/Reals/Rlimit.v | 58 | ||||
| -rw-r--r-- | theories/Reals/Rseries.v | 16 | ||||
| -rw-r--r-- | theories/Reals/Rsigma.v | 14 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo.v | 268 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_fun.v | 2 |
13 files changed, 640 insertions, 640 deletions
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 1f6abb175c..2152188b6e 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -37,7 +37,7 @@ Generalize (Rle_compatibility r (Rplus (IZR (up r)) Rewrite <-(Rplus_assoc r (Ropp r) (IZR (up r))) in H1; Rewrite (Rplus_Ropp_r r) in H1;Elim (Rplus_ne (IZR (up r)));Intros a b; Rewrite b in H1;Clear a b;Apply (single_z_r_R1 r z (up r));Auto with zarith real. -Save. +Qed. (**********) Lemma up_tech:(r:R)(z:Z)(Rle (IZR z) r)->(Rlt r (IZR `z+1`))-> @@ -47,7 +47,7 @@ Intros;Generalize (Rle_compatibility R1 (IZR z) r H);Intro;Clear H; Cut (R1==(IZR `1`));Auto with zarith real. Intro;Generalize H1;Pattern 1 R1;Rewrite H;Intro;Clear H H1; Rewrite <-(plus_IZR z `1`) in H2;Apply (tech_up r `z+1`);Auto with zarith real. -Save. +Qed. (**********) Lemma fp_R0:(frac_part R0)==R0. @@ -62,7 +62,7 @@ Elim (archimed R0);Intros;Clear H2;Unfold Rgt in H1; Rewrite (minus_R0 (IZR (up R0))) in H0; Generalize (lt_O_IZR (up R0) H1);Intro;Clear H1; Generalize (le_IZR_R1 (up R0) H0);Intro;Clear H H0;Omega. -Save. +Qed. (**********) Lemma for_base_fp:(r:R)(Rgt (Rminus (IZR (up r)) r) R0)/\ @@ -75,7 +75,7 @@ Apply archimed. Intro; Elim H; Intros. Exact H1. Apply archimed. -Save. +Qed. (**********) Lemma base_fp:(r:R)(Rge (frac_part r) R0)/\(Rlt (frac_part r) R1). @@ -98,7 +98,7 @@ Rewrite <- Z_R_minus; Simpl;Intro; Unfold Rminus; Apply Rlt_compatibility;Auto with zarith real. Elim (for_base_fp r);Intros;Rewrite <-Ropp_O; Rewrite<-Ropp_distr2;Apply Rgt_Ropp;Auto with zarith real. -Save. +Qed. (*********************************************************) (** Properties *) @@ -129,7 +129,7 @@ Generalize (Rgt_plus_plus_r (Ropp R1) (IZR (up r)) r H);Intro; Rewrite (Rplus_assoc (Ropp R1) r (Ropp r)) in H2; Rewrite (Rplus_Ropp_r r) in H2;Elim (Rplus_ne (Ropp R1));Intros a b; Rewrite a in H2;Clear a b;Auto with zarith real. -Save. +Qed. (**********) Lemma Int_part_INR:(n : nat) (Int_part (INR n)) = (inject_nat n). @@ -143,17 +143,17 @@ Apply lt_INR; Auto. Rewrite Zplus_sym; Rewrite <- inj_plus; Simpl; Auto. Rewrite plus_IZR; Simpl; Auto with real. Repeat Rewrite <- INR_IZR_INZ; Auto with real. -Save. +Qed. (**********) Lemma fp_nat:(r:R)(frac_part r)==R0->(Ex [c:Z](r==(IZR c))). Unfold frac_part;Intros;Split with (Int_part r);Apply Rminus_eq; Auto with zarith real. -Save. +Qed. (**********) Lemma R0_fp_O:(r:R)~R0==(frac_part r)->~R0==r. Red;Intros;Rewrite <- H0 in H;Generalize fp_R0;Intro;Auto with zarith real. -Save. +Qed. (**********) Lemma Rminus_Int_part1:(r1,r2:R)(Rge (frac_part r1) (frac_part r2))-> @@ -236,7 +236,7 @@ Intro;Rewrite H1 in H;Clear H1; Rewrite <-(plus_IZR `(Int_part r1)-(Int_part r2)` `1`) in H; Generalize (up_tech (Rminus r1 r2) `(Int_part r1)-(Int_part r2)` H0 H);Intros;Clear H H0;Unfold 1 Int_part;Omega. -Save. +Qed. (**********) Lemma Rminus_Int_part2:(r1,r2:R)(Rlt (frac_part r1) (frac_part r2))-> @@ -325,7 +325,7 @@ Intro;Rewrite H1 in H;Rewrite H1 in H0;Clear H1; Intro;Clear H; Generalize (up_tech (Rminus r1 r2) `(Int_part r1)-(Int_part r2)-1` H1 H0);Intros;Clear H0 H1;Unfold 1 Int_part;Omega. -Save. +Qed. (**********) Lemma Rminus_fp1:(r1,r2:R)(Rge (frac_part r1) (frac_part r2))-> @@ -345,7 +345,7 @@ Intros;Unfold frac_part; Rewrite <- (Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2) (IZR (Int_part r2))); Rewrite -> (Rplus_sym (Ropp r2) (Ropp (IZR (Int_part r1))));Auto with zarith real. -Save. +Qed. (**********) Lemma Rminus_fp2:(r1,r2:R)(Rlt (frac_part r1) (frac_part r2))-> @@ -373,7 +373,7 @@ Intros;Unfold frac_part;Generalize (Rminus_Int_part2 r1 r2 H);Intro; Rewrite <- (Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2) (IZR (Int_part r2))); Rewrite -> (Rplus_sym (Ropp r2) (Ropp (IZR (Int_part r1))));Auto with zarith real. -Save. +Qed. (**********) Lemma plus_Int_part1:(r1,r2:R)(Rge (Rplus (frac_part r1) (frac_part r2)) R1)-> @@ -439,7 +439,7 @@ Intro;Rewrite H1 in H0;Rewrite H1 in H;Clear H1; Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)+1` `1`) in H0; Generalize (up_tech (Rplus r1 r2) `(Int_part r1)+(Int_part r2)+1` H H0);Intro; Clear H H0;Unfold 1 Int_part;Omega. -Save. +Qed. (**********) Lemma plus_Int_part2:(r1,r2:R)(Rlt (Rplus (frac_part r1) (frac_part r2)) R1)-> @@ -500,7 +500,7 @@ Intro;Rewrite H in H1;Clear H; Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)` `1`) in H1; Generalize (up_tech (Rplus r1 r2) `(Int_part r1)+(Int_part r2)` H0 H1);Intro; Clear H0 H1;Unfold 1 Int_part;Omega. -Save. +Qed. (**********) Lemma plus_frac_part1:(r1,r2:R) @@ -527,7 +527,7 @@ Intros;Unfold frac_part; (Ropp R1)); Rewrite <-(Ropp_distr1 (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) R1); Trivial with zarith real. -Save. +Qed. (**********) Lemma plus_frac_part2:(r1,r2:R) @@ -547,4 +547,4 @@ Intros;Unfold frac_part; (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))); Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2)));Unfold Rminus; Trivial with zarith real. -Save. +Qed. diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 78a29437c8..7af4dd5f67 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -21,35 +21,35 @@ Tactic Definition SqRing := Unfold Rsqr; Ring. Lemma Rsqr_neg : (x:R) ``(Rsqr x)==(Rsqr (-x))``. Intros; SqRing. -Save. +Qed. Lemma Rsqr_times : (x,y:R) ``(Rsqr (x*y))==(Rsqr x)*(Rsqr y)``. Intros; SqRing. -Save. +Qed. Lemma Rsqr_plus : (x,y:R) ``(Rsqr (x+y))==(Rsqr x)+(Rsqr y)+2*x*y``. Intros; SqRing. -Save. +Qed. Lemma Rsqr_minus : (x,y:R) ``(Rsqr (x-y))==(Rsqr x)+(Rsqr y)-2*x*y``. Intros; SqRing. -Save. +Qed. Lemma Rsqr_neg_minus : (x,y:R) ``(Rsqr (x-y))==(Rsqr (y-x))``. Intros; SqRing. -Save. +Qed. Lemma Rsqr_1 : ``(Rsqr 1)==1``. SqRing. -Save. +Qed. Lemma Rsqr_gt_0_0 : (x:R) ``0<(Rsqr x)`` -> ~``x==0``. Intros; Red; Intro; Rewrite H0 in H; Rewrite Rsqr_O in H; Elim (Rlt_antirefl ``0`` H). -Save. +Qed. Lemma Rsqr_pos_lt : (x:R) ~(x==R0)->``0<(Rsqr x)``. Intros; Case (total_order R0 x); Intro; [Unfold Rsqr; Apply Rmult_lt_pos; Assumption | Elim H0; Intro; [Elim H; Symmetry; Exact H1 | Rewrite Rsqr_neg; Generalize (Rlt_Ropp x ``0`` H1); Rewrite Ropp_O; Intro; Unfold Rsqr; Apply Rmult_lt_pos; Assumption]]. -Save. +Qed. Lemma Rsqr_div : (x,y:R) ~``y==0`` -> ``(Rsqr (x/y))==(Rsqr x)/(Rsqr y)``. Intros; Unfold Rsqr. @@ -63,81 +63,81 @@ Apply Rmult_mult_r. Reflexivity. Assumption. Assumption. -Save. +Qed. Lemma Rsqr_eq_0 : (x:R) ``(Rsqr x)==0`` -> ``x==0``. Unfold Rsqr; Intros; Generalize (without_div_Od x x H); Intro; Elim H0; Intro ; Assumption. -Save. +Qed. Lemma Rsqr_minus_plus : (a,b:R) ``(a-b)*(a+b)==(Rsqr a)-(Rsqr b)``. Intros; SqRing. -Save. +Qed. Lemma Rsqr_plus_minus : (a,b:R) ``(a+b)*(a-b)==(Rsqr a)-(Rsqr b)``. Intros; SqRing. -Save. +Qed. Lemma Rsqr_incr_0 : (x,y:R) ``(Rsqr x)<=(Rsqr y)`` -> ``0<=x`` -> ``0<=y`` -> ``x<=y``. Intros; Case (total_order_Rle x y); Intro; [Assumption | Cut ``y<x``; [Intro; Unfold Rsqr in H; Generalize (Rmult_lt2 y x y x H1 H1 H2 H2); Intro; Generalize (Rle_lt_trans ``x*x`` ``y*y`` ``x*x`` H H3); Intro; Elim (Rlt_antirefl ``x*x`` H4) | Auto with real]]. -Save. +Qed. Lemma Rsqr_incr_0_var : (x,y:R) ``(Rsqr x)<=(Rsqr y)`` -> ``0<=y`` -> ``x<=y``. Intros; Case (total_order_Rle x y); Intro; [Assumption | Cut ``y<x``; [Intro; Unfold Rsqr in H; Generalize (Rmult_lt2 y x y x H0 H0 H1 H1); Intro; Generalize (Rle_lt_trans ``x*x`` ``y*y`` ``x*x`` H H2); Intro; Elim (Rlt_antirefl ``x*x`` H3) | Auto with real]]. -Save. +Qed. Lemma Rsqr_incr_1 : (x,y:R) ``x<=y``->``0<=x``->``0<= y``->``(Rsqr x)<=(Rsqr y)``. Intros; Unfold Rsqr; Apply Rle_Rmult_comp; Assumption. -Save. +Qed. Lemma Rsqr_incrst_0 : (x,y:R) ``(Rsqr x)<(Rsqr y)``->``0<=x``->``0<=y``-> ``x<y``. Intros; Case (total_order x y); Intro; [Assumption | Elim H2; Intro; [Rewrite H3 in H; Elim (Rlt_antirefl (Rsqr y) H) | Generalize (Rmult_lt2 y x y x H1 H1 H3 H3); Intro; Unfold Rsqr in H; Generalize (Rlt_trans ``x*x`` ``y*y`` ``x*x`` H H4); Intro; Elim (Rlt_antirefl ``x*x`` H5)]]. -Save. +Qed. Lemma Rsqr_incrst_1 : (x,y:R) ``x<y``->``0<=x``->``0<=y``->``(Rsqr x)<(Rsqr y)``. Intros; Unfold Rsqr; Apply Rmult_lt2; Assumption. -Save. +Qed. Lemma Rsqr_neg_pos_le_0 : (x,y:R) ``(Rsqr x)<=(Rsqr y)``->``0<=y``->``-y<=x``. Intros; Case (case_Rabsolu x); Intro. Generalize (Rlt_Ropp x ``0`` r); Rewrite Ropp_O; Intro; Generalize (Rlt_le ``0`` ``-x`` H1); Intro; Rewrite (Rsqr_neg x) in H; Generalize (Rsqr_incr_0 (Ropp x) y H H2 H0); Intro; Rewrite <- (Ropp_Ropp x); Apply Rge_Ropp; Apply Rle_sym1; Assumption. Apply Rle_trans with ``0``; [Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Assumption | Apply Rle_sym2; Assumption]. -Save. +Qed. Lemma Rsqr_neg_pos_le_1 : (x,y:R) ``(-y)<=x`` -> ``x<=y`` -> ``0<=y`` -> ``(Rsqr x)<=(Rsqr y)``. Intros; Case (case_Rabsolu x); Intro. Generalize (Rlt_Ropp x ``0`` r); Rewrite Ropp_O; Intro; Generalize (Rlt_le ``0`` ``-x`` H2); Intro; Generalize (Rle_Ropp ``-y`` x H); Rewrite Ropp_Ropp; Intro; Generalize (Rle_sym2 ``-x`` y H4); Intro; Rewrite (Rsqr_neg x); Apply Rsqr_incr_1; Assumption. Generalize (Rle_sym2 ``0`` x r); Intro; Apply Rsqr_incr_1; Assumption. -Save. +Qed. Lemma neg_pos_Rsqr_le : (x,y:R) ``(-y)<=x``->``x<=y``->``(Rsqr x)<=(Rsqr y)``. Intros; Case (case_Rabsolu x); Intro. Generalize (Rlt_Ropp x ``0`` r); Rewrite Ropp_O; Intro; Generalize (Rle_Ropp ``-y`` x H); Rewrite Ropp_Ropp; Intro; Generalize (Rle_sym2 ``-x`` y H2); Intro; Generalize (Rlt_le ``0`` ``-x`` H1); Intro; Generalize (Rle_trans ``0`` ``-x`` y H4 H3); Intro; Rewrite (Rsqr_neg x); Apply Rsqr_incr_1; Assumption. Generalize (Rle_sym2 ``0`` x r); Intro; Generalize (Rle_trans ``0`` x y H1 H0); Intro; Apply Rsqr_incr_1; Assumption. -Save. +Qed. Lemma Rsqr_abs : (x:R) ``(Rsqr x)==(Rsqr (Rabsolu x))``. Intro; Unfold Rabsolu; Case (case_Rabsolu x); Intro; [Apply Rsqr_neg | Reflexivity]. -Save. +Qed. Lemma Rsqr_le_abs_0 : (x,y:R) ``(Rsqr x)<=(Rsqr y)`` -> ``(Rabsolu x)<=(Rabsolu y)``. Intros; Apply Rsqr_incr_0; Repeat Rewrite <- Rsqr_abs; [Assumption | Apply Rabsolu_pos | Apply Rabsolu_pos]. -Save. +Qed. Lemma Rsqr_le_abs_1 : (x,y:R) ``(Rabsolu x)<=(Rabsolu y)`` -> ``(Rsqr x)<=(Rsqr y)``. Intros; Rewrite (Rsqr_abs x); Rewrite (Rsqr_abs y); Apply (Rsqr_incr_1 (Rabsolu x) (Rabsolu y) H (Rabsolu_pos x) (Rabsolu_pos y)). -Save. +Qed. Lemma Rsqr_lt_abs_0 : (x,y:R) ``(Rsqr x)<(Rsqr y)`` -> ``(Rabsolu x)<(Rabsolu y)``. Intros; Apply Rsqr_incrst_0; Repeat Rewrite <- Rsqr_abs; [Assumption | Apply Rabsolu_pos | Apply Rabsolu_pos]. -Save. +Qed. Lemma Rsqr_lt_abs_1 : (x,y:R) ``(Rabsolu x)<(Rabsolu y)`` -> ``(Rsqr x)<(Rsqr y)``. Intros; Rewrite (Rsqr_abs x); Rewrite (Rsqr_abs y); Apply (Rsqr_incrst_1 (Rabsolu x) (Rabsolu y) H (Rabsolu_pos x) (Rabsolu_pos y)). -Save. +Qed. Lemma Rsqr_inj : (x,y:R) ``0<=x`` -> ``0<=y`` -> (Rsqr x)==(Rsqr y) -> x==y. Intros; Generalize (Rle_le_eq (Rsqr x) (Rsqr y)); Intro; Elim H2; Intros _ H3; Generalize (H3 H1); Intro; Elim H4; Intros; Apply Rle_antisym; Apply Rsqr_incr_0; Assumption. -Save. +Qed. Lemma Rsqr_eq_abs_0 : (x,y:R) (Rsqr x)==(Rsqr y) -> (Rabsolu x)==(Rabsolu y). Intros; Unfold Rabsolu; Case (case_Rabsolu x); Case (case_Rabsolu y); Intros. @@ -145,25 +145,25 @@ Rewrite -> (Rsqr_neg x) in H; Rewrite -> (Rsqr_neg y) in H; Generalize (Rlt_Ropp Rewrite -> (Rsqr_neg x) in H; Generalize (Rle_sym2 ``0`` y r); Intro; Generalize (Rlt_Ropp x ``0`` r0); Rewrite Ropp_O; Intro; Generalize (Rlt_le ``0`` ``-x`` H1); Intro; Apply Rsqr_inj; Assumption. Rewrite -> (Rsqr_neg y) in H; Generalize (Rle_sym2 ``0`` x r0); Intro; Generalize (Rlt_Ropp y ``0`` r); Rewrite Ropp_O; Intro; Generalize (Rlt_le ``0`` ``-y`` H1); Intro; Apply Rsqr_inj; Assumption. Generalize (Rle_sym2 ``0`` x r0); Generalize (Rle_sym2 ``0`` y r); Intros; Apply Rsqr_inj; Assumption. -Save. +Qed. Lemma Rsqr_eq_asb_1 : (x,y:R) (Rabsolu x)==(Rabsolu y) -> (Rsqr x)==(Rsqr y). Intros; Cut ``(Rsqr (Rabsolu x))==(Rsqr (Rabsolu y))``. Intro; Repeat Rewrite <- Rsqr_abs in H0; Assumption. Rewrite H; Reflexivity. -Save. +Qed. Lemma triangle_rectangle : (x,y,z:R) ``0<=z``->``(Rsqr x)+(Rsqr y)<=(Rsqr z)``->``-z<=x<=z`` /\``-z<=y<=z``. Intros; Generalize (plus_le_is_le (Rsqr x) (Rsqr y) (Rsqr z) (pos_Rsqr y) H0); Rewrite Rplus_sym in H0; Generalize (plus_le_is_le (Rsqr y) (Rsqr x) (Rsqr z) (pos_Rsqr x) H0); Intros; Split; [Split; [Apply Rsqr_neg_pos_le_0; Assumption | Apply Rsqr_incr_0_var; Assumption] | Split; [Apply Rsqr_neg_pos_le_0; Assumption | Apply Rsqr_incr_0_var; Assumption]]. -Save. +Qed. Lemma triangle_rectangle_lt : (x,y,z:R) ``(Rsqr x)+(Rsqr y)<(Rsqr z)`` -> ``(Rabsolu x)<(Rabsolu z)``/\``(Rabsolu y)<(Rabsolu z)``. Intros; Split; [Generalize (plus_lt_is_lt (Rsqr x) (Rsqr y) (Rsqr z) (pos_Rsqr y) H); Intro; Apply Rsqr_lt_abs_0; Assumption | Rewrite Rplus_sym in H; Generalize (plus_lt_is_lt (Rsqr y) (Rsqr x) (Rsqr z) (pos_Rsqr x) H); Intro; Apply Rsqr_lt_abs_0; Assumption]. -Save. +Qed. Lemma triangle_rectangle_le : (x,y,z:R) ``(Rsqr x)+(Rsqr y)<=(Rsqr z)`` -> ``(Rabsolu x)<=(Rabsolu z)``/\``(Rabsolu y)<=(Rabsolu z)``. Intros; Split; [Generalize (plus_le_is_le (Rsqr x) (Rsqr y) (Rsqr z) (pos_Rsqr y) H); Intro; Apply Rsqr_le_abs_0; Assumption | Rewrite Rplus_sym in H; Generalize (plus_le_is_le (Rsqr y) (Rsqr x) (Rsqr z) (pos_Rsqr x) H); Intro; Apply Rsqr_le_abs_0; Assumption]. -Save. +Qed. (*********************************************************************) @@ -178,91 +178,91 @@ Axiom bar : (x:R) ``0<=x`` -> ``(sqrt x)*(sqrt x)==x``. Lemma sqrt_0 : ``(sqrt 0)==0``. Apply Rsqr_eq_0; Unfold Rsqr; Apply bar; Right; Reflexivity. -Save. +Qed. Lemma sqrt_1 : ``(sqrt 1)==1``. Apply (Rsqr_inj (sqrt R1) R1); [Apply foo; Left | Left | Unfold Rsqr; Rewrite -> bar; [Ring | Left]]; Apply Rlt_R0_R1. -Save. +Qed. Lemma sqrt_eq_0 : (x:R) ``0<=x``->``(sqrt x)==0``->``x==0``. Intros; Cut ``(Rsqr (sqrt x))==0``. Intro; Unfold Rsqr in H1; Rewrite -> bar in H1; Assumption. Rewrite H0; Apply Rsqr_O. -Save. +Qed. Lemma sqrt_lem_0 : (x,y:R) ``0<=x``->``0<=y``->(sqrt x)==y->``y*y==x``. Intros; Rewrite <- H1; Apply (bar x H). -Save. +Qed. Lemma sqtr_lem_1 : (x,y:R) ``0<=x``->``0<=y``->``y*y==x``->(sqrt x)==y. Intros; Apply Rsqr_inj; [Apply (foo x H) | Assumption | Unfold Rsqr; Rewrite -> H1; Apply (bar x H)]. -Save. +Qed. Lemma sqrt_def : (x:R) ``0<=x``->``(sqrt x)*(sqrt x)==x``. Intros; Apply (bar x H). -Save. +Qed. Lemma sqrt_square : (x:R) ``0<=x``->``(sqrt (x*x))==x``. Intros; Apply (Rsqr_inj (sqrt (Rsqr x)) x (foo (Rsqr x) (pos_Rsqr x)) H); Unfold Rsqr; Apply (bar (Rsqr x) (pos_Rsqr x)). -Save. +Qed. Lemma sqrt_Rsqr : (x:R) ``0<=x``->``(sqrt (Rsqr x))==x``. Intros; Unfold Rsqr; Apply sqrt_square; Assumption. -Save. +Qed. Lemma sqrt_Rsqr_abs : (x:R) (sqrt (Rsqr x))==(Rabsolu x). Intro x; Rewrite -> Rsqr_abs; Apply sqrt_Rsqr; Apply Rabsolu_pos. -Save. +Qed. Lemma Rsqr_sqrt : (x:R) ``0<=x``->(Rsqr (sqrt x))==x. Intros x H1; Unfold Rsqr; Apply (bar x H1). -Save. +Qed. Lemma sqrt_times : (x,y:R) ``0<=x``->``0<=y``->``(sqrt (x*y))==(sqrt x)*(sqrt y)``. Intros x y H1 H2; Apply (Rsqr_inj (sqrt (Rmult x y)) (Rmult (sqrt x) (sqrt y)) (foo (Rmult x y) (Rmult_le_pos x y H1 H2)) (Rmult_le_pos (sqrt x) (sqrt y) (foo x H1) (foo y H2))); Rewrite Rsqr_times; Repeat Rewrite Rsqr_sqrt; [Ring | Assumption |Assumption | Apply (Rmult_le_pos x y H1 H2)]. -Save. +Qed. Lemma sqrt_lt_R0 : (x:R) ``0<x`` -> ``0<(sqrt x)``. Intros x H1; Apply Rsqr_incrst_0; [Rewrite Rsqr_O; Rewrite Rsqr_sqrt ; [Assumption | Left; Assumption] | Right; Reflexivity | Apply (foo x (Rlt_le R0 x H1))]. -Save. +Qed. Lemma sqrt_div : (x,y:R) ``0<=x``->``0<y``->``(sqrt (x/y))==(sqrt x)/(sqrt y)``. Intros x y H1 H2; Apply Rsqr_inj; [ Apply foo; Apply (Rmult_le_pos x (Rinv y)); [ Assumption | Generalize (Rlt_Rinv y H2); Clear H2; Intro H2; Left; Assumption] | Apply (Rmult_le_pos (sqrt x) (Rinv (sqrt y))) ; [ Apply (foo x H1) | Generalize (sqrt_lt_R0 y H2); Clear H2; Intro H2; Generalize (Rlt_Rinv (sqrt y) H2); Clear H2; Intro H2; Left; Assumption] | Rewrite Rsqr_div; Repeat Rewrite Rsqr_sqrt; [ Reflexivity | Left; Assumption | Assumption | Generalize (Rlt_Rinv y H2); Intro H3; Generalize (Rlt_le R0 (Rinv y) H3); Intro H4; Apply (Rmult_le_pos x (Rinv y) H1 H4) |Red; Intro H3; Generalize (Rlt_le R0 y H2); Intro H4; Generalize (sqrt_eq_0 y H4 H3); Intro H5; Rewrite H5 in H2; Elim (Rlt_antirefl R0 H2)]]. -Save. +Qed. Lemma sqrt_lt_0 : (x,y:R) ``0<=x``->``0<=y``->``(sqrt x)<(sqrt y)``->``x<y``. Intros x y H1 H2 H3; Generalize (Rsqr_incrst_1 (sqrt x) (sqrt y) H3 (foo x H1) (foo y H2)); Intro H4; Rewrite (Rsqr_sqrt x H1) in H4; Rewrite (Rsqr_sqrt y H2) in H4; Assumption. -Save. +Qed. Lemma sqrt_lt_1 : (x,y:R) ``0<=x``->``0<=y``->``x<y``->``(sqrt x)<(sqrt y)``. Intros x y H1 H2 H3; Apply Rsqr_incrst_0; [Rewrite (Rsqr_sqrt x H1); Rewrite (Rsqr_sqrt y H2); Assumption | Apply (foo x H1) | Apply (foo y H2)]. -Save. +Qed. Lemma sqrt_le_0 : (x,y:R) ``0<=x``->``0<=y``->``(sqrt x)<=(sqrt y)``->``x<=y``. Intros x y H1 H2 H3; Generalize (Rsqr_incr_1 (sqrt x) (sqrt y) H3 (foo x H1) (foo y H2)); Intro H4; Rewrite (Rsqr_sqrt x H1) in H4; Rewrite (Rsqr_sqrt y H2) in H4; Assumption. -Save. +Qed. Lemma sqrt_le_1 : (x,y:R) ``0<=x``->``0<=y``->``x<=y``->``(sqrt x)<=(sqrt y)``. Intros x y H1 H2 H3; Apply Rsqr_incr_0; [ Rewrite (Rsqr_sqrt x H1); Rewrite (Rsqr_sqrt y H2); Assumption | Apply (foo x H1) | Apply (foo y H2)]. -Save. +Qed. Lemma sqrt_inj : (x,y:R) ``0<=x``->``0<=y``->(sqrt x)==(sqrt y)->x==y. Intros; Cut ``(Rsqr (sqrt x))==(Rsqr (sqrt y))``. Intro; Rewrite (Rsqr_sqrt x H) in H2; Rewrite (Rsqr_sqrt y H0) in H2; Assumption. Rewrite H1; Reflexivity. -Save. +Qed. Lemma sqrt_less : (x:R) ``0<=x``->``1<x``->``(sqrt x)<x``. Intros x H1 H2; Generalize (sqrt_lt_1 R1 x (Rlt_le R0 R1 (Rlt_R0_R1)) H1 H2); Intro H3; Rewrite sqrt_1 in H3; Generalize (Rmult_ne (sqrt x)); Intro H4; Elim H4; Intros H5 H6; Rewrite <- H5; Pattern 2 x; Rewrite <- (sqrt_def x H1); Apply (Rlt_monotony (sqrt x) R1 (sqrt x) (sqrt_lt_R0 x (Rlt_trans R0 R1 x Rlt_R0_R1 H2)) H3). -Save. +Qed. Lemma sqrt_more : (x:R) ``0<x``->``x<1``->``x<(sqrt x)``. Intros x H1 H2; Generalize (sqrt_lt_1 x R1 (Rlt_le R0 x H1) (Rlt_le R0 R1 (Rlt_R0_R1)) H2); Intro H3; Rewrite sqrt_1 in H3; Generalize (Rmult_ne (sqrt x)); Intro H4; Elim H4; Intros H5 H6; Rewrite <- H5; Pattern 1 x; Rewrite <- (sqrt_def x (Rlt_le R0 x H1)); Apply (Rlt_monotony (sqrt x) (sqrt x) R1 (sqrt_lt_R0 x H1) H3). -Save. +Qed. Lemma sqrt_cauchy : (a,b,c,d:R) ``a*c+b*d<=(sqrt ((Rsqr a)+(Rsqr b)))*(sqrt ((Rsqr c)+(Rsqr d)))``. Intros a b c d; Apply Rsqr_incr_0_var; [Rewrite Rsqr_times; Repeat Rewrite Rsqr_sqrt; Unfold Rsqr; [Replace ``(a*c+b*d)*(a*c+b*d)`` with ``(a*a*c*c+b*b*d*d)+(2*a*b*c*d)``; [Replace ``(a*a+b*b)*(c*c+d*d)`` with ``(a*a*c*c+b*b*d*d)+(a*a*d*d+b*b*c*c)``; [Apply Rle_compatibility; Replace ``a*a*d*d+b*b*c*c`` with ``(2*a*b*c*d)+(a*a*d*d+b*b*c*c-2*a*b*c*d)``; [Pattern 1 ``2*a*b*c*d``; Rewrite <- Rplus_Or; Apply Rle_compatibility; Replace ``a*a*d*d+b*b*c*c-2*a*b*c*d`` with (Rsqr (Rminus (Rmult a d) (Rmult b c))); [Apply pos_Rsqr | Unfold Rsqr; Ring] | Ring] | Ring] | Ring] | Apply (ge0_plus_ge0_is_ge0 (Rsqr c) (Rsqr d) (pos_Rsqr c) (pos_Rsqr d)) | Apply (ge0_plus_ge0_is_ge0 (Rsqr a) (Rsqr b) (pos_Rsqr a) (pos_Rsqr b))] | Apply Rmult_le_pos; Apply foo; Apply ge0_plus_ge0_is_ge0; Apply pos_Rsqr]. -Save. +Qed. (************************************************************) (* Resolution of [a*X^2+b*X+c=0] *) @@ -279,7 +279,7 @@ Definition sol_x2 [a:nonzeroreal;b,c:R] : R := ``(-b-(sqrt (Delta a b c)))/(2*a) Lemma Rsqr_inv : (x:R) ~``x==0`` -> ``(Rsqr (/x))==/(Rsqr x)``. Intros; Unfold Rsqr. Rewrite Rinv_Rmult; Try Reflexivity Orelse Assumption. -Save. +Qed. Lemma Rsqr_sol_eq_0_1 : (a:nonzeroreal;b,c,x:R) (Delta_is_pos a b c) -> (x==(sol_x1 a b c))\/(x==(sol_x2 a b c)) -> ``a*(Rsqr x)+b*x+c==0``. Intros; Elim H0; Intro. @@ -363,7 +363,7 @@ Apply prod_neq_R0; DiscrR Orelse Apply (cond_nonzero a). Apply prod_neq_R0; DiscrR Orelse Apply (cond_nonzero a). Apply prod_neq_R0; DiscrR Orelse Apply (cond_nonzero a). Assumption. -Save. +Qed. Lemma canonical_Rsqr : (a:nonzeroreal;b,c,x:R) ``a*(Rsqr x)+b*x+c == a* (Rsqr (x+b/(2*a))) + (4*a*c - (Rsqr b))/(4*a)``. Intros. @@ -419,7 +419,7 @@ DiscrR. Apply (cond_nonzero a). DiscrR. Apply (cond_nonzero a). -Save. +Qed. Lemma Rsqr_eq : (x,y:R) (Rsqr x)==(Rsqr y) -> x==y \/ x==``-y``. Intros; Unfold Rsqr in H; Generalize (Rplus_plus_r ``-(y*y)`` ``x*x`` ``y*y`` H); Rewrite Rplus_Ropp_l; Replace ``-(y*y)+x*x`` with ``(x-y)*(x+y)``. @@ -427,7 +427,7 @@ Intro; Generalize (without_div_Od ``x-y`` ``x+y`` H0); Intro; Elim H1; Intros. Left; Apply Rminus_eq; Assumption. Right; Apply Rminus_eq; Unfold Rminus; Rewrite Ropp_Ropp; Assumption. Ring. -Save. +Qed. Lemma Rsqr_sol_eq_0_0 : (a:nonzeroreal;b,c,x:R) (Delta_is_pos a b c) -> ``a*(Rsqr x)+b*x+c==0`` -> (x==(sol_x1 a b c))\/(x==(sol_x2 a b c)). Intros; Rewrite (canonical_Rsqr a b c x) in H0; Rewrite Rplus_sym in H0; Generalize (Rplus_Ropp ``(4*a*c-(Rsqr b))/(4*a)`` ``a*(Rsqr (x+b/(2*a)))`` H0); Cut ``(Rsqr b)-4*a*c==(Delta a b c)``. @@ -462,4 +462,4 @@ Unfold Rdiv; Rewrite <- Ropp_mul1. Rewrite Ropp_distr2. Reflexivity. Reflexivity. -Save. +Qed. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index a771d2b98d..15b31daea7 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -53,22 +53,22 @@ Definition continuity_pt [f:R->R; x0:R] : Prop := (continue_in f no_cond x0). (**********) Lemma sum_continuous : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (plus_fct f1 f2) x0). Unfold continuity_pt plus_fct; Unfold continue_in; Intros; Apply limit_plus; Assumption. -Save. +Qed. (**********) Lemma diff_continuous : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (minus_fct f1 f2) x0). Unfold continuity_pt minus_fct; Unfold continue_in; Intros; Apply limit_minus; Assumption. -Save. +Qed. (**********) Lemma prod_continuous : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (mult_fct f1 f2) x0). Unfold continuity_pt mult_fct; Unfold continue_in; Intros; Apply limit_mul; Assumption. -Save. +Qed. (**********) Lemma const_continuous : (f:R->R; x0:R) (constant f) -> (continuity_pt f x0). Unfold constant continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Intros; Exists ``1``; Split; [Apply Rlt_R0_R1 | Intros; Generalize (H x x0); Intro; Rewrite H2; Simpl; Rewrite R_dist_eq; Assumption]. -Save. +Qed. (**********) Lemma scal_continuous : (f:R->R;a:R; x0:R) (continuity_pt f x0) -> (continuity_pt (mult_real_fct a f) x0). @@ -77,62 +77,62 @@ Unfold limit1_in; Unfold limit_in; Intros; Exists ``1``; Split. Apply Rlt_R0_R1. Intros; Rewrite R_dist_eq; Assumption. Assumption. -Save. +Qed. (**********) Lemma opp_continuous : (f:R->R; x0:R) (continuity_pt f x0) -> (continuity_pt (opp_fct f) x0). Unfold continuity_pt opp_fct; Unfold continue_in; Intros; Apply limit_Ropp; Assumption. -Save. +Qed. (**********) Lemma inv_continuous : (f:R->R; x0:R) (continuity_pt f x0) -> ~``(f x0)==0`` -> (continuity_pt ([x:R] ``/(f x)``) x0). Unfold continuity_pt; Unfold continue_in; Intros; Apply limit_inv; Assumption. -Save. +Qed. Lemma div_eq_inv : (f1,f2:R->R) (div_fct f1 f2)==(mult_fct f1 ([x:R]``/(f2 x)``)). Intros; Unfold div_fct; Unfold mult_fct; Unfold Rdiv; Apply fct_eq; Intro x; Reflexivity. -Save. +Qed. (**********) Lemma div_continuous : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> ~``(f2 x0)==0`` -> (continuity_pt (div_fct f1 f2) x0). Intros; Rewrite -> (div_eq_inv f1 f2); Apply prod_continuous; [Assumption | Apply inv_continuous; Assumption]. -Save. +Qed. (**********) Definition continuity [f:R->R] : Prop := (x:R) (continuity_pt f x). Lemma sum_continuity : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (plus_fct f1 f2)). Unfold continuity; Intros; Apply (sum_continuous f1 f2 x (H x) (H0 x)). -Save. +Qed. Lemma diff_continuity : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (minus_fct f1 f2)). Unfold continuity; Intros; Apply (diff_continuous f1 f2 x (H x) (H0 x)). -Save. +Qed. Lemma prod_continuity : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (mult_fct f1 f2)). Unfold continuity; Intros; Apply (prod_continuous f1 f2 x (H x) (H0 x)). -Save. +Qed. Lemma const_continuity : (f:R->R) (constant f) -> (continuity f). Unfold continuity; Intros; Apply (const_continuous f x H). -Save. +Qed. Lemma scal_continuity : (f:R->R;a:R) (continuity f) -> (continuity (mult_real_fct a f)). Unfold continuity; Intros; Apply (scal_continuous f a x (H x)). -Save. +Qed. Lemma opp_continuity : (f:R->R) (continuity f)->(continuity (opp_fct f)). Unfold continuity; Intros; Apply (opp_continuous f x (H x)). -Save. +Qed. Lemma div_continuity : (f1,f2:R->R) (continuity f1)->(continuity f2)->((x:R) ~``(f2 x)==0``)->(continuity (div_fct f1 f2)). Unfold continuity; Intros; Apply (div_continuous f1 f2 x (H x) (H0 x) (H1 x)). -Save. +Qed. Lemma inv_continuity : (f:R->R) (continuity f)->((x:R) ~``(f x)==0``)->(continuity ([x:R] ``/(f x)``)). Unfold continuity; Intros; Apply (inv_continuous f x (H x) (H0 x)). -Save. +Qed. (*****************************************************) (** Derivative's definition using Landau's kernel *) @@ -148,12 +148,12 @@ Axiom derive_pt_def : (f:R->R;x,l:R) ((eps:R) ``0<eps``->(EXT delta : posreal | (**********) Lemma derive_pt_def_0 : (f:R->R;x,l:R) ((eps:R) ``0<eps``->(EXT delta : posreal | ((h:R) ~``h==0``->``(Rabsolu h)<delta`` -> ``(Rabsolu ((((f (x+h))-(f x))/h)-l))<eps``))) -> (derive_pt f x)==l. Intros; Elim (derive_pt_def f x l); Intros; Apply (H0 H). -Save. +Qed. (**********) Lemma derive_pt_def_1 : (f:R->R;x,l:R) (derive_pt f x)==l -> ((eps:R) ``0<eps``->(EXT delta : posreal | ((h:R) ~``h==0``->``(Rabsolu h)<delta`` -> ``(Rabsolu ((((f (x+h))-(f x))/h)-l))<eps``))). Intros; Elim (derive_pt_def f x l); Intros; Apply (H2 H eps H0). -Save. +Qed. (**********) Definition derive [f:R->R] := [x:R] (derive_pt f x). @@ -173,12 +173,12 @@ cond_D2 : (derivable (derive d2)) }. (**********) Lemma derivable_derive : (f:R->R;x:R) (derivable_pt f x) -> (EXT l : R | (derive_pt f x)==l). Intros f x; Unfold derivable_pt; Intro H; Elim H; Intros l H0; Rewrite (derive_pt_def_0 f x l); [Exists l; Reflexivity | Assumption]. -Save. +Qed. (**********) Lemma derive_derivable : (f:R->R;x,l:R) (derive_pt f x)==l -> (derivable_pt f x). Intros; Unfold derivable_pt; Generalize (derive_pt_def_1 f x l H); Intro H0; Exists l; Assumption. -Save. +Qed. (********************************************************************) (** Equivalence of this definition with the one using limit concept *) @@ -196,7 +196,7 @@ Intro; Generalize (H2 ``x0-x`` H8 H5); Replace ``x+(x0-x)`` with x0. Intro; Assumption. Ring. Auto with real. -Save. +Qed. Definition fct_cte [a:R] : R->R := [x:R]a. @@ -216,11 +216,11 @@ Generalize (H5 H1); Intro. Unfold continuity_pt. Apply (cont_deriv f (fct_cte l) no_cond x H6). Unfold fct_cte; Reflexivity. -Save. +Qed. Theorem derivable_continuous : (f:R->R) (derivable f) -> (continuity f). Unfold derivable continuity; Intros; Apply (derivable_continuous_pt f x (H x)). -Save. +Qed. (****************************************************************) (** Main rules *) @@ -245,62 +245,62 @@ Unfold Rminus. Repeat Rewrite Ropp_distr1. Ring. Discriminate. -Save. +Qed. Lemma sum_derivable_pt : (f1,f2:R->R;x:R) (derivable_pt f1 x)->(derivable_pt f2 x)->(derivable_pt (plus_fct f1 f2) x). Intros; Generalize (derivable_derive f1 x H); Intro; Generalize (derivable_derive f2 x H0); Intro; Elim H1; Clear H1; Intros l1 H1; Elim H2; Clear H2; Intros l2 H2; Apply (derive_derivable (plus_fct f1 f2) x ``l1+l2``); Rewrite <- H1; Rewrite <- H2; Apply deriv_sum; Assumption. -Save. +Qed. Lemma sum_derivable : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (plus_fct f1 f2)). Unfold derivable; Intros f1 f2 H1 H2 x; Apply sum_derivable_pt; [Exact (H1 x) | Exact (H2 x)]. -Save. +Qed. Lemma sum_derivable_pt_var : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derivable_pt ([y:R]``(f1 y)+(f2 y)``) x). Intros; Generalize (sum_derivable_pt f1 f2 x H H0); Unfold plus_fct; Intro; Assumption. -Save. +Qed. Lemma derive_sum : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derive_pt ([y:R]``(f1 y)+(f2 y)``) x)==``(derive_pt f1 x)+(derive_pt f2 x)``. Intros; Generalize (deriv_sum f1 f2 x H H0); Unfold plus_fct; Intro; Assumption. -Save. +Qed. (* Opposite *) Lemma deriv_opposite : (f:R->R;x:R) (derivable_pt f x) -> ``(derive_pt (opp_fct f) x)==-(derive_pt f x)``. Intros; Generalize (derivable_derive f x H); Intro H0; Elim H0; Intros l H1; Rewrite H1; Unfold opp_fct; Apply derive_pt_def_0; Intros; Generalize (derive_pt_def_1 f x l H1); Intro H3; Elim (H3 eps H2); Intros delta H4; Exists delta; Intros; Replace ``( -(f (x+h))- -(f x))/h- -l`` with ``- (((f (x+h))-(f x))/h-l)``. Rewrite Rabsolu_Ropp; Apply (H4 h H5 H6). Unfold Rminus Rdiv; Rewrite Ropp_distr1; Repeat Rewrite Ropp_Ropp; Rewrite <- Ropp_mul1; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Reflexivity. -Save. +Qed. Lemma opposite_derivable_pt : (f:R->R;x:R) (derivable_pt f x) -> (derivable_pt (opp_fct f) x). Unfold opp_fct derivable_pt; Intros; Elim H; Intros; Exists ``-x0``; Intros; Elim (H0 eps H1); Intros; Exists x1; Intros; Generalize (H2 h H3 H4); Intro H5; Replace ``( -(f (x+h))- -(f x))/h- -x0`` with ``- (((f (x+h))-(f x))/h-x0)``. Rewrite Rabsolu_Ropp; Assumption. Unfold Rminus Rdiv; Rewrite Ropp_distr1; Repeat Rewrite Ropp_Ropp; Rewrite <- Ropp_mul1; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Reflexivity. -Save. +Qed. Lemma opposite_derivable : (f:R->R) (derivable f) -> (derivable (opp_fct f)). Unfold derivable; Intros f H1 x; Apply opposite_derivable_pt; Exact (H1 x). -Save. +Qed. (* Difference *) Lemma diff_plus_opp : (f1,f2:R->R) (minus_fct f1 f2)==(plus_fct f1 (opp_fct f2)). Intros; Unfold minus_fct plus_fct opp_fct; Apply fct_eq; Intro x; Ring. -Save. +Qed. Lemma deriv_diff : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> ``(derive_pt (minus_fct f1 f2) x)==(derive_pt f1 x)-(derive_pt f2 x)``. Intros; Rewrite diff_plus_opp; Unfold Rminus; Rewrite <- (deriv_opposite f2 x H0); Apply deriv_sum; [Assumption | Apply opposite_derivable_pt; Assumption]. -Save. +Qed. Lemma diff_derivable_pt : (f1,f2:R->R;x:R) (derivable_pt f1 x)->(derivable_pt f2 x)->(derivable_pt (minus_fct f1 f2) x). Intros; Rewrite (diff_plus_opp f1 f2); Apply sum_derivable_pt; [Assumption | Apply opposite_derivable_pt; Assumption]. -Save. +Qed. Lemma diff_derivable : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (minus_fct f1 f2)). Unfold derivable; Intros f1 f2 H1 H2 x; Apply diff_derivable_pt; [ Exact (H1 x) | Exact (H2 x)]. -Save. +Qed. Lemma derive_diff : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derive_pt ([y:R]``(f1 y)-(f2 y)``) x)==``(derive_pt f1 x)-(derive_pt f2 x)``. Intros; Generalize (deriv_diff f1 f2 x H H0); Unfold minus_fct; Intro; Assumption. -Save. +Qed. (**********) Lemma deriv_scal : (f:R->R;a,x:R) (derivable_pt f x) -> ``(derive_pt (mult_real_fct a f) x)==a*(derive_pt f x)``. @@ -319,7 +319,7 @@ Rewrite <- Rmult_assoc. Rewrite Rminus_distr. Reflexivity. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply (Rabsolu_pos_lt a H1)]. -Save. +Qed. Lemma scal_derivable_pt : (f:R->R;a:R; x:R) (derivable_pt f x) -> (derivable_pt (mult_real_fct a f) x). @@ -338,19 +338,19 @@ Rewrite <- Rmult_assoc. Rewrite Rminus_distr. Reflexivity. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply (Rabsolu_pos_lt a H1)]. -Save. +Qed. Lemma scal_derivable_pt_var : (f:R->R;a:R; x:R) (derivable_pt f x) -> (derivable_pt ([y:R]``a*(f y)``) x). Intros; Generalize (scal_derivable_pt f a x H); Unfold mult_real_fct; Intro; Assumption. -Save. +Qed. Lemma scal_derivable : (f:R->R;a:R) (derivable f) -> (derivable (mult_real_fct a f)). Unfold derivable; Intros f a H1 x; Apply scal_derivable_pt; Exact (H1 x). -Save. +Qed. Lemma derive_scal : (f:R->R;a,x:R) (derivable_pt f x) -> (derive_pt ([x:R]``a*(f x)``) x)==``a*(derive_pt f x)``. Intros; Generalize (deriv_scal f a x H); Unfold mult_real_fct; Intro; Assumption. -Save. +Qed. (* Multiplication *) Lemma deriv_prod : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> ``(derive_pt (mult_fct f1 f2) x)==(derive_pt f1 x)*(f2 x)+(derive_pt f2 x)*(f1 x)``. @@ -361,29 +361,29 @@ Generalize (H5 (mult_fct f1 f2) (plus_fct (mult_fct (fct_cte l1) f2) (mult_fct f Unfold plus_fct mult_fct fct_cte; Ring. Unfold fct_cte; Reflexivity. Unfold fct_cte; Reflexivity. -Save. +Qed. Lemma prod_derivable_pt : (f1,f2:R->R;x:R) (derivable_pt f1 x)->(derivable_pt f2 x)->(derivable_pt (mult_fct f1 f2) x). Intros; Generalize (deriv_prod f1 f2 x H H0); Intro; Apply (derive_derivable (mult_fct f1 f2) x ``(derive_pt f1 x)*(f2 x)+(derive_pt f2 x)*(f1 x)`` H1). -Save. +Qed. Lemma prod_derivable : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (mult_fct f1 f2)). Unfold derivable; Intros f1 f2 H1 H2 x; Apply prod_derivable_pt; [ Exact (H1 x) | Exact (H2 x)]. -Save. +Qed. Lemma derive_prod : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derive_pt ([x:R]``(f1 x)*(f2 x)``) x)==``(derive_pt f1 x)*(f2 x)+(derive_pt f2 x)*(f1 x)``. Intros; Generalize (deriv_prod f1 f2 x H H0); Unfold mult_fct; Intro; Assumption. -Save. +Qed. (**********) Lemma deriv_const : (a:R;x:R) (derive_pt ([x:R] a) x)==``0``. Intros; Apply derive_pt_def_0; Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Replace ``a-a`` with ``0``; [Unfold Rdiv; Rewrite Rmult_Ol; Rewrite minus_R0; Rewrite Rabsolu_R0; Assumption | Ring]. -Save. +Qed. Lemma const_derivable : (a:R) (derivable ([x:R] a)). Unfold derivable; Unfold derivable_pt; Intros; Exists ``0``; Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Unfold Rminus; Rewrite Rplus_Ropp_r; Unfold Rdiv; Rewrite Rmult_Ol; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. -Save. +Qed. (**********) Lemma deriv_id : (x:R) (derive_pt ([y:R] y) x)==``1``. @@ -393,7 +393,7 @@ Unfold Rminus; Rewrite Rplus_assoc; Rewrite (Rplus_sym x); Rewrite Rplus_assoc. Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite <- Rinv_r_sym. Symmetry; Apply Rplus_Ropp_r. Assumption. -Save. +Qed. Lemma diff_id : (derivable ([x:R] x)). Unfold derivable; Intro x; Unfold derivable_pt; Exists ``1``; Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``(x+h-x)/h-1`` with ``0``. @@ -404,20 +404,20 @@ Unfold Rminus; Rewrite Rplus_assoc; Rewrite (Rplus_sym x); Rewrite Rplus_assoc. Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite <- Rinv_r_sym. Symmetry; Apply Rplus_Ropp_r. Assumption. -Save. +Qed. (**********) Lemma sum_fct_cte_derive_pt : (f:R->R;t,a:R) (derivable_pt f t) -> (derive_pt ([x:R]``(f x)+a``) t)==(derive_pt f t). Intros; Generalize (derivable_derive f t H); Intro; Elim H0; Intros l H1; Rewrite H1; Apply derive_pt_def_0; Intros; Generalize (derive_pt_def_1 f t l H1); Intros; Elim (H3 eps H2); Intros delta H4; Exists delta; Intros; Replace ``(f (t+h))+a-((f t)+a)`` with ``(f (t+h))-(f t)``; [Apply (H4 h H5 H6) | Ring]. -Save. +Qed. Lemma sum_fct_cte_derivable_pt : (f:R->R;t,a:R) (derivable_pt f t)->(derivable_pt ([t:R]``(f t)+a``) t). Unfold derivable_pt; Intros; Elim H; Intros; Exists x; Intros; Elim (H0 eps H1); Intros; Exists x0; Intro h; Replace ``(f (t+h))+a-((f t)+a)`` with ``(f (t+h))-(f t)``; [Exact (H2 h) | Ring]. -Save. +Qed. Lemma sum_fct_cte_derivable : (f:R->R;a:R) (derivable f)->(derivable ([t:R]``(f t)+a``)). Unfold derivable; Intros; Apply sum_fct_cte_derivable_pt; Apply (H x). -Save. +Qed. (**********) Lemma deriv_Rsqr : (x:R) (derive Rsqr x)==``2*x``. @@ -430,7 +430,7 @@ Repeat Rewrite Rmult_1r; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r. Rewrite Rplus_Or; Reflexivity. Assumption. Unfold Rsqr; Reflexivity. -Save. +Qed. Lemma diff_Rsqr : (derivable Rsqr). Unfold derivable; Intro x; Unfold Rsqr; Unfold derivable_pt; Exists ``2*x``; Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``((x+h)*(x+h)-x*x)/h-2*x`` with ``h``. @@ -442,26 +442,26 @@ Repeat Rewrite Rmult_1r; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r. Rewrite Rplus_Or; Reflexivity. Assumption. Unfold Rsqr; Reflexivity. -Save. +Qed. Lemma Rsqr_derivable_pt : (f:R->R;t:R) (derivable_pt f t) -> (derivable_pt ([x:R](Rsqr (f x))) t). Unfold Rsqr; Intros; Generalize (prod_derivable_pt f f t H H); Unfold mult_fct; Intro H0; Assumption. -Save. +Qed. Lemma Rsqr_derivable : (f:R->R) (derivable f)->(derivable ([x:R](Rsqr (f x)))). Unfold derivable; Intros; Apply (Rsqr_derivable_pt f x (H x)). -Save. +Qed. (* SQRT *) Axiom deriv_sqrt : (x:R) ``0<x`` -> (derive sqrt)==[y:R] ``1/(2*(sqrt y))``. Lemma eq_fct : (x:R;f1,f2:R->R) f1==f2 -> (f1 x)==(f2 x). Intros; Rewrite H; Reflexivity. -Save. +Qed. Lemma diff_sqrt : (x:R) ``0<x`` -> (derivable_pt sqrt x). Intros; Generalize (deriv_sqrt x H); Unfold derive; Intro; Generalize (eq_fct x ([x:R](derive_pt sqrt x)) ([y:R]``1/(2*(sqrt y))``) H0); Intro; Apply (derive_derivable sqrt x ``1/(2*(sqrt x))`` H1). -Save. +Qed. (* Composition *) @@ -493,27 +493,27 @@ Assumption. Unfold mult_fct fct_cte; Rewrite Rmult_sym; Reflexivity. Unfold fct_cte; Reflexivity. Unfold fct_cte; Reflexivity. -Save. +Qed. Lemma composition_derivable : (f,g:R->R;x:R) (derivable_pt f x) -> (derivable_pt g (f x)) -> (derivable_pt (comp g f) x). Intros; Generalize (deriv_composition f g x H H0); Intro; Apply (derive_derivable (comp g f) x ``(derive_pt g (f x))*(derive_pt f x)`` H1). -Save. +Qed. Lemma derive_composition : (f,g:R->R;x:R) (derivable_pt f x) -> (derivable_pt g (f x)) -> (derive_pt ([x:R]``(g (f x))``) x)==``(derive_pt g (f x))*(derive_pt f x)``. Intros; Generalize (deriv_composition f g x H H0); Unfold comp; Intro; Assumption. -Save. +Qed. Lemma composition_derivable_var : (f,g:R->R;x:R) (derivable_pt f x) -> (derivable_pt g (f x)) -> (derivable_pt ([x:R](g (f x))) x). Intros; Generalize (composition_derivable f g x H H0); Unfold comp; Intro; Assumption. -Save. +Qed. Lemma diff_comp : (f,g:R->R) (derivable f)->(derivable g)->(derivable (comp g f)). Intros f g; Unfold derivable; Intros H1 H2 x; Apply (composition_derivable f g x (H1 x) (H2 (f x))). -Save. +Qed. Lemma Rsqr_derive : (f:R->R;t:R) (derivable_pt f t)->(derive_pt ([x:R](Rsqr (f x))) t)==(Rmult ``2`` (Rmult (derive_pt f t) (f t))). Intros; Generalize diff_Rsqr; Unfold derivable; Intro H0; Generalize (deriv_composition f Rsqr t H (H0 (f t))); Unfold comp; Intro H1; Rewrite H1; Generalize (deriv_Rsqr (f t)); Unfold derive; Intro H2; Rewrite H2; Rewrite Rmult_assoc; Rewrite <- (Rmult_sym (derive_pt f t)); Reflexivity. -Save. +Qed. (* SIN and COS *) Axiom deriv_sin : (derive sin)==cos. @@ -522,7 +522,7 @@ Lemma diff_sin : (derivable sin). Unfold derivable; Intro; Generalize deriv_sin; Unfold derive; Intro; Generalize (eq_fct x ([x:R](derive_pt sin x)) cos H); Intro; Apply (derive_derivable sin x (cos x) H0). -Save. +Qed. Lemma diff_cos : (derivable cos). Unfold derivable; Intro; Cut ([x:R]``(sin (x+PI/2))``)==cos. @@ -530,11 +530,11 @@ Intro; Rewrite <- H; Apply (composition_derivable_var ([x:R]``x+PI/2``) sin x). Apply (sum_fct_cte_derivable_pt ([x:R]x) x ``PI/2``); Apply diff_id. Apply diff_sin. Apply fct_eq; Intro; Symmetry; Rewrite Rplus_sym; Apply cos_sin. -Save. +Qed. Lemma derive_pt_sin : (x:R) (derive_pt sin x)==(cos x). Intro; Generalize deriv_sin; Unfold derive; Intro; Apply (eq_fct x [x:R](derive_pt sin x) cos H). -Save. +Qed. Lemma deriv_cos : (derive cos)==(opp_fct sin). Unfold opp_fct derive; Apply fct_eq; Intro; Cut ([x:R]``(sin (x+PI/2))``)==cos. @@ -545,11 +545,11 @@ Apply diff_id. Apply (sum_fct_cte_derivable_pt ([x:R]x) x ``PI/2``); Apply diff_id. Apply diff_sin. Apply fct_eq; Intro; Symmetry; Rewrite Rplus_sym; Apply cos_sin. -Save. +Qed. Lemma derive_pt_cos : (x:R) (derive_pt cos x)==``-(sin x)``. Intro; Generalize deriv_cos; Unfold derive; Intro; Unfold opp_fct in H; Apply (eq_fct x [x:R](derive_pt cos x) [x:R]``-(sin x)`` H). -Save. +Qed. (************************************************************) (** Local extremum's condition *) @@ -727,15 +727,15 @@ Unfold Rdiv; Apply Rmult_lt_pos. Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. Apply (Rlt_Rinv ``2`` Rgt_2_0). Unfold Rdiv; Apply Ropp_mul1. -Save. +Qed. Theorem deriv_minimum : (f:R->R;a,b,c:R) ``a<c``->``c<b``->(derivable_pt f c)->((x:R) ``a<x``->``x<b``->``(f c)<=(f x)``)->``(derive_pt f c)==0``. Intros; Generalize (opposite_derivable_pt f c H1); Intro; Rewrite <- (Ropp_Ropp (derive_pt f c)); Apply eq_RoppO; Rewrite <- (deriv_opposite f c H1); Apply (deriv_maximum (opp_fct f) a b c H H0 H3); Intros; Unfold opp_fct; Apply Rge_Ropp; Apply Rle_sym1; Apply (H2 x H4 H5). -Save. +Qed. Theorem deriv_constant2 : (f:R->R;a,b,c:R) ``a<c``->``c<b``->(derivable_pt f c)->((x:R) ``a<x``->``x<b``->``(f x)==(f c)``)->``(derive_pt f c)==0``. Intros; Apply (deriv_maximum f a b c H H0 H1); Intros; Right; Apply (H2 x H3 H4). -Save. +Qed. (**********) Lemma nonneg_derivative_0 : (f:R->R) (derivable f)->(increasing f) -> ((x:R) ``0<=(derive_pt f x)``). @@ -789,7 +789,7 @@ Rewrite <- Rmult_assoc. Apply Rinv_r_simpl_m. Apply aze. Rewrite <- Ropp_O; Apply Rlt_Ropp; Unfold Rdiv; Generalize (Rlt_monotony_r ``/2`` l ``0`` (Rlt_Rinv ``2`` Rgt_2_0) H4); Rewrite Rmult_Ol; Intro; Assumption. -Save. +Qed. (**********) Axiom nonneg_derivative_1 : (f:R->R) (derivable f)->((x:R) ``0<=(derive_pt f x)``) -> (increasing f). @@ -877,17 +877,17 @@ Apply aze. Unfold Rdiv; Apply Rmult_lt_pos. Assumption. Apply Rlt_Rinv; Apply Rgt_2_0. -Save. +Qed. (**********) Lemma increasing_decreasing_opp : (f:R->R) (increasing f) -> (decreasing (opp_fct f)). Unfold increasing decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Apply Rge_Ropp; Apply Rle_sym1; Assumption. -Save. +Qed. (**********) Lemma opp_opp_fct : (f:R->R) (opp_fct (opp_fct f))==f. Intro; Unfold opp_fct; Apply fct_eq; Intro; Rewrite Ropp_Ropp; Reflexivity. -Save. +Qed. (**********) Lemma nonpos_derivative_1 : (f:R->R) (derivable f)->((x:R) ``(derive_pt f x)<=0``) -> (decreasing f). @@ -897,7 +897,7 @@ Cut (x:R)``0<=(derive_pt (opp_fct f) x)``. Intros; Apply (nonneg_derivative_1 (opp_fct f) H2 H1). Intros; Rewrite (deriv_opposite f x (H x)); Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Apply (H0 x). Apply (opposite_derivable f H). -Save. +Qed. (**********) Axiom positive_derivative : (f:R->R) (derivable f)->((x:R) ``0<(derive_pt f x)``)->(strict_increasing f). @@ -905,7 +905,7 @@ Axiom positive_derivative : (f:R->R) (derivable f)->((x:R) ``0<(derive_pt f x)`` (**********) Lemma strictincreasing_strictdecreasing_opp : (f:R->R) (strict_increasing f) -> (strict_decreasing (opp_fct f)). Unfold strict_increasing strict_decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Apply Rlt_Ropp; Assumption. -Save. +Qed. (**********) Lemma negative_derivative : (f:R->R) (derivable f)->((x:R) ``(derive_pt f x)<0``)->(strict_decreasing f). @@ -915,12 +915,12 @@ Cut (x:R)``0<(derive_pt (opp_fct f) x)``. Intros; Apply (positive_derivative (opp_fct f) H2 H1). Intros; Rewrite (deriv_opposite f x (H x)); Rewrite <- Ropp_O; Apply Rlt_Ropp; Apply (H0 x). Apply (opposite_derivable f H). -Save. +Qed. (**********) Lemma null_derivative_0 : (f:R->R) (constant f)->((x:R) ``(derive_pt f x)==0``). Intros; Unfold constant in H; Apply derive_pt_def_0; Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Rewrite (H x ``x+h``); Unfold Rminus; Unfold Rdiv; Rewrite Rplus_Ropp_r; Rewrite Rmult_Ol; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. -Save. +Qed. (**********) Lemma increasing_decreasing : (f:R->R) (increasing f) -> (decreasing f) -> (constant f). @@ -929,7 +929,7 @@ Generalize (Rlt_le x y H1); Intro; Apply (Rle_antisym (f x) (f y) (H x y H2) (H0 Elim H1; Intro. Rewrite H2; Reflexivity. Generalize (Rlt_le y x H2); Intro; Symmetry; Apply (Rle_antisym (f y) (f x) (H y x H3) (H0 y x H3)). -Save. +Qed. (**********) Lemma null_derivative_1 : (f:R->R) (derivable f)->((x:R) ``(derive_pt f x)==0``)->(constant f). @@ -943,7 +943,7 @@ Apply increasing_decreasing; Assumption. Intro. Right; Symmetry; Apply (H0 x). Intro; Right; Apply (H0 x). -Save. +Qed. (**********) Axiom derive_increasing_interv_ax : (a,b:R;f:R->R) ``a<b``-> (((t:R) ``a<t<b`` -> ``0<(derive_pt f t)``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<(f y)``)) /\ (((t:R) ``a<t<b`` -> ``0<=(derive_pt f t)``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<=(f y)``)). @@ -951,12 +951,12 @@ Axiom derive_increasing_interv_ax : (a,b:R;f:R->R) ``a<b``-> (((t:R) ``a<t<b`` - (**********) Lemma derive_increasing_interv : (a,b:R;f:R->R) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<(derive_pt f t)``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<(f y)``). Intros; Generalize (derive_increasing_interv_ax a b f H); Intro; Elim H4; Intros H5 _; Apply (H5 H0 x y H1 H2 H3). -Save. +Qed. (**********) Lemma derive_increasing_interv_var : (a,b:R;f:R->R) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<=(derive_pt f t)``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<=(f y)``). Intros; Generalize (derive_increasing_interv_ax a b f H); Intro; Elim H4; Intros _ H5; Apply (H5 H0 x y H1 H2 H3). -Save. +Qed. (**********) (**********) diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index f20254f629..fd243969bc 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -48,22 +48,22 @@ Add Field R Rplus Rmult R1 R0 Ropp [x,y:R]false Rinv RTheory Rinv_l (**********) Lemma Rlt_antirefl:(r:R)~``r<r``. Generalize Rlt_antisym. Intuition EAuto. -Save. +Qed. Hints Resolve Rlt_antirefl : real. Lemma Rlt_not_eq:(r1,r2:R)``r1<r2``->``r1<>r2``. Red; Intros r1 r2 H H0; Apply (Rlt_antirefl r1). Pattern 2 r1; Rewrite H0; Trivial. -Save. +Qed. Lemma Rgt_not_eq:(r1,r2:R)``r1>r2``->``r1<>r2``. Intros; Apply sym_not_eqT; Apply Rlt_not_eq; Auto with real. -Save. +Qed. (**********) Lemma imp_not_Req:(r1,r2:R)(``r1<r2``\/ ``r1>r2``) -> ``r1<>r2``. Generalize Rlt_not_eq Rgt_not_eq. Intuition EAuto. -Save. +Qed. Hints Resolve imp_not_Req : real. (** Reasoning by case on equalities and order *) @@ -71,18 +71,18 @@ Hints Resolve imp_not_Req : real. (**********) Lemma Req_EM:(r1,r2:R)(r1==r2)\/``r1<>r2``. Intros ; Generalize (total_order_T r1 r2) imp_not_Req ; Intuition EAuto 3. -Save. +Qed. Hints Resolve Req_EM : real. (**********) Lemma total_order:(r1,r2:R)``r1<r2``\/(r1==r2)\/``r1>r2``. Intros;Generalize (total_order_T r1 r2);Tauto. -Save. +Qed. (**********) Lemma not_Req:(r1,r2:R)``r1<>r2``->(``r1<r2``\/``r1>r2``). Intros; Generalize (total_order_T r1 r2) ; Tauto. -Save. +Qed. (*********************************************************************************) @@ -92,23 +92,23 @@ Save. (**********) Lemma Rlt_le:(r1,r2:R)``r1<r2``-> ``r1<=r2``. Intros ; Red ; Tauto. -Save. +Qed. Hints Resolve Rlt_le : real. (**********) Lemma Rle_ge : (r1,r2:R)``r1<=r2`` -> ``r2>=r1``. NewDestruct 1; Red; Auto with real. -Save. +Qed. (**********) Lemma Rge_le : (r1,r2:R)``r1>=r2`` -> ``r2<=r1``. NewDestruct 1; Red; Auto with real. -Save. +Qed. (**********) Lemma not_Rle:(r1,r2:R)~(``r1<=r2``)->``r1>r2``. Intros r1 r2 ; Generalize (total_order r1 r2) ; Unfold Rle; Tauto. -Save. +Qed. Hints Immediate Rle_ge Rge_le not_Rle : real. @@ -116,7 +116,7 @@ Hints Immediate Rle_ge Rge_le not_Rle : real. Lemma Rlt_le_not:(r1,r2:R)``r2<r1``->~(``r1<=r2``). Generalize Rlt_antisym imp_not_Req ; Unfold Rle. Intuition EAuto 3. -Save. +Qed. Lemma Rle_not:(r1,r2:R)``r1>r2`` -> ~(``r1<=r2``). Proof Rlt_le_not. @@ -126,109 +126,109 @@ Hints Immediate Rlt_le_not : real. Lemma Rle_not_lt: (r1, r2:R) ``r2 <= r1`` ->~ (``r1<r2``). Intros r1 r2. Generalize (Rlt_antisym r1 r2) (imp_not_Req r1 r2). Unfold Rle; Intuition. -Save. +Qed. (**********) Lemma Rlt_ge_not:(r1,r2:R)``r1<r2``->~(``r1>=r2``). Generalize Rlt_le_not. Unfold Rle Rge. Intuition EAuto 3. -Save. +Qed. Hints Immediate Rlt_ge_not : real. (**********) Lemma eq_Rle:(r1,r2:R)r1==r2->``r1<=r2``. Unfold Rle; Tauto. -Save. +Qed. Hints Immediate eq_Rle : real. Lemma eq_Rge:(r1,r2:R)r1==r2->``r1>=r2``. Unfold Rge; Tauto. -Save. +Qed. Hints Immediate eq_Rge : real. Lemma eq_Rle_sym:(r1,r2:R)r2==r1->``r1<=r2``. Unfold Rle; Auto. -Save. +Qed. Hints Immediate eq_Rle_sym : real. Lemma eq_Rge_sym:(r1,r2:R)r2==r1->``r1>=r2``. Unfold Rge; Auto. -Save. +Qed. Hints Immediate eq_Rge_sym : real. Lemma Rle_antisym : (r1,r2:R)``r1<=r2`` -> ``r2<=r1``-> r1==r2. Intros r1 r2; Generalize (Rlt_antisym r1 r2) ; Unfold Rle ; Intuition. -Save. +Qed. Hints Resolve Rle_antisym : real. (**********) Lemma Rle_le_eq:(r1,r2:R)(``r1<=r2``/\``r2<=r1``)<->(r1==r2). Intuition. -Save. +Qed. Lemma Rlt_rew : (x,x',y,y':R)``x==x'``->``x'<y'`` -> `` y' == y`` -> ``x < y``. Intros; Replace x with x'; Replace y with y'; Assumption. -Save. +Qed. (**********) Lemma Rle_trans:(r1,r2,r3:R) ``r1<=r2``->``r2<=r3``->``r1<=r3``. Generalize trans_eqT Rlt_trans Rlt_rew. Unfold Rle. Intuition EAuto 2. -Save. +Qed. (**********) Lemma Rle_lt_trans:(r1,r2,r3:R)``r1<=r2``->``r2<r3``->``r1<r3``. Generalize Rlt_trans Rlt_rew. Unfold Rle. Intuition EAuto 2. -Save. +Qed. (**********) Lemma Rlt_le_trans:(r1,r2,r3:R)``r1<r2``->``r2<=r3``->``r1<r3``. Generalize Rlt_trans Rlt_rew; Unfold Rle; Intuition EAuto 2. -Save. +Qed. (** Decidability of the order *) Lemma total_order_Rlt:(r1,r2:R)(sumboolT ``r1<r2`` ~(``r1<r2``)). Intros;Generalize (total_order_T r1 r2) (imp_not_Req r1 r2) ; Intuition. -Save. +Qed. (**********) Lemma total_order_Rle:(r1,r2:R)(sumboolT ``r1<=r2`` ~(``r1<=r2``)). Intros r1 r2. Generalize (total_order_T r1 r2) (imp_not_Req r1 r2). Intuition EAuto 4 with real. -Save. +Qed. (**********) Lemma total_order_Rgt:(r1,r2:R)(sumboolT ``r1>r2`` ~(``r1>r2``)). Intros;Unfold Rgt;Intros;Apply total_order_Rlt. -Save. +Qed. (**********) Lemma total_order_Rge:(r1,r2:R)(sumboolT (``r1>=r2``) ~(``r1>=r2``)). Intros;Generalize (total_order_Rle r2 r1);Intuition. -Save. +Qed. Lemma total_order_Rlt_Rle:(r1,r2:R)(sumboolT ``r1<r2`` ``r2<=r1``). Intros;Generalize (total_order_T r1 r2); Intuition. -Save. +Qed. Lemma Rle_or_lt: (n, m:R)(Rle n m) \/ (Rlt m n). Intros n m; Elim (total_order_Rlt_Rle m n);Auto with real. -Save. +Qed. Lemma total_order_Rle_Rlt_eq :(r1,r2:R)``r1<=r2``-> (sumboolT ``r1<r2`` ``r1==r2``). Intros r1 r2 H;Generalize (total_order_T r1 r2); Intuition. -Save. +Qed. (**********) Lemma inser_trans_R:(n,m,p,q:R)``n<=m<p``-> (sumboolT ``n<=m<q`` ``q<=m<p``). Intros; Generalize (total_order_Rlt_Rle m q); Intuition. -Save. +Qed. (****************************************************************) (** Field Lemmas *) @@ -240,18 +240,18 @@ Save. Lemma Rplus_ne:(r:R)``r+0==r``/\``0+r==r``. Intro;Split;Ring. -Save. +Qed. Hints Resolve Rplus_ne : real v62. Lemma Rplus_Or:(r:R)``r+0==r``. Intro; Ring. -Save. +Qed. Hints Resolve Rplus_Or : real. (**********) Lemma Rplus_Ropp_l:(r:R)``(-r)+r==0``. Intro; Ring. -Save. +Qed. Hints Resolve Rplus_Ropp_l : real. @@ -260,14 +260,14 @@ 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. +Qed. (*i New i*) Hint eqT_R_congr : real := Resolve (congr_eqT R). Lemma Rplus_plus_r:(r,r1,r2:R)(r1==r2)->``r+r1==r+r2``. Auto with real. -Save. +Qed. (*i Old i*)Hints Resolve Rplus_plus_r : v62. @@ -278,14 +278,14 @@ Lemma r_Rplus_plus:(r,r1,r2:R)``r+r1==r+r2``->r1==r2. Transitivity ``(-r+r)+r2``. Repeat Rewrite -> Rplus_assoc; Rewrite <- H; Reflexivity. Ring. -Save. +Qed. Hints Resolve r_Rplus_plus : real. (**********) 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. +Qed. (***********************************************************) (** Multiplication *) @@ -294,47 +294,47 @@ Save. (**********) Lemma Rinv_r:(r:R)``r<>0``->``r* (/r)==1``. Intros; Rewrite -> Rmult_sym; Auto with real. -Save. +Qed. Hints Resolve Rinv_r : real. Lemma Rinv_l_sym:(r:R)``r<>0``->``1==(/r) * r``. Symmetry; Auto with real. -Save. +Qed. Lemma Rinv_r_sym:(r:R)``r<>0``->``1==r* (/r)``. Symmetry; Auto with real. -Save. +Qed. Hints Resolve Rinv_l_sym Rinv_r_sym : real. (**********) Lemma Rmult_Or :(r:R) ``r*0==0``. Intro; Ring. -Save. +Qed. Hints Resolve Rmult_Or : real v62. (**********) Lemma Rmult_Ol:(r:R)(``0*r==0``). Intro; Ring. -Save. +Qed. Hints Resolve Rmult_Ol : real v62. (**********) Lemma Rmult_ne:(r:R)``r*1==r``/\``1*r==r``. Intro;Split;Ring. -Save. +Qed. Hints Resolve Rmult_ne : real v62. (**********) Lemma Rmult_1r:(r:R)(``r*1==r``). Intro; Ring. -Save. +Qed. Hints Resolve Rmult_1r : real. (**********) Lemma Rmult_mult_r:(r,r1,r2:R)r1==r2->``r*r1==r*r2``. Auto with real. -Save. +Qed. (*i OLD i*)Hints Resolve Rmult_mult_r : v62. @@ -345,7 +345,7 @@ Lemma r_Rmult_mult:(r,r1,r2:R)(``r*r1==r*r2``)->``r<>0``->(r1==r2). Transitivity ``(/r * r)*r2``. Repeat Rewrite Rmult_assoc; Rewrite H; Trivial. Rewrite Rinv_l; Auto with real. -Save. +Qed. (**********) Lemma without_div_Od:(r1,r2:R)``r1*r2==0`` -> ``r1==0`` \/ ``r2==0``. @@ -353,43 +353,43 @@ Lemma without_div_Od:(r1,r2:R)``r1*r2==0`` -> ``r1==0`` \/ ``r2==0``. Auto. Right; Apply r_Rmult_mult with r1; Trivial. Rewrite H; Auto with real. -Save. +Qed. (**********) 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. +Qed. Hints Resolve without_div_Oi : real. (**********) Lemma without_div_Oi1:(r1,r2:R) ``r1==0`` -> ``r1*r2==0``. Auto with real. -Save. +Qed. (**********) Lemma without_div_Oi2:(r1,r2:R) ``r2==0`` -> ``r1*r2==0``. Auto with real. -Save. +Qed. (**********) 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. +Qed. (**********) 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. +Qed. Hints Resolve mult_non_zero : real. (**********) Lemma Rmult_Rplus_distrl: (r1,r2,r3:R) ``(r1+r2)*r3 == (r1*r3)+(r2*r3)``. Intros; Ring. -Save. +Qed. (** Square function *) @@ -399,12 +399,12 @@ Definition Rsqr:R->R:=[r:R]``r*r``. (***********) Lemma Rsqr_O:(Rsqr ``0``)==``0``. Unfold Rsqr; Auto with real. -Save. +Qed. (***********) Lemma Rsqr_r_R0:(r:R)(Rsqr r)==``0``->``r==0``. Unfold Rsqr;Intros;Elim (without_div_Od r r H);Trivial. -Save. +Qed. (*********************************************************) (** Opposite *) @@ -413,25 +413,25 @@ Save. (**********) Lemma eq_Ropp:(r1,r2:R)(r1==r2)->``-r1 == -r2``. Auto with real. -Save. +Qed. Hints Resolve eq_Ropp : real. (**********) Lemma Ropp_O:``-0==0``. Ring. -Save. +Qed. Hints Resolve Ropp_O : real v62. (**********) Lemma eq_RoppO:(r:R)``r==0``-> ``-r==0``. Intros; Rewrite -> H; Auto with real. -Save. +Qed. Hints Resolve eq_RoppO : real. (**********) Lemma Ropp_Ropp:(r:R)``-(-r)==r``. Intro; Ring. -Save. +Qed. Hints Resolve Ropp_Ropp : real. (*********) @@ -439,115 +439,115 @@ Lemma Ropp_neq:(r:R)``r<>0``->``-r<>0``. Red;Intros r H H0. Apply H. Transitivity ``-(-r)``; Auto with real. -Save. +Qed. Hints Resolve Ropp_neq : real. (**********) Lemma Ropp_distr1:(r1,r2:R)``-(r1+r2)==(-r1 + -r2)``. Intros; Ring. -Save. +Qed. Hints Resolve Ropp_distr1 : real. (** Opposite and multiplication *) Lemma Ropp_mul1:(r1,r2:R)``(-r1)*r2 == -(r1*r2)``. Intros; Ring. -Save. +Qed. Hints Resolve Ropp_mul1 : real. (**********) Lemma Ropp_mul2:(r1,r2:R)``(-r1)*(-r2)==r1*r2``. Intros; Ring. -Save. +Qed. Hints Resolve Ropp_mul2 : real. (** Substraction *) Lemma minus_R0:(r:R)``r-0==r``. Intro;Ring. -Save. +Qed. Hints Resolve minus_R0 : real. Lemma Rminus_Ropp:(r:R)``0-r==-r``. Intro;Ring. -Save. +Qed. Hints Resolve Rminus_Ropp : real. (**********) Lemma Ropp_distr2:(r1,r2:R)``-(r1-r2)==r2-r1``. Intros; Ring. -Save. +Qed. Hints Resolve Ropp_distr2 : real. Lemma Ropp_distr3:(r1,r2:R)``-(r2-r1)==r1-r2``. Intros; Ring. -Save. +Qed. Hints Resolve Ropp_distr3 : real. (**********) Lemma eq_Rminus:(r1,r2:R)(r1==r2)->``r1-r2==0``. Intros; Rewrite H; Ring. -Save. +Qed. Hints Resolve eq_Rminus : 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. +Qed. Hints Immediate Rminus_eq : real. Lemma Rminus_eq_right:(r1,r2:R)``r2-r1==0`` -> r1==r2. Intros;Generalize (Rminus_eq r2 r1 H);Clear H;Intro H;Rewrite H;Ring. -Save. +Qed. Hints Immediate Rminus_eq_right : real. Lemma Rplus_Rminus: (p,q:R)``p+(q-p)``==q. Intros; Ring. -Save. +Qed. Hints Resolve Rplus_Rminus:real. (**********) Lemma Rminus_eq_contra:(r1,r2:R)``r1<>r2``->``r1-r2<>0``. Red; Intros r1 r2 H H0. Apply H; Auto with real. -Save. +Qed. Hints Resolve Rminus_eq_contra : real. Lemma Rminus_not_eq:(r1,r2:R)``r1-r2<>0``->``r1<>r2``. Red; Intros; Elim H; Apply eq_Rminus; Auto. -Save. +Qed. Hints Resolve Rminus_not_eq : real. Lemma Rminus_not_eq_right:(r1,r2:R)``r2-r1<>0`` -> ``r1<>r2``. Red; Intros;Elim H;Rewrite H0; Ring. -Save. +Qed. Hints Resolve Rminus_not_eq_right : real. (**********) Lemma Rminus_distr: (x,y,z:R) ``x*(y-z)==(x*y) - (x*z)``. Intros; Ring. -Save. +Qed. (** Inverse *) Lemma Rinv_R1:``/1==1``. Apply (r_Rmult_mult ``1`` ``/1`` ``1``); Auto with real. Rewrite (Rinv_r R1 R1_neq_R0);Auto with real. -Save. +Qed. Hints Resolve Rinv_R1 : real. (*********) Lemma Rinv_neq_R0:(r:R)``r<>0``->``(/r)<>0``. Red; Intros; Apply R1_neq_R0. Replace ``1`` with ``(/r) * r``; Auto with real. -Save. +Qed. Hints Resolve Rinv_neq_R0 : real. (*********) Lemma Rinv_Rinv:(r:R)``r<>0``->``/(/r)==r``. Intros;Apply (r_Rmult_mult ``/r``); Auto with real. Transitivity ``1``; Auto with real. -Save. +Qed. Hints Resolve Rinv_Rinv : real. (*********) @@ -558,30 +558,30 @@ Transitivity ``(r1*/r1)*(r2*(/r2))``; Auto with real. Rewrite Rinv_r; Trivial. Rewrite Rinv_r; Auto with real. Ring. -Save. +Qed. (*********) Lemma Ropp_Rinv:(r:R)``r<>0``->``-(/r)==/(-r)``. Intros; Apply (r_Rmult_mult ``-r``);Auto with real. Transitivity ``1``; Auto with real. Rewrite (Ropp_mul2 r ``/r``); Auto with real. -Save. +Qed. Lemma Rinv_r_simpl_r : (r1,r2:R)``r1<>0``->``r1*(/r1)*r2==r2``. Intros; Transitivity ``1*r2``; Auto with real. Rewrite Rinv_r; Auto with real. -Save. +Qed. Lemma Rinv_r_simpl_l : (r1,r2:R)``r1<>0``->``r2*r1*(/r1)==r2``. Intros; Transitivity ``r2*1``; Auto with real. Transitivity ``r2*(r1*/r1)``; Auto with real. -Save. +Qed. Lemma Rinv_r_simpl_m : (r1,r2:R)``r1<>0``->``r1*r2*(/r1)==r2``. Intros; Transitivity ``r2*1``; Auto with real. Transitivity ``r2*(r1*/r1)``; Auto with real. Ring. -Save. +Qed. Hints Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m : real. (*********) @@ -589,14 +589,14 @@ Lemma Rinv_Rmult_simpl:(a,b,c:R)``a<>0``->``(a*(/b))*(c*(/a))==c*(/b)``. Intros. Transitivity ``(a*/a)*(c*(/b))``; Auto with real. Ring. -Save. +Qed. (** Order and addition *) Lemma Rlt_compatibility_r:(r,r1,r2:R)``r1<r2``->``r1+r<r2+r``. Intros. Rewrite (Rplus_sym r1 r); Rewrite (Rplus_sym r2 r); Auto with real. -Save. +Qed. Hints Resolve Rlt_compatibility_r : real. @@ -608,21 +608,21 @@ 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. +Qed. (**********) 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. +Qed. (**********) 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. +Qed. Hints Resolve Rle_compatibility Rle_compatibility_r : real. @@ -631,7 +631,7 @@ 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. +Qed. (**********) Lemma sum_inequa_Rle_lt:(a,x,b,c,y,d:R)``a<=x`` -> ``x<b`` -> @@ -639,28 +639,28 @@ Lemma sum_inequa_Rle_lt:(a,x,b,c,y,d:R)``a<=x`` -> ``x<b`` -> Intros;Split. Apply Rlt_le_trans with ``a+y``; Auto with real. Apply Rlt_le_trans with ``b+y``; Auto with real. -Save. +Qed. (*********) Lemma Rplus_lt:(r1,r2,r3,r4:R)``r1<r2`` -> ``r3<r4`` -> ``r1+r3 < r2+r4``. Intros; Apply Rlt_trans with ``r2+r3``; Auto with real. -Save. +Qed. Lemma Rplus_le:(r1,r2,r3,r4:R)``r1<=r2`` -> ``r3<=r4`` -> ``r1+r3 <= r2+r4``. Intros; Apply Rle_trans with ``r2+r3``; Auto with real. -Save. +Qed. (*********) Lemma Rplus_lt_le_lt:(r1,r2,r3,r4:R)``r1<r2`` -> ``r3<=r4`` -> ``r1+r3 < r2+r4``. Intros; Apply Rlt_le_trans with ``r2+r3``; Auto with real. -Save. +Qed. (*********) Lemma Rplus_le_lt_lt:(r1,r2,r3,r4:R)``r1<=r2`` -> ``r3<r4`` -> ``r1+r3 < r2+r4``. Intros; Apply Rle_lt_trans with ``r2+r3``; Auto with real. -Save. +Qed. Hints Immediate Rplus_lt Rplus_le Rplus_lt_le_lt Rplus_le_lt_lt : real. @@ -675,30 +675,30 @@ Replace ``r2+r1+(-r2)`` with r1. Trivial. Ring. Ring. -Save. +Qed. Hints Resolve Rgt_Ropp. (**********) Lemma Rlt_Ropp:(r1,r2:R) ``r1 < r2`` -> ``-r1 > -r2``. Unfold Rgt; Auto with real. -Save. +Qed. Hints Resolve Rlt_Ropp : real. Lemma Ropp_Rlt: (x,y:R) ``-y < -x`` ->``x<y``. Intros x y H'. Rewrite <- (Ropp_Ropp x); Rewrite <- (Ropp_Ropp y); Auto with real. -Save. +Qed. Hints Resolve Ropp_Rlt : real. Lemma Rlt_Ropp1:(r1,r2:R) ``r2 < r1`` -> ``-r1 < -r2``. Auto with real. -Save. +Qed. Hints Resolve Rlt_Ropp1 : real. (**********) Lemma Rle_Ropp:(r1,r2:R) ``r1 <= r2`` -> ``-r1 >= -r2``. Unfold Rge; Intros r1 r2 [H|H]; Auto with real. -Save. +Qed. Hints Resolve Rle_Ropp : real. Lemma Ropp_Rle: (x,y:R) ``-y <= -x`` ->``x <= y``. @@ -706,50 +706,50 @@ Intros x y H. Elim H;Auto with real. Intro H1;Rewrite <-(Ropp_Ropp x);Rewrite <-(Ropp_Ropp y);Rewrite H1; Auto with real. -Save. +Qed. Hints Resolve Ropp_Rle : real. Lemma Rle_Ropp1:(r1,r2:R) ``r2 <= r1`` -> ``-r1 <= -r2``. Intros r1 r2 H;Elim H;Auto with real. Intro H1;Rewrite H1;Auto with real. -Save. +Qed. Hints Resolve Rle_Ropp1 : real. (**********) Lemma Rge_Ropp:(r1,r2:R) ``r1 >= r2`` -> ``-r1 <= -r2``. Unfold Rge; Intros r1 r2 [H|H]; Auto with real. -Save. +Qed. Hints Resolve Rge_Ropp : real. (**********) Lemma Rlt_RO_Ropp:(r:R) ``0 < r`` -> ``0 > -r``. Intros; Replace ``0`` with ``-0``; Auto with real. -Save. +Qed. Hints Resolve Rlt_RO_Ropp : real. (**********) Lemma Rgt_RO_Ropp:(r:R) ``0 > r`` -> ``0 < -r``. Intros; Replace ``0`` with ``-0``; Auto with real. -Save. +Qed. Hints Resolve Rgt_RO_Ropp : real. (**********) Lemma Rle_RO_Ropp:(r:R) ``0 <= r`` -> ``0 >= -r``. Intros; Replace ``0`` with ``-0``; Auto with real. -Save. +Qed. Hints Resolve Rle_RO_Ropp : real. (**********) Lemma Rge_RO_Ropp:(r:R) ``0 >= r`` -> ``0 <= -r``. Intros; Replace ``0`` with ``-0``; Auto with real. -Save. +Qed. Hints Resolve Rge_RO_Ropp : real. (** Order and multiplication *) Lemma Rlt_monotony_r:(r,r1,r2:R)``0<r`` -> ``r1 < r2`` -> ``r1*r < r2*r``. Intros; Rewrite (Rmult_sym r1 r); Rewrite (Rmult_sym r2 r); Auto with real. -Save. +Qed. Hints Resolve Rlt_monotony_r. Lemma Rlt_monotony_contra: @@ -760,27 +760,27 @@ Case (total_order x y); Intros Eq0; Auto; Elim Eq0; Clear Eq0; Intros Eq0. Generalize (Rlt_monotony z y x H Eq0);Intro;ElimType False; Generalize (Rlt_trans ``z*x`` ``z*y`` ``z*x`` H0 H1);Intro; Apply (Rlt_antirefl ``z*x``);Auto. -Save. +Qed. 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. +Qed. (**********) 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. +Qed. Hints Resolve Rle_monotony : real. 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. +Qed. Hints Resolve Rle_monotony_r : real. Lemma Rle_monotony_contra: @@ -793,14 +793,14 @@ Replace y with (Rmult (Rinv z) (Rmult z y)). Rewrite H1;Auto with real. Rewrite <- Rmult_assoc; Rewrite Rinv_l; Auto with real. Rewrite <- Rmult_assoc; Rewrite Rinv_l; Auto with real. -Save. +Qed. 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. +Qed. Hints Resolve Rle_anti_monotony : real. Lemma Rle_Rmult_comp: @@ -811,13 +811,13 @@ Apply Rle_trans with r2 := ``x*t``; Auto with real. Repeat Rewrite [x:?](Rmult_sym x t). Apply Rle_monotony; Auto. Apply Rle_trans with z; Auto. -Save. +Qed. Hints Resolve Rle_Rmult_comp :real. 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. +Qed. (** Order and Substractions *) Lemma Rlt_minus:(r1,r2:R)``r1 < r2`` -> ``r1-r2 < 0``. @@ -825,33 +825,33 @@ Intros; Apply (Rlt_anti_compatibility ``r2``). Replace ``r2+(r1-r2)`` with r1. Replace ``r2+0`` with r2; Auto with real. Ring. -Save. +Qed. Hints Resolve Rlt_minus : real. (**********) Lemma Rle_minus:(r1,r2:R)``r1 <= r2`` -> ``r1-r2 <= 0``. Unfold Rle; Intros; Elim H; Auto with real. -Save. +Qed. (**********) 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. +Qed. (**********) 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. +Qed. (**********) Lemma tech_Rplus:(r,s:R)``0<=r`` -> ``0<s`` -> ``r+s<>0``. Intros; Apply sym_not_eqT; Apply Rlt_not_eq. Rewrite Rplus_sym; Replace ``0`` with ``0+0``; Auto with real. -Save. +Qed. Hints Immediate tech_Rplus : real. (** Order and the square function *) @@ -860,7 +860,7 @@ 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. +Qed. (***********) Lemma pos_Rsqr1:(r:R)``r<>0``->``0<(Rsqr r)``. @@ -868,14 +868,14 @@ 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. +Qed. Hints Resolve pos_Rsqr pos_Rsqr1 : real. (** 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. +Qed. Hints Resolve Rlt_R0_R1 : real. (** Order and inverse *) @@ -884,7 +884,7 @@ Intros; Change ``/r>0``; Apply not_Rle; Red; Intros. Absurd ``1<=0``; Auto with real. Replace ``1`` with ``r*(/r)``; Auto with real. Replace ``0`` with ``r*0``; Auto with real. -Save. +Qed. Hints Resolve Rlt_Rinv : real. (*********) @@ -893,7 +893,7 @@ Intros; Change ``0>/r``; Apply not_Rle; Red; Intros. Absurd ``1<=0``; Auto with real. Replace ``1`` with ``r*(/r)``; Auto with real. Replace ``0`` with ``r*0``; Auto with real. -Save. +Qed. Hints Resolve Rlt_Rinv2 : real. (**********) @@ -905,7 +905,7 @@ Transitivity ``r*/r*r2``; Auto with real. Ring. Transitivity ``r*/r*r1``; Auto with real. Ring. -Save. +Qed. (*********) Lemma Rinv_lt:(r1,r2:R)``0 < r1*r2`` -> ``r1 < r2`` -> ``/r2 < /r1``. @@ -915,7 +915,7 @@ Replace ``r1*r2*/r2`` with r1. Replace ``r1*r2*/r1`` with r2; Trivial. Symmetry; Auto with real. Symmetry; Auto with real. -Save. +Qed. Lemma Rlt_Rinv_R1: (x, y:R) ``1 <= x`` -> ``x<y`` ->``/y< /x``. Intros x y H' H'0. @@ -931,7 +931,7 @@ Rewrite (Rmult_sym x); Rewrite <- Rmult_assoc; Rewrite (Rmult_sym y (Rinv y)); Rewrite Rinv_l; Auto with real. Apply imp_not_Req; Right. Red; Apply Rlt_trans with r2 := x; Auto with real. -Save. +Qed. Hints Resolve Rlt_Rinv_R1 :real. (*********************************************************) @@ -941,30 +941,30 @@ Hints Resolve Rlt_Rinv_R1 :real. (**********) Lemma Rge_ge_eq:(r1,r2:R)``r1 >= r2`` -> ``r2 >= r1`` -> r1==r2. Intros; Apply Rle_antisym; Auto with real. -Save. +Qed. (**********) Lemma Rlt_not_ge:(r1,r2:R)~(``r1<r2``)->``r1>=r2``. Intros; Unfold Rge; Elim (total_order r1 r2); Intro. Absurd ``r1<r2``; Trivial. Case H0; Auto. -Save. +Qed. (**********) 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. +Qed. (**********) Lemma Rgt_ge:(r1,r2:R)``r1>r2`` -> ``r1 >= r2``. Red; Auto with real. -Save. +Qed. (**********) Lemma Rlt_sym:(r1,r2:R)``r1<r2`` <-> ``r2>r1``. Split; Unfold Rgt; Auto with real. -Save. +Qed. (**********) Lemma Rle_sym1:(r1,r2:R)``r1<=r2``->``r2>=r1``. @@ -977,38 +977,38 @@ Proof [r1,r2](Rge_le r2 r1). (**********) Lemma Rle_sym:(r1,r2:R)``r1<=r2``<->``r2>=r1``. Split; Auto with real. -Save. +Qed. (**********) 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. +Qed. (**********) 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. +Qed. (**********) 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. +Qed. (**********) 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. +Qed. (**********) Lemma Rgt_RoppO:(r:R)``r>0``->``(-r)<0``. Intros; Rewrite <- Ropp_O; Auto with real. -Save. +Qed. (**********) Lemma Rlt_RoppO:(r:R)``r<0``->``-r>0``. Intros; Rewrite <- Ropp_O; Auto with real. -Save. +Qed. Hints Resolve Rgt_RoppO Rlt_RoppO: real. (**********) @@ -1016,87 +1016,87 @@ Lemma Rlt_r_plus_R1:(r:R)``0<=r`` -> ``0<r+1``. Intros. Apply Rlt_le_trans with ``1``; Auto with real. Pattern 1 ``1``; Replace ``1`` with ``0+1``; Auto with real. -Save. +Qed. Hints Resolve Rlt_r_plus_R1: real. (**********) Lemma Rlt_r_r_plus_R1:(r:R)``r<r+1``. Intros. Pattern 1 r; Replace r with ``r+0``; Auto with real. -Save. +Qed. Hints Resolve Rlt_r_r_plus_R1: real. (**********) Lemma tech_Rgt_minus:(r1,r2:R)``0<r2``->``r1>r1-r2``. Red; Unfold Rminus; Intros. Pattern 2 r1; Replace r1 with ``r1+0``; Auto with real. -Save. +Qed. (***********) Lemma Rgt_plus_plus_r:(r,r1,r2:R)``r1>r2``->``r+r1 > r+r2``. Unfold Rgt; Auto with real. -Save. +Qed. Hints Resolve Rgt_plus_plus_r : real. (***********) 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. +Qed. (***********) Lemma Rge_plus_plus_r:(r,r1,r2:R)``r1>=r2`` -> ``r+r1 >= r+r2``. Intros; Apply Rle_ge; Auto with real. -Save. +Qed. Hints Resolve Rge_plus_plus_r : real. (***********) 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. +Qed. (***********) Lemma Rge_monotony: (x,y,z:R) ``z>=0`` -> ``x>=y`` -> ``x*z >= y*z``. Intros; Apply Rle_ge; Auto with real. -Save. +Qed. (***********) 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. +Qed. (*********) 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. -Save. +Qed. (**********) 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. +Qed. (*********) 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. -Save. +Qed. (*********) 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. +Qed. (*********) Lemma Rmult_lt_0 :(r1,r2,r3,r4:R)``r3>=0``->``r2>0``->``r1<r2``->``r3<r4``->``r1*r3<r2*r4``. Intros; Apply Rle_lt_trans with ``r2*r3``; Auto with real. -Save. +Qed. (*********) Lemma Rmult_lt_pos:(x,y:R)``0<x`` -> ``0<y`` -> ``0<x*y``. @@ -1108,7 +1108,7 @@ Intros a b [H|H] H0 H1; Auto with real. Absurd ``0<a+b``. Rewrite H1; Auto with real. Replace ``0`` with ``0+0``; Auto with real. -Save. +Qed. Lemma Rplus_eq_R0 @@ -1117,20 +1117,20 @@ 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. +Qed. (***********) 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. +Qed. 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. +Qed. (**********************************************************) @@ -1140,13 +1140,13 @@ Save. (**********) Lemma S_INR:(n:nat)(INR (S n))==``(INR n)+1``. Intro; Case n; Auto with real. -Save. +Qed. (**********) Lemma S_O_plus_INR:(n:nat) (INR (plus (S O) n))==``(INR (S O))+(INR n)``. Intro; Simpl; Case n; Intros; Auto with real. -Save. +Qed. (**********) Lemma plus_INR:(n,m:nat)(INR (plus n m))==``(INR n)+(INR m)``. @@ -1155,7 +1155,7 @@ 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. +Qed. (**********) Lemma minus_INR:(n,m:nat)(le m n)->(INR (minus n m))==``(INR n)-(INR m)``. @@ -1163,7 +1163,7 @@ 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. +Qed. (*********) Lemma mult_INR:(n,m:nat)(INR (mult n m))==(Rmult (INR n) (INR m)). @@ -1171,7 +1171,7 @@ Intros n m; Induction n. Simpl; Auto with real. Intros; Repeat Rewrite S_INR; Simpl. Rewrite plus_INR; Rewrite Hrecn; Ring. -Save. +Qed. Hints Resolve plus_INR minus_INR mult_INR : real. @@ -1179,19 +1179,19 @@ Hints Resolve plus_INR minus_INR mult_INR : real. Lemma lt_INR_0:(n:nat)(lt O n)->``0 < (INR n)``. Induction 1; Intros; Auto with real. Rewrite S_INR; Auto with real. -Save. +Qed. Hints Resolve lt_INR_0: real. Lemma lt_INR:(n,m:nat)(lt n m)->``(INR n) < (INR m)``. Induction 1; Intros; Auto with real. Rewrite S_INR; Auto with real. Rewrite S_INR; Apply Rlt_trans with (INR m0); Auto with real. -Save. +Qed. Hints Resolve lt_INR: real. Lemma INR_lt_1:(n:nat)(lt (S O) n)->``1 < (INR n)``. Intros;Replace ``1`` with (INR (S O));Auto with real. -Save. +Qed. Hints Resolve INR_lt_1: real. (**********) @@ -1199,7 +1199,7 @@ Lemma INR_pos : (p:positive)``0<(INR (convert p))``. Intro; Apply lt_INR_0. Simpl; Auto with real. Apply compare_convert_O. -Save. +Qed. Hints Resolve INR_pos : real. (**********) @@ -1207,7 +1207,7 @@ Lemma pos_INR:(n:nat)``0 <= (INR n)``. Intro n; Case n. Simpl; Auto with real. Auto with arith real. -Save. +Qed. Hints Resolve pos_INR: real. Lemma INR_lt:(n,m:nat)``(INR n) < (INR m)``->(lt n m). @@ -1222,7 +1222,7 @@ Do 2 Rewrite S_INR in H1;Cut ``(INR n1) < (INR n0)``. Intro H2;Generalize (H0 n0 H2);Intro;Auto with arith. Apply (Rlt_anti_compatibility ``1`` (INR n1) (INR n0)). Rewrite Rplus_sym;Rewrite (Rplus_sym ``1`` (INR n0));Trivial. -Save. +Qed. Hints Resolve INR_lt: real. (*********) @@ -1230,7 +1230,7 @@ Lemma le_INR:(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. +Qed. Hints Resolve le_INR: real. (**********) @@ -1238,7 +1238,7 @@ Lemma not_INR_O:(n:nat)``(INR n)<>0``->~n=O. Red; Intros n H H1. Apply H. Rewrite H1; Trivial. -Save. +Qed. Hints Immediate not_INR_O : real. (**********) @@ -1247,7 +1247,7 @@ Intro n; Case n. Intro; Absurd (0)=(0); Trivial. Intros; Rewrite S_INR. Apply Rgt_not_eq; Red; Auto with real. -Save. +Qed. Hints Resolve not_O_INR : real. Lemma not_nm_INR:(n,m:nat)~n=m->``(INR n)<>(INR m)``. @@ -1256,7 +1256,7 @@ Case (le_lt_or_eq ? ? H1); Intros H2. Apply imp_not_Req; Auto with real. ElimType False;Auto. Apply sym_not_eqT; Apply imp_not_Req; Auto with real. -Save. +Qed. Hints Resolve not_nm_INR : real. Lemma INR_eq: (n,m:nat)(INR n)==(INR m)->n=m. @@ -1270,19 +1270,19 @@ Symmetry;Cut ~m=n. Intro H3;Generalize (not_nm_INR m n H3);Intro H4; ElimType False;Auto. Omega. -Save. +Qed. Hints Resolve INR_eq : real. Lemma INR_le: (n, m : nat) (Rle (INR n) (INR m)) -> (le n m). Intros;Elim H;Intro. Generalize (INR_lt n m H0);Intro;Auto with arith. Generalize (INR_eq n m H0);Intro;Rewrite H1;Auto. -Save. +Qed. Hints Resolve INR_le : real. Lemma not_1_INR:(n:nat)~n=(S O)->``(INR n)<>1``. Replace ``1`` with (INR (S O)); Auto with real. -Save. +Qed. Hints Resolve not_1_INR : real. (**********************************************************) @@ -1295,13 +1295,13 @@ Definition INZ:=inject_nat. (**********) Lemma IZN:(z:Z)(`0<=z`)->(Ex [n:nat] z=(INZ n)). Unfold INZ;Intros;Apply inject_nat_complete;Assumption. -Save. +Qed. (**********) Lemma INR_IZR_INZ:(n:nat)(INR n)==(IZR (INZ n)). Induction n; Auto with real. Intros; Simpl; Rewrite bij1; Auto with real. -Save. +Qed. Lemma plus_IZR_NEG_POS : (p,q:positive)(IZR `(POS p)+(NEG q)`)==``(IZR (POS p))+(IZR (NEG q))``. @@ -1319,7 +1319,7 @@ 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. +Qed. (**********) Lemma plus_IZR:(z,t:Z)(IZR `z+t`)==``(IZR z)+(IZR t)``. @@ -1328,7 +1328,7 @@ 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. +Qed. (**********) Lemma mult_IZR:(z,t:Z)(IZR `z*t`)==``(IZR z)*(IZR t)``. @@ -1342,18 +1342,18 @@ Intros t1 z1; Rewrite times_convert; Auto with real. Rewrite Ropp_mul1; Auto with real. Intros t1 z1; Rewrite times_convert; Auto with real. Rewrite Ropp_mul2; Auto with real. -Save. +Qed. (**********) Lemma Ropp_Ropp_IZR:(z:Z)(IZR (`-z`))==``-(IZR z)``. Intro z; Case z; Simpl; Auto with real. -Save. +Qed. (**********) 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. +Qed. (**********) Lemma lt_O_IZR:(z:Z)``0 < (IZR z)``->`0<z`. @@ -1362,7 +1362,7 @@ Absurd ``0<0``; Auto with real. Unfold Zlt; Simpl; Trivial. Case Rlt_le_not with 1:=H. Replace ``0`` with ``-0``; Auto with real. -Save. +Qed. (**********) Lemma lt_IZR:(z1,z2:Z)``(IZR z1)<(IZR z2)``->`z1<z2`. @@ -1370,34 +1370,34 @@ Intros; Apply Zlt_O_minus_lt. Apply lt_O_IZR. Rewrite <- Z_R_minus. Exact (Rgt_minus (IZR z2) (IZR z1) H). -Save. +Qed. (**********) Lemma eq_IZR_R0:(z:Z)``(IZR z)==0``->`z=0`. NewDestruct 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. -Save. +Qed. (**********) Lemma eq_IZR:(z1,z2:Z)(IZR z1)==(IZR z2)->z1=z2. Intros;Generalize (eq_Rminus (IZR z1) (IZR z2) H); Rewrite (Z_R_minus z1 z2);Intro;Generalize (eq_IZR_R0 `z1-z2` H0); Intro;Omega. -Save. +Qed. (**********) Lemma not_O_IZR:(z:Z)`z<>0`->``(IZR z)<>0``. Intros z H; Red; Intros H0; Case H. Apply eq_IZR; Auto. -Save. +Qed. (*********) 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. +Qed. (**********) Lemma le_IZR:(z1,z2:Z)``(IZR z1)<=(IZR z2)``->`z1<=z2`. @@ -1405,31 +1405,31 @@ 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. +Qed. (**********) 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. +Qed. (**********) 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. +Qed. Lemma IZR_le: (m,n:Z) `m<= n` -> ``(IZR m)<=(IZR n)``. Intros;Apply Rgt_not_le;Red;Intro. Unfold Rgt in H0;Generalize (lt_IZR n m H0); Intro; Omega. -Save. +Qed. Lemma IZR_lt: (m,n:Z) `m< n` -> ``(IZR m)<(IZR n)``. Intros;Cut `m<=n`. Intro H0;Elim (IZR_le m n H0);Intro;Auto. Generalize (eq_IZR m n H1);Intro;ElimType False;Omega. Omega. -Save. +Qed. Lemma one_IZR_lt1 : (z:Z)``-1<(IZR z)<1``->`z=0`. Intros z (H1,H2). @@ -1437,7 +1437,7 @@ 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. +Qed. Lemma one_IZR_r_R1 : (r:R)(z,x:Z)``r<(IZR z)<=r+1``->``r<(IZR x)<=r+1``->z=x. @@ -1451,7 +1451,7 @@ Ring. Replace ``1`` with ``(r+1)-r``. Unfold Rminus; Apply Rplus_le_lt_lt; Auto with real. Ring. -Save. +Qed. (**********) @@ -1459,7 +1459,7 @@ 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. +Qed. (**********) Lemma tech_single_z_r_R1 @@ -1467,7 +1467,7 @@ Lemma tech_single_z_r_R1 -> (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. +Qed. (*****************************************************************) (** Definitions of new types *) @@ -1496,12 +1496,12 @@ cond_nonzero : ~``nonzero==0`` }. (**********) Lemma prod_neq_R0 : (x,y:R) ~``x==0``->~``y==0``->~``x*y==0``. Intros; Red; Intro; Generalize (without_div_Od x y H1); Intro; Elim H2; Intro; [Rewrite H3 in H; Elim H | Rewrite H3 in H0; Elim H0]; Reflexivity. -Save. +Qed. (*********) Lemma Rmult_le_pos : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``0<=x*y``. Intros; Rewrite <- (Rmult_Ol x); Rewrite <- (Rmult_sym x); Apply (Rle_monotony x R0 y H H0). -Save. +Qed. (**********************************************************) (** Other rules about < and <= *) @@ -1509,31 +1509,31 @@ Save. Lemma gt0_plus_gt0_is_gt0 : (x,y:R) ``0<x`` -> ``0<y`` -> ``0<x+y``. Intros; Apply Rlt_trans with x; [Assumption | Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rlt_compatibility; Assumption]. -Save. +Qed. Lemma ge0_plus_gt0_is_gt0 : (x,y:R) ``0<=x`` -> ``0<y`` -> ``0<x+y``. Intros; Apply Rle_lt_trans with x; [Assumption | Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rlt_compatibility; Assumption]. -Save. +Qed. Lemma gt0_plus_ge0_is_gt0 : (x,y:R) ``0<x`` -> ``0<=y`` -> ``0<x+y``. Intros; Rewrite <- Rplus_sym; Apply ge0_plus_gt0_is_gt0; Assumption. -Save. +Qed. Lemma ge0_plus_ge0_is_ge0 : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``0<=x+y``. Intros; Apply Rle_trans with x; [Assumption | Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption]. -Save. +Qed. Lemma plus_le_is_le : (x,y,z:R) ``0<=y`` -> ``x+y<=z`` -> ``x<=z``. Intros; Apply Rle_trans with ``x+y``; [Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption | Assumption]. -Save. +Qed. Lemma plus_lt_is_lt : (x,y,z:R) ``0<=y`` -> ``x+y<z`` -> ``x<z``. Intros; Apply Rle_lt_trans with ``x+y``; [Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption | Assumption]. -Save. +Qed. Lemma Rmult_lt2 : (r1,r2,r3,r4:R) ``0<=r1`` -> ``0<=r3`` -> ``r1<r2`` -> ``r3<r4`` -> ``r1*r3<r2*r4``. Intros; Apply Rle_lt_trans with ``r2*r3``; [Apply Rle_monotony_r; [Assumption | Left; Assumption] | Apply Rlt_monotony; [Apply Rle_lt_trans with r1; Assumption | Assumption]]. -Save. +Qed. Lemma le_epsilon : (x,y:R) ((eps : R) ``0<eps``->``x<=y+eps``) -> ``x<=y``. Intros; Elim (total_order x y); Intro. @@ -1564,7 +1564,7 @@ Discriminate. Unfold INR; Reflexivity. Intro; Ring. Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR; Intro; Assumption | Discriminate]. -Save. +Qed. (*****************************************************) (** Complementary results about [INR] *) @@ -1580,8 +1580,8 @@ end. Theorem INR_eq_INR2 : (n:nat) (INR n)==(INR2 n). Induction n; [Unfold INR INR2; Reflexivity | Intros; Unfold INR INR2; Fold INR INR2; Rewrite H; Case n0; [Reflexivity | Intros; Ring]]. -Save. +Qed. Lemma add_auto : (p,q:nat) ``(INR2 (S p))+(INR2 q)==(INR2 p)+(INR2 (S q))``. Intros; Repeat Rewrite <- INR_eq_INR2; Repeat Rewrite S_INR; Ring. -Save.
\ No newline at end of file +Qed.
\ No newline at end of file diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 7ecd0e143a..6698d627b3 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -38,14 +38,14 @@ Unfold Rgt;Unfold Rgt in H;Exact (Rlt_le_trans r r1 r2 H r0). Split. Generalize (not_Rle r1 r2 n);Intro;Exact (Rgt_trans r1 r2 r H0 H). Assumption. -Save. +Qed. (*********) Lemma Rmin_Rgt_r:(r1,r2,r:R)(((Rgt r1 r)/\(Rgt r2 r)) -> (Rgt (Rmin r1 r2) r)). Intros;Unfold Rmin;Case (total_order_Rle r1 r2);Elim H;Clear H;Intros; Assumption. -Save. +Qed. (*********) Lemma Rmin_Rgt:(r1,r2,r:R)(Rgt (Rmin r1 r2) r)<-> @@ -53,22 +53,22 @@ Lemma Rmin_Rgt:(r1,r2,r:R)(Rgt (Rmin r1 r2) r)<-> Intros; Split. Exact (Rmin_Rgt_l r1 r2 r). Exact (Rmin_Rgt_r r1 r2 r). -Save. +Qed. (*********) Lemma Rmin_l : (x,y:R) ``(Rmin x y)<=x``. Intros; Unfold Rmin; Case (total_order_Rle x y); Intro H1; [Right; Reflexivity | Auto with real]. -Save. +Qed. (*********) Lemma Rmin_r : (x,y:R) ``(Rmin x y)<=y``. Intros; Unfold Rmin; Case (total_order_Rle x y); Intro H1; [Assumption | Auto with real]. -Save. +Qed. (*********) Lemma Rmin_stable_in_posreal : (x,y:posreal) ``0<(Rmin x y)``. Intros; Apply Rmin_Rgt_r; Split; [Apply (cond_pos x) | Apply (cond_pos y)]. -Save. +Qed. (*******************************) (** Rmax *) @@ -90,21 +90,21 @@ Intro;Unfold Rmax;Case (total_order_Rle r1 r2);Elim H;Clear H;Intros;Auto. Apply (Rle_trans r r1 r2);Auto. Generalize (not_Rle r1 r2 n);Clear n;Intro;Unfold Rgt in H0; Apply (Rlt_le r r1 (Rle_lt_trans r r2 r1 H H0)). -Save. +Qed. Lemma RmaxLess1: (r1, r2 : R) (Rle r1 (Rmax r1 r2)). Intros r1 r2; Unfold Rmax; Case (total_order_Rle r1 r2); Auto with real. -Save. +Qed. Lemma RmaxLess2: (r1, r2 : R) (Rle r2 (Rmax r1 r2)). Intros r1 r2; Unfold Rmax; Case (total_order_Rle r1 r2); Auto with real. -Save. +Qed. Lemma RmaxSym: (p, q : R) (Rmax p q) == (Rmax q p). Intros p q; Unfold Rmax; Case (total_order_Rle p q); Case (total_order_Rle q p); Auto; Intros H1 H2; Apply Rle_antisym; Auto with real. -Save. +Qed. Lemma RmaxRmult: (p, q, r : R) @@ -119,11 +119,11 @@ Case H; Intros E1. Case H2; Auto with real. Apply Rle_monotony_contra with z := r; Auto. Rewrite <- E1; Repeat Rewrite Rmult_Ol; Auto. -Save. +Qed. Lemma Rmax_stable_in_negreal : (x,y:negreal) ``(Rmax x y)<0``. Intros; Unfold Rmax; Case (total_order_Rle x y); Intro; [Apply (cond_neg y) | Apply (cond_neg x)]. -Save. +Qed. (*******************************) (** Rabsolu *) @@ -134,7 +134,7 @@ Lemma case_Rabsolu:(r:R)(sumboolT (Rlt r R0) (Rge r R0)). Intro;Generalize (total_order_Rle R0 r);Intro;Elim X;Intro;Clear X. Right;Apply (Rle_sym1 R0 r a). Left;Fold (Rgt R0 r);Apply (not_Rle R0 r b). -Save. +Qed. (*********) Definition Rabsolu:R->R:= @@ -147,25 +147,25 @@ Definition Rabsolu:R->R:= Lemma Rabsolu_R0:(Rabsolu R0)==R0. Unfold Rabsolu;Case (case_Rabsolu R0);Auto;Intro. Generalize (Rlt_antirefl R0);Intro;ElimType False;Auto. -Save. +Qed. Lemma Rabsolu_R1: (Rabsolu R1)==R1. Unfold Rabsolu; Case (case_Rabsolu R1); Auto with real. Intros H; Absurd ``1 < 0``;Auto with real. -Save. +Qed. (*********) Lemma Rabsolu_no_R0:(r:R)~r==R0->~(Rabsolu r)==R0. Intros;Unfold Rabsolu;Case (case_Rabsolu r);Intro;Auto. Apply Ropp_neq;Auto. -Save. +Qed. (*********) Lemma Rabsolu_left: (r:R)(Rlt r R0)->((Rabsolu r) == (Ropp r)). Intros;Unfold Rabsolu;Case (case_Rabsolu r);Trivial;Intro;Absurd (Rge r R0). Exact (Rlt_ge_not r R0 H). Assumption. -Save. +Qed. (*********) Lemma Rabsolu_right: (r:R)(Rge r R0)->((Rabsolu r) == r). @@ -174,13 +174,13 @@ Absurd (Rge r R0). Exact (Rlt_ge_not r R0 r0). Assumption. Trivial. -Save. +Qed. Lemma Rabsolu_left1: (a : R) (Rle a R0) -> (Rabsolu a) == (Ropp a). Intros a H; Case H; Intros H1. Apply Rabsolu_left; Auto. Rewrite H1; Simpl; Rewrite Rabsolu_right; Auto with real. -Save. +Qed. (*********) Lemma Rabsolu_pos:(x:R)(Rle R0 (Rabsolu x)). @@ -188,23 +188,23 @@ Intros;Unfold Rabsolu;Case (case_Rabsolu x);Intro. Generalize (Rlt_Ropp x R0 r);Intro;Unfold Rgt in H; Rewrite Ropp_O in H;Unfold Rle;Left;Assumption. Apply Rle_sym2;Assumption. -Save. +Qed. Lemma Rle_Rabsolu: (x:R) (Rle x (Rabsolu x)). Intro; Unfold Rabsolu;Case (case_Rabsolu x);Intros;Fourier. -Save. +Qed. (*********) Lemma Rabsolu_pos_eq:(x:R)(Rle R0 x)->(Rabsolu x)==x. Intros;Unfold Rabsolu;Case (case_Rabsolu x);Intro; [Generalize (Rle_not R0 x r);Intro;ElimType False;Auto|Trivial]. -Save. +Qed. (*********) Lemma Rabsolu_Rabsolu:(x:R)(Rabsolu (Rabsolu x))==(Rabsolu x). Intro;Apply (Rabsolu_pos_eq (Rabsolu x) (Rabsolu_pos x)). -Save. +Qed. (*********) Lemma Rabsolu_pos_lt:(x:R)(~x==R0)->(Rlt R0 (Rabsolu x)). @@ -214,7 +214,7 @@ ElimType False;Clear H0;Elim H;Clear H;Generalize H1; Unfold Rabsolu;Case (case_Rabsolu x);Intros;Auto. Clear r H1; Generalize (Rplus_plus_r x R0 (Ropp x) H0); Rewrite (let (H1,H2)=(Rplus_ne x) in H1);Rewrite (Rplus_Ropp_r x);Trivial. -Save. +Qed. (*********) Lemma Rabsolu_minus_sym:(x,y:R) @@ -232,7 +232,7 @@ Generalize (Rgt_RoppO (Rminus x y) H);Rewrite (Ropp_distr2 x y); Rewrite (Rminus_eq x y H);Trivial. Rewrite (Rminus_eq y x H0);Trivial. Rewrite (Rminus_eq y x H0);Trivial. -Save. +Qed. (*********) Lemma Rabsolu_mult:(x,y:R) @@ -277,7 +277,7 @@ Generalize (imp_not_Req y R0 (or_introl (Rlt y R0) (Rgt y R0) r)); Rewrite H0 in H;Rewrite (Rmult_Ol y) in H;Unfold Rgt in H; Generalize (Rlt_antirefl R0);Intro;ElimType False;Auto. Rewrite H0;Rewrite (Rmult_Ol y);Rewrite (Rmult_Ol (Ropp y));Trivial. -Save. +Qed. (*********) Lemma Rabsolu_Rinv:(r:R)(~r==R0)->(Rabsolu (Rinv r))== @@ -296,7 +296,7 @@ Unfold Rge in r1;Elim r1;Clear r1;Intro. Unfold Rgt in H0;Generalize (Rlt_antisym R0 (Rinv r) (Rlt_Rinv r H0));Intro;ElimType False;Auto. ElimType False;Auto. -Save. +Qed. Lemma Rabsolu_Ropp: (x:R) (Rabsolu (Ropp x))==(Rabsolu x). @@ -315,7 +315,7 @@ Intro;Generalize (Rle_not R1 R0 Rlt_R0_R1);Intro; Generalize (Rle_sym2 R1 R0 H2);Intro; ElimType False;Auto. Ring. -Save. +Qed. (*********) Lemma Rabsolu_triang:(a,b:R)(Rle (Rabsolu (Rplus a b)) @@ -376,7 +376,7 @@ Apply (Rle_compatibility a b (Ropp b)); Apply (Rlt_le (Rplus b b) R0 H0). (**) Unfold Rle;Right;Reflexivity. -Save. +Qed. (*********) Lemma Rabsolu_triang_inv:(a,b:R)(Rle (Rminus (Rabsolu a) (Rabsolu b)) @@ -397,7 +397,7 @@ Intros; Rewrite (Rplus_assoc b a (Ropp b)). Exact (Rabsolu_triang b (Rplus a (Ropp b))). Rewrite (proj1 ? ? (Rplus_ne a));Trivial. -Save. +Qed. (*********) Lemma Rabsolu_def1:(x,a:R)(Rlt x a)->(Rlt (Ropp a) x)->(Rlt (Rabsolu x) a). @@ -405,7 +405,7 @@ Unfold Rabsolu;Intros;Case (case_Rabsolu x);Intro. Generalize (Rlt_Ropp (Ropp a) x H0);Unfold Rgt;Rewrite Ropp_Ropp;Intro; Assumption. Assumption. -Save. +Qed. (*********) Lemma Rabsolu_def2:(x,a:R)(Rlt (Rabsolu x) a)->(Rlt x a)/\(Rlt (Ropp a) x). @@ -418,7 +418,7 @@ Fold (Rgt a x) in H;Generalize (Rgt_ge_trans a x R0 H r);Intro; Generalize (Rgt_RoppO a H0);Intro;Fold (Rgt R0 (Ropp a)); Generalize (Rge_gt_trans x R0 (Ropp a) r H1);Unfold Rgt;Intro;Split; Assumption. -Save. +Qed. Lemma RmaxAbs: (p, q, r : R) @@ -443,7 +443,7 @@ Apply RmaxLess1; Auto. Rewrite (Rabsolu_left r); Auto. Apply Rle_trans with (Ropp p); Auto with real. Apply RmaxLess1; Auto. -Save. +Qed. Lemma Rabsolu_Zabs: (z : Z) (Rabsolu (IZR z)) == (IZR (Zabs z)). Intros z; Case z; Simpl; Auto with real. @@ -451,5 +451,5 @@ Apply Rabsolu_right; Auto with real. Intros p0; Apply Rabsolu_right; Auto with real zarith. Intros p0; Rewrite Rabsolu_Ropp. Apply Rabsolu_right; Auto with real zarith. -Save. +Qed. diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 5e4cf7ac57..37fa2aa77e 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -198,7 +198,7 @@ Intro;Generalize (Rlt_antisym R0 (Rplus R1 R1) H7);Intro;ElimType False; Fourier. Apply Rabsolu_no_R0. DiscrR. -Save. +Qed. (*********) @@ -212,7 +212,7 @@ Intros;Rewrite (eq_Rminus y y (refl_eqT R y)); Absurd (Rlt R0 R0);Auto. Red;Intro;Apply (Rlt_antirefl R0 H1). Unfold Rgt in H0;Assumption. -Save. +Qed. (*********) Lemma Dx:(D:R->Prop)(x0:R)(D_in [x:R]x [x:R]R1 D x0). @@ -228,7 +228,7 @@ Intros;Elim H0;Clear H0;Intros;Unfold D_x in H0; Absurd (Rlt R0 R0);Auto. Red;Intro;Apply (Rlt_antirefl R0 r). Unfold Rgt in H;Assumption. -Save. +Qed. (*********) Lemma Dadd:(D:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R) @@ -252,7 +252,7 @@ Unfold D_in;Intros;Generalize (limit_plus (Rminus (Rplus (f x1) (g x1)) (Rplus (f x0) (g x0))). Intro;Rewrite H3 in H1;Assumption. Ring. -Save. +Qed. (*********) Lemma Dmult:(D:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R) @@ -298,7 +298,7 @@ Ring. Unfold limit1_in;Unfold limit_in;Simpl;Intros; Split with eps;Split;Auto;Intros;Elim (R_dist_refl (g x0) (g x0)); Intros a b;Rewrite (b (refl_eqT R (g x0)));Unfold Rgt in H;Assumption. -Save. +Qed. (*********) Lemma Dmult_const:(D:R->Prop)(f,df:R->R)(x0:R)(a:R)(D_in f df D x0)-> @@ -308,7 +308,7 @@ Intros;Generalize (Dmult D [_:R]R0 df [_:R]a f x0 (Dconst D a x0) H); Rewrite (Rmult_Ol (f x0)) in H0; Rewrite (let (H1,H2)=(Rplus_ne (Rmult a (df x0))) in H2) in H0; Assumption. -Save. +Qed. (*********) Lemma Dopp:(D:R->Prop)(f,df:R->R)(x0:R)(D_in f df D x0)-> @@ -322,7 +322,7 @@ Intros;Generalize (H2 x1 H3);Clear H2;Intro;Rewrite Ropp_mul1 in H2; Rewrite (let (H1,H2)=(Rmult_ne (f x1)) in H2) in H2; Rewrite (let (H1,H2)=(Rmult_ne (f x0)) in H2) in H2; Rewrite (let (H1,H2)=(Rmult_ne (df x0)) in H2) in H2;Assumption. -Save. +Qed. (*********) Lemma Dminus:(D:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R) @@ -330,7 +330,7 @@ Lemma Dminus:(D:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R) (D_in [x:R](Rminus (f x) (g x)) [x:R](Rminus (df x) (dg x)) D x0). Unfold Rminus;Intros;Generalize (Dopp D g dg x0 H0);Intro; Apply (Dadd D df [x:R](Ropp (dg x)) f [x:R](Ropp (g x)) x0);Assumption. -Save. +Qed. (*********) Lemma Dx_pow_n:(n:nat)(D:R->Prop)(x0:R) @@ -360,7 +360,7 @@ Rewrite cond in H2;Rewrite cond;Simpl in H2;Simpl; Cut ~(n0=O)->(S (minus n0 (1)))=n0;[Intro|Omega]; Rewrite (H3 cond) in H2; Rewrite (Rmult_sym (pow x0 n0) (INR n0)) in H2; Rewrite (tech_pow_Rplus x0 n0 n0) in H2; Assumption. -Save. +Qed. (*********) Lemma Dcomp:(Df,Dg:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R) @@ -428,7 +428,7 @@ Clear H5 H3 H4 H2;Unfold limit1_in;Unfold limit_in;Simpl; Split with x;Split;Auto;Intros;Unfold D_x Dgf in H4 H3; Elim H4;Clear H4;Intros;Elim H4;Clear H4;Intros; Exact (H3 x1 (conj (Df x1)/\~x0==x1 (Rlt (R_dist x1 x0) x) H4 H5)). -Save. +Qed. (*********) Lemma D_pow_n:(n:nat)(D:R->Prop)(x0:R)(expr,dexpr:R->R) @@ -445,5 +445,5 @@ Intros n D x0 expr dexpr H; Cut ``((dexpr x0)*((INR n)*(pow (expr x0) (minus n (S O)))))== ((INR n)*(pow (expr x0) (minus n (S O)))*(dexpr x0))``; [Intro Rew;Rewrite <- Rew;Exact (H2 x1 H3)|Ring]. -Save. +Qed. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 90f297bbd4..7bb1236adb 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -41,12 +41,12 @@ Intro;Apply H;Assumption. Replace (plus n0 (1)) with (S n0);[Auto|Ring]. Intros;Ring. Double Induction 1 2;Simpl;Auto. -Save. +Qed. (*********) Lemma INR_fact_neq_0:(n:nat)~(INR (fact n))==R0. Intro;Red;Intro;Apply (not_O_INR (fact n) (fact_neq_0 n));Assumption. -Save. +Qed. (*********) Lemma simpl_fact:(n:nat)(Rmult (Rinv (INR (fact (S n)))) @@ -61,7 +61,7 @@ Rewrite (Rmult_assoc (Rinv (INR (S n))) (Rinv (INR (fact n))) Apply (let (H1,H2)=(Rmult_ne (Rinv (INR (S n)))) in H1). Apply not_O_INR;Auto. Apply INR_fact_neq_0. -Save. +Qed. (*******************************) (* Power *) @@ -75,17 +75,17 @@ Fixpoint pow [r:R;n:nat]:R:= Lemma pow_O: (e : R) (pow e O) == R1. Simpl; Auto with real. -Save. +Qed. Lemma pow_1: (e : R) (pow e (1)) == e. Simpl; Auto with real. -Save. +Qed. Lemma pow_add: (e : R) (n, m : nat) (pow e (plus n m)) == (Rmult (pow e n) (pow e m)). Intros e n; Elim n; Simpl; Auto with real. Intros n0 H' m; Rewrite H'; Auto with real. -Save. +Qed. Lemma pow_nonzero: (x:R) (n:nat) ~(x==R0) -> ~((pow x n)==R0). @@ -94,7 +94,7 @@ Intro; Red;Intro;Apply R1_neq_R0;Assumption. Intros;Red; Intro;Elim (without_div_Od x (pow x n0) H1). Intro; Auto. Apply H;Assumption. -Save. +Qed. Hints Resolve pow_O pow_1 pow_add pow_nonzero:real. @@ -105,12 +105,12 @@ Lemma pow_RN_plus: Intros e n; Elim n; Simpl; Auto with real. Intros n0 H' m H'0. Rewrite Rmult_assoc; Rewrite <- H'; Auto. -Save. +Qed. Lemma pow_lt: (e : R) (n : nat) (Rlt R0 e) -> (Rlt R0 (pow e n)). Intros e n; Elim n; Simpl; Auto with real. Intros n0 H' H'0; Replace R0 with (Rmult e R0); Auto with real. -Save. +Qed. Hints Resolve pow_lt :real. Lemma Rlt_pow_R1: @@ -125,7 +125,7 @@ Apply Rlt_trans with r2 := (Rmult e R1); Auto with real. Apply Rlt_monotony; Auto with real. Apply Rlt_trans with r2 := R1; Auto with real. Apply H'; Auto with arith. -Save. +Qed. Hints Resolve Rlt_pow_R1 :real. Lemma Rlt_pow: @@ -145,13 +145,13 @@ Apply Rlt_pow_R1; Auto with arith. Apply simpl_lt_plus_l with p := n; Auto with arith. Rewrite le_plus_minus_r; Auto with arith; Rewrite <- plus_n_O; Auto. Rewrite plus_sym; Auto with arith. -Save. +Qed. Hints Resolve Rlt_pow :real. (*********) Lemma tech_pow_Rmult:(x:R)(n:nat)(Rmult x (pow x n))==(pow x (S n)). Induction n; Simpl; Trivial. -Save. +Qed. (*********) Lemma tech_pow_Rplus:(x:R)(a,n:nat) @@ -163,7 +163,7 @@ Intros; Pattern 1 (pow x a); Rewrite <- (Rmult_Rplus_distr (pow x a) R1 (INR n)); Rewrite (Rplus_sym R1 (INR n)); Rewrite <-(S_INR n); Apply Rmult_sym. -Save. +Qed. Lemma poly: (n:nat)(e:R)(Rlt R0 e)-> (Rle (Rplus R1 (Rmult (INR n) e)) (pow (Rplus R1 e) n)). @@ -195,7 +195,7 @@ Rewrite Rplus_sym; Apply (Rlt_r_plus_R1 e (Rlt_le R0 e H)). Assumption. Rewrite H1;Unfold Rle;Right;Trivial. -Save. +Qed. Lemma Power_monotonic: (x:R) (m,n:nat) (Rgt (Rabsolu x) R1) @@ -216,14 +216,14 @@ Apply Rle_monotony. Apply Rabsolu_pos. Unfold Rgt in H. Apply Rlt_le; Assumption. -Save. +Qed. Lemma Pow_Rabsolu: (x:R) (n:nat) (pow (Rabsolu x) n)==(Rabsolu (pow x n)). Intro;Induction n;Simpl. Apply sym_eqT;Apply Rabsolu_pos_eq;Apply Rlt_le;Apply Rlt_R0_R1. Intros; Rewrite H;Apply sym_eqT;Apply Rabsolu_mult. -Save. +Qed. Lemma Pow_x_infinity: @@ -281,7 +281,7 @@ Exists O;Apply (Rge_trans (INR (0)) Rewrite INR_IZR_INZ;Apply IZR_ge;Simpl;Omega. Unfold Rge; Left; Assumption. Omega. -Save. +Qed. Lemma pow_ne_zero: (n:nat) ~(n=(0))-> (pow R0 n) == R0. @@ -289,7 +289,7 @@ Induction n. Simpl;Auto. Intros;Elim H;Reflexivity. Intros; Simpl;Apply Rmult_Ol. -Save. +Qed. Lemma Rinv_pow: (x:R) (n:nat) ~(x==R0) -> (Rinv (pow x n))==(pow (Rinv x) n). @@ -299,7 +299,7 @@ Intro m;Intro;Rewrite Rinv_Rmult. Rewrite H0; Reflexivity;Assumption. Assumption. Apply pow_nonzero;Assumption. -Save. +Qed. Lemma pow_lt_1_zero: (x:R) (Rlt (Rabsolu x) R1) @@ -353,7 +353,7 @@ Rewrite Rinv_R1; Apply Rlt_R0_R1. Rewrite Rinv_R1; Assumption. Assumption. Red;Intro; Apply R1_neq_R0;Assumption. -Save. +Qed. Lemma pow_R1: (r : R) (n : nat) (pow r n) == R1 -> (Rabsolu r) == R1 \/ n = O. @@ -389,7 +389,7 @@ Absurd (Rlt (pow (Rabsolu r) O) (pow (Rabsolu r) (S n0))); Repeat Rewrite Pow_Rabsolu; Rewrite H'0; Simpl; Auto with real. Red;Intro;Absurd ``(pow r (S n0)) == 1``;Auto. Simpl; Rewrite H; Rewrite Rmult_Ol; Auto with real. -Save. +Qed. (*******************************) (** PowerRZ *) @@ -409,19 +409,19 @@ Definition powerRZ := Lemma Zpower_NR0: (e : Z) (n : nat) (Zle ZERO e) -> (Zle ZERO (Zpower_nat e n)). Intros e n; Elim n; Unfold Zpower_nat; Simpl; Auto with zarith. -Save. +Qed. Lemma powerRZ_O: (e : R) (powerRZ e ZERO) == R1. Simpl; Auto. -Save. +Qed. Lemma powerRZ_1: (e : R) (powerRZ e (Zs ZERO)) == e. Simpl; Auto with real. -Save. +Qed. Lemma powerRZ_NOR: (e : R) (z : Z) ~ e == R0 -> ~ (powerRZ e z) == R0. Intros e z; Case z; Simpl; Auto with real. -Save. +Qed. Lemma powerRZ_add: (e : R) @@ -469,7 +469,7 @@ Intros H'; Rewrite pow_add; Auto with real. Apply Rinv_Rmult; Auto. Apply pow_nonzero; Auto. Apply pow_nonzero; Auto. -Save. +Qed. Hints Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add :real. Lemma Zpower_nat_powerRZ: @@ -485,16 +485,16 @@ Rewrite H'; Simpl. Case m1; Simpl; Auto with real. Intros m2; Rewrite bij1; Auto. Unfold Zpower_nat; Auto. -Save. +Qed. Lemma powerRZ_lt: (e : R) (z : Z) (Rlt R0 e) -> (Rlt R0 (powerRZ e z)). Intros e z; Case z; Simpl; Auto with real. -Save. +Qed. Hints Resolve powerRZ_lt :real. Lemma powerRZ_le: (e : R) (z : Z) (Rlt R0 e) -> (Rle R0 (powerRZ e z)). Intros e z H'; Apply Rlt_le; Auto with real. -Save. +Qed. Hints Resolve powerRZ_le :real. Lemma Zpower_nat_powerRZ_absolu: @@ -505,7 +505,7 @@ Intros p H'; Elim (convert p); Simpl; Auto with zarith. Intros n0 H'0; Rewrite <- H'0; Simpl; Auto with zarith. Rewrite <- mult_IZR; Auto. Intros p H'; Absurd `0 <= (NEG p)`;Auto with zarith. -Save. +Qed. Lemma powerRZ_R1: (n : Z) (powerRZ R1 n) == R1. Intros n; Case n; Simpl; Auto. @@ -514,7 +514,7 @@ Intros p; Elim (convert p); Simpl. Exact Rinv_R1. Intros n1 H'; Rewrite Rinv_Rmult; Try Rewrite Rinv_R1; Try Rewrite H'; Auto with real. -Save. +Qed. (*******************************) (** Sum of n first naturals *) @@ -561,7 +561,7 @@ Ring. Rewrite Rmult_Rplus_distrl;Rewrite Hrecn;Cut (plus n (1))=(S n). Intro H;Rewrite H;Simpl;Ring. Omega. -Save. +Qed. Lemma sum_f_R0_triangle: (x:nat->R)(n:nat) (Rle (Rabsolu (sum_f_R0 x n)) @@ -578,7 +578,7 @@ Apply Rabsolu_triang. Rewrite Rplus_sym;Rewrite (Rplus_sym (sum_f_R0 [i:nat](Rabsolu (x i)) m) (Rabsolu (x (S m)))); Apply Rle_compatibility;Assumption. -Save. +Qed. (*******************************) diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index c9fec070b4..5f357f307c 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -17,19 +17,19 @@ Definition dist_euc [x0,y0,x1,y1:R] : R := ``(sqrt ((Rsqr (x0-x1))+(Rsqr (y0-y1) Lemma distance_refl : (x0,y0:R) ``(dist_euc x0 y0 x0 y0)==0``. Intros x0 y0; Unfold dist_euc; Apply Rsqr_inj; [Apply foo; Apply ge0_plus_ge0_is_ge0; [Apply pos_Rsqr | Apply pos_Rsqr] | Right; Reflexivity | Rewrite Rsqr_O; Rewrite Rsqr_sqrt; [Unfold Rsqr; Ring | Apply ge0_plus_ge0_is_ge0; [Apply pos_Rsqr | Apply pos_Rsqr]]]. -Save. +Qed. Lemma distance_symm : (x0,y0,x1,y1:R) ``(dist_euc x0 y0 x1 y1) == (dist_euc x1 y1 x0 y0)``. Intros x0 y0 x1 y1; Unfold dist_euc; Apply Rsqr_inj; [ Apply foo; Apply ge0_plus_ge0_is_ge0 | Apply foo; Apply ge0_plus_ge0_is_ge0 | Repeat Rewrite Rsqr_sqrt; [Unfold Rsqr; Ring | Apply ge0_plus_ge0_is_ge0 |Apply ge0_plus_ge0_is_ge0]]; Apply pos_Rsqr. -Save. +Qed. Lemma law_cosines : (x0,y0,x1,y1,x2,y2,ac:R) let a = (dist_euc x1 y1 x0 y0) in let b=(dist_euc x2 y2 x0 y0) in let c=(dist_euc x2 y2 x1 y1) in ( ``a*c*(cos ac) == ((x0-x1)*(x2-x1) + (y0-y1)*(y2-y1))`` -> ``(Rsqr b)==(Rsqr c)+(Rsqr a)-2*(a*c*(cos ac))`` ). Unfold dist_euc; Intros; Repeat Rewrite -> Rsqr_sqrt; [ Rewrite H; Unfold Rsqr; Ring | Apply ge0_plus_ge0_is_ge0 | Apply ge0_plus_ge0_is_ge0 | Apply ge0_plus_ge0_is_ge0]; Apply pos_Rsqr. -Save. +Qed. Lemma triangle : (x0,y0,x1,y1,x2,y2:R) ``(dist_euc x0 y0 x1 y1)<=(dist_euc x0 y0 x2 y2)+(dist_euc x2 y2 x1 y1)``. Intros; Unfold dist_euc; Apply Rsqr_incr_0; [Rewrite Rsqr_plus; Repeat Rewrite Rsqr_sqrt; [Replace ``(Rsqr (x0-x1))`` with ``(Rsqr (x0-x2))+(Rsqr (x2-x1))+2*(x0-x2)*(x2-x1)``; [Replace ``(Rsqr (y0-y1))`` with ``(Rsqr (y0-y2))+(Rsqr (y2-y1))+2*(y0-y2)*(y2-y1)``; [Apply Rle_anti_compatibility with ``-(Rsqr (x0-x2))-(Rsqr (x2-x1))-(Rsqr (y0-y2))-(Rsqr (y2-y1))``; Replace `` -(Rsqr (x0-x2))-(Rsqr (x2-x1))-(Rsqr (y0-y2))-(Rsqr (y2-y1))+((Rsqr (x0-x2))+(Rsqr (x2-x1))+2*(x0-x2)*(x2-x1)+((Rsqr (y0-y2))+(Rsqr (y2-y1))+2*(y0-y2)*(y2-y1)))`` with ``2*((x0-x2)*(x2-x1)+(y0-y2)*(y2-y1))``; [Replace ``-(Rsqr (x0-x2))-(Rsqr (x2-x1))-(Rsqr (y0-y2))-(Rsqr (y2-y1))+((Rsqr (x0-x2))+(Rsqr (y0-y2))+((Rsqr (x2-x1))+(Rsqr (y2-y1)))+2*(sqrt ((Rsqr (x0-x2))+(Rsqr (y0-y2))))*(sqrt ((Rsqr (x2-x1))+(Rsqr (y2-y1)))))`` with ``2*((sqrt ((Rsqr (x0-x2))+(Rsqr (y0-y2))))*(sqrt ((Rsqr (x2-x1))+(Rsqr (y2-y1)))))``; [Apply Rle_monotony; [Left; Cut ~(O=(2)); [Intros; Generalize (lt_INR_0 (2) (neq_O_lt (2) H)); Intro H0; Assumption | Discriminate] | Apply sqrt_cauchy] | Ring] | Ring] | SqRing] | SqRing] | Apply ge0_plus_ge0_is_ge0; Apply pos_Rsqr | Apply ge0_plus_ge0_is_ge0; Apply pos_Rsqr | Apply ge0_plus_ge0_is_ge0; Apply pos_Rsqr] | Apply foo; Apply ge0_plus_ge0_is_ge0; Apply pos_Rsqr | Apply ge0_plus_ge0_is_ge0; Apply foo; Apply ge0_plus_ge0_is_ge0; Apply pos_Rsqr]. -Save. +Qed. (******************************************************************) (** Translation *) @@ -40,11 +40,11 @@ Definition yt[y,ty:R] : R := ``y+ty``. Lemma translation_0 : (x,y:R) ``(xt x 0)==x``/\``(yt y 0)==y``. Intros x y; Split; [Unfold xt | Unfold yt]; Ring. -Save. +Qed. Lemma isometric_translation : (x1,x2,y1,y2,tx,ty:R) ``(Rsqr (x1-x2))+(Rsqr (y1-y2))==(Rsqr ((xt x1 tx)-(xt x2 tx)))+(Rsqr ((yt y1 ty)-(yt y2 ty)))``. Intros; Unfold Rsqr xt yt; Ring. -Save. +Qed. (******************************************************************) (** Rotation *) @@ -55,19 +55,19 @@ Definition yr [x,y,theta:R] : R := ``-x*(sin theta)+y*(cos theta)``. Lemma rotation_0 : (x,y:R) ``(xr x y 0)==x`` /\ ``(yr x y 0)==y``. Intros x y; Unfold xr yr; Split; Rewrite cos_0; Rewrite sin_0; Ring. -Save. +Qed. Lemma rotation_PI2 : (x,y:R) ``(xr x y PI/2)==y`` /\ ``(yr x y PI/2)==-x``. Intros x y; Unfold xr yr; Split; Rewrite cos_PI2; Rewrite sin_PI2; Ring. -Save. +Qed. Lemma isometric_rotation_0 : (x1,y1,x2,y2,theta:R) ``(Rsqr (x1-x2))+(Rsqr (y1-y2)) == (Rsqr ((xr x1 y1 theta))-(xr x2 y2 theta)) + (Rsqr ((yr x1 y1 theta))-(yr x2 y2 theta))``. Intros; Unfold xr yr; Replace ``x1*(cos theta)+y1*(sin theta)-(x2*(cos theta)+y2*(sin theta))`` with ``(cos theta)*(x1-x2)+(sin theta)*(y1-y2)``; [Replace ``-x1*(sin theta)+y1*(cos theta)-( -x2*(sin theta)+y2*(cos theta))`` with ``(cos theta)*(y1-y2)+(sin theta)*(x2-x1)``; [Repeat Rewrite Rsqr_plus; Repeat Rewrite Rsqr_times; Repeat Rewrite cos2; Ring; Replace ``x2-x1`` with ``-(x1-x2)``; [Rewrite <- Rsqr_neg; Ring | Ring] |Ring] | Ring]. -Save. +Qed. Lemma isometric_rotation : (x1,y1,x2,y2,theta:R) ``(dist_euc x1 y1 x2 y2) == (dist_euc (xr x1 y1 theta) (yr x1 y1 theta) (xr x2 y2 theta) (yr x2 y2 theta))``. Unfold dist_euc; Intros; Apply Rsqr_inj; [Apply foo; Apply ge0_plus_ge0_is_ge0 | Apply foo; Apply ge0_plus_ge0_is_ge0 | Repeat Rewrite Rsqr_sqrt; [ Apply isometric_rotation_0 | Apply ge0_plus_ge0_is_ge0 | Apply ge0_plus_ge0_is_ge0]]; Apply pos_Rsqr. -Save. +Qed. (******************************************************************) (** Similarity *) @@ -75,8 +75,8 @@ Save. Lemma isometric_rot_trans : (x1,y1,x2,y2,tx,ty,theta:R) ``(Rsqr (x1-x2))+(Rsqr (y1-y2)) == (Rsqr ((xr (xt x1 tx) (yt y1 ty) theta)-(xr (xt x2 tx) (yt y2 ty) theta))) + (Rsqr ((yr (xt x1 tx) (yt y1 ty) theta)-(yr (xt x2 tx) (yt y2 ty) theta)))``. Intros; Rewrite <- isometric_rotation_0; Apply isometric_translation. -Save. +Qed. Lemma isometric_trans_rot : (x1,y1,x2,y2,tx,ty,theta:R) ``(Rsqr (x1-x2))+(Rsqr (y1-y2)) == (Rsqr ((xt (xr x1 y1 theta) tx)-(xt (xr x2 y2 theta) tx))) + (Rsqr ((yt (yr x1 y1 theta) ty)-(yt (yr x2 y2 theta) ty)))``. Intros; Rewrite <- isometric_translation; Apply isometric_rotation_0. -Save. +Qed. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index dfab20d09d..7b8d1100ac 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -23,16 +23,16 @@ Require SplitAbsolu. (** Modif **) Lemma double : (x:R) ``2*x==x+x``. Intro; Ring. -Save. +Qed. Lemma aze : ``2<>0``. DiscrR. -Save. +Qed. Lemma double_var : (x:R) ``x == x/2 + x/2``. Intro; Rewrite <- double; Unfold Rdiv; Rewrite <- Rmult_assoc; Symmetry; Apply Rinv_r_simpl_m. Apply aze. -Save. +Qed. (*******************************) (* Calculus *) @@ -41,7 +41,7 @@ Save. Lemma eps2_Rgt_R0:(eps:R)(Rgt eps R0)-> (Rgt (Rmult eps (Rinv (Rplus R1 R1))) R0). Intros;Fourier. -Save. +Qed. (*********) Lemma eps2:(eps:R)(Rplus (Rmult eps (Rinv (Rplus R1 R1))) @@ -50,7 +50,7 @@ Intro esp. Assert H := (double_var esp). Unfold Rdiv in H. Symmetry; Exact H. -Save. +Qed. (*********) Lemma eps4:(eps:R) @@ -68,7 +68,7 @@ Reflexivity. Apply aze. Apply aze. Ring. -Save. +Qed. (*********) Lemma Rlt_eps2_eps:(eps:R)(Rgt eps R0)-> @@ -83,7 +83,7 @@ Fourier. Rewrite Rmult_1r; Rewrite <- Rinv_r_sym. Fourier. DiscrR. -Save. +Qed. (*********) Lemma Rlt_eps4_eps:(eps:R)(Rgt eps R0)-> @@ -102,7 +102,7 @@ Rewrite Rmult_1r; Rewrite <- Rinv_r_sym. Fourier. DiscrR. Ring. -Save. +Qed. (*********) Lemma prop_eps:(r:R)((eps:R)(Rgt eps R0)->(Rlt r eps))->(Rle r R0). @@ -112,7 +112,7 @@ Elim H0; Intro. Apply eq_Rle; Assumption. Clear H0;Generalize (H r H1); Intro;Generalize (Rlt_antirefl r); Intro;ElimType False; Auto. -Save. +Qed. (*********) Definition mul_factor := [l,l':R](Rinv (Rplus R1 (Rplus (Rabsolu l) @@ -129,7 +129,7 @@ Exact (Rle_trans ? ? ?). Exact (Rabsolu_pos (Rplus l l')). Exact (Rabsolu_triang ? ?). Exact Rlt_R0_R1. -Save. +Qed. (*********) Lemma mul_factor_gt:(eps:R)(l,l':R)(Rgt eps R0)-> @@ -150,7 +150,7 @@ Exact (Rle_trans ? ? ?). Exact (Rabsolu_pos ?). Exact (Rabsolu_triang ? ?). Rewrite (proj1 ? ? (Rplus_ne R1));Trivial. -Save. +Qed. (*********) Lemma mul_factor_gt_f:(eps:R)(l,l':R)(Rgt eps R0)-> @@ -158,7 +158,7 @@ Lemma mul_factor_gt_f:(eps:R)(l,l':R)(Rgt eps R0)-> Intros;Apply Rmin_Rgt_r;Split. Exact Rlt_R0_R1. Exact (mul_factor_gt eps l l' H). -Save. +Qed. (*******************************) @@ -200,7 +200,7 @@ Lemma R_dist_pos:(x,y:R)(Rge (R_dist x y) R0). Intros;Unfold R_dist;Unfold Rabsolu;Case (case_Rabsolu (Rminus x y));Intro l. Unfold Rge;Left;Apply (Rlt_RoppO (Rminus x y) l). Trivial. -Save. +Qed. (*********) Lemma R_dist_sym:(x,y:R)(R_dist x y)==(R_dist y x). @@ -212,7 +212,7 @@ Generalize (Rlt_RoppO (Rminus y x) r); Intro; Generalize (minus_Rge y x r); Intro; Generalize (minus_Rge x y r0); Intro; Generalize (Rge_ge_eq x y H0 H); Intro;Rewrite H1;Ring. -Save. +Qed. (*********) Lemma R_dist_refl:(x,y:R)((R_dist x y)==R0<->x==y). @@ -223,11 +223,11 @@ Rewrite (Ropp_distr2 x y);Generalize (sym_eqT R x y H);Intro; Apply (eq_Rminus y x H0). Apply (Rminus_eq x y H). Apply (eq_Rminus x y H). -Save. +Qed. Lemma R_dist_eq:(x:R)(R_dist x x)==R0. Unfold R_dist;Intros;SplitAbsolu;Intros;Ring. -Save. +Qed. (***********) Lemma R_dist_tri:(x,y,z:R)(Rle (R_dist x y) @@ -353,7 +353,7 @@ Unfold 2 3 Rminus; Rewrite (Rplus_Ropp_l z);Elim (Rplus_ne (Ropp y));Intros a b;Rewrite b; Clear a b;Fold (Rminus x y); Apply (eq_Rle (Rminus x y) (Rminus x y) (refl_eqT R (Rminus x y))). -Save. +Qed. (*********) Lemma R_dist_plus: (a,b,c,d:R)(Rle (R_dist (Rplus a c) (Rplus b d)) @@ -363,7 +363,7 @@ Intros;Unfold R_dist; with (Rplus (Rminus a b) (Rminus c d)). Exact (Rabsolu_triang (Rminus a b) (Rminus c d)). Ring. -Save. +Qed. (*******************************) (* R is a metric space *) @@ -396,19 +396,19 @@ Elim (H0 (R_dist (f x0) l) H3);Intros;Elim H2;Clear H2 H0; Clear H2;Generalize (Rlt_antirefl (R_dist (f x0) l));Intro;Auto. Elim (R_dist_refl (f x0) l);Intros a b;Clear b;Generalize (a H3);Intro; Generalize (sym_eqT R (f x0) l H2);Intro;Auto. -Save. +Qed. (*********) Lemma tech_limit_contr:(f:R->R)(D:R->Prop)(l:R)(x0:R)(D x0)->~l==(f x0) ->~(limit1_in f D l x0). Intros;Generalize (tech_limit f D l x0);Tauto. -Save. +Qed. (*********) Lemma lim_x:(D:R->Prop)(x0:R)(limit1_in [x:R]x D x0 x0). Unfold limit1_in; Unfold limit_in; Simpl; Intros;Split with eps; Split; Auto;Intros;Elim H0; Intros; Auto. -Save. +Qed. (*********) Lemma limit_plus:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R) @@ -435,7 +435,7 @@ Generalize (H3 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H4 H6)); (Rmult eps (Rinv (Rplus R1 R1)))). Exact (Rplus_lt ? ? ? ? H7 H8). Exact (eps2 eps). -Save. +Qed. (*********) Lemma limit_Ropp:(f:R->R)(D:R->Prop)(l:R)(x0:R) @@ -446,7 +446,7 @@ Unfold limit1_in;Unfold limit_in;Simpl;Intros;Elim (H eps H0);Clear H; Rewrite (Ropp_Ropp l);Rewrite (Rplus_sym (Ropp (f x1)) l); Fold (Rminus l (f x1));Fold (R_dist l (f x1));Rewrite R_dist_sym; Assumption. -Save. +Qed. (*********) Lemma limit_minus:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R) @@ -454,7 +454,7 @@ Lemma limit_minus:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R) (limit1_in [x:R](Rminus (f x) (g x)) D (Rminus l l') x0). Intros;Unfold Rminus;Generalize (limit_Ropp g D l' x0 H0);Intro; Exact (limit_plus f [x:R](Ropp (g x)) D l (Ropp l') x0 H H1). -Save. +Qed. (*********) Lemma limit_free:(f:R->R)(D:R->Prop)(x:R)(x0:R) @@ -462,7 +462,7 @@ Lemma limit_free:(f:R->R)(D:R->Prop)(x:R)(x0:R) Unfold limit1_in;Unfold limit_in;Simpl;Intros;Split with eps;Split; Auto;Intros;Elim (R_dist_refl (f x) (f x));Intros a b; Rewrite (b (refl_eqT R (f x)));Unfold Rgt in H;Assumption. -Save. +Qed. (*********) Lemma limit_mul:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R) @@ -533,7 +533,7 @@ Rewrite (Rmult_sym (Rplus R1 (Rabsolu l)) (Rmult eps (mul_factor l l'))); (mul_factor_wd l l')); Rewrite (proj1 ? ? (Rmult_ne eps));Apply eq_Rle;Trivial. Ring. -Save. +Qed. (*********) Definition adhDa:(R->Prop)->R->Prop:=[D:R->Prop][a:R] @@ -616,7 +616,7 @@ Intros;Unfold adhDa in H;Elim (H0 eps H2);Intros;Elim (H1 eps H2); Apply (Rle_lt_trans (Rabsolu (Rminus l l')) (Rplus (Rabsolu (Rminus l (f x2))) (Rabsolu (Rminus (f x2) l'))) (Rplus eps eps) H3 H1). -Save. +Qed. (*********) Lemma limit_comp:(f,g:R->R)(Df,Dg:R->Prop)(l,l':R)(x0:R) @@ -630,7 +630,7 @@ Unfold limit1_in;Unfold limit_in;Simpl;Intros; Generalize (H3 x2 (conj (Df x2) (Rlt (R_dist x2 x0) x1) H4 H5)); Intro;Exact (H2 (f x2) (conj (Dg (f x2)) (Rlt (R_dist (f x2) l) x) H6 H7)). -Save. +Qed. (*********) @@ -729,4 +729,4 @@ Assumption. Apply Rsqr_pos_lt; Assumption. Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H3; Generalize (lt_INR_0 (2) (neq_O_lt (2) H3)); Unfold INR; Intro; Assumption | Discriminate]. Change ``0<(Rabsolu l)/2``; Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H3; Generalize (lt_INR_0 (2) (neq_O_lt (2) H3)); Unfold INR; Intro; Assumption | Discriminate]]. -Save. +Qed. diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index a388e2ae3b..c88cdfaf20 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -49,18 +49,18 @@ Definition Un_growing:Prop:=(n:nat)(Rle (Un n) (Un (S n))). (*********) Lemma EUn_noempty:(ExT [r:R] (EUn r)). Unfold EUn;Split with (Un O);Split with O;Trivial. -Save. +Qed. (*********) Lemma Un_in_EUn:(n:nat)(EUn (Un n)). Intro;Unfold EUn;Split with n;Trivial. -Save. +Qed. (*********) Lemma Un_bound_imp:(x:R)((n:nat)(Rle (Un n) x))->(is_upper_bound EUn x). Intros;Unfold is_upper_bound;Intros;Unfold EUn in H0;Elim H0;Clear H0; Intros;Generalize (H x1);Intro;Rewrite <- H0 in H1;Trivial. -Save. +Qed. (*********) Lemma growing_prop:(n,m:nat)Un_growing->(ge n m)->(Rge (Un n) (Un m)). @@ -81,7 +81,7 @@ Unfold ge in H0;Generalize (H0 (S n0) H1 (lt_le_S n0 n1 y));Intro; Unfold Un_growing in H1; Apply (Rge_trans (Un (S n1)) (Un n1) (Un (S n0)) (Rle_sym1 (Un n1) (Un (S n1)) (H1 n1)) H3). -Save. +Qed. (* classical is needed: [not_all_not_ex] *) @@ -123,7 +123,7 @@ Intro;Elim (H6 N);Intro;Unfold Rle. Left;Unfold Rgt in H7;Assumption. Right;Auto. Apply (H1 (Un n) (Un_in_EUn n)). -Save. +Qed. (*********) Lemma finite_greater:(N:nat)(ExT [M:R] (n:nat)(le n N)->(Rle (Un n) M)). @@ -137,7 +137,7 @@ Rewrite <-H1;Rewrite <-H1 in H2; (eq_Rle (Un n) (Un n) (refl_eqT R (Un n))))). Apply (H2 (or_intror (Rle (Un n) (Un (S N))) (Rle (Un n) x) (H n H3))). -Save. +Qed. (*********) Lemma cauchy_bound:Cauchy_crit->(bound EUn). @@ -159,7 +159,7 @@ Unfold ge in H0;Generalize (H0 x2 (le_n x) y);Clear H0;Intro; Generalize (H2 x2 y);Clear H2 H0;Intro;Rewrite<-H in H0; Elim (Rmax_Rle x0 (Rplus (Un x) R1) x1);Intros;Clear H1;Apply H2; Left;Assumption. -Save. +Qed. End sequence. @@ -271,7 +271,7 @@ Assumption. Apply Rabsolu_pos_lt. Apply Rinv_neq_R0. Assumption. -Save. +Qed. diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 379b6485d8..91f5a9d5c7 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -27,7 +27,7 @@ Hypothesis def_sigma : (low,high:nat) (le low high) -> (sigma low high)==(sigma Lemma sigma_aux_inv : (diff,low,high,high2:nat) (sigma_aux low high diff)==(sigma_aux low high2 diff). Unfold sigma_aux; Induction diff; [Intros; Reflexivity | Intros; Rewrite (H (S low) high high2); Reflexivity]. -Save. +Qed. Theorem sigma_split : (low,high,k:nat) (le low k)->(lt k high)->``(sigma low high)==(sigma low k)+(sigma (S k) high)``. Intros. @@ -57,26 +57,26 @@ Apply INR_eq; Repeat Rewrite plus_INR Orelse Rewrite S_INR; Try Ring. Apply lt_le_S; Assumption. Assumption. Apply lt_le_weak; Apply le_lt_trans with k; Assumption. -Save. +Qed. Theorem sigma_diff : (low,high,k:nat) (le low k) -> (lt k high )->``(sigma low high)-(sigma low k)==(sigma (S k) high)``. Intros low high k H1 H2; Symmetry; Rewrite -> (sigma_split H1 H2); Ring. -Save. +Qed. Theorem sigma_diff_neg : (low,high,k:nat) (le low k) -> (lt k high)-> ``(sigma low k)-(sigma low high)==-(sigma (S k) high)``. Intros low high k H1 H2; Rewrite -> (sigma_split H1 H2); Ring. -Save. +Qed. Theorem sigma_first : (low,high:nat) (lt low high) -> ``(sigma low high)==(f low)+(sigma (S low) high)``. Intros low high H1; Generalize (lt_le_S low high H1); Intro H2; Generalize (lt_le_weak low high H1); Intro H3; Replace ``(f low)`` with ``(sigma low low)``; [Apply sigma_split; Trivial | Rewrite def_sigma; [Replace (minus low low) with O; Ring; Apply minus_n_n | Trivial]]. -Save. +Qed. Theorem sigma_last : (low,high:nat) (lt low high) -> ``(sigma low high)==(f high)+(sigma low (pred high))``. Intros low high H1; Generalize (lt_le_S low high H1); Intro H2; Generalize (lt_le_weak low high H1); Intro H3; Replace ``(f high)`` with ``(sigma high high)``; [Rewrite Rplus_sym; Pattern 3 high; Rewrite (S_pred high low H1); Apply sigma_split; [Apply gt_S_le; Rewrite <- (S_pred high low H1); Assumption | Pattern 2 high; Rewrite (S_pred high low H1); Apply lt_n_Sn] | Rewrite def_sigma; [ Rewrite <- (minus_n_n high) | Trivial ]; Trivial]. -Save. +Qed. Theorem sigma_eq_arg : (low:nat) (sigma low low)==(f low). Intro low; Rewrite def_sigma; [Rewrite <- (minus_n_n low); Trivial | Trivial]. -Save. +Qed. End Sigma. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 4eeb015f0b..e2cdb2434c 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -25,7 +25,7 @@ Lemma PI_neq0 : ~``PI==0``. Red; Intro. Generalize PI_RGT_0; Intro; Rewrite H in H0. Elim (Rlt_antirefl ``0`` H0). -Save. +Qed. (******************************************************************) (* Axiomatic definitions of cos and sin *) @@ -49,7 +49,7 @@ Axiom sin_PI2 : ``(sin (PI/2))==1``. (**********) Lemma sin2_cos2 : (x:R) ``(Rsqr (sin x)) + (Rsqr (cos x))==1``. Intro; Unfold Rsqr; Rewrite Rplus_sym; Rewrite <- (cos_minus x x); Unfold Rminus; Rewrite Rplus_Ropp_r; Apply cos_0. -Save. +Qed. (**********) @@ -57,7 +57,7 @@ Definition tan [x:R] : R := ``(sin x)/(cos x)``. Lemma Ropp_mul3 : (r1,r2:R) ``r1*(-r2) == -(r1*r2)``. Intros; Rewrite <- Ropp_mul1; Ring. -Save. +Qed. Lemma tan_plus : (x,y:R) ~``(cos x)==0`` -> ~``(cos y)==0`` -> ~``(cos (x+y))==0`` -> ~``1-(tan x)*(tan y)==0`` -> ``(tan (x+y))==((tan x)+(tan y))/(1-(tan x)*(tan y))``. Intros; Unfold tan; Rewrite sin_plus; Rewrite cos_plus; Unfold Rdiv; Replace ``((cos x)*(cos y)-(sin x)*(sin y))`` with ``((cos x)*(cos y))*(1-(sin x)*/(cos x)*((sin y)*/(cos y)))``. @@ -76,7 +76,7 @@ Rewrite Rmult_1l; Rewrite (Rmult_sym (sin x)); Rewrite <- Ropp_mul3; Repeat Rewr Apply Rmult_1r. Assumption. Assumption. -Save. +Qed. (*******************************************************) (* Some properties of cos, sin and tan *) @@ -84,75 +84,75 @@ Save. Lemma cos2 : (x:R) ``(Rsqr (cos x))==1-(Rsqr (sin x))``. Intro x; Generalize (sin2_cos2 x); Intro H1; Rewrite <- H1; Unfold Rminus; Rewrite <- (Rplus_sym (Rsqr (cos x))); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Symmetry; Apply Rplus_Or. -Save. +Qed. Lemma sin2 : (x:R) ``(Rsqr (sin x))==1-(Rsqr (cos x))``. Intro x; Generalize (cos2 x); Intro H1; Rewrite -> H1. Unfold Rminus; Rewrite Ropp_distr1; Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Ol; Symmetry; Apply Ropp_Ropp. -Save. +Qed. Axiom arc_sin_cos : (x,y,z:R) ``0<=x`` -> ``0<=y`` -> ``0<=z`` -> ``(Rsqr x)+(Rsqr y)==(Rsqr z)`` -> (EXT t : R | (x==(Rmult z (cos t))) /\ (y==(Rmult z (sin t)))). Lemma pythagorean : (x,y,z:R) ``(Rsqr x)+(Rsqr y)==(Rsqr z)`` -> ``0<=x`` -> ``0<=y`` -> ``0<=z`` -> (EXT t : R | z==(Rplus (Rmult x (cos t)) (Rmult y (sin t)))). Intros x y z H1 H2 H3 H4; Generalize (arc_sin_cos x y z H2 H3 H4); Intro H5; Elim H5; [ Intros x0 H6; Elim H6; Intros H7 H8; Exists x0; Rewrite H7; Rewrite H8; Replace ``z*(cos x0)*(cos x0)+z*(sin x0)*(sin x0)`` with ``z*((Rsqr (sin x0))+(Rsqr (cos x0)))``; [ Rewrite sin2_cos2; Ring | Unfold Rsqr; Ring] | Assumption]. -Save. +Qed. Lemma double : (x:R) ``2*x==x+x``. Intro; Ring. -Save. +Qed. Lemma aze : ``2<>0``. DiscrR. -Save. +Qed. Lemma double_var : (x:R) ``x == x/2 + x/2``. Intro; Rewrite <- double; Unfold Rdiv; Rewrite <- Rmult_assoc; Symmetry; Apply Rinv_r_simpl_m. Apply aze. -Save. +Qed. Lemma sin_2a : (x:R) ``(sin (2*x))==2*(sin x)*(cos x)``. Intro x; Rewrite double; Rewrite sin_plus. Rewrite <- (Rmult_sym (sin x)); Symmetry; Rewrite Rmult_assoc; Apply double. -Save. +Qed. Lemma cos_2a : (x:R) ``(cos (2*x))==(cos x)*(cos x)-(sin x)*(sin x)``. Intro x; Rewrite double; Apply cos_plus. -Save. +Qed. Lemma cos_2a_cos : (x:R) ``(cos (2*x))==2*(cos x)*(cos x)-1``. Intro x; Rewrite double; Unfold Rminus; Rewrite Rmult_assoc; Rewrite cos_plus; Generalize (sin2_cos2 x); Rewrite double; Intro H1; Rewrite <- H1; SqRing. -Save. +Qed. Lemma cos_2a_sin : (x:R) ``(cos (2*x))==1-2*(sin x)*(sin x)``. Intro x; Rewrite Rmult_assoc; Unfold Rminus; Repeat Rewrite double. Generalize (sin2_cos2 x); Intro H1; Rewrite <- H1; Rewrite cos_plus; SqRing. -Save. +Qed. Lemma tan_2a : (x:R) ~``(cos x)==0`` -> ~``(cos (2*x))==0`` -> ~``1-(tan x)*(tan x)==0`` ->``(tan (2*x))==(2*(tan x))/(1-(tan x)*(tan x))``. Repeat Rewrite double; Intros; Repeat Rewrite double; Rewrite double in H0; Apply tan_plus; Assumption. -Save. +Qed. Lemma sin_0 : ``(sin 0)==0``. Apply Rsqr_eq_0; Rewrite sin2; Rewrite cos_0; SqRing. -Save. +Qed. Lemma sin_neg : (x:R) ``(sin (-x))==-(sin x)``. Intro x; Replace ``-x`` with ``0-x``; Ring; Replace `` -(sin x)`` with ``(sin 0)*(cos x)-(cos 0)*(sin x)``; [ Apply sin_minus |Rewrite -> sin_0; Rewrite -> cos_0; Ring ]. -Save. +Qed. Lemma cos_neg : (x:R) ``(cos (-x))==(cos x)``. Intro x; Replace ``(-x)`` with ``(0-x)``; Ring; Replace ``(cos x)`` with ``(cos 0)*(cos x)+(sin 0)*(sin x)``; [ Apply cos_minus | Rewrite -> cos_0; Rewrite -> sin_0; Ring ]. -Save. +Qed. Lemma tan_0 : ``(tan 0)==0``. Unfold tan; Rewrite -> sin_0; Rewrite -> cos_0. Unfold Rdiv; Apply Rmult_Ol. -Save. +Qed. Lemma tan_neg : (x:R) ``(tan (-x))==-(tan x)``. Intros x; Unfold tan; Rewrite sin_neg; Rewrite cos_neg; Unfold Rdiv. Apply Ropp_mul1. -Save. +Qed. Lemma tan_minus : (x,y:R) ~``(cos x)==0`` -> ~``(cos y)==0`` -> ~``(cos (x-y))==0`` -> ~``1+(tan x)*(tan y)==0`` -> ``(tan (x-y))==((tan x)-(tan y))/(1+(tan x)*(tan y))``. Intros; Unfold Rminus; Rewrite tan_plus. @@ -161,11 +161,11 @@ Assumption. Rewrite cos_neg; Assumption. Assumption. Rewrite tan_neg; Unfold Rminus; Rewrite <- Ropp_mul1; Rewrite Ropp_mul2; Assumption. -Save. +Qed. Lemma cos_PI2 : ``(cos (PI/2))==0``. Apply Rsqr_eq_0; Rewrite cos2; Rewrite sin_PI2; Rewrite Rsqr_1; Unfold Rminus; Apply Rplus_Ropp_r. -Save. +Qed. Lemma sin_PI : ``(sin PI)==0``. Replace ``PI`` with ``2*(PI/2)``. @@ -173,7 +173,7 @@ Rewrite -> sin_2a; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. Unfold Rdiv. Repeat Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m. Apply aze. -Save. +Qed. Lemma cos_PI : ``(cos PI)==(-1)``. Replace ``PI`` with ``2*(PI/2)``. @@ -184,104 +184,104 @@ Unfold Rdiv. Repeat Rewrite <- Rmult_assoc. Apply Rinv_r_simpl_m. Apply aze. -Save. +Qed. Lemma tan_PI : ``(tan PI)==0``. Unfold tan; Rewrite -> sin_PI; Rewrite -> cos_PI. Unfold Rdiv; Apply Rmult_Ol. -Save. +Qed. Lemma sin_3PI2 : ``(sin (3*(PI/2)))==(-1)``. Replace ``3*(PI/2)`` with ``PI+(PI/2)``. Rewrite -> sin_plus; Rewrite -> sin_PI; Rewrite -> cos_PI; Rewrite -> sin_PI2; Ring. Pattern 1 PI; Rewrite (double_var PI). Ring. -Save. +Qed. Lemma cos_3PI2 : ``(cos (3*(PI/2)))==0``. Replace ``3*(PI/2)`` with ``PI+(PI/2)``. Rewrite -> cos_plus; Rewrite -> sin_PI; Rewrite -> cos_PI2; Ring. Pattern 1 PI; Rewrite (double_var PI). Ring. -Save. +Qed. Lemma sin_2PI : ``(sin (2*PI))==0``. Rewrite -> sin_2a; Rewrite -> sin_PI. Rewrite Rmult_Or. Rewrite Rmult_Ol. Reflexivity. -Save. +Qed. Lemma cos_2PI : ``(cos (2*PI))==1``. Rewrite -> cos_2a; Rewrite -> sin_PI; Rewrite -> cos_PI; Rewrite Rmult_Or; Rewrite minus_R0; Rewrite Ropp_mul1; Rewrite Rmult_1l; Apply Ropp_Ropp. -Save. +Qed. Lemma tan_2PI : ``(tan (2*PI))==0``. Unfold tan; Rewrite sin_2PI; Unfold Rdiv; Apply Rmult_Ol. -Save. +Qed. Lemma neg_cos : (x:R) ``(cos (x+PI))==-(cos x)``. Intro x; Rewrite -> cos_plus; Rewrite -> sin_PI; Rewrite -> cos_PI; Rewrite Rmult_Or; Rewrite minus_R0; Rewrite Ropp_mul3; Rewrite Rmult_1r; Reflexivity. -Save. +Qed. Lemma neg_sin : (x:R) ``(sin (x+PI))==-(sin x)``. Intro x; Rewrite -> sin_plus; Rewrite -> sin_PI; Rewrite -> cos_PI. Rewrite Rmult_Or; Rewrite Rplus_Or; Rewrite Ropp_mul3; Rewrite Rmult_1r; Reflexivity. -Save. +Qed. Lemma sin_PI_x : (x:R) ``(sin (PI-x))==(sin x)``. Intro x; Rewrite -> sin_minus; Rewrite -> sin_PI; Rewrite -> cos_PI; Rewrite Rmult_Ol; Unfold Rminus; Rewrite Rplus_Ol; Rewrite Ropp_mul1; Rewrite Ropp_Ropp; Apply Rmult_1l. -Save. +Qed. Lemma sin_period : (x:R)(k:nat) ``(sin (x+2*(INR k)*PI))==(sin x)``. Intros x k; Induction k. Cut ``x+2*(INR O)*PI==x``; [Intro; Rewrite H; Reflexivity | Ring]. Replace ``x+2*(INR (S k))*PI`` with ``(x+2*(INR k)*PI)+(2*PI)``; [Rewrite -> sin_plus; Rewrite -> sin_2PI; Rewrite -> cos_2PI; Ring; Apply Hreck | Rewrite -> S_INR; Ring]. -Save. +Qed. Lemma cos_period : (x:R)(k:nat) ``(cos (x+2*(INR k)*PI))==(cos x)``. Intros x k; Induction k. Cut ``x+2*(INR O)*PI==x``; [Intro; Rewrite H; Reflexivity | Ring]. Replace ``x+2*(INR (S k))*PI`` with ``(x+2*(INR k)*PI)+(2*PI)``; [Rewrite -> cos_plus; Rewrite -> sin_2PI; Rewrite -> cos_2PI; Ring; Apply Hreck | Rewrite -> S_INR; Ring]. -Save. +Qed. Lemma sin_shift : (x:R) ``(sin (PI/2-x))==(cos x)``. Intro x; Rewrite -> sin_minus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. -Save. +Qed. Lemma cos_shift : (x:R) ``(cos (PI/2-x))==(sin x)``. Intro x; Rewrite -> cos_minus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. -Save. +Qed. Lemma cos_sin : (x:R) ``(cos x)==(sin (PI/2+x))``. Intro x; Rewrite -> sin_plus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. -Save. +Qed. Lemma sin_cos : (x:R) ``(sin x)==-(cos (PI/2+x))``. Intro x; Rewrite -> cos_plus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. -Save. +Qed. Axiom sin_eq_0 : (x:R) (sin x)==R0 <-> (EXT k:Z | x==(Rmult (IZR k) PI)). Lemma sin_eq_0_0 : (x:R) (sin x)==R0 -> (EXT k:Z | x==(Rmult (IZR k) PI)). Intros; Elim (sin_eq_0 x); Intros; Apply (H0 H). -Save. +Qed. Lemma sin_eq_0_1 : (x:R) (EXT k:Z | x==(Rmult (IZR k) PI)) -> (sin x)==R0. Intros; Elim (sin_eq_0 x); Intros; Apply (H1 H). -Save. +Qed. Lemma cos_eq_0_0 : (x:R) (cos x)==R0 -> (EXT k : Z | ``x==(IZR k)*PI+PI/2``). Intros x H; Rewrite -> cos_sin in H; Generalize (sin_eq_0_0 (Rplus (Rdiv PI (INR (2))) x) H); Intro H2; Elim H2; Intros x0 H3; Exists (Zminus x0 (inject_nat (S O))); Rewrite <- Z_R_minus; Ring; Rewrite Rmult_sym; Rewrite <- H3; Unfold INR. Rewrite (double_var ``-PI``); Unfold Rdiv; Ring. -Save. +Qed. Lemma cos_eq_0_1 : (x:R) (EXT k : Z | ``x==(IZR k)*PI+PI/2``) -> ``(cos x)==0``. Intros x H1; Rewrite cos_sin; Elim H1; Intros x0 H2; Rewrite H2; Replace ``PI/2+((IZR x0)*PI+PI/2)`` with ``(IZR x0)*PI+PI``. Rewrite neg_sin; Rewrite <- Ropp_O. Apply eq_Ropp; Apply sin_eq_0_1; Exists x0; Reflexivity. Pattern 2 PI; Rewrite (double_var PI); Ring. -Save. +Qed. Lemma sin_eq_O_2PI_0 : (x:R) ``0<=x`` -> ``x<=2*PI`` -> ``(sin x)==0`` -> ``x==0``\/``x==PI``\/``x==2*PI``. Intros; Generalize (sin_eq_0_0 x H1); Intro. @@ -326,19 +326,19 @@ Assumption. Assumption. Apply PI_neq0. Apply PI_neq0. -Save. +Qed. Lemma sin_eq_O_2PI_1 : (x:R) ``0<=x`` -> ``x<=2*PI`` -> ``x==0``\/``x==PI``\/``x==2*PI`` -> ``(sin x)==0``. Intros x H1 H2 H3; Elim H3; Intro H4; [ Rewrite H4; Rewrite -> sin_0; Reflexivity | Elim H4; Intro H5; [Rewrite H5; Rewrite -> sin_PI; Reflexivity | Rewrite H5; Rewrite -> sin_2PI; Reflexivity]]. -Save. +Qed. Lemma PI2_RGT_0 : ``0<PI/2``. Cut ~(O=(2)); [Intro H; Generalize (lt_INR_0 (2) (neq_O_lt (2) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (Rmult_lt_pos PI (Rinv ``2``) PI_RGT_0 (Rlt_Rinv ``2`` H1)); Intro H2; Assumption | Discriminate]. -Save. +Qed. Lemma Rgt_2_0 : ``0<2``. Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR; Intro H; Assumption | Discriminate]. -Save. +Qed. Lemma cos_eq_0_2PI_0 : (x:R) ``R0<=x`` -> ``x<=2*PI`` -> ``(cos x)==0`` -> ``x==(PI/2)``\/``x==3*(PI/2)``. Intros; Case (total_order x ``3*(PI/2)``); Intro. @@ -431,11 +431,11 @@ Apply PI_neq0. Rewrite double; Pattern 3 4 PI; Rewrite double_var; Ring. Ring. Pattern 1 PI; Rewrite double_var; Ring. -Save. +Qed. Lemma cos_eq_0_2PI_1 : (x:R) ``0<=x`` -> ``x<=2*PI`` -> ``x==PI/2``\/``x==3*(PI/2)`` -> ``(cos x)==0``. Intros x H1 H2 H3; Elim H3; Intro H4; [ Rewrite H4; Rewrite -> cos_PI2; Reflexivity | Rewrite H4; Rewrite -> cos_3PI2; Reflexivity ]. -Save. +Qed. Lemma SIN_bound : (x:R) ``-1<=(sin x)<=1``. Intro; Case (total_order_Rle ``-1`` (sin x)); Intro. @@ -447,7 +447,7 @@ Auto with real. Cut ``(sin x)< -1``. Intro; Generalize (Rlt_Ropp (sin x) ``-1`` H); Rewrite Ropp_Ropp; Clear H; Intro; Generalize (Rsqr_incrst_1 ``1`` ``-(sin x)`` H (Rlt_le ``0`` ``1`` Rlt_R0_R1) (Rlt_le ``0`` ``-(sin x)`` (Rlt_trans ``0`` ``1`` ``-(sin x)`` Rlt_R0_R1 H))); Rewrite Rsqr_1; Intro; Rewrite <- Rsqr_neg in H0; Rewrite sin2 in H0; Unfold Rminus in H0; Generalize (Rlt_compatibility ``-1`` ``1`` ``1+ -(Rsqr (cos x))`` H0); Repeat Rewrite <- Rplus_assoc; Repeat Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Intro; Rewrite <- Ropp_O in H1; Generalize (Rlt_Ropp ``-0`` ``-(Rsqr (cos x))`` H1); Repeat Rewrite Ropp_Ropp; Intro; Generalize (pos_Rsqr (cos x)); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` (Rsqr (cos x)) ``0`` H3 H2)). Auto with real. -Save. +Qed. Lemma COS_bound : (x:R) ``-1<=(cos x)<=1``. Intro; Case (total_order_Rle ``-1`` (cos x)); Intro. @@ -459,15 +459,15 @@ Auto with real. Cut ``(cos x)< -1``. Intro; Generalize (Rlt_Ropp (cos x) ``-1`` H); Rewrite Ropp_Ropp; Clear H; Intro; Generalize (Rsqr_incrst_1 ``1`` ``-(cos x)`` H (Rlt_le ``0`` ``1`` Rlt_R0_R1) (Rlt_le ``0`` ``-(cos x)`` (Rlt_trans ``0`` ``1`` ``-(cos x)`` Rlt_R0_R1 H))); Rewrite Rsqr_1; Intro; Rewrite <- Rsqr_neg in H0; Rewrite cos2 in H0; Unfold Rminus in H0; Generalize (Rlt_compatibility ``-1`` ``1`` ``1+ -(Rsqr (sin x))`` H0); Repeat Rewrite <- Rplus_assoc; Repeat Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Intro; Rewrite <- Ropp_O in H1; Generalize (Rlt_Ropp ``-0`` ``-(Rsqr (sin x))`` H1); Repeat Rewrite Ropp_Ropp; Intro; Generalize (pos_Rsqr (sin x)); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` (Rsqr (sin x)) ``0`` H3 H2)). Auto with real. -Save. +Qed. Lemma cos_sin_0 : (x:R) ~(``(cos x)==0``/\``(sin x)==0``). Intro; Red; Intro; Elim H; Intros; Generalize (sin2_cos2 x); Intro; Rewrite H0 in H2; Rewrite H1 in H2; Repeat Rewrite Rsqr_O in H2; Rewrite Rplus_Or in H2; Generalize Rlt_R0_R1; Intro; Rewrite <- H2 in H3; Elim (Rlt_antirefl ``0`` H3). -Save. +Qed. Lemma cos_sin_0_var : (x:R) ~``(cos x)==0``\/~``(sin x)==0``. Intro; Apply not_and_or; Apply cos_sin_0. -Save. +Qed. (*****************************************************************) (* Using series definitions of cos and sin *) @@ -494,24 +494,24 @@ Axiom sin_lb_gt_0 : (a:R) ``0<a``->``a<=PI/2``->``0<(sin_lb a)``. Lemma SIN : (a:R) ``0<=a`` -> ``a<=PI`` -> ``(sin_lb a)<=(sin a)<=(sin_ub a)``. Intros; Unfold sin_lb sin_ub; Apply (sin_bound a (S O) H H0). -Save. +Qed. Lemma COS : (a:R) ``-PI/2<=a`` -> ``a<=PI/2`` -> ``(cos_lb a)<=(cos a)<=(cos_ub a)``. Intros; Unfold cos_lb cos_ub; Apply (cos_bound a (S O) H H0). -Save. +Qed. (**********) Lemma PI4_RGT_0 : ``0<PI/4``. Cut ~(O=(4)); [Intro H; Generalize (lt_INR_0 (4) (neq_O_lt (4) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (Rmult_lt_pos PI (Rinv ``4``) PI_RGT_0 (Rlt_Rinv ``4`` H1)); Intro H2; Assumption | Discriminate]. -Save. +Qed. Lemma PI6_RGT_0 : ``0<PI/6``. Cut ~(O=(6)); [Intro H; Generalize (lt_INR_0 (6) (neq_O_lt (6) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (Rmult_lt_pos PI (Rinv ``6``) PI_RGT_0 (Rlt_Rinv ``6`` H1)); Intro H2; Assumption | Discriminate]. -Save. +Qed. Lemma _PI2_RLT_0 : ``-(PI/2)<0``. Rewrite <- Ropp_O; Apply Rlt_Ropp1; Apply PI2_RGT_0. -Save. +Qed. Lemma PI4_RLT_PI2 : ``PI/4<PI/2``. Cut ~(O=(2)). @@ -525,39 +525,39 @@ Clear H3; Intro H3; Generalize (Rlt_Rinv_R1 ``2`` ``4`` (Rlt_le ``1`` ``2`` H3) Ring. Discriminate. Discriminate. -Save. +Qed. Lemma PI6_RLT_PI2 : ``PI/6<PI/2``. Cut ~(O=(4)); [ Intro H; Cut ~(O=(1)); [Intro H0; Generalize (lt_INR_0 (4) (neq_O_lt (4) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (Rlt_compatibility ``2`` ``0`` ``4`` H1); Rewrite Rplus_sym; Rewrite Rplus_Ol; Replace ``2+4`` with ``6``; [Intro H2; Generalize (lt_INR_0 (1) (neq_O_lt (1) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H3; Generalize (Rlt_compatibility ``1`` ``0`` ``1`` H3); Rewrite Rplus_sym; Rewrite Rplus_Ol; Clear H3; Intro H3; Generalize (Rlt_Rinv_R1 ``2`` ``6`` (Rlt_le ``1`` ``2`` H3) H2); Intro H4; Generalize (Rlt_monotony PI (Rinv ``6``) (Rinv ``2``) PI_RGT_0 H4); Intro H5; Assumption | Ring] | Discriminate] | Discriminate ]. -Save. +Qed. Lemma Rgt_3_0 : ``0<3``. Cut ~(O=(3)); [Intro H0; Generalize (lt_INR_0 (3) (neq_O_lt (3) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H; Assumption | Discriminate]. -Save. +Qed. Lemma sqrt2_neq_0 : ~``(sqrt 2)==0``. Generalize (Rlt_le ``0`` ``2`` Rgt_2_0); Intro H1; Red; Intro H2; Generalize (sqrt_eq_0 ``2`` H1 H2); Intro H; Absurd ``2==0``; [ DiscrR | Assumption]. -Save. +Qed. Lemma R1_sqrt2_neq_0 : ~``1/(sqrt 2)==0``. Generalize (Rinv_neq_R0 ``(sqrt 2)`` sqrt2_neq_0); Intro H; Generalize (prod_neq_R0 ``1`` ``(Rinv (sqrt 2))`` R1_neq_R0 H); Intro H0; Assumption. -Save. +Qed. Lemma sqrt3_2_neq_0 : ~``2*(sqrt 3)==0``. Apply prod_neq_R0; [DiscrR | Generalize (Rlt_le ``0`` ``3`` Rgt_3_0); Intro H1; Red; Intro H2; Generalize (sqrt_eq_0 ``3`` H1 H2); Intro H; Absurd ``3==0``; [ DiscrR | Assumption]]. -Save. +Qed. Lemma not_sym : (r1,r2:R) ``r1<>r2`` -> ``r2<>r1``. Intros; Red; Intro H0; Rewrite H0 in H; Elim H; Reflexivity. -Save. +Qed. Lemma Rlt_sqrt2_0 : ``0<(sqrt 2)``. Generalize (foo ``2`` (Rlt_le ``0`` ``2`` Rgt_2_0)); Intro H1; Elim H1; Intro H2; [Assumption | Absurd ``0 == (sqrt 2)``; [Apply not_sym; Apply sqrt2_neq_0 | Assumption]]. -Save. +Qed. Lemma Rlt_sqrt3_0 : ``0<(sqrt 3)``. Cut ~(O=(1)); [Intro H0; Generalize (Rlt_le ``0`` ``2`` Rgt_2_0); Intro H1; Generalize (Rlt_le ``0`` ``3`` Rgt_3_0); Intro H2; Generalize (lt_INR_0 (1) (neq_O_lt (1) H0)); Unfold INR; Intro H3; Generalize (Rlt_compatibility ``2`` ``0`` ``1`` H3); Rewrite Rplus_sym; Rewrite Rplus_Ol; Replace ``2+1`` with ``3``; [Intro H4; Generalize (sqrt_lt_1 ``2`` ``3`` H1 H2 H4); Clear H3; Intro H3; Apply (Rlt_trans ``0`` ``(sqrt 2)`` ``(sqrt 3)`` Rlt_sqrt2_0 H3) | Ring] | Discriminate]. -Save. +Qed. Lemma PI2_Rlt_PI : ``PI/2<PI``. Cut ~(O=(1)). @@ -568,7 +568,7 @@ Rewrite Rmult_1r. Intro; Assumption. Right; Reflexivity. Discriminate. -Save. +Qed. Theorem sin_gt_0 : (x:R) ``0<x`` -> ``x<PI`` -> ``0<(sin x)``. Intros; Elim (SIN x (Rlt_le R0 x H) (Rlt_le x PI H0)); Intros H1 _; Case (total_order x ``PI/2``); Intro H2. @@ -585,24 +585,24 @@ Intro H7; Elim (SIN ``PI-x`` (Rlt_le R0 ``PI-x`` H7) (Rlt_le ``PI-x`` PI (Rlt_tr Reflexivity. Pattern 2 PI; Rewrite double_var; Ring. Reflexivity. -Save. +Qed. Theorem cos_gt_0 : (x:R) ``-(PI/2)<x`` -> ``x<PI/2`` -> ``0<(cos x)``. Intros; Rewrite cos_sin; Generalize (Rlt_compatibility ``PI/2`` ``-(PI/2)`` x H). Rewrite Rplus_Ropp_r; Intro H1; Generalize (Rlt_compatibility ``PI/2`` x ``PI/2`` H0); Rewrite <- double_var; Intro H2; Apply (sin_gt_0 ``PI/2+x`` H1 H2). -Save. +Qed. Lemma sin_ge_0 : (x:R) ``0<=x`` -> ``x<=PI`` -> ``0<=(sin x)``. Intros x H1 H2; Elim H1; Intro H3; [ Elim H2; Intro H4; [ Left ; Apply (sin_gt_0 x H3 H4) | Rewrite H4; Right; Symmetry; Apply sin_PI ] | Rewrite <- H3; Right; Symmetry; Apply sin_0]. -Save. +Qed. Lemma cos_ge_0 : (x:R) ``-(PI/2)<=x`` -> ``x<=PI/2`` -> ``0<=(cos x)``. Intros x H1 H2; Elim H1; Intro H3; [ Elim H2; Intro H4; [ Left ; Apply (cos_gt_0 x H3 H4) | Rewrite H4; Right; Symmetry; Apply cos_PI2 ] | Rewrite <- H3; Rewrite cos_neg; Right; Symmetry; Apply cos_PI2 ]. -Save. +Qed. Lemma sin_le_0 : (x:R) ``PI<=x`` -> ``x<=2*PI`` -> ``(sin x)<=0``. Intros x H1 H2; Apply Rle_sym2; Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp (sin x)); Apply Rle_Ropp; Rewrite <- neg_sin; Replace ``x+PI`` with ``(x-PI)+2*(INR (S O))*PI``; [Rewrite -> (sin_period (Rminus x PI) (S O)); Apply sin_ge_0; [Replace ``x-PI`` with ``x+(-PI)``; [Rewrite Rplus_sym; Replace ``0`` with ``(-PI)+PI``; [Apply Rle_compatibility; Assumption | Ring] | Ring] | Replace ``x-PI`` with ``x+(-PI)``; Rewrite Rplus_sym; [Pattern 2 PI; Replace ``PI`` with ``(-PI)+2*PI``; [Apply Rle_compatibility; Assumption | Ring] | Ring]] |Unfold INR; Ring]. -Save. +Qed. Lemma cos_le_0 : (x:R) ``PI/2<=x``->``x<=3*(PI/2)``->``(cos x)<=0``. @@ -615,15 +615,15 @@ Unfold Rminus; Rewrite Rplus_sym; Replace ``PI/2`` with ``(-PI)+3*(PI/2)``. Apply Rle_compatibility; Assumption. Pattern 1 PI; Rewrite (double_var PI); Rewrite Ropp_distr1; Ring. Unfold INR; Ring. -Save. +Qed. Lemma sin_lt_0 : (x:R) ``PI<x`` -> ``x<2*PI`` -> ``(sin x)<0``. Intros x H1 H2; Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp (sin x)); Apply Rlt_Ropp; Rewrite <- neg_sin; Replace ``x+PI`` with ``(x-PI)+2*(INR (S O))*PI``; [Rewrite -> (sin_period (Rminus x PI) (S O)); Apply sin_gt_0; [Replace ``x-PI`` with ``x+(-PI)``; [Rewrite Rplus_sym; Replace ``0`` with ``(-PI)+PI``; [Apply Rlt_compatibility; Assumption | Ring] | Ring] | Replace ``x-PI`` with ``x+(-PI)``; Rewrite Rplus_sym; [Pattern 2 PI; Replace ``PI`` with ``(-PI)+2*PI``; [Apply Rlt_compatibility; Assumption | Ring] | Ring]] |Unfold INR; Ring]. -Save. +Qed. Lemma sin_lt_0_var : (x:R) ``-PI<x`` -> ``x<0`` -> ``(sin x)<0``. Intros; Generalize (Rlt_compatibility ``2*PI`` ``-PI`` x H); Replace ``2*PI+(-PI)`` with ``PI``; [Intro H1; Rewrite Rplus_sym in H1; Generalize (Rlt_compatibility ``2*PI`` x ``0`` H0); Intro H2; Rewrite (Rplus_sym ``2*PI``) in H2; Rewrite <- (Rplus_sym R0) in H2; Rewrite Rplus_Ol in H2; Rewrite <- (sin_period x (1)); Unfold INR; Replace ``2*1*PI`` with ``2*PI``; [Apply (sin_lt_0 ``x+2*PI`` H1 H2) | Ring] | Ring]. -Save. +Qed. Lemma cos_lt_0 : (x:R) ``PI/2<x`` -> ``x<3*(PI/2)``-> ``(cos x)<0``. Intros x H1 H2; Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp (cos x)); Apply Rlt_Ropp; Rewrite <- neg_cos; Replace ``x+PI`` with ``(x-PI)+2*(INR (S O))*PI``. @@ -635,13 +635,13 @@ Unfold Rminus; Rewrite Rplus_sym; Replace ``PI/2`` with ``(-PI)+3*(PI/2)``. Apply Rlt_compatibility; Assumption. Pattern 1 PI; Rewrite (double_var PI); Rewrite Ropp_distr1; Ring. Unfold INR; Ring. -Save. +Qed. Lemma tan_gt_0 : (x:R) ``0<x`` -> ``x<PI/2`` -> ``0<(tan x)``. Intros x H1 H2; Unfold tan; Generalize _PI2_RLT_0; Generalize (Rlt_trans R0 x ``PI/2`` H1 H2); Intros; Generalize (Rlt_trans ``-(PI/2)`` R0 x H0 H1); Intro H5; Generalize (Rlt_trans x ``PI/2`` PI H2 PI2_Rlt_PI); Intro H7; Unfold Rdiv; Apply Rmult_lt_pos. Apply sin_gt_0; Assumption. Apply Rlt_Rinv; Apply cos_gt_0; Assumption. -Save. +Qed. Lemma tan_lt_0 : (x:R) ``-(PI/2)<x``->``x<0``->``(tan x)<0``. Intros x H1 H2; Unfold tan; Generalize (cos_gt_0 x H1 (Rlt_trans x ``0`` ``PI/2`` H2 PI2_RGT_0)); Intro H3; Rewrite <- Ropp_O; Replace ``(sin x)/(cos x)`` with ``- ((-(sin x))/(cos x))``. @@ -653,7 +653,7 @@ Rewrite <- (Ropp_Ropp ``PI/2``); Apply Rgt_Ropp; Assumption. Apply PI2_Rlt_PI. Apply Rlt_Rinv; Assumption. Unfold Rdiv; Ring. -Save. +Qed. Lemma cos_ge_0_3PI2 : (x:R) ``3*(PI/2)<=x``->``x<=2*PI``->``0<=(cos x)``. Intros; Rewrite <- cos_neg; Rewrite <- (cos_period ``-x`` (1)); Unfold INR; Replace ``-x+2*1*PI`` with ``2*PI-x``. @@ -664,7 +664,7 @@ Replace ``2*PI+ -(3*PI/2)`` with ``PI/2``. Intro H4; Apply (cos_ge_0 ``2*PI-x`` (Rlt_le ``-(PI/2)`` ``2*PI-x`` (Rlt_le_trans ``-(PI/2)`` ``0`` ``2*PI-x`` _PI2_RLT_0 H2)) H4). Rewrite double; Pattern 2 3 PI; Rewrite double_var; Ring. Ring. -Save. +Qed. Lemma form1 : (p,q:R) ``(cos p)+(cos q)==2*(cos ((p-q)/2))*(cos ((p+q)/2))``. Intros p q; Pattern 1 p; Replace ``p`` with ``(p-q)/2+(p+q)/2``. @@ -673,7 +673,7 @@ Rewrite cos_plus; Rewrite cos_minus; Ring. Unfold Rdiv Rminus; Rewrite Rmult_Rplus_distrl; Ring. Rewrite (Rmult_sym ``/2``); Repeat Rewrite <- Ropp_mul1; Assert H := (double_var ``-q``); Unfold Rdiv in H; Symmetry ; Assumption. Unfold Rdiv Rminus; Rewrite Rmult_Rplus_distrl; Ring; Rewrite (Rmult_sym ``/2``); Repeat Rewrite <- Ropp_mul1; Assert H := (double_var ``p``); Unfold Rdiv in H; Symmetry ; Assumption. -Save. +Qed. Lemma form2 : (p,q:R) ``(cos p)-(cos q)==-2*(sin ((p-q)/2))*(sin ((p+q)/2))``. Intros p q; Pattern 1 p; Replace ``p`` with ``(p-q)/2+(p+q)/2``. @@ -681,7 +681,7 @@ Rewrite <- (cos_neg q); Replace``-q`` with ``(p-q)/2-(p+q)/2``. Rewrite cos_plus; Rewrite cos_minus; Ring. Unfold Rdiv Rminus; Rewrite Rmult_Rplus_distrl; Ring; Rewrite (Rmult_sym ``/2``); Repeat Rewrite <- Ropp_mul1; Assert H := (double_var ``-q``); Unfold Rdiv in H; Symmetry ; Assumption. Unfold Rdiv Rminus; Rewrite Rmult_Rplus_distrl; Ring; Rewrite (Rmult_sym ``/2``); Repeat Rewrite <- Ropp_mul1; Assert H := (double_var ``p``); Unfold Rdiv in H; Symmetry ; Assumption. -Save. +Qed. Lemma form3 : (p,q:R) ``(sin p)+(sin q)==2*(cos ((p-q)/2))*(sin ((p+q)/2))``. Intros p q; Pattern 1 p; Replace ``p`` with ``(p-q)/2+(p+q)/2``. @@ -701,7 +701,7 @@ Rewrite (Rmult_sym ``/2``). Repeat Rewrite <- Ropp_mul1. Assert H := (double_var ``p``). Unfold Rdiv in H; Symmetry ; Assumption. -Save. +Qed. Lemma form4 : (p,q:R) ``(sin p)-(sin q)==2*(cos ((p+q)/2))*(sin ((p-q)/2))``. Intros p q; Pattern 1 p; Replace ``p`` with ``(p-q)/2+(p+q)/2``. @@ -721,7 +721,7 @@ Rewrite (Rmult_sym ``/2``). Repeat Rewrite <- Ropp_mul1. Assert H := (double_var ``p``). Unfold Rdiv in H; Symmetry ; Assumption. -Save. +Qed. Lemma sin_increasing_0 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``(sin x)<(sin y)``->``x<y``. Intros; Cut ``(sin ((x-y)/2))<0``. @@ -767,7 +767,7 @@ Unfold Rdiv; Apply Rmult_sym. Pattern 1 PI; Rewrite double_var. Rewrite Ropp_distr1. Reflexivity. -Save. +Qed. Lemma sin_increasing_1 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``x<y``->``(sin x)<(sin y)``. Intros; Generalize (Rlt_compatibility ``x`` ``x`` ``y`` H3); Intro H4; Generalize (Rplus_le ``-(PI/2)`` x ``-(PI/2)`` x H H); Replace ``-(PI/2)+ (-(PI/2))`` with ``-PI``. @@ -804,7 +804,7 @@ Apply Rmult_sym. Pattern 1 PI; Rewrite double_var. Rewrite Ropp_distr1. Reflexivity. -Save. +Qed. Lemma sin_decreasing_0 : (x,y:R) ``x<=3*(PI/2)``-> ``PI/2<=x`` -> ``y<=3*(PI/2)``-> ``PI/2<=y`` -> ``(sin x)<(sin y)`` -> ``y<x``. Intros; Rewrite <- (sin_PI_x x) in H3; Rewrite <- (sin_PI_x y) in H3; Generalize (Rlt_Ropp ``(sin (PI-x))`` ``(sin (PI-y))`` H3); Repeat Rewrite <- sin_neg; Generalize (Rle_compatibility ``-PI`` x ``3*(PI/2)`` H); Generalize (Rle_compatibility ``-PI`` ``PI/2`` x H0); Generalize (Rle_compatibility ``-PI`` y ``3*(PI/2)`` H1); Generalize (Rle_compatibility ``-PI`` ``PI/2`` y H2); Replace ``-PI+x`` with ``x-PI``. @@ -832,7 +832,7 @@ Pattern 2 PI; Rewrite double_var. Rewrite Ropp_distr1. Ring. Unfold Rminus; Apply Rplus_sym. -Save. +Qed. Lemma sin_decreasing_1 : (x,y:R) ``x<=3*(PI/2)``-> ``PI/2<=x`` -> ``y<=3*(PI/2)``-> ``PI/2<=y`` -> ``x<y`` -> ``(sin y)<(sin x)``. Intros; Rewrite <- (sin_PI_x x); Rewrite <- (sin_PI_x y); Generalize (Rle_compatibility ``-PI`` x ``3*(PI/2)`` H); Generalize (Rle_compatibility ``-PI`` ``PI/2`` x H0); Generalize (Rle_compatibility ``-PI`` y ``3*(PI/2)`` H1); Generalize (Rle_compatibility ``-PI`` ``PI/2`` y H2); Generalize (Rlt_compatibility ``-PI`` x y H3); Replace ``-PI+PI/2`` with ``-(PI/2)``. @@ -852,7 +852,7 @@ Unfold Rminus; Apply Rplus_sym. Pattern 2 PI; Rewrite double_var; Ring. Unfold Rminus; Apply Rplus_sym. Pattern 2 PI; Rewrite double_var; Ring. -Save. +Qed. Lemma cos_increasing_0 : (x,y:R) ``PI<=x`` -> ``x<=2*PI`` ->``PI<=y`` -> ``y<=2*PI`` -> ``(cos x)<(cos y)`` -> ``x<y``. Intros x y H1 H2 H3 H4; Rewrite <- (cos_neg x); Rewrite <- (cos_neg y); Rewrite <- (cos_period ``-x`` (1)); Rewrite <- (cos_period ``-y`` (1)); Unfold INR; Replace ``-x+2*1*PI`` with ``PI/2-(x-3*(PI/2))``. @@ -887,7 +887,7 @@ Ring. Rewrite Rmult_1r. Rewrite (double PI); Pattern 3 4 PI; Rewrite double_var. Ring. -Save. +Qed. Lemma cos_increasing_1 : (x,y:R) ``PI<=x`` -> ``x<=2*PI`` ->``PI<=y`` -> ``y<=2*PI`` -> ``x<y`` -> ``(cos x)<(cos y)``. Intros x y H1 H2 H3 H4 H5; Generalize (Rle_compatibility ``-3*(PI/2)`` PI x H1); Generalize (Rle_compatibility ``-3*(PI/2)`` x ``2*PI`` H2); Generalize (Rle_compatibility ``-3*(PI/2)`` PI y H3); Generalize (Rle_compatibility ``-3*(PI/2)`` y ``2*PI`` H4); Generalize (Rlt_compatibility ``-3*(PI/2)`` x y H5); Rewrite <- (cos_neg x); Rewrite <- (cos_neg y); Rewrite <- (cos_period ``-x`` (1)); Rewrite <- (cos_period ``-y`` (1)); Unfold INR; Replace ``-3*(PI/2)+x`` with ``x-3*(PI/2)``. @@ -912,19 +912,19 @@ Apply Rplus_sym. Unfold Rminus. Rewrite <- Ropp_mul1. Apply Rplus_sym. -Save. +Qed. Lemma cos_decreasing_0 : (x,y:R) ``0<=x``->``x<=PI``->``0<=y``->``y<=PI``->``(cos x)<(cos y)``->``y<x``. Intros; Generalize (Rlt_Ropp (cos x) (cos y) H3); Repeat Rewrite <- neg_cos; Intro H4; Change ``(cos (y+PI))<(cos (x+PI))`` in H4; Rewrite (Rplus_sym x) in H4; Rewrite (Rplus_sym y) in H4; Generalize (Rle_compatibility PI ``0`` x H); Generalize (Rle_compatibility PI x PI H0); Generalize (Rle_compatibility PI ``0`` y H1); Generalize (Rle_compatibility PI y PI H2); Rewrite Rplus_Or. Rewrite <- double. Clear H H0 H1 H2 H3; Intros; Apply Rlt_anti_compatibility with ``PI``; Apply (cos_increasing_0 ``PI+y`` ``PI+x`` H0 H H2 H1 H4). -Save. +Qed. Lemma cos_decreasing_1 : (x,y:R) ``0<=x``->``x<=PI``->``0<=y``->``y<=PI``->``x<y``->``(cos y)<(cos x)``. Intros; Apply Ropp_Rlt; Repeat Rewrite <- neg_cos; Rewrite (Rplus_sym x); Rewrite (Rplus_sym y); Generalize (Rle_compatibility PI ``0`` x H); Generalize (Rle_compatibility PI x PI H0); Generalize (Rle_compatibility PI ``0`` y H1); Generalize (Rle_compatibility PI y PI H2); Rewrite Rplus_Or. Rewrite <- double. Generalize (Rlt_compatibility PI x y H3); Clear H H0 H1 H2 H3; Intros; Apply (cos_increasing_1 ``PI+x`` ``PI+y`` H3 H2 H1 H0 H). -Save. +Qed. Lemma tan_diff : (x,y:R) ~``(cos x)==0``->~``(cos y)==0``->``(tan x)-(tan y)==(sin (x-y))/((cos x)*(cos y))``. Intros; Unfold tan;Rewrite sin_minus. @@ -953,7 +953,7 @@ Assumption. Assumption. Assumption. Assumption. -Save. +Qed. Lemma tan_increasing_0 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI/4``->``(tan x)<(tan y)``->``x<y``. @@ -996,7 +996,7 @@ Rewrite Rinv_Rmult. Reflexivity. Assumption. Assumption. -Save. +Qed. Lemma tan_increasing_1 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI/4``->``x<y``->``(tan x)<(tan y)``. Intros; Apply Rminus_lt; Generalize PI4_RLT_PI2; Intro H4; Generalize (Rlt_Ropp ``PI/4`` ``PI/2`` H4); Intro H5; Change ``-(PI/2)< -(PI/4)`` in H5; Generalize (cos_gt_0 x (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` x H5 H) (Rle_lt_trans x ``PI/4`` ``PI/2`` H0 H4)); Intro HP1; Generalize (cos_gt_0 y (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` y H5 H1) (Rle_lt_trans y ``PI/4`` ``PI/2`` H2 H4)); Intro HP2; Generalize (not_sym ``0`` (cos x) (Rlt_not_eq ``0`` (cos x) (cos_gt_0 x (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` x H5 H) (Rle_lt_trans x ``PI/4`` ``PI/2`` H0 H4)))); Intro H6; Generalize (not_sym ``0`` (cos y) (Rlt_not_eq ``0`` (cos y) (cos_gt_0 y (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` y H5 H1) (Rle_lt_trans y ``PI/4`` ``PI/2`` H2 H4)))); Intro H7; Rewrite (tan_diff x y H6 H7); Generalize (Rlt_Rinv (cos x) HP1); Intro H10; Generalize (Rlt_Rinv (cos y) HP2); Intro H11; Generalize (Rmult_lt_pos (Rinv (cos x)) (Rinv (cos y)) H10 H11); Replace ``/(cos x)*/(cos y)`` with ``/((cos x)*(cos y))``. @@ -1016,69 +1016,69 @@ Apply aze. Apply aze. Reflexivity. Apply Rinv_Rmult; Assumption. -Save. +Qed. Lemma sin_incr_0 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``(sin x)<=(sin y)``->``x<=y``. Intros; Case (total_order (sin x) (sin y)); Intro H4; [Left; Apply (sin_increasing_0 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order x y); Intro H6; [Left; Assumption | Elim H6; Intro H7; [Right; Assumption | Generalize (sin_increasing_1 y x H1 H2 H H0 H7); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl (sin y) H8)]] | Elim (Rlt_antirefl (sin x) (Rle_lt_trans (sin x) (sin y) (sin x) H3 H5))]]. -Save. +Qed. Lemma sin_incr_1 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``x<=y``->``(sin x)<=(sin y)``. Intros; Case (total_order x y); Intro H4; [Left; Apply (sin_increasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order (sin x) (sin y)); Intro H6; [Left; Assumption | Elim H6; Intro H7; [Right; Assumption | Generalize (sin_increasing_0 y x H1 H2 H H0 H7); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl y H8)]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]]. -Save. +Qed. Lemma sin_decr_0 : (x,y:R) ``x<=3*(PI/2)``->``PI/2<=x``->``y<=3*(PI/2)``->``PI/2<=y``-> ``(sin x)<=(sin y)`` -> ``y<=x``. Intros; Case (total_order (sin x) (sin y)); Intro H4; [Left; Apply (sin_decreasing_0 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order x y); Intro H6; [Generalize (sin_decreasing_1 x y H H0 H1 H2 H6); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl (sin y) H8) | Elim H6; Intro H7; [Right; Symmetry; Assumption | Left; Assumption]] | Elim (Rlt_antirefl (sin x) (Rle_lt_trans (sin x) (sin y) (sin x) H3 H5))]]. -Save. +Qed. Lemma sin_decr_1 : (x,y:R) ``x<=3*(PI/2)``-> ``PI/2<=x`` -> ``y<=3*(PI/2)``-> ``PI/2<=y`` -> ``x<=y`` -> ``(sin y)<=(sin x)``. Intros; Case (total_order x y); Intro H4; [Left; Apply (sin_decreasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order (sin x) (sin y)); Intro H6; [Generalize (sin_decreasing_0 x y H H0 H1 H2 H6); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl y H8) | Elim H6; Intro H7; [Right; Symmetry; Assumption | Left; Assumption]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]]. -Save. +Qed. Lemma cos_incr_0 : (x,y:R) ``PI<=x`` -> ``x<=2*PI`` ->``PI<=y`` -> ``y<=2*PI`` -> ``(cos x)<=(cos y)`` -> ``x<=y``. Intros; Case (total_order (cos x) (cos y)); Intro H4; [Left; Apply (cos_increasing_0 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order x y); Intro H6; [Left; Assumption | Elim H6; Intro H7; [Right; Assumption | Generalize (cos_increasing_1 y x H1 H2 H H0 H7); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl (cos y) H8)]] | Elim (Rlt_antirefl (cos x) (Rle_lt_trans (cos x) (cos y) (cos x) H3 H5))]]. -Save. +Qed. Lemma cos_incr_1 : (x,y:R) ``PI<=x`` -> ``x<=2*PI`` ->``PI<=y`` -> ``y<=2*PI`` -> ``x<=y`` -> ``(cos x)<=(cos y)``. Intros; Case (total_order x y); Intro H4; [Left; Apply (cos_increasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order (cos x) (cos y)); Intro H6; [Left; Assumption | Elim H6; Intro H7; [Right; Assumption | Generalize (cos_increasing_0 y x H1 H2 H H0 H7); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl y H8)]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]]. -Save. +Qed. Lemma cos_decr_0 : (x,y:R) ``0<=x``->``x<=PI``->``0<=y``->``y<=PI``->``(cos x)<=(cos y)`` -> ``y<=x``. Intros; Case (total_order (cos x) (cos y)); Intro H4; [Left; Apply (cos_decreasing_0 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order x y); Intro H6; [Generalize (cos_decreasing_1 x y H H0 H1 H2 H6); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl (cos y) H8) | Elim H6; Intro H7; [Right; Symmetry; Assumption | Left; Assumption]] | Elim (Rlt_antirefl (cos x) (Rle_lt_trans (cos x) (cos y) (cos x) H3 H5))]]. -Save. +Qed. Lemma cos_decr_1 : (x,y:R) ``0<=x``->``x<=PI``->``0<=y``->``y<=PI``->``x<=y``->``(cos y)<=(cos x)``. Intros; Case (total_order x y); Intro H4; [Left; Apply (cos_decreasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order (cos x) (cos y)); Intro H6; [Generalize (cos_decreasing_0 x y H H0 H1 H2 H6); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl y H8) | Elim H6; Intro H7; [Right; Symmetry; Assumption | Left; Assumption]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]]. -Save. +Qed. Lemma tan_incr_0 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI/4``->``(tan x)<=(tan y)``->``x<=y``. Intros; Case (total_order (tan x) (tan y)); Intro H4; [Left; Apply (tan_increasing_0 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order x y); Intro H6; [Left; Assumption | Elim H6; Intro H7; [Right; Assumption | Generalize (tan_increasing_1 y x H1 H2 H H0 H7); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl (tan y) H8)]] | Elim (Rlt_antirefl (tan x) (Rle_lt_trans (tan x) (tan y) (tan x) H3 H5))]]. -Save. +Qed. Lemma tan_incr_1 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI/4``->``x<=y``->``(tan x)<=(tan y)``. Intros; Case (total_order x y); Intro H4; [Left; Apply (tan_increasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order (tan x) (tan y)); Intro H6; [Left; Assumption | Elim H6; Intro H7; [Right; Assumption | Generalize (tan_increasing_0 y x H1 H2 H H0 H7); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl y H8)]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]]. -Save. +Qed. Lemma Rgt_3PI2_0 : ``0<3*(PI/2)``. Cut ~(O=(3)); [Intro H1; Generalize (lt_INR_0 (3) (neq_O_lt (3) H1)); Rewrite INR_eq_INR2; Unfold INR2; Intro H2; Generalize (Rlt_monotony ``PI/2`` ``0`` ``3`` PI2_RGT_0 H2); Rewrite Rmult_Or; Rewrite Rmult_sym; Intro H3; Assumption | Discriminate]. -Save. +Qed. Lemma Rgt_2PI_0 : ``0<2*PI``. Cut ~(O=(2)); [Intro H1; Generalize (lt_INR_0 (2) (neq_O_lt (2) H1)); Unfold INR; Intro H2; Generalize (Rlt_monotony PI ``0`` ``2`` PI_RGT_0 H2); Rewrite Rmult_Or; Rewrite Rmult_sym; Intro H3; Assumption | Discriminate]. -Save. +Qed. Lemma Rlt_PI_3PI2 : ``PI<3*(PI/2)``. Generalize PI2_RGT_0; Intro H1; Generalize (Rlt_compatibility PI ``0`` ``PI/2`` H1); Replace ``PI+(PI/2)`` with ``3*(PI/2)``. Rewrite Rplus_Or; Intro H2; Assumption. Pattern 2 PI; Rewrite double_var. Ring. -Save. +Qed. Lemma Rlt_3PI2_2PI : ``3*(PI/2)<2*PI``. Generalize PI2_RGT_0; Intro H1; Generalize (Rlt_compatibility ``3*(PI/2)`` ``0`` ``PI/2`` H1); Replace ``3*(PI/2)+(PI/2)`` with ``2*PI``. Rewrite Rplus_Or; Intro H2; Assumption. Rewrite double; Pattern 1 2 PI; Rewrite double_var. Ring. -Save. +Qed. Lemma sin_cos_PI4 : ``(sin (PI/4)) == (cos (PI/4))``. Rewrite cos_sin; Replace ``PI/2+PI/4`` with ``-(PI/4)+PI``. @@ -1098,7 +1098,7 @@ Apply aze. Ring. Symmetry; Apply double_var. Symmetry; Apply double_var. -Save. +Qed. Lemma cos_PI4 : ``(cos (PI/4))==1/(sqrt 2)``. Apply Rsqr_inj. @@ -1136,11 +1136,11 @@ Reflexivity. Apply aze. Left; Apply Rgt_2_0. Apply sqrt2_neq_0. -Save. +Qed. Lemma sin_PI4 : ``(sin (PI/4))==1/(sqrt 2)``. Rewrite sin_cos_PI4; Apply cos_PI4. -Save. +Qed. Lemma cos3PI4 : ``(cos (3*(PI/4)))==-1/(sqrt 2)``. Replace ``3*(PI/4)`` with ``(PI/2)-(-(PI/4))``. @@ -1160,7 +1160,7 @@ Ring. Ring. Apply aze. Apply aze. -Save. +Qed. Lemma sin3PI4 : ``(sin (3*(PI/4)))==1/(sqrt 2)``. Replace ``3*(PI/4)`` with ``(PI/2)-(-(PI/4))``. @@ -1177,7 +1177,7 @@ Ring. Ring. Apply aze. Apply aze. -Save. +Qed. Lemma tan_PI4 : ``(tan (PI/4))==1``. Unfold tan; Rewrite sin_cos_PI4. @@ -1186,7 +1186,7 @@ Apply Rinv_r. Replace ``PI*/4`` with ``PI/4``. Rewrite cos_PI4; Apply R1_sqrt2_neq_0. Unfold Rdiv; Reflexivity. -Save. +Qed. Lemma sin_PI3_cos_PI6 : ``(sin (PI/3))==(cos (PI/6))``. Replace ``PI/6`` with ``(PI/2)-(PI/3)``. @@ -1217,7 +1217,7 @@ Rewrite Rmult_assoc. Rewrite <- Rinv_l_sym. Rewrite Rmult_1r; Reflexivity. DiscrR. -Save. +Qed. Lemma sin_PI6_cos_PI3 : ``(cos (PI/3))==(sin (PI/6))``. Replace ``PI/6`` with ``(PI/2)-(PI/3)``. @@ -1248,7 +1248,7 @@ Rewrite Rmult_assoc. Rewrite <- Rinv_l_sym. Rewrite Rmult_1r; Reflexivity. DiscrR. -Save. +Qed. Lemma sin_PI6 : ``(sin (PI/6))==1/2``. Apply r_Rmult_mult with ``2*(cos (PI/6))``. @@ -1278,7 +1278,7 @@ DiscrR. Ring. Ring. Apply prod_neq_R0; [DiscrR | Cut ``0<(cos (PI/6))``; [Intro H1; Auto with real | Apply cos_gt_0; [Apply (Rlt_trans ``-(PI/2)`` ``0`` ``PI/6`` _PI2_RLT_0 PI6_RGT_0) | Apply PI6_RLT_PI2]]]. -Save. +Qed. Lemma cos_PI6 : ``(cos (PI/6))==(sqrt 3)/2``. Apply Rsqr_inj. @@ -1313,7 +1313,7 @@ Apply aze. Apply aze. Left; Apply Rgt_3_0. Apply aze. -Save. +Qed. Lemma tan_PI6 : ``(tan (PI/6))==1/(sqrt 3)``. Unfold tan; Rewrite sin_PI6; Rewrite cos_PI6. @@ -1332,15 +1332,15 @@ Assert H1 := Rlt_sqrt3_0. Rewrite H in H1; Elim (Rlt_antirefl ``0`` H1). Apply Rinv_neq_R0. Apply aze. -Save. +Qed. Lemma sin_PI3 : ``(sin (PI/3))==(sqrt 3)/2``. Rewrite sin_PI3_cos_PI6; Apply cos_PI6. -Save. +Qed. Lemma cos_PI3 : ``(cos (PI/3))==1/2``. Rewrite sin_PI6_cos_PI3; Apply sin_PI6. -Save. +Qed. Lemma tan_PI3 : ``(tan (PI/3))==(sqrt 3)``. Unfold tan; Rewrite sin_PI3; Rewrite cos_PI3. @@ -1352,7 +1352,7 @@ Rewrite <- Rinv_l_sym. Apply Rmult_1r. Apply aze. Apply aze. -Save. +Qed. Lemma sin_2PI3 : ``(sin (2*(PI/3)))==(sqrt 3)/2``. Rewrite double. @@ -1370,7 +1370,7 @@ Reflexivity. Ring. Apply aze. Apply aze. -Save. +Qed. Lemma cos_2PI3 : ``(cos (2*(PI/3)))==-1/2``. Rewrite double. @@ -1412,7 +1412,7 @@ Apply aze. Apply aze. Apply aze. Apply prod_neq_R0; Apply aze. -Save. +Qed. Lemma tan_2PI3 : ``(tan (2*(PI/3)))==-(sqrt 3)``. Unfold tan; Rewrite sin_2PI3; Rewrite cos_2PI3. @@ -1432,7 +1432,7 @@ Apply aze. Apply aze. DiscrR. Apply Rinv_neq_R0; Apply aze. -Save. +Qed. Lemma cos_5PI4 : ``(cos (5*(PI/4)))==-1/(sqrt 2)``. Replace ``5*(PI/4)`` with ``(PI/4)+(PI)``. @@ -1450,7 +1450,7 @@ Ring. Ring. Apply aze. Apply aze. -Save. +Qed. Lemma sin_5PI4 : ``(sin (5*(PI/4)))==-1/(sqrt 2)``. Replace ``5*(PI/4)`` with ``(PI/4)+(PI)``. @@ -1467,11 +1467,11 @@ Ring. Ring. Apply aze. Apply aze. -Save. +Qed. Lemma sin_cos5PI4 : ``(cos (5*(PI/4)))==(sin (5*(PI/4)))``. Rewrite cos_5PI4; Rewrite sin_5PI4; Reflexivity. -Save. +Qed. (***************************************************************) (* Radian -> Degree | Degree -> Radian *) @@ -1494,7 +1494,7 @@ Apply PI_neq0. Unfold plat. Apply not_O_IZR. Discriminate. -Save. +Qed. Lemma toRad_inj : (x,y:R) (toRad x)==(toRad y) -> x==y. Intros; Unfold toRad in H; Apply r_Rmult_mult with PI. @@ -1506,11 +1506,11 @@ Unfold plat. Apply not_O_IZR. Discriminate. Apply PI_neq0. -Save. +Qed. Lemma deg_rad : (x:R) (toDeg (toRad x))==x. Intro x; Apply toRad_inj; Rewrite -> (rad_deg (toRad x)); Reflexivity. -Save. +Qed. Definition sind [x:R] : R := (sin (toRad x)). Definition cosd [x:R] : R := (cos (toRad x)). @@ -1518,7 +1518,7 @@ Definition tand [x:R] : R := (tan (toRad x)). Lemma Rsqr_sin_cos_d_one : (x:R) ``(Rsqr (sind x))+(Rsqr (cosd x))==1``. Intro x; Unfold sind; Unfold cosd; Apply sin2_cos2. -Save. +Qed. (***************************************************) (* Other properties *) @@ -1535,4 +1535,4 @@ Simpl; Discriminate. Simpl; Discriminate. Simpl; Discriminate. Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` a ``0`` H H2)). -Save.
\ No newline at end of file +Qed.
\ No newline at end of file diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index 2bc5063eb4..1bf7e72b1c 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -105,7 +105,7 @@ Left;Unfold Rgt in H; Right;Rewrite H0;Rewrite Rinv_R1;Apply sym_eqT;Apply eq_Rminus;Auto. Elim (archimed (Rminus (Rinv eps) R1));Intros;Clear H1; Unfold Rgt in H0;Apply Rlt_le;Assumption. -Save. +Qed. |