diff options
Diffstat (limited to 'theories7/Reals/R_Ifp.v')
| -rw-r--r-- | theories7/Reals/R_Ifp.v | 552 |
1 files changed, 552 insertions, 0 deletions
diff --git a/theories7/Reals/R_Ifp.v b/theories7/Reals/R_Ifp.v new file mode 100644 index 00000000..621cca64 --- /dev/null +++ b/theories7/Reals/R_Ifp.v @@ -0,0 +1,552 @@ +(************************************************************************) +(* 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. |