diff options
Diffstat (limited to 'theories7/Reals/R_Ifp.v')
| -rw-r--r-- | theories7/Reals/R_Ifp.v | 552 |
1 files changed, 0 insertions, 552 deletions
diff --git a/theories7/Reals/R_Ifp.v b/theories7/Reals/R_Ifp.v deleted file mode 100644 index 621cca64..00000000 --- a/theories7/Reals/R_Ifp.v +++ /dev/null @@ -1,552 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: R_Ifp.v,v 1.1.2.1 2004/07/16 19:31:33 herbelin Exp $ i*) - -(**********************************************************) -(** Complements for the reals.Integer and fractional part *) -(* *) -(**********************************************************) - -Require Rbase. -Require Omega. -V7only [ Import nat_scope. Import Z_scope. Import R_scope. ]. -Open Local Scope R_scope. - -(*********************************************************) -(** Fractional part *) -(*********************************************************) - -(**********) -Definition Int_part:R->Z:=[r:R](`(up r)-1`). - -(**********) -Definition frac_part:R->R:=[r:R](Rminus r (IZR (Int_part r))). - -(**********) -Lemma tech_up:(r:R)(z:Z)(Rlt r (IZR z))->(Rle (IZR z) (Rplus r R1))-> - z=(up r). -Intros;Generalize (archimed r);Intro;Elim H1;Intros;Clear H1; - Unfold Rgt in H2;Unfold Rminus in H3; -Generalize (Rle_compatibility r (Rplus (IZR (up r)) - (Ropp r)) R1 H3);Intro;Clear H3; - Rewrite (Rplus_sym (IZR (up r)) (Ropp r)) in H1; - 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. -Qed. - -(**********) -Lemma up_tech:(r:R)(z:Z)(Rle (IZR z) r)->(Rlt r (IZR `z+1`))-> - `z+1`=(up r). -Intros;Generalize (Rle_compatibility R1 (IZR z) r H);Intro;Clear H; - Rewrite (Rplus_sym R1 (IZR z)) in H1;Rewrite (Rplus_sym R1 r) in H1; - 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. -Qed. - -(**********) -Lemma fp_R0:(frac_part R0)==R0. -Unfold frac_part; Unfold Int_part; Elim (archimed R0); - Intros; Unfold Rminus; - Elim (Rplus_ne (Ropp (IZR `(up R0)-1`))); Intros a b; - Rewrite b;Clear a b;Rewrite <- Z_R_minus;Cut (up R0)=`1`. -Intro;Rewrite H1; - Rewrite (eq_Rminus (IZR `1`) (IZR `1`) (refl_eqT R (IZR `1`))); - Apply Ropp_O. -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. -Qed. - -(**********) -Lemma for_base_fp:(r:R)(Rgt (Rminus (IZR (up r)) r) R0)/\ - (Rle (Rminus (IZR (up r)) r) R1). -Intro; Split; - Cut (Rgt (IZR (up r)) r)/\(Rle (Rminus (IZR (up r)) r) R1). -Intro; Elim H; Intros. -Apply (Rgt_minus (IZR (up r)) r H0). -Apply archimed. -Intro; Elim H; Intros. -Exact H1. -Apply archimed. -Qed. - -(**********) -Lemma base_fp:(r:R)(Rge (frac_part r) R0)/\(Rlt (frac_part r) R1). -Intro; Unfold frac_part; Unfold Int_part; Split. - (*sup a O*) -Cut (Rge (Rminus r (IZR (up r))) (Ropp R1)). -Rewrite <- Z_R_minus;Simpl;Intro; Unfold Rminus; - Rewrite Ropp_distr1;Rewrite <-Rplus_assoc; - Fold (Rminus r (IZR (up r))); - Fold (Rminus (Rminus r (IZR (up r))) (Ropp R1)); - Apply Rge_minus;Auto with zarith real. -Rewrite <- Ropp_distr2;Apply Rle_Ropp;Elim (for_base_fp r); Auto with zarith real. - (*inf a 1*) -Cut (Rlt (Rminus r (IZR (up r))) R0). -Rewrite <- Z_R_minus; Simpl;Intro; Unfold Rminus; - Rewrite Ropp_distr1;Rewrite <-Rplus_assoc; - Fold (Rminus r (IZR (up r)));Rewrite Ropp_Ropp; - Elim (Rplus_ne R1);Intros a b;Pattern 2 R1;Rewrite <-a;Clear a b; - Rewrite (Rplus_sym (Rminus r (IZR (up r))) R1); - 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. -Qed. - -(*********************************************************) -(** Properties *) -(*********************************************************) - -(**********) -Lemma base_Int_part:(r:R)(Rle (IZR (Int_part r)) r)/\ - (Rgt (Rminus (IZR (Int_part r)) r) (Ropp R1)). -Intro;Unfold Int_part;Elim (archimed r);Intros. -Split;Rewrite <- (Z_R_minus (up r) `1`);Simpl. -Generalize (Rle_minus (Rminus (IZR (up r)) r) R1 H0);Intro; - Unfold Rminus in H1; - Rewrite (Rplus_assoc (IZR (up r)) (Ropp r) (Ropp R1)) in - H1;Rewrite (Rplus_sym (Ropp r) (Ropp R1)) in H1; - Rewrite <-(Rplus_assoc (IZR (up r)) (Ropp R1) (Ropp r)) in - H1;Fold (Rminus (IZR (up r)) R1) in H1; - Fold (Rminus (Rminus (IZR (up r)) R1) r) in H1; - Apply Rminus_le;Auto with zarith real. -Generalize (Rgt_plus_plus_r (Ropp R1) (IZR (up r)) r H);Intro; - Rewrite (Rplus_sym (Ropp R1) (IZR (up r))) in H1; - Generalize (Rgt_plus_plus_r (Ropp r) - (Rplus (IZR (up r)) (Ropp R1)) (Rplus (Ropp R1) r) H1); - Intro;Clear H H0 H1; - Rewrite (Rplus_sym (Ropp r) (Rplus (IZR (up r)) (Ropp R1))) - in H2;Fold (Rminus (IZR (up r)) R1) in H2; - Fold (Rminus (Rminus (IZR (up r)) R1) r) in H2; - Rewrite (Rplus_sym (Ropp r) (Rplus (Ropp R1) r)) in H2; - 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. -Qed. - -(**********) -Lemma Int_part_INR:(n : nat) (Int_part (INR n)) = (inject_nat n). -Intros n; Unfold Int_part. -Cut (up (INR n)) = (Zplus (inject_nat n) (inject_nat (1))). -Intros H'; Rewrite H'; Simpl; Ring. -Apply sym_equal; Apply tech_up; Auto. -Replace (Zplus (inject_nat n) (inject_nat (1))) with (INZ (S n)). -Repeat Rewrite <- INR_IZR_INZ. -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. -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. -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. -Qed. - -(**********) -Lemma Rminus_Int_part1:(r1,r2:R)(Rge (frac_part r1) (frac_part r2))-> - (Int_part (Rminus r1 r2))=(Zminus (Int_part r1) (Int_part r2)). -Intros;Elim (base_fp r1);Elim (base_fp r2);Intros; - Generalize (Rle_sym2 R0 (frac_part r2) H0);Intro;Clear H0; - Generalize (Rle_Ropp R0 (frac_part r2) H4);Intro;Clear H4; - Rewrite (Ropp_O) in H0; - Generalize (Rle_sym2 (Ropp (frac_part r2)) R0 H0);Intro;Clear H0; - Generalize (Rle_sym2 R0 (frac_part r1) H2);Intro;Clear H2; - Generalize (Rlt_Ropp (frac_part r2) R1 H1);Intro;Clear H1; - Unfold Rgt in H2; - Generalize (sum_inequa_Rle_lt R0 (frac_part r1) R1 (Ropp R1) - (Ropp (frac_part r2)) R0 H0 H3 H2 H4);Intro;Elim H1;Intros; - Clear H1;Elim (Rplus_ne R1);Intros a b;Rewrite a in H6;Clear a b H5; - Generalize (Rge_minus (frac_part r1) (frac_part r2) H);Intro;Clear H; - Fold (Rminus (frac_part r1) (frac_part r2)) in H6; - Generalize (Rle_sym2 R0 (Rminus (frac_part r1) (frac_part r2)) H1); - Intro;Clear H1 H3 H4 H0 H2;Unfold frac_part in H6 H; - Unfold Rminus in H6 H; - Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H; - Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H; - Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus (Ropp r2) (IZR (Int_part r2)))) in H; - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2) - (IZR (Int_part r2))) in H; - Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H; - Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1))) - (IZR (Int_part r2))) in H; - Rewrite <-(Rplus_assoc r1 (Ropp r2) - (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H; - Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H; - Fold (Rminus r1 r2) in H;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) - in H;Generalize (Rle_compatibility - (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) R0 - (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) H);Intro; - Clear H;Rewrite (Rplus_sym (Rminus r1 r2) - (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H0; - Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H0; - Unfold Rminus in H0;Fold (Rminus r1 r2) in H0; - Rewrite (Rplus_assoc (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))) - (Rplus (IZR (Int_part r2)) (Ropp (IZR (Int_part r1))))) in H0; - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r2))) (IZR (Int_part r2)) - (Ropp (IZR (Int_part r1)))) in H0;Rewrite (Rplus_Ropp_l (IZR (Int_part r2))) in - H0;Elim (Rplus_ne (Ropp (IZR (Int_part r1))));Intros a b;Rewrite b in H0; - Clear a b; - Elim (Rplus_ne (Rplus (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))))); - Intros a b;Rewrite a in H0;Clear a b;Rewrite (Rplus_Ropp_r (IZR (Int_part r1))) - in H0;Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H0; - Clear a b;Fold (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) in H0; - Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H6; - Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H6; - Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus (Ropp r2) (IZR (Int_part r2)))) in H6; - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2) - (IZR (Int_part r2))) in H6; - Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H6; - Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1))) - (IZR (Int_part r2))) in H6; - Rewrite <-(Rplus_assoc r1 (Ropp r2) - (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H6; - Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H6; - Fold (Rminus r1 r2) in H6;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) - in H6;Generalize (Rlt_compatibility - (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) R1 H6); - Intro;Clear H6; - Rewrite (Rplus_sym (Rminus r1 r2) - (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H; - Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H; - Rewrite <-(Ropp_distr2 (IZR (Int_part r1)) (IZR (Int_part r2))) in H; - Rewrite (Rplus_Ropp_r (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H; - Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H;Clear a b; - Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; - Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - Cut R1==(IZR `1`);Auto with zarith real. -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. -Qed. - -(**********) -Lemma Rminus_Int_part2:(r1,r2:R)(Rlt (frac_part r1) (frac_part r2))-> - (Int_part (Rminus r1 r2))=(Zminus (Zminus (Int_part r1) (Int_part r2)) `1`). -Intros;Elim (base_fp r1);Elim (base_fp r2);Intros; - Generalize (Rle_sym2 R0 (frac_part r2) H0);Intro;Clear H0; - Generalize (Rle_Ropp R0 (frac_part r2) H4);Intro;Clear H4; - Rewrite (Ropp_O) in H0; - Generalize (Rle_sym2 (Ropp (frac_part r2)) R0 H0);Intro;Clear H0; - Generalize (Rle_sym2 R0 (frac_part r1) H2);Intro;Clear H2; - Generalize (Rlt_Ropp (frac_part r2) R1 H1);Intro;Clear H1; - Unfold Rgt in H2; - Generalize (sum_inequa_Rle_lt R0 (frac_part r1) R1 (Ropp R1) - (Ropp (frac_part r2)) R0 H0 H3 H2 H4);Intro;Elim H1;Intros; - Clear H1;Elim (Rplus_ne (Ropp R1));Intros a b;Rewrite b in H5; - Clear a b H6;Generalize (Rlt_minus (frac_part r1) (frac_part r2) H); - Intro;Clear H;Fold (Rminus (frac_part r1) (frac_part r2)) in H5; - Clear H3 H4 H0 H2;Unfold frac_part in H5 H1; - Unfold Rminus in H5 H1; - Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H5; - Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H5; - Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus (Ropp r2) (IZR (Int_part r2)))) in H5; - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2) - (IZR (Int_part r2))) in H5; - Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H5; - Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1))) - (IZR (Int_part r2))) in H5; - Rewrite <-(Rplus_assoc r1 (Ropp r2) - (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H5; - Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H5; - Fold (Rminus r1 r2) in H5;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) - in H5;Generalize (Rlt_compatibility - (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) (Ropp R1) - (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) H5); - Intro;Clear H5;Rewrite (Rplus_sym (Rminus r1 r2) - (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H; - Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H; - Unfold Rminus in H;Fold (Rminus r1 r2) in H; - Rewrite (Rplus_assoc (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))) - (Rplus (IZR (Int_part r2)) (Ropp (IZR (Int_part r1))))) in H; - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r2))) (IZR (Int_part r2)) - (Ropp (IZR (Int_part r1)))) in H;Rewrite (Rplus_Ropp_l (IZR (Int_part r2))) in - H;Elim (Rplus_ne (Ropp (IZR (Int_part r1))));Intros a b;Rewrite b in H; - Clear a b;Rewrite (Rplus_Ropp_r (IZR (Int_part r1))) in H; - Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H; - Clear a b;Fold (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) in H; - Fold (Rminus (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) R1) in H; - Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H1; - Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H1; - Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus (Ropp r2) (IZR (Int_part r2)))) in H1; - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2) - (IZR (Int_part r2))) in H1; - Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H1; - Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1))) - (IZR (Int_part r2))) in H1; - Rewrite <-(Rplus_assoc r1 (Ropp r2) - (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H1; - Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H1; - Fold (Rminus r1 r2) in H1;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) - in H1;Generalize (Rlt_compatibility - (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) R0 H1); - Intro;Clear H1; - Rewrite (Rplus_sym (Rminus r1 r2) - (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H0; - Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H0; - Rewrite <-(Ropp_distr2 (IZR (Int_part r1)) (IZR (Int_part r2))) in H0; - Rewrite (Rplus_Ropp_r (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H0; - Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H0;Clear a b; - Rewrite <-(Rplus_Ropp_l R1) in H0; - Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Ropp R1) R1) in H0; - Fold (Rminus (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) R1) in H0; - Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; - Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - Cut R1==(IZR `1`);Auto with zarith real. -Intro;Rewrite H1 in H;Rewrite H1 in H0;Clear H1; - Rewrite (Z_R_minus `(Int_part r1)-(Int_part r2)` `1`) in H; - Rewrite (Z_R_minus `(Int_part r1)-(Int_part r2)` `1`) in H0; - Rewrite <-(plus_IZR `(Int_part r1)-(Int_part r2)-1` `1`) in H0; - Generalize (Rlt_le (IZR `(Int_part r1)-(Int_part r2)-1`) (Rminus r1 r2) H); - 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. -Qed. - -(**********) -Lemma Rminus_fp1:(r1,r2:R)(Rge (frac_part r1) (frac_part r2))-> - (frac_part (Rminus r1 r2))==(Rminus (frac_part r1) (frac_part r2)). -Intros;Unfold frac_part; - Generalize (Rminus_Int_part1 r1 r2 H);Intro;Rewrite -> H0; - Rewrite <- (Z_R_minus (Int_part r1) (Int_part r2));Unfold Rminus; - Rewrite -> (Ropp_distr1 (IZR (Int_part r1)) (Ropp (IZR (Int_part r2)))); - Rewrite -> (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))); - Rewrite -> (Ropp_Ropp (IZR (Int_part r2))); - Rewrite -> (Rplus_assoc r1 (Ropp r2) - (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))); - Rewrite -> (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus (Ropp r2) (IZR (Int_part r2)))); - Rewrite <- (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1))) - (IZR (Int_part r2))); - 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. -Qed. - -(**********) -Lemma Rminus_fp2:(r1,r2:R)(Rlt (frac_part r1) (frac_part r2))-> - (frac_part (Rminus r1 r2))== - (Rplus (Rminus (frac_part r1) (frac_part r2)) R1). -Intros;Unfold frac_part;Generalize (Rminus_Int_part2 r1 r2 H);Intro; - Rewrite -> H0; - Rewrite <- (Z_R_minus (Zminus (Int_part r1) (Int_part r2)) `1`); - Rewrite <- (Z_R_minus (Int_part r1) (Int_part r2));Unfold Rminus; - Rewrite -> (Ropp_distr1 (Rplus (IZR (Int_part r1)) (Ropp (IZR (Int_part r2)))) - (Ropp (IZR `1`))); - Rewrite -> (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))); - Rewrite -> (Ropp_Ropp (IZR `1`)); - Rewrite -> (Ropp_Ropp (IZR (Int_part r2))); - Rewrite -> (Ropp_distr1 (IZR (Int_part r1))); - Rewrite -> (Ropp_Ropp (IZR (Int_part r2)));Simpl; - Rewrite <- (Rplus_assoc (Rplus r1 (Ropp r2)) - (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) R1); - Rewrite -> (Rplus_assoc r1 (Ropp r2) - (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))); - Rewrite -> (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus (Ropp r2) (IZR (Int_part r2)))); - Rewrite <- (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1))) - (IZR (Int_part r2))); - 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. -Qed. - -(**********) -Lemma plus_Int_part1:(r1,r2:R)(Rge (Rplus (frac_part r1) (frac_part r2)) R1)-> - (Int_part (Rplus r1 r2))=(Zplus (Zplus (Int_part r1) (Int_part r2)) `1`). -Intros; - Generalize (Rle_sym2 R1 (Rplus (frac_part r1) (frac_part r2)) H); - Intro;Clear H;Elim (base_fp r1);Elim (base_fp r2);Intros;Clear H H2; - Generalize (Rlt_compatibility (frac_part r2) (frac_part r1) R1 H3); - Intro;Clear H3; - Generalize (Rlt_compatibility R1 (frac_part r2) R1 H1);Intro;Clear H1; - Rewrite (Rplus_sym R1 (frac_part r2)) in H2; - Generalize (Rlt_trans (Rplus (frac_part r2) (frac_part r1)) - (Rplus (frac_part r2) R1) (Rplus R1 R1) H H2);Intro;Clear H H2; - Rewrite (Rplus_sym (frac_part r2) (frac_part r1)) in H1; - Unfold frac_part in H0 H1;Unfold Rminus in H0 H1; - Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus r2 (Ropp (IZR (Int_part r2))))) in H1; - Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H1; - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))) - r2) in H1; - Rewrite (Rplus_sym - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H1; - Rewrite <-(Rplus_assoc r1 r2 - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H1; - Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H1; - Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus r2 (Ropp (IZR (Int_part r2))))) in H0; - Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H0; - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))) - r2) in H0; - Rewrite (Rplus_sym - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H0; - Rewrite <-(Rplus_assoc r1 r2 - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H0; - Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H0; - Generalize (Rle_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) - R1 (Rplus (Rplus r1 r2) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) H0);Intro; - Clear H0; - Generalize (Rlt_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Rplus (Rplus r1 r2) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) (Rplus R1 R1) H1); - Intro;Clear H1; - Rewrite (Rplus_sym (Rplus r1 r2) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H; - Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H; - Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H; - Elim (Rplus_ne (Rplus r1 r2));Intros a b;Rewrite b in H;Clear a b; - Rewrite (Rplus_sym (Rplus r1 r2) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H0; - Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H0; - Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H0; - Elim (Rplus_ne (Rplus r1 r2));Intros a b;Rewrite b in H0;Clear a b; - Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) R1 R1) in - H0;Cut R1==(IZR `1`);Auto with zarith real. -Intro;Rewrite H1 in H0;Rewrite H1 in H;Clear H1; - Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H; - Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H0; - Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)` `1`) in H; - Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)` `1`) in H0; - 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. -Qed. - -(**********) -Lemma plus_Int_part2:(r1,r2:R)(Rlt (Rplus (frac_part r1) (frac_part r2)) R1)-> - (Int_part (Rplus r1 r2))=(Zplus (Int_part r1) (Int_part r2)). -Intros;Elim (base_fp r1);Elim (base_fp r2);Intros;Clear H1 H3; - Generalize (Rle_sym2 R0 (frac_part r2) H0);Intro;Clear H0; - Generalize (Rle_sym2 R0 (frac_part r1) H2);Intro;Clear H2; - Generalize (Rle_compatibility (frac_part r1) R0 (frac_part r2) H1); - Intro;Clear H1;Elim (Rplus_ne (frac_part r1));Intros a b; - Rewrite a in H2;Clear a b;Generalize (Rle_trans R0 (frac_part r1) - (Rplus (frac_part r1) (frac_part r2)) H0 H2);Intro;Clear H0 H2; - Unfold frac_part in H H1;Unfold Rminus in H H1; - Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus r2 (Ropp (IZR (Int_part r2))))) in H1; - Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H1; - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))) - r2) in H1; - Rewrite (Rplus_sym - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H1; - Rewrite <-(Rplus_assoc r1 r2 - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H1; - Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H1; - Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus r2 (Ropp (IZR (Int_part r2))))) in H; - Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H; - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))) - r2) in H; - Rewrite (Rplus_sym - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H; - Rewrite <-(Rplus_assoc r1 r2 - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H; - Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H; - Generalize (Rle_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) - R0 (Rplus (Rplus r1 r2) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) H1);Intro; - Clear H1; - Generalize (Rlt_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Rplus (Rplus r1 r2) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) R1 H); - Intro;Clear H; - Rewrite (Rplus_sym (Rplus r1 r2) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H1; - Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H1; - Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H1; - Elim (Rplus_ne (Rplus r1 r2));Intros a b;Rewrite b in H1;Clear a b; - Rewrite (Rplus_sym (Rplus r1 r2) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H0; - Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H0; - Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H0; - Elim (Rplus_ne (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))));Intros a b; - Rewrite a in H0;Clear a b;Elim (Rplus_ne (Rplus r1 r2));Intros a b; - Rewrite b in H0;Clear a b;Cut R1==(IZR `1`);Auto with zarith real. -Intro;Rewrite H in H1;Clear H; - Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H0; - Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H1; - 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. -Qed. - -(**********) -Lemma plus_frac_part1:(r1,r2:R) - (Rge (Rplus (frac_part r1) (frac_part r2)) R1)-> - (frac_part (Rplus r1 r2))== - (Rminus (Rplus (frac_part r1) (frac_part r2)) R1). -Intros;Unfold frac_part; - Generalize (plus_Int_part1 r1 r2 H);Intro;Rewrite H0; - Rewrite (plus_IZR `(Int_part r1)+(Int_part r2)` `1`); - Rewrite (plus_IZR (Int_part r1) (Int_part r2));Simpl;Unfold 3 4 Rminus; - Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus r2 (Ropp (IZR (Int_part r2))))); - Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))); - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))) - r2); - Rewrite (Rplus_sym - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2); - Rewrite <-(Rplus_assoc r1 r2 - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))); - Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))); - Unfold Rminus; - Rewrite (Rplus_assoc (Rplus r1 r2) - (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) - (Ropp R1)); - Rewrite <-(Ropp_distr1 (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) R1); - Trivial with zarith real. -Qed. - -(**********) -Lemma plus_frac_part2:(r1,r2:R) - (Rlt (Rplus (frac_part r1) (frac_part r2)) R1)-> -(frac_part (Rplus r1 r2))==(Rplus (frac_part r1) (frac_part r2)). -Intros;Unfold frac_part; - Generalize (plus_Int_part2 r1 r2 H);Intro;Rewrite H0; - Rewrite (plus_IZR (Int_part r1) (Int_part r2));Unfold 2 3 Rminus; - Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) - (Rplus r2 (Ropp (IZR (Int_part r2))))); - Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))); - Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))) - r2); - Rewrite (Rplus_sym - (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2); - Rewrite <-(Rplus_assoc r1 r2 - (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. -Qed. |