From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- theories7/Reals/RiemannInt_SF.v | 1400 --------------------------------------- 1 file changed, 1400 deletions(-) delete mode 100644 theories7/Reals/RiemannInt_SF.v (limited to 'theories7/Reals/RiemannInt_SF.v') diff --git a/theories7/Reals/RiemannInt_SF.v b/theories7/Reals/RiemannInt_SF.v deleted file mode 100644 index 3e2cc457..00000000 --- a/theories7/Reals/RiemannInt_SF.v +++ /dev/null @@ -1,1400 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Prop] : Prop := (EX n:nat | (i:nat)(I i)->(le i n)). - -Lemma IZN_var:(z:Z)(`0<=z`)->{ n:nat | z=(INZ n)}. -Intros; Apply inject_nat_complete_inf; Assumption. -Qed. - -Lemma Nzorn : (I:nat->Prop) (EX n:nat | (I n)) -> (Nbound I) -> (sigTT ? [n:nat](I n)/\(i:nat)(I i)->(le i n)). -Intros I H H0; Pose E := [x:R](EX i:nat | (I i)/\(INR i)==x); Assert H1 : (bound E). -Unfold Nbound in H0; Elim H0; Intros N H1; Unfold bound; Exists (INR N); Unfold is_upper_bound; Intros; Unfold E in H2; Elim H2; Intros; Elim H3; Intros; Rewrite <- H5; Apply le_INR; Apply H1; Assumption. -Assert H2 : (EXT x:R | (E x)). -Elim H; Intros; Exists (INR x); Unfold E; Exists x; Split; [Assumption | Reflexivity]. -Assert H3 := (complet E H1 H2); Elim H3; Intros; Unfold is_lub in p; Elim p; Clear p; Intros; Unfold is_upper_bound in H4 H5; Assert H6 : ``0<=x``. -Elim H2; Intros; Unfold E in H6; Elim H6; Intros; Elim H7; Intros; Apply Rle_trans with x0; [Rewrite <- H9; Change ``(INR O)<=(INR x1)``; Apply le_INR; Apply le_O_n | Apply H4; Assumption]. -Assert H7 := (archimed x); Elim H7; Clear H7; Intros; Assert H9 : ``x<=(IZR (up x))-1``. -Apply H5; Intros; Assert H10 := (H4 ? H9); Unfold E in H9; Elim H9; Intros; Elim H11; Intros; Rewrite <- H13; Apply Rle_anti_compatibility with R1; Replace ``1+((IZR (up x))-1)`` with (IZR (up x)); [Idtac | Ring]; Replace ``1+(INR x1)`` with (INR (S x1)); [Idtac | Rewrite S_INR; Ring]. -Assert H14 : `0<=(up x)`. -Apply le_IZR; Apply Rle_trans with x; [Apply H6 | Left; Assumption]. -Assert H15 := (IZN ? H14); Elim H15; Clear H15; Intros; Rewrite H15; Rewrite <- INR_IZR_INZ; Apply le_INR; Apply lt_le_S; Apply INR_lt; Rewrite H13; Apply Rle_lt_trans with x; [Assumption | Rewrite INR_IZR_INZ; Rewrite <- H15; Assumption]. -Assert H10 : ``x==(IZR (up x))-1``. -Apply Rle_antisym; [Assumption | Apply Rle_anti_compatibility with ``-x+1``; Replace `` -x+1+((IZR (up x))-1)`` with ``(IZR (up x))-x``; [Idtac | Ring]; Replace ``-x+1+x`` with R1; [Assumption | Ring]]. -Assert H11 : `0<=(up x)`. -Apply le_IZR; Apply Rle_trans with x; [Apply H6 | Left; Assumption]. -Assert H12 := (IZN_var H11); Elim H12; Clear H12; Intros; Assert H13 : (E x). -Elim (classic (E x)); Intro; Try Assumption. -Cut ((y:R)(E y)->``y<=x-1``). -Intro; Assert H14 := (H5 ? H13); Cut ``x-1Prop := [x:R]``aProp := [x:R]``a<=xR;a,b:R;l,lf:Rlist] : Prop := (ordered_Rlist l)/\``(pos_Rl l O)==(Rmin a b)``/\``(pos_Rl l (pred (Rlength l)))==(Rmax a b)``/\(Rlength l)=(S (Rlength lf))/\(i:nat)(lt i (pred (Rlength l)))->(constant_D_eq f (open_interval (pos_Rl l i) (pos_Rl l (S i))) (pos_Rl lf i)). - -Definition adapted_couple_opt [f:R->R;a,b:R;l,lf:Rlist] := (adapted_couple f a b l lf)/\((i:nat)(lt i (pred (Rlength lf)))->(``(pos_Rl lf i)<>(pos_Rl lf (S i))``\/``(f (pos_Rl l (S i)))<>(pos_Rl lf i)``))/\((i:nat)(lt i (pred (Rlength l)))->``(pos_Rl l i)<>(pos_Rl l (S i))``). - -Definition is_subdivision [f:R->R;a,b:R;l:Rlist] : Type := (sigTT ? [l0:Rlist](adapted_couple f a b l l0)). - -Definition IsStepFun [f:R->R;a,b:R] : Type := (SigT ? [l:Rlist](is_subdivision f a b l)). - -(* Class of step functions *) -Record StepFun [a,b:R] : Type := mkStepFun { - fe:> R->R; - pre:(IsStepFun fe a b)}. - -Definition subdivision [a,b:R;f:(StepFun a b)] : Rlist := (projT1 ? ? (pre f)). - -Definition subdivision_val [a,b:R;f:(StepFun a b)] : Rlist := Cases (projT2 ? ? (pre f)) of (existTT a b) => a end. - -Fixpoint Int_SF [l:Rlist] : Rlist -> R := -[k:Rlist] Cases l of -| nil => R0 -| (cons a l') => Cases k of - | nil => R0 - | (cons x nil) => R0 - | (cons x (cons y k')) => ``a*(y-x)+(Int_SF l' (cons y k'))`` - end -end. - -(* Integral of step functions *) -Definition RiemannInt_SF [a,b:R;f:(StepFun a b)] : R := -Cases (total_order_Rle a b) of - (leftT _) => (Int_SF (subdivision_val f) (subdivision f)) -| (rightT _) => ``-(Int_SF (subdivision_val f) (subdivision f))`` -end. - -(********************************) -(* Properties of step functions *) -(********************************) - -Lemma StepFun_P1 : (a,b:R;f:(StepFun a b)) (adapted_couple f a b (subdivision f) (subdivision_val f)). -Intros a b f; Unfold subdivision_val; Case (projT2 Rlist ([l:Rlist](is_subdivision f a b l)) (pre f)); Intros; Apply a0. -Qed. - -Lemma StepFun_P2 : (a,b:R;f:R->R;l,lf:Rlist) (adapted_couple f a b l lf) -> (adapted_couple f b a l lf). -Unfold adapted_couple; Intros; Decompose [and] H; Clear H; Repeat Split; Try Assumption. -Rewrite H2; Unfold Rmin; Case (total_order_Rle a b); Intro; Case (total_order_Rle b a); Intro; Try Reflexivity. -Apply Rle_antisym; Assumption. -Apply Rle_antisym; Auto with real. -Rewrite H1; Unfold Rmax; Case (total_order_Rle a b); Intro; Case (total_order_Rle b a); Intro; Try Reflexivity. -Apply Rle_antisym; Assumption. -Apply Rle_antisym; Auto with real. -Qed. - -Lemma StepFun_P3 : (a,b,c:R) ``a<=b`` -> (adapted_couple (fct_cte c) a b (cons a (cons b nil)) (cons c nil)). -Intros; Unfold adapted_couple; Repeat Split. -Unfold ordered_Rlist; Intros; Simpl in H0; Inversion H0; [Simpl; Assumption | Elim (le_Sn_O ? H2)]. -Simpl; Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Simpl; Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Unfold constant_D_eq open_interval; Intros; Simpl in H0; Inversion H0; [Reflexivity | Elim (le_Sn_O ? H3)]. -Qed. - -Lemma StepFun_P4 : (a,b,c:R) (IsStepFun (fct_cte c) a b). -Intros; Unfold IsStepFun; Case (total_order_Rle a b); Intro. -Apply Specif.existT with (cons a (cons b nil)); Unfold is_subdivision; Apply existTT with (cons c nil); Apply (StepFun_P3 c r). -Apply Specif.existT with (cons b (cons a nil)); Unfold is_subdivision; Apply existTT with (cons c nil); Apply StepFun_P2; Apply StepFun_P3; Auto with real. -Qed. - -Lemma StepFun_P5 : (a,b:R;f:R->R;l:Rlist) (is_subdivision f a b l) -> (is_subdivision f b a l). -Unfold is_subdivision; Intros; Elim X; Intros; Exists x; Unfold adapted_couple in p; Decompose [and] p; Clear p; Unfold adapted_couple; Repeat Split; Try Assumption. -Rewrite H1; Unfold Rmin; Case (total_order_Rle a b); Intro; Case (total_order_Rle b a); Intro; Try Reflexivity. -Apply Rle_antisym; Assumption. -Apply Rle_antisym; Auto with real. -Rewrite H0; Unfold Rmax; Case (total_order_Rle a b); Intro; Case (total_order_Rle b a); Intro; Try Reflexivity. -Apply Rle_antisym; Assumption. -Apply Rle_antisym; Auto with real. -Qed. - -Lemma StepFun_P6 : (f:R->R;a,b:R) (IsStepFun f a b) -> (IsStepFun f b a). -Unfold IsStepFun; Intros; Elim X; Intros; Apply Specif.existT with x; Apply StepFun_P5; Assumption. -Qed. - -Lemma StepFun_P7 : (a,b,r1,r2,r3:R;f:R->R;l,lf:Rlist) ``a<=b`` -> (adapted_couple f a b (cons r1 (cons r2 l)) (cons r3 lf)) -> (adapted_couple f r2 b (cons r2 l) lf). -Unfold adapted_couple; Intros; Decompose [and] H0; Clear H0; Assert H5 : (Rmax a b)==b. -Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Assert H7 : ``r2<=b``. -Rewrite H5 in H2; Rewrite <- H2; Apply RList_P7; [Assumption | Simpl; Right; Left; Reflexivity]. -Repeat Split. -Apply RList_P4 with r1; Assumption. -Rewrite H5 in H2; Unfold Rmin; Case (total_order_Rle r2 b); Intro; [Reflexivity | Elim n; Assumption]. -Unfold Rmax; Case (total_order_Rle r2 b); Intro; [Rewrite H5 in H2; Rewrite <- H2; Reflexivity | Elim n; Assumption]. -Simpl in H4; Simpl; Apply INR_eq; Apply r_Rplus_plus with R1; Do 2 Rewrite (Rplus_sym R1); Do 2 Rewrite <- S_INR; Rewrite H4; Reflexivity. -Intros; Unfold constant_D_eq open_interval; Intros; Unfold constant_D_eq open_interval in H6; Assert H9 : (lt (S i) (pred (Rlength (cons r1 (cons r2 l))))). -Simpl; Simpl in H0; Apply lt_n_S; Assumption. -Assert H10 := (H6 ? H9); Apply H10; Assumption. -Qed. - -Lemma StepFun_P8 : (f:R->R;l1,lf1:Rlist;a,b:R) (adapted_couple f a b l1 lf1) -> a==b -> (Int_SF lf1 l1)==R0. -Induction l1. -Intros; Induction lf1; Reflexivity. -Induction r0. -Intros; Induction lf1. -Reflexivity. -Unfold adapted_couple in H0; Decompose [and] H0; Clear H0; Simpl in H5; Discriminate. -Intros; Induction lf1. -Reflexivity. -Simpl; Cut r==r1. -Intro; Rewrite H3; Rewrite (H0 lf1 r b). -Ring. -Rewrite H3; Apply StepFun_P7 with a r r3; [Right; Assumption | Assumption]. -Clear H H0 Hreclf1 r0; Unfold adapted_couple in H1; Decompose [and] H1; Intros; Simpl in H4; Rewrite H4; Unfold Rmin; Case (total_order_Rle a b); Intro; [Assumption | Reflexivity]. -Unfold adapted_couple in H1; Decompose [and] H1; Intros; Apply Rle_antisym. -Apply (H3 O); Simpl; Apply lt_O_Sn. -Simpl in H5; Rewrite H2 in H5; Rewrite H5; Replace (Rmin b b) with (Rmax a b); [Rewrite <- H4; Apply RList_P7; [Assumption | Simpl; Right; Left; Reflexivity] | Unfold Rmin Rmax; Case (total_order_Rle b b); Case (total_order_Rle a b); Intros; Try Assumption Orelse Reflexivity]. -Qed. - -Lemma StepFun_P9 : (a,b:R;f:R->R;l,lf:Rlist) (adapted_couple f a b l lf) -> ``a<>b`` -> (le (2) (Rlength l)). -Intros; Unfold adapted_couple in H; Decompose [and] H; Clear H; Induction l; [Simpl in H4; Discriminate | Induction l; [Simpl in H3; Simpl in H2; Generalize H3; Generalize H2; Unfold Rmin Rmax; Case (total_order_Rle a b); Intros; Elim H0; Rewrite <- H5; Rewrite <- H7; Reflexivity | Simpl; Do 2 Apply le_n_S; Apply le_O_n]]. -Qed. - -Lemma StepFun_P10 : (f:R->R;l,lf:Rlist;a,b:R) ``a<=b`` -> (adapted_couple f a b l lf) -> (EXT l':Rlist | (EXT lf':Rlist | (adapted_couple_opt f a b l' lf'))). -Induction l. -Intros; Unfold adapted_couple in H0; Decompose [and] H0; Simpl in H4; Discriminate. -Intros; Case (Req_EM a b); Intro. -Exists (cons a nil); Exists nil; Unfold adapted_couple_opt; Unfold adapted_couple; Unfold ordered_Rlist; Repeat Split; Try (Intros; Simpl in H3; Elim (lt_n_O ? H3)). -Simpl; Rewrite <- H2; Unfold Rmin; Case (total_order_Rle a a); Intro; Reflexivity. -Simpl; Rewrite <- H2; Unfold Rmax; Case (total_order_Rle a a); Intro; Reflexivity. -Elim (RList_P20 ? (StepFun_P9 H1 H2)); Intros t1 [t2 [t3 H3]]; Induction lf. -Unfold adapted_couple in H1; Decompose [and] H1; Rewrite H3 in H7; Simpl in H7; Discriminate. -Clear Hreclf; Assert H4 : (adapted_couple f t2 b r0 lf). -Rewrite H3 in H1; Assert H4 := (RList_P21 ? ? H3); Simpl in H4; Rewrite H4; EApply StepFun_P7; [Apply H0 | Apply H1]. -Cut ``t2<=b``. -Intro; Assert H6 := (H ? ? ? H5 H4); Case (Req_EM t1 t2); Intro Hyp_eq. -Replace a with t2. -Apply H6. -Rewrite <- Hyp_eq; Rewrite H3 in H1; Unfold adapted_couple in H1; Decompose [and] H1; Clear H1; Simpl in H9; Rewrite H9; Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Elim H6; Clear H6; Intros l' [lf' H6]; Case (Req_EM t2 b); Intro. -Exists (cons a (cons b nil)); Exists (cons r1 nil); Unfold adapted_couple_opt; Unfold adapted_couple; Repeat Split. -Unfold ordered_Rlist; Intros; Simpl in H8; Inversion H8; [Simpl; Assumption | Elim (le_Sn_O ? H10)]. -Simpl; Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Simpl; Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Intros; Simpl in H8; Inversion H8. -Unfold constant_D_eq open_interval; Intros; Simpl; Simpl in H9; Rewrite H3 in H1; Unfold adapted_couple in H1; Decompose [and] H1; Apply (H16 O). -Simpl; Apply lt_O_Sn. -Unfold open_interval; Simpl; Rewrite H7; Simpl in H13; Rewrite H13; Unfold Rmin; Case (total_order_Rle a b); Intro; [Assumption | Elim n; Assumption]. -Elim (le_Sn_O ? H10). -Intros; Simpl in H8; Elim (lt_n_O ? H8). -Intros; Simpl in H8; Inversion H8; [Simpl; Assumption | Elim (le_Sn_O ? H10)]. -Assert Hyp_min : (Rmin t2 b)==t2. -Unfold Rmin; Case (total_order_Rle t2 b); Intro; [Reflexivity | Elim n; Assumption]. -Unfold adapted_couple in H6; Elim H6; Clear H6; Intros; Elim (RList_P20 ? (StepFun_P9 H6 H7)); Intros s1 [s2 [s3 H9]]; Induction lf'. -Unfold adapted_couple in H6; Decompose [and] H6; Rewrite H9 in H13; Simpl in H13; Discriminate. -Clear Hreclf'; Case (Req_EM r1 r2); Intro. -Case (Req_EM (f t2) r1); Intro. -Exists (cons t1 (cons s2 s3)); Exists (cons r1 lf'); Rewrite H3 in H1; Rewrite H9 in H6; Unfold adapted_couple in H6 H1; Decompose [and] H1; Decompose [and] H6; Clear H1 H6; Unfold adapted_couple_opt; Unfold adapted_couple; Repeat Split. -Unfold ordered_Rlist; Intros; Simpl in H1; Induction i. -Simpl; Apply Rle_trans with s1. -Replace s1 with t2. -Apply (H12 O). -Simpl; Apply lt_O_Sn. -Simpl in H19; Rewrite H19; Symmetry; Apply Hyp_min. -Apply (H16 O); Simpl; Apply lt_O_Sn. -Change ``(pos_Rl (cons s2 s3) i)<=(pos_Rl (cons s2 s3) (S i))``; Apply (H16 (S i)); Simpl; Assumption. -Simpl; Simpl in H14; Rewrite H14; Reflexivity. -Simpl; Simpl in H18; Rewrite H18; Unfold Rmax; Case (total_order_Rle a b); Case (total_order_Rle t2 b); Intros; Reflexivity Orelse Elim n; Assumption. -Simpl; Simpl in H20; Apply H20. -Intros; Simpl in H1; Unfold constant_D_eq open_interval; Intros; Induction i. -Simpl; Simpl in H6; Case (total_order_T x t2); Intro. -Elim s; Intro. -Apply (H17 O); [Simpl; Apply lt_O_Sn | Unfold open_interval; Simpl; Elim H6; Intros; Split; Assumption]. -Rewrite b0; Assumption. -Rewrite H10; Apply (H22 O); [Simpl; Apply lt_O_Sn | Unfold open_interval; Simpl; Replace s1 with t2; [Elim H6; Intros; Split; Assumption | Simpl in H19; Rewrite H19; Rewrite Hyp_min; Reflexivity]]. -Simpl; Simpl in H6; Apply (H22 (S i)); [Simpl; Assumption | Unfold open_interval; Simpl; Apply H6]. -Intros; Simpl in H1; Rewrite H10; Change ``(pos_Rl (cons r2 lf') i)<>(pos_Rl (cons r2 lf') (S i))``\/``(f (pos_Rl (cons s1 (cons s2 s3)) (S i)))<>(pos_Rl (cons r2 lf') i)``; Rewrite <- H9; Elim H8; Intros; Apply H6; Simpl; Apply H1. -Intros; Induction i. -Simpl; Red; Intro; Elim Hyp_eq; Apply Rle_antisym. -Apply (H12 O); Simpl; Apply lt_O_Sn. -Rewrite <- Hyp_min; Rewrite H6; Simpl in H19; Rewrite <- H19; Apply (H16 O); Simpl; Apply lt_O_Sn. -Elim H8; Intros; Rewrite H9 in H21; Apply (H21 (S i)); Simpl; Simpl in H1; Apply H1. -Exists (cons t1 l'); Exists (cons r1 (cons r2 lf')); Rewrite H9 in H6; Rewrite H3 in H1; Unfold adapted_couple in H1 H6; Decompose [and] H6; Decompose [and] H1; Clear H6 H1; Unfold adapted_couple_opt; Unfold adapted_couple; Repeat Split. -Rewrite H9; Unfold ordered_Rlist; Intros; Simpl in H1; Induction i. -Simpl; Replace s1 with t2. -Apply (H16 O); Simpl; Apply lt_O_Sn. -Simpl in H14; Rewrite H14; Rewrite Hyp_min; Reflexivity. -Change ``(pos_Rl (cons s1 (cons s2 s3)) i)<=(pos_Rl (cons s1 (cons s2 s3)) (S i))``; Apply (H12 i); Simpl; Apply lt_S_n; Assumption. -Simpl; Simpl in H19; Apply H19. -Rewrite H9; Simpl; Simpl in H13; Rewrite H13; Unfold Rmax; Case (total_order_Rle t2 b); Case (total_order_Rle a b); Intros; Reflexivity Orelse Elim n; Assumption. -Rewrite H9; Simpl; Simpl in H15; Rewrite H15; Reflexivity. -Intros; Simpl in H1; Unfold constant_D_eq open_interval; Intros; Induction i. -Simpl; Rewrite H9 in H6; Simpl in H6; Apply (H22 O). -Simpl; Apply lt_O_Sn. -Unfold open_interval; Simpl. -Replace t2 with s1. -Assumption. -Simpl in H14; Rewrite H14; Rewrite Hyp_min; Reflexivity. -Change (f x)==(pos_Rl (cons r2 lf') i); Clear Hreci; Apply (H17 i). -Simpl; Rewrite H9 in H1; Simpl in H1; Apply lt_S_n; Apply H1. -Rewrite H9 in H6; Unfold open_interval; Apply H6. -Intros; Simpl in H1; Induction i. -Simpl; Rewrite H9; Right; Simpl; Replace s1 with t2. -Assumption. -Simpl in H14; Rewrite H14; Rewrite Hyp_min; Reflexivity. -Elim H8; Intros; Apply (H6 i). -Simpl; Apply lt_S_n; Apply H1. -Intros; Rewrite H9; Induction i. -Simpl; Red; Intro; Elim Hyp_eq; Apply Rle_antisym. -Apply (H16 O); Simpl; Apply lt_O_Sn. -Rewrite <- Hyp_min; Rewrite H6; Simpl in H14; Rewrite <- H14; Right; Reflexivity. -Elim H8; Intros; Rewrite <- H9; Apply (H21 i); Rewrite H9; Rewrite H9 in H1; Simpl; Simpl in H1; Apply lt_S_n; Apply H1. -Exists (cons t1 l'); Exists (cons r1 (cons r2 lf')); Rewrite H9 in H6; Rewrite H3 in H1; Unfold adapted_couple in H1 H6; Decompose [and] H6; Decompose [and] H1; Clear H6 H1; Unfold adapted_couple_opt; Unfold adapted_couple; Repeat Split. -Rewrite H9; Unfold ordered_Rlist; Intros; Simpl in H1; Induction i. -Simpl; Replace s1 with t2. -Apply (H15 O); Simpl; Apply lt_O_Sn. -Simpl in H13; Rewrite H13; Rewrite Hyp_min; Reflexivity. -Change ``(pos_Rl (cons s1 (cons s2 s3)) i)<=(pos_Rl (cons s1 (cons s2 s3)) (S i))``; Apply (H11 i); Simpl; Apply lt_S_n; Assumption. -Simpl; Simpl in H18; Apply H18. -Rewrite H9; Simpl; Simpl in H12; Rewrite H12; Unfold Rmax; Case (total_order_Rle t2 b); Case (total_order_Rle a b); Intros; Reflexivity Orelse Elim n; Assumption. -Rewrite H9; Simpl; Simpl in H14; Rewrite H14; Reflexivity. -Intros; Simpl in H1; Unfold constant_D_eq open_interval; Intros; Induction i. -Simpl; Rewrite H9 in H6; Simpl in H6; Apply (H21 O). -Simpl; Apply lt_O_Sn. -Unfold open_interval; Simpl; Replace t2 with s1. -Assumption. -Simpl in H13; Rewrite H13; Rewrite Hyp_min; Reflexivity. -Change (f x)==(pos_Rl (cons r2 lf') i); Clear Hreci; Apply (H16 i). -Simpl; Rewrite H9 in H1; Simpl in H1; Apply lt_S_n; Apply H1. -Rewrite H9 in H6; Unfold open_interval; Apply H6. -Intros; Simpl in H1; Induction i. -Simpl; Left; Assumption. -Elim H8; Intros; Apply (H6 i). -Simpl; Apply lt_S_n; Apply H1. -Intros; Rewrite H9; Induction i. -Simpl; Red; Intro; Elim Hyp_eq; Apply Rle_antisym. -Apply (H15 O); Simpl; Apply lt_O_Sn. -Rewrite <- Hyp_min; Rewrite H6; Simpl in H13; Rewrite <- H13; Right; Reflexivity. -Elim H8; Intros; Rewrite <- H9; Apply (H20 i); Rewrite H9; Rewrite H9 in H1; Simpl; Simpl in H1; Apply lt_S_n; Apply H1. -Rewrite H3 in H1; Clear H4; Unfold adapted_couple in H1; Decompose [and] H1; Clear H1; Clear H H7 H9; Cut (Rmax a b)==b; [Intro; Rewrite H in H5; Rewrite <- H5; Apply RList_P7; [Assumption | Simpl; Right; Left; Reflexivity] | Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]]. -Qed. - -Lemma StepFun_P11 : (a,b,r,r1,r3,s1,s2,r4:R;r2,lf1,s3,lf2:Rlist;f:R->R) ``a (adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1)) -> (adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2)) -> ``r1<=s2``. -Intros; Unfold adapted_couple_opt in H1; Elim H1; Clear H1; Intros; Unfold adapted_couple in H0 H1; Decompose [and] H0; Decompose [and] H1; Clear H0 H1; Assert H12 : r==s1. -Simpl in H10; Simpl in H5; Rewrite H10; Rewrite H5; Reflexivity. -Assert H14 := (H3 O (lt_O_Sn ?)); Simpl in H14; Elim H14; Intro. -Assert H15 := (H7 O (lt_O_Sn ?)); Simpl in H15; Elim H15; Intro. -Rewrite <- H12 in H1; Case (total_order_Rle r1 s2); Intro; Try Assumption. -Assert H16 : ``s2R;l,lf:Rlist) (adapted_couple_opt f a b l lf) -> (adapted_couple_opt f b a l lf). -Unfold adapted_couple_opt; Unfold adapted_couple; Intros; Decompose [and] H; Clear H; Repeat Split; Try Assumption. -Rewrite H0; Unfold Rmin; Case (total_order_Rle a b); Intro; Case (total_order_Rle b a); Intro; Try Reflexivity. -Apply Rle_antisym; Assumption. -Apply Rle_antisym; Auto with real. -Rewrite H3; Unfold Rmax; Case (total_order_Rle a b); Intro; Case (total_order_Rle b a); Intro; Try Reflexivity. -Apply Rle_antisym; Assumption. -Apply Rle_antisym; Auto with real. -Qed. - -Lemma StepFun_P13 : (a,b,r,r1,r3,s1,s2,r4:R;r2,lf1,s3,lf2:Rlist;f:R->R) ``a<>b`` -> (adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1)) -> (adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2)) -> ``r1<=s2``. -Intros; Case (total_order_T a b); Intro. -Elim s; Intro. -EApply StepFun_P11; [Apply a0 | Apply H0 | Apply H1]. -Elim H; Assumption. -EApply StepFun_P11; [Apply r0 | Apply StepFun_P2; Apply H0 | Apply StepFun_P12; Apply H1]. -Qed. - -Lemma StepFun_P14 : (f:R->R;l1,l2,lf1,lf2:Rlist;a,b:R) ``a<=b`` -> (adapted_couple f a b l1 lf1) -> (adapted_couple_opt f a b l2 lf2) -> (Int_SF lf1 l1)==(Int_SF lf2 l2). -Induction l1. -Intros l2 lf1 lf2 a b Hyp H H0; Unfold adapted_couple in H; Decompose [and] H; Clear H H0 H2 H3 H1 H6; Simpl in H4; Discriminate. -Induction r0. -Intros; Case (Req_EM a b); Intro. -Unfold adapted_couple_opt in H2; Elim H2; Intros; Rewrite (StepFun_P8 H4 H3); Rewrite (StepFun_P8 H1 H3); Reflexivity. -Assert H4 := (StepFun_P9 H1 H3); Simpl in H4; Elim (le_Sn_O ? (le_S_n ? ? H4)). -Intros; Clear H; Unfold adapted_couple_opt in H3; Elim H3; Clear H3; Intros; Case (Req_EM a b); Intro. -Rewrite (StepFun_P8 H2 H4); Rewrite (StepFun_P8 H H4); Reflexivity. -Assert Hyp_min : (Rmin a b)==a. -Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Assert Hyp_max : (Rmax a b)==b. -Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Elim (RList_P20 ? (StepFun_P9 H H4)); Intros s1 [s2 [s3 H5]]; Rewrite H5 in H; Rewrite H5; Induction lf1. -Unfold adapted_couple in H2; Decompose [and] H2; Clear H H2 H4 H5 H3 H6 H8 H7 H11; Simpl in H9; Discriminate. -Clear Hreclf1; Induction lf2. -Unfold adapted_couple in H; Decompose [and] H; Clear H H2 H4 H5 H3 H6 H8 H7 H11; Simpl in H9; Discriminate. -Clear Hreclf2; Assert H6 : r==s1. -Unfold adapted_couple in H H2; Decompose [and] H; Decompose [and] H2; Clear H H2; Simpl in H13; Simpl in H8; Rewrite H13; Rewrite H8; Reflexivity. -Assert H7 : r3==r4\/r==r1. -Case (Req_EM r r1); Intro. -Right; Assumption. -Left; Cut ``r1<=s2``. -Intro; Unfold adapted_couple in H2 H; Decompose [and] H; Decompose [and] H2; Clear H H2; Pose x := ``(r+r1)/2``; Assert H18 := (H14 O); Assert H20 := (H19 O); Unfold constant_D_eq open_interval in H18 H20; Simpl in H18; Simpl in H20; Rewrite <- (H18 (lt_O_Sn ?) x). -Rewrite <- (H20 (lt_O_Sn ?) x). -Reflexivity. -Assert H21 := (H13 O (lt_O_Sn ?)); Simpl in H21; Elim H21; Intro; [Idtac | Elim H7; Assumption]; Unfold x; Split. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Apply H | DiscrR]]. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite <- (Rplus_sym r1); Rewrite double; Apply Rlt_compatibility; Apply H | DiscrR]]. -Rewrite <- H6; Assert H21 := (H13 O (lt_O_Sn ?)); Simpl in H21; Elim H21; Intro; [Idtac | Elim H7; Assumption]; Unfold x; Split. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Apply H | DiscrR]]. -Apply Rlt_le_trans with r1; [Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite <- (Rplus_sym r1); Rewrite double; Apply Rlt_compatibility; Apply H | DiscrR]] | Assumption]. -EApply StepFun_P13. -Apply H4. -Apply H2. -Unfold adapted_couple_opt; Split. -Apply H. -Rewrite H5 in H3; Apply H3. -Assert H8 : ``r1<=s2``. -EApply StepFun_P13. -Apply H4. -Apply H2. -Unfold adapted_couple_opt; Split. -Apply H. -Rewrite H5 in H3; Apply H3. -Elim H7; Intro. -Simpl; Elim H8; Intro. -Replace ``r4*(s2-s1)`` with ``r3*(r1-r)+r3*(s2-r1)``; [Idtac | Rewrite H9; Rewrite H6; Ring]. -Rewrite Rplus_assoc; Apply Rplus_plus_r; Change (Int_SF lf1 (cons r1 r2))==(Int_SF (cons r3 lf2) (cons r1 (cons s2 s3))); Apply H0 with r1 b. -Unfold adapted_couple in H2; Decompose [and] H2; Clear H2; Replace b with (Rmax a b). -Rewrite <- H12; Apply RList_P7; [Assumption | Simpl; Right; Left; Reflexivity]. -EApply StepFun_P7. -Apply H1. -Apply H2. -Unfold adapted_couple_opt; Split. -Apply StepFun_P7 with a a r3. -Apply H1. -Unfold adapted_couple in H2 H; Decompose [and] H2; Decompose [and] H; Clear H H2; Assert H20 : r==a. -Simpl in H13; Rewrite H13; Apply Hyp_min. -Unfold adapted_couple; Repeat Split. -Unfold ordered_Rlist; Intros; Simpl in H; Induction i. -Simpl; Rewrite <- H20; Apply (H11 O). -Simpl; Apply lt_O_Sn. -Induction i. -Simpl; Assumption. -Change ``(pos_Rl (cons s2 s3) i)<=(pos_Rl (cons s2 s3) (S i))``; Apply (H15 (S i)); Simpl; Apply lt_S_n; Assumption. -Simpl; Symmetry; Apply Hyp_min. -Rewrite <- H17; Reflexivity. -Simpl in H19; Simpl; Rewrite H19; Reflexivity. -Intros; Simpl in H; Unfold constant_D_eq open_interval; Intros; Induction i. -Simpl; Apply (H16 O). -Simpl; Apply lt_O_Sn. -Simpl in H2; Rewrite <- H20 in H2; Unfold open_interval; Simpl; Apply H2. -Clear Hreci; Induction i. -Simpl; Simpl in H2; Rewrite H9; Apply (H21 O). -Simpl; Apply lt_O_Sn. -Unfold open_interval; Simpl; Elim H2; Intros; Split. -Apply Rle_lt_trans with r1; Try Assumption; Rewrite <- H6; Apply (H11 O); Simpl; Apply lt_O_Sn. -Assumption. -Clear Hreci; Simpl; Apply (H21 (S i)). -Simpl; Apply lt_S_n; Assumption. -Unfold open_interval; Apply H2. -Elim H3; Clear H3; Intros; Split. -Rewrite H9; Change (i:nat) (lt i (pred (Rlength (cons r4 lf2)))) ->``(pos_Rl (cons r4 lf2) i)<>(pos_Rl (cons r4 lf2) (S i))``\/``(f (pos_Rl (cons s1 (cons s2 s3)) (S i)))<>(pos_Rl (cons r4 lf2) i)``; Rewrite <- H5; Apply H3. -Rewrite H5 in H11; Intros; Simpl in H12; Induction i. -Simpl; Red; Intro; Rewrite H13 in H10; Elim (Rlt_antirefl ? H10). -Clear Hreci; Apply (H11 (S i)); Simpl; Apply H12. -Rewrite H9; Rewrite H10; Rewrite H6; Apply Rplus_plus_r; Rewrite <- H10; Apply H0 with r1 b. -Unfold adapted_couple in H2; Decompose [and] H2; Clear H2; Replace b with (Rmax a b). -Rewrite <- H12; Apply RList_P7; [Assumption | Simpl; Right; Left; Reflexivity]. -EApply StepFun_P7. -Apply H1. -Apply H2. -Unfold adapted_couple_opt; Split. -Apply StepFun_P7 with a a r3. -Apply H1. -Unfold adapted_couple in H2 H; Decompose [and] H2; Decompose [and] H; Clear H H2; Assert H20 : r==a. -Simpl in H13; Rewrite H13; Apply Hyp_min. -Unfold adapted_couple; Repeat Split. -Unfold ordered_Rlist; Intros; Simpl in H; Induction i. -Simpl; Rewrite <- H20; Apply (H11 O); Simpl; Apply lt_O_Sn. -Rewrite H10; Apply (H15 (S i)); Simpl; Assumption. -Simpl; Symmetry; Apply Hyp_min. -Rewrite <- H17; Rewrite H10; Reflexivity. -Simpl in H19; Simpl; Apply H19. -Intros; Simpl in H; Unfold constant_D_eq open_interval; Intros; Induction i. -Simpl; Apply (H16 O). -Simpl; Apply lt_O_Sn. -Simpl in H2; Rewrite <- H20 in H2; Unfold open_interval; Simpl; Apply H2. -Clear Hreci; Simpl; Apply (H21 (S i)). -Simpl; Assumption. -Rewrite <- H10; Unfold open_interval; Apply H2. -Elim H3; Clear H3; Intros; Split. -Rewrite H5 in H3; Intros; Apply (H3 (S i)). -Simpl; Replace (Rlength lf2) with (S (pred (Rlength lf2))). -Apply lt_n_S; Apply H12. -Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H12; Elim (lt_n_O ? H12). -Intros; Simpl in H12; Rewrite H10; Rewrite H5 in H11; Apply (H11 (S i)); Simpl; Apply lt_n_S; Apply H12. -Simpl; Rewrite H9; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rmult_Or; Rewrite Rplus_Ol; Change (Int_SF lf1 (cons r1 r2))==(Int_SF (cons r4 lf2) (cons s1 (cons s2 s3))); EApply H0. -Apply H1. -2: Rewrite H5 in H3; Unfold adapted_couple_opt; Split; Assumption. -Assert H10 : r==a. -Unfold adapted_couple in H2; Decompose [and] H2; Clear H2; Simpl in H12; Rewrite H12; Apply Hyp_min. -Rewrite <- H9; Rewrite H10; Apply StepFun_P7 with a r r3; [Apply H1 | Pattern 2 a; Rewrite <- H10; Pattern 2 r; Rewrite H9; Apply H2]. -Qed. - -Lemma StepFun_P15 : (f:R->R;l1,l2,lf1,lf2:Rlist;a,b:R) (adapted_couple f a b l1 lf1) -> (adapted_couple_opt f a b l2 lf2) -> (Int_SF lf1 l1)==(Int_SF lf2 l2). -Intros; Case (total_order_Rle a b); Intro; [Apply (StepFun_P14 r H H0) | Assert H1 : ``b<=a``; [Auto with real | EApply StepFun_P14; [Apply H1 | Apply StepFun_P2; Apply H | Apply StepFun_P12; Apply H0]]]. -Qed. - -Lemma StepFun_P16 : (f:R->R;l,lf:Rlist;a,b:R) (adapted_couple f a b l lf) -> (EXT l':Rlist | (EXT lf':Rlist | (adapted_couple_opt f a b l' lf'))). -Intros; Case (total_order_Rle a b); Intro; [Apply (StepFun_P10 r H) | Assert H1 : ``b<=a``; [Auto with real | Assert H2 := (StepFun_P10 H1 (StepFun_P2 H)); Elim H2; Intros l' [lf' H3]; Exists l'; Exists lf'; Apply StepFun_P12; Assumption]]. -Qed. - -Lemma StepFun_P17 : (f:R->R;l1,l2,lf1,lf2:Rlist;a,b:R) (adapted_couple f a b l1 lf1) -> (adapted_couple f a b l2 lf2) -> (Int_SF lf1 l1)==(Int_SF lf2 l2). -Intros; Elim (StepFun_P16 H); Intros l' [lf' H1]; Rewrite (StepFun_P15 H H1); Rewrite (StepFun_P15 H0 H1); Reflexivity. -Qed. - -Lemma StepFun_P18 : (a,b,c:R) (RiemannInt_SF (mkStepFun (StepFun_P4 a b c)))==``c*(b-a)``. -Intros; Unfold RiemannInt_SF; Case (total_order_Rle a b); Intro. -Replace (Int_SF (subdivision_val (mkStepFun (StepFun_P4 a b c))) (subdivision (mkStepFun (StepFun_P4 a b c)))) with (Int_SF (cons c nil) (cons a (cons b nil))); [Simpl; Ring | Apply StepFun_P17 with (fct_cte c) a b; [Apply StepFun_P3; Assumption | Apply (StepFun_P1 (mkStepFun (StepFun_P4 a b c)))]]. -Replace (Int_SF (subdivision_val (mkStepFun (StepFun_P4 a b c))) (subdivision (mkStepFun (StepFun_P4 a b c)))) with (Int_SF (cons c nil) (cons b (cons a nil))); [Simpl; Ring | Apply StepFun_P17 with (fct_cte c) a b; [Apply StepFun_P2; Apply StepFun_P3; Auto with real | Apply (StepFun_P1 (mkStepFun (StepFun_P4 a b c)))]]. -Qed. - -Lemma StepFun_P19 : (l1:Rlist;f,g:R->R;l:R) (Int_SF (FF l1 [x:R]``(f x)+l*(g x)``) l1)==``(Int_SF (FF l1 f) l1)+l*(Int_SF (FF l1 g) l1)``. -Intros; Induction l1; [Simpl; Ring | Induction l1; Simpl; [Ring | Simpl in Hrecl1; Rewrite Hrecl1; Ring]]. -Qed. - -Lemma StepFun_P20 : (l:Rlist;f:R->R) (lt O (Rlength l)) -> (Rlength l)=(S (Rlength (FF l f))). -Intros l f H; NewInduction l; [Elim (lt_n_n ? H) | Simpl; Rewrite RList_P18; Rewrite RList_P14; Reflexivity]. -Qed. - -Lemma StepFun_P21 : (a,b:R;f:R->R;l:Rlist) (is_subdivision f a b l) -> (adapted_couple f a b l (FF l f)). -Intros; Unfold adapted_couple; Unfold is_subdivision in X; Unfold adapted_couple in X; Elim X; Clear X; Intros; Decompose [and] p; Clear p; Repeat Split; Try Assumption. -Apply StepFun_P20; Rewrite H2; Apply lt_O_Sn. -Intros; Assert H5 := (H4 ? H3); Unfold constant_D_eq open_interval in H5; Unfold constant_D_eq open_interval; Intros; Induction l. -Discriminate. -Unfold FF; Rewrite RList_P12. -Simpl; Change (f x0)==(f (pos_Rl (mid_Rlist (cons r l) r) (S i))); Rewrite RList_P13; Try Assumption; Rewrite (H5 x0 H6); Rewrite H5. -Reflexivity. -Split. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Elim H6; Intros; Apply Rlt_trans with x0; Assumption | DiscrR]]. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Rewrite (Rplus_sym (pos_Rl (cons r l) i)); Apply Rlt_compatibility; Elim H6; Intros; Apply Rlt_trans with x0; Assumption | DiscrR]]. -Rewrite RList_P14; Simpl in H3; Apply H3. -Qed. - -Lemma StepFun_P22 : (a,b:R;f,g:R->R;lf,lg:Rlist) ``a<=b`` -> (is_subdivision f a b lf) -> (is_subdivision g a b lg) -> (is_subdivision f a b (cons_ORlist lf lg)). -Unfold is_subdivision; Intros a b f g lf lg Hyp X X0; Elim X; Elim X0; Clear X X0; Intros lg0 p lf0 p0; Assert Hyp_min : (Rmin a b)==a. -Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Assert Hyp_max : (Rmax a b)==b. -Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Apply existTT with (FF (cons_ORlist lf lg) f); Unfold adapted_couple in p p0; Decompose [and] p; Decompose [and] p0; Clear p p0; Rewrite Hyp_min in H6; Rewrite Hyp_min in H1; Rewrite Hyp_max in H0; Rewrite Hyp_max in H5; Unfold adapted_couple; Repeat Split. -Apply RList_P2; Assumption. -Rewrite Hyp_min; Symmetry; Apply Rle_antisym. -Induction lf. -Simpl; Right; Symmetry; Assumption. -Assert H10 : (In (pos_Rl (cons_ORlist (cons r lf) lg) (0)) (cons_ORlist (cons r lf) lg)). -Elim (RList_P3 (cons_ORlist (cons r lf) lg) (pos_Rl (cons_ORlist (cons r lf) lg) (0))); Intros _ H10; Apply H10; Exists O; Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_O_Sn]. -Elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) (0))); Intros H12 _; Assert H13 := (H12 H10); Elim H13; Intro. -Elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) (0))); Intros H11 _; Assert H14 := (H11 H8); Elim H14; Intros; Elim H15; Clear H15; Intros; Rewrite H15; Rewrite <- H6; Elim (RList_P6 (cons r lf)); Intros; Apply H17; [Assumption | Apply le_O_n | Assumption]. -Elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) (0))); Intros H11 _; Assert H14 := (H11 H8); Elim H14; Intros; Elim H15; Clear H15; Intros; Rewrite H15; Rewrite <- H1; Elim (RList_P6 lg); Intros; Apply H17; [Assumption | Apply le_O_n | Assumption]. -Induction lf. -Simpl; Right; Assumption. -Assert H8 : (In a (cons_ORlist (cons r lf) lg)). -Elim (RList_P9 (cons r lf) lg a); Intros; Apply H10; Left; Elim (RList_P3 (cons r lf) a); Intros; Apply H12; Exists O; Split; [Symmetry; Assumption | Simpl; Apply lt_O_Sn]. -Apply RList_P5; [Apply RList_P2; Assumption | Assumption]. -Rewrite Hyp_max; Apply Rle_antisym. -Induction lf. -Simpl; Right; Assumption. -Assert H8 : (In (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg)))) (cons_ORlist (cons r lf) lg)). -Elim (RList_P3 (cons_ORlist (cons r lf) lg) (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg))))); Intros _ H10; Apply H10; Exists (pred (Rlength (cons_ORlist (cons r lf) lg))); Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_n_Sn]. -Elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg))))); Intros H10 _. -Assert H11 := (H10 H8); Elim H11; Intro. -Elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg))))); Intros H13 _; Assert H14 := (H13 H12); Elim H14; Intros; Elim H15; Clear H15; Intros; Rewrite H15; Rewrite <- H5; Elim (RList_P6 (cons r lf)); Intros; Apply H17; [Assumption | Simpl; Simpl in H14; Apply lt_n_Sm_le; Assumption | Simpl; Apply lt_n_Sn]. -Elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg))))); Intros H13 _; Assert H14 := (H13 H12); Elim H14; Intros; Elim H15; Clear H15; Intros. -Rewrite H15; Assert H17 : (Rlength lg)=(S (pred (Rlength lg))). -Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H17 in H16; Elim (lt_n_O ? H16). -Rewrite <- H0; Elim (RList_P6 lg); Intros; Apply H18; [Assumption | Rewrite H17 in H16; Apply lt_n_Sm_le; Assumption | Apply lt_pred_n_n; Rewrite H17; Apply lt_O_Sn]. -Induction lf. -Simpl; Right; Symmetry; Assumption. -Assert H8 : (In b (cons_ORlist (cons r lf) lg)). -Elim (RList_P9 (cons r lf) lg b); Intros; Apply H10; Left; Elim (RList_P3 (cons r lf) b); Intros; Apply H12; Exists (pred (Rlength (cons r lf))); Split; [Symmetry; Assumption | Simpl; Apply lt_n_Sn]. -Apply RList_P7; [Apply RList_P2; Assumption | Assumption]. -Apply StepFun_P20; Rewrite RList_P11; Rewrite H2; Rewrite H7; Simpl; Apply lt_O_Sn. -Intros; Unfold constant_D_eq open_interval; Intros; Cut (EXT l:R | (constant_D_eq f (open_interval (pos_Rl (cons_ORlist lf lg) i) (pos_Rl (cons_ORlist lf lg) (S i))) l)). -Intros; Elim H11; Clear H11; Intros; Assert H12 := H11; Assert Hyp_cons : (EXT r:R | (EXT r0:Rlist | (cons_ORlist lf lg)==(cons r r0))). -Apply RList_P19; Red; Intro; Rewrite H13 in H8; Elim (lt_n_O ? H8). -Elim Hyp_cons; Clear Hyp_cons; Intros r [r0 Hyp_cons]; Rewrite Hyp_cons; Unfold FF; Rewrite RList_P12. -Change (f x)==(f (pos_Rl (mid_Rlist (cons r r0) r) (S i))); Rewrite <- Hyp_cons; Rewrite RList_P13. -Assert H13 := (RList_P2 ? ? H ? H8); Elim H13; Intro. -Unfold constant_D_eq open_interval in H11 H12; Rewrite (H11 x H10); Assert H15 : ``(pos_Rl (cons_ORlist lf lg) i)<((pos_Rl (cons_ORlist lf lg) i)+(pos_Rl (cons_ORlist lf lg) (S i)))/2<(pos_Rl (cons_ORlist lf lg) (S i))``. -Split. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Assumption | DiscrR]]. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Rewrite (Rplus_sym (pos_Rl (cons_ORlist lf lg) i)); Apply Rlt_compatibility; Assumption | DiscrR]]. -Rewrite (H11 ? H15); Reflexivity. -Elim H10; Intros; Rewrite H14 in H15; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H16 H15)). -Apply H8. -Rewrite RList_P14; Rewrite Hyp_cons in H8; Simpl in H8; Apply H8. -Assert H11 : ``aR;lf,lg:Rlist) (is_subdivision f a b lf) -> (is_subdivision g a b lg) -> (is_subdivision f a b (cons_ORlist lf lg)). -Intros; Case (total_order_Rle a b); Intro; [Apply StepFun_P22 with g; Assumption | Apply StepFun_P5; Apply StepFun_P22 with g; [Auto with real | Apply StepFun_P5; Assumption | Apply StepFun_P5; Assumption]]. -Qed. - -Lemma StepFun_P24 : (a,b:R;f,g:R->R;lf,lg:Rlist) ``a<=b`` -> (is_subdivision f a b lf) -> (is_subdivision g a b lg) -> (is_subdivision g a b (cons_ORlist lf lg)). -Unfold is_subdivision; Intros a b f g lf lg Hyp X X0; Elim X; Elim X0; Clear X X0; Intros lg0 p lf0 p0; Assert Hyp_min : (Rmin a b)==a. -Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Assert Hyp_max : (Rmax a b)==b. -Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Apply existTT with (FF (cons_ORlist lf lg) g); Unfold adapted_couple in p p0; Decompose [and] p; Decompose [and] p0; Clear p p0; Rewrite Hyp_min in H1; Rewrite Hyp_min in H6; Rewrite Hyp_max in H0; Rewrite Hyp_max in H5; Unfold adapted_couple; Repeat Split. -Apply RList_P2; Assumption. -Rewrite Hyp_min; Symmetry; Apply Rle_antisym. -Induction lf. -Simpl; Right; Symmetry; Assumption. -Assert H10 : (In (pos_Rl (cons_ORlist (cons r lf) lg) (0)) (cons_ORlist (cons r lf) lg)). -Elim (RList_P3 (cons_ORlist (cons r lf) lg) (pos_Rl (cons_ORlist (cons r lf) lg) (0))); Intros _ H10; Apply H10; Exists O; Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_O_Sn]. -Elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) (0))); Intros H12 _; Assert H13 := (H12 H10); Elim H13; Intro. -Elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) (0))); Intros H11 _; Assert H14 := (H11 H8); Elim H14; Intros; Elim H15; Clear H15; Intros; Rewrite H15; Rewrite <- H6; Elim (RList_P6 (cons r lf)); Intros; Apply H17; [Assumption | Apply le_O_n | Assumption]. -Elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) (0))); Intros H11 _; Assert H14 := (H11 H8); Elim H14; Intros; Elim H15; Clear H15; Intros; Rewrite H15; Rewrite <- H1; Elim (RList_P6 lg); Intros; Apply H17; [Assumption | Apply le_O_n | Assumption]. -Induction lf. -Simpl; Right; Assumption. -Assert H8 : (In a (cons_ORlist (cons r lf) lg)). -Elim (RList_P9 (cons r lf) lg a); Intros; Apply H10; Left; Elim (RList_P3 (cons r lf) a); Intros; Apply H12; Exists O; Split; [Symmetry; Assumption | Simpl; Apply lt_O_Sn]. -Apply RList_P5; [Apply RList_P2; Assumption | Assumption]. -Rewrite Hyp_max; Apply Rle_antisym. -Induction lf. -Simpl; Right; Assumption. -Assert H8 : (In (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg)))) (cons_ORlist (cons r lf) lg)). -Elim (RList_P3 (cons_ORlist (cons r lf) lg) (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg))))); Intros _ H10; Apply H10; Exists (pred (Rlength (cons_ORlist (cons r lf) lg))); Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_n_Sn]. -Elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg))))); Intros H10 _; Assert H11 := (H10 H8); Elim H11; Intro. -Elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg))))); Intros H13 _; Assert H14 := (H13 H12); Elim H14; Intros; Elim H15; Clear H15; Intros; Rewrite H15; Rewrite <- H5; Elim (RList_P6 (cons r lf)); Intros; Apply H17; [Assumption | Simpl; Simpl in H14; Apply lt_n_Sm_le; Assumption | Simpl; Apply lt_n_Sn]. -Elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg))))); Intros H13 _; Assert H14 := (H13 H12); Elim H14; Intros; Elim H15; Clear H15; Intros; Rewrite H15; Assert H17 : (Rlength lg)=(S (pred (Rlength lg))). -Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H17 in H16; Elim (lt_n_O ? H16). -Rewrite <- H0; Elim (RList_P6 lg); Intros; Apply H18; [Assumption | Rewrite H17 in H16; Apply lt_n_Sm_le; Assumption | Apply lt_pred_n_n; Rewrite H17; Apply lt_O_Sn]. -Induction lf. -Simpl; Right; Symmetry; Assumption. -Assert H8 : (In b (cons_ORlist (cons r lf) lg)). -Elim (RList_P9 (cons r lf) lg b); Intros; Apply H10; Left; Elim (RList_P3 (cons r lf) b); Intros; Apply H12; Exists (pred (Rlength (cons r lf))); Split; [Symmetry; Assumption | Simpl; Apply lt_n_Sn]. -Apply RList_P7; [Apply RList_P2; Assumption | Assumption]. -Apply StepFun_P20; Rewrite RList_P11; Rewrite H7; Rewrite H2; Simpl; Apply lt_O_Sn. -Unfold constant_D_eq open_interval; Intros; Cut (EXT l:R | (constant_D_eq g (open_interval (pos_Rl (cons_ORlist lf lg) i) (pos_Rl (cons_ORlist lf lg) (S i))) l)). -Intros; Elim H11; Clear H11; Intros; Assert H12 := H11; Assert Hyp_cons : (EXT r:R | (EXT r0:Rlist | (cons_ORlist lf lg)==(cons r r0))). -Apply RList_P19; Red; Intro; Rewrite H13 in H8; Elim (lt_n_O ? H8). -Elim Hyp_cons; Clear Hyp_cons; Intros r [r0 Hyp_cons]; Rewrite Hyp_cons; Unfold FF; Rewrite RList_P12. -Change (g x)==(g (pos_Rl (mid_Rlist (cons r r0) r) (S i))); Rewrite <- Hyp_cons; Rewrite RList_P13. -Assert H13 := (RList_P2 ? ? H ? H8); Elim H13; Intro. -Unfold constant_D_eq open_interval in H11 H12; Rewrite (H11 x H10); Assert H15 : ``(pos_Rl (cons_ORlist lf lg) i)<((pos_Rl (cons_ORlist lf lg) i)+(pos_Rl (cons_ORlist lf lg) (S i)))/2<(pos_Rl (cons_ORlist lf lg) (S i))``. -Split. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Assumption | DiscrR]]. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Rewrite (Rplus_sym (pos_Rl (cons_ORlist lf lg) i)); Apply Rlt_compatibility; Assumption | DiscrR]]. -Rewrite (H11 ? H15); Reflexivity. -Elim H10; Intros; Rewrite H14 in H15; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H16 H15)). -Apply H8. -Rewrite RList_P14; Rewrite Hyp_cons in H8; Simpl in H8; Apply H8. -Assert H11 : ``aR;lf,lg:Rlist) (is_subdivision f a b lf) -> (is_subdivision g a b lg) -> (is_subdivision g a b (cons_ORlist lf lg)). -Intros a b f g lf lg H H0; Case (total_order_Rle a b); Intro; [Apply StepFun_P24 with f; Assumption | Apply StepFun_P5; Apply StepFun_P24 with f; [Auto with real | Apply StepFun_P5; Assumption | Apply StepFun_P5; Assumption]]. -Qed. - -Lemma StepFun_P26 : (a,b,l:R;f,g:R->R;l1:Rlist) (is_subdivision f a b l1) -> (is_subdivision g a b l1) -> (is_subdivision [x:R]``(f x)+l*(g x)`` a b l1). -Intros a b l f g l1; Unfold is_subdivision; Intros; Elim X; Elim X0; Intros; Clear X X0; Unfold adapted_couple in p p0; Decompose [and] p; Decompose [and] p0; Clear p p0; Apply existTT with (FF l1 [x:R]``(f x)+l*(g x)``); Unfold adapted_couple; Repeat Split; Try Assumption. -Apply StepFun_P20; Apply neq_O_lt; Red; Intro; Rewrite <- H8 in H7; Discriminate. -Intros; Unfold constant_D_eq open_interval; Unfold constant_D_eq open_interval in H9 H4; Intros; Rewrite (H9 ? H8 ? H10); Rewrite (H4 ? H8 ? H10); Assert H11 : ~l1==nil. -Red; Intro; Rewrite H11 in H8; Elim (lt_n_O ? H8). -Assert H12 := (RList_P19 ? H11); Elim H12; Clear H12; Intros r [r0 H12]; Rewrite H12; Unfold FF; Change ``(pos_Rl x0 i)+l*(pos_Rl x i)`` == (pos_Rl (app_Rlist (mid_Rlist (cons r r0) r) [x2:R]``(f x2)+l*(g x2)``) (S i)); Rewrite RList_P12. -Rewrite RList_P13. -Rewrite <- H12; Rewrite (H9 ? H8); Try Rewrite (H4 ? H8); Reflexivity Orelse (Elim H10; Clear H10; Intros; Split; [Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Apply Rlt_trans with x1; Assumption | DiscrR]] | Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Rewrite (Rplus_sym (pos_Rl l1 i)); Apply Rlt_compatibility; Apply Rlt_trans with x1; Assumption | DiscrR]]]). -Rewrite <- H12; Assumption. -Rewrite RList_P14; Simpl; Rewrite H12 in H8; Simpl in H8; Apply lt_n_S; Apply H8. -Qed. - -Lemma StepFun_P27 : (a,b,l:R;f,g:R->R;lf,lg:Rlist) (is_subdivision f a b lf) -> (is_subdivision g a b lg) -> (is_subdivision [x:R]``(f x)+l*(g x)`` a b (cons_ORlist lf lg)). -Intros a b l f g lf lg H H0; Apply StepFun_P26; [Apply StepFun_P23 with g; Assumption | Apply StepFun_P25 with f; Assumption]. -Qed. - -(* The set of step functions on [a,b] is a vectorial space *) -Lemma StepFun_P28 : (a,b,l:R;f,g:(StepFun a b)) (IsStepFun [x:R]``(f x)+l*(g x)`` a b). -Intros a b l f g; Unfold IsStepFun; Assert H := (pre f); Assert H0 := (pre g); Unfold IsStepFun in H H0; Elim H; Elim H0; Intros; Apply Specif.existT with (cons_ORlist x0 x); Apply StepFun_P27; Assumption. -Qed. - -Lemma StepFun_P29 : (a,b:R;f:(StepFun a b)) (is_subdivision f a b (subdivision f)). -Intros a b f; Unfold is_subdivision; Apply existTT with (subdivision_val f); Apply StepFun_P1. -Qed. - -Lemma StepFun_P30 : (a,b,l:R;f,g:(StepFun a b)) ``(RiemannInt_SF (mkStepFun (StepFun_P28 l f g)))==(RiemannInt_SF f)+l*(RiemannInt_SF g)``. -Intros a b l f g; Unfold RiemannInt_SF; Case (total_order_Rle a b); (Intro; Replace ``(Int_SF (subdivision_val (mkStepFun (StepFun_P28 l f g))) (subdivision (mkStepFun (StepFun_P28 l f g))))`` with (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) [x:R]``(f x)+l*(g x)``) (cons_ORlist (subdivision f) (subdivision g))); [Rewrite StepFun_P19; Replace (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) f) (cons_ORlist (subdivision f) (subdivision g))) with (Int_SF (subdivision_val f) (subdivision f)); [Replace (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) g) (cons_ORlist (subdivision f) (subdivision g))) with (Int_SF (subdivision_val g) (subdivision g)); [Ring | Apply StepFun_P17 with (fe g) a b; [Apply StepFun_P1 | Apply StepFun_P21; Apply StepFun_P25 with (fe f); Apply StepFun_P29]] | Apply StepFun_P17 with (fe f) a b; [Apply StepFun_P1 | Apply StepFun_P21; Apply StepFun_P23 with (fe g); Apply StepFun_P29]] | Apply StepFun_P17 with [x:R]``(f x)+l*(g x)`` a b; [Apply StepFun_P21; Apply StepFun_P27; Apply StepFun_P29 | Apply (StepFun_P1 (mkStepFun (StepFun_P28 l f g)))]]). -Qed. - -Lemma StepFun_P31 : (a,b:R;f:R->R;l,lf:Rlist) (adapted_couple f a b l lf) -> (adapted_couple [x:R](Rabsolu (f x)) a b l (app_Rlist lf Rabsolu)). -Unfold adapted_couple; Intros; Decompose [and] H; Clear H; Repeat Split; Try Assumption. -Symmetry; Rewrite H3; Rewrite RList_P18; Reflexivity. -Intros; Unfold constant_D_eq open_interval; Unfold constant_D_eq open_interval in H5; Intros; Rewrite (H5 ? H ? H4); Rewrite RList_P12; [Reflexivity | Rewrite H3 in H; Simpl in H; Apply H]. -Qed. - -Lemma StepFun_P32 : (a,b:R;f:(StepFun a b)) (IsStepFun [x:R](Rabsolu (f x)) a b). -Intros a b f; Unfold IsStepFun; Apply Specif.existT with (subdivision f); Unfold is_subdivision; Apply existTT with (app_Rlist (subdivision_val f) Rabsolu); Apply StepFun_P31; Apply StepFun_P1. -Qed. - -Lemma StepFun_P33 : (l2,l1:Rlist) (ordered_Rlist l1) -> ``(Rabsolu (Int_SF l2 l1))<=(Int_SF (app_Rlist l2 Rabsolu) l1)``. -Induction l2; Intros. -Simpl; Rewrite Rabsolu_R0; Right; Reflexivity. -Simpl; Induction l1. -Rewrite Rabsolu_R0; Right; Reflexivity. -Induction l1. -Rewrite Rabsolu_R0; Right; Reflexivity. -Apply Rle_trans with ``(Rabsolu (r*(r2-r1)))+(Rabsolu (Int_SF r0 (cons r2 l1)))``. -Apply Rabsolu_triang. -Rewrite Rabsolu_mult; Rewrite (Rabsolu_right ``r2-r1``); [Apply Rle_compatibility; Apply H; Apply RList_P4 with r1; Assumption | Apply Rge_minus; Apply Rle_sym1; Apply (H0 O); Simpl; Apply lt_O_Sn]. -Qed. - -Lemma StepFun_P34 : (a,b:R;f:(StepFun a b)) ``a<=b`` -> ``(Rabsolu (RiemannInt_SF f))<=(RiemannInt_SF (mkStepFun (StepFun_P32 f)))``. -Intros; Unfold RiemannInt_SF; Case (total_order_Rle a b); Intro. -Replace (Int_SF (subdivision_val (mkStepFun (StepFun_P32 f))) (subdivision (mkStepFun (StepFun_P32 f)))) with (Int_SF (app_Rlist (subdivision_val f) Rabsolu) (subdivision f)). -Apply StepFun_P33; Assert H0 := (StepFun_P29 f); Unfold is_subdivision in H0; Elim H0; Intros; Unfold adapted_couple in p; Decompose [and] p; Assumption. -Apply StepFun_P17 with [x:R](Rabsolu (f x)) a b; [Apply StepFun_P31; Apply StepFun_P1 | Apply (StepFun_P1 (mkStepFun (StepFun_P32 f)))]. -Elim n; Assumption. -Qed. - -Lemma StepFun_P35 : (l:Rlist;a,b:R;f,g:R->R) (ordered_Rlist l) -> (pos_Rl l O)==a -> (pos_Rl l (pred (Rlength l)))==b -> ((x:R)``a``(f x)<=(g x)``) -> ``(Int_SF (FF l f) l)<=(Int_SF (FF l g) l)``. -Induction l; Intros. -Right; Reflexivity. -Simpl; Induction r0. -Right; Reflexivity. -Simpl; Apply Rplus_le. -Case (Req_EM r r0); Intro. -Rewrite H4; Right; Ring. -Do 2 Rewrite <- (Rmult_sym ``r0-r``); Apply Rle_monotony. -Apply Rle_sym2; Apply Rge_minus; Apply Rle_sym1; Apply (H0 O); Simpl; Apply lt_O_Sn. -Apply H3; Split. -Apply Rlt_monotony_contra with ``2``. -Sup0. -Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. -Assert H5 : r==a. -Apply H1. -Rewrite H5; Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility. -Assert H6 := (H0 O (lt_O_Sn ?)). -Simpl in H6. -Elim H6; Intro. -Rewrite H5 in H7; Apply H7. -Elim H4; Assumption. -DiscrR. -Apply Rlt_monotony_contra with ``2``. -Sup0. -Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1l; Rewrite double; Assert H5 : ``r0<=b``. -Replace b with (pos_Rl (cons r (cons r0 r1)) (pred (Rlength (cons r (cons r0 r1))))). -Replace r0 with (pos_Rl (cons r (cons r0 r1)) (S O)). -Elim (RList_P6 (cons r (cons r0 r1))); Intros; Apply H5. -Assumption. -Simpl; Apply le_n_S. -Apply le_O_n. -Simpl; Apply lt_n_Sn. -Reflexivity. -Apply Rle_lt_trans with ``r+b``. -Apply Rle_compatibility; Assumption. -Rewrite (Rplus_sym r); Apply Rlt_compatibility. -Apply Rlt_le_trans with r0. -Assert H6 := (H0 O (lt_O_Sn ?)). -Simpl in H6. -Elim H6; Intro. -Apply H7. -Elim H4; Assumption. -Assumption. -DiscrR. -Simpl in H; Apply H with r0 b. -Apply RList_P4 with r; Assumption. -Reflexivity. -Rewrite <- H2; Reflexivity. -Intros; Apply H3; Elim H4; Intros; Split; Try Assumption. -Apply Rle_lt_trans with r0; Try Assumption. -Rewrite <- H1. -Simpl; Apply (H0 O); Simpl; Apply lt_O_Sn. -Qed. - -Lemma StepFun_P36 : (a,b:R;f,g:(StepFun a b);l:Rlist) ``a<=b`` -> (is_subdivision f a b l) -> (is_subdivision g a b l) -> ((x:R)``a``(f x)<=(g x)``) -> ``(RiemannInt_SF f) <= (RiemannInt_SF g)``. -Intros; Unfold RiemannInt_SF; Case (total_order_Rle a b); Intro. -Replace (Int_SF (subdivision_val f) (subdivision f)) with (Int_SF (FF l f) l). -Replace (Int_SF (subdivision_val g) (subdivision g)) with (Int_SF (FF l g) l). -Unfold is_subdivision in X; Elim X; Clear X; Intros; Unfold adapted_couple in p; Decompose [and] p; Clear p; Assert H5 : (Rmin a b)==a; [Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption] | Assert H7 : (Rmax a b)==b; [Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption] | Rewrite H5 in H3; Rewrite H7 in H2; EApply StepFun_P35 with a b; Assumption]]. -Apply StepFun_P17 with (fe g) a b; [Apply StepFun_P21; Assumption | Apply StepFun_P1]. -Apply StepFun_P17 with (fe f) a b; [Apply StepFun_P21; Assumption | Apply StepFun_P1]. -Elim n; Assumption. -Qed. - -Lemma StepFun_P37 : (a,b:R;f,g:(StepFun a b)) ``a<=b`` -> ((x:R)``a``(f x)<=(g x)``) -> ``(RiemannInt_SF f) <= (RiemannInt_SF g)``. -Intros; EApply StepFun_P36; Try Assumption. -EApply StepFun_P25; Apply StepFun_P29. -EApply StepFun_P23; Apply StepFun_P29. -Qed. - -Lemma StepFun_P38 : (l:Rlist;a,b:R;f:R->R) (ordered_Rlist l) -> (pos_Rl l O)==a -> (pos_Rl l (pred (Rlength l)))==b -> (sigTT ? [g:(StepFun a b)](g b)==(f b)/\(i:nat)(lt i (pred (Rlength l)))->(constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i))) (f (pos_Rl l i)))). -Intros l a b f; Generalize a; Clear a; NewInduction l. -Intros a H H0 H1; Simpl in H0; Simpl in H1; Exists (mkStepFun (StepFun_P4 a b (f b))); Split. -Reflexivity. -Intros; Elim (lt_n_O ? H2). -Intros; NewDestruct l as [|r1 l]. -Simpl in H1; Simpl in H0; Exists (mkStepFun (StepFun_P4 a b (f b))); Split. -Reflexivity. -Intros i H2; Elim (lt_n_O ? H2). -Intros; Assert H2 : (ordered_Rlist (cons r1 l)). -Apply RList_P4 with r; Assumption. -Assert H3 : (pos_Rl (cons r1 l) O)==r1. -Reflexivity. -Assert H4 : (pos_Rl (cons r1 l) (pred (Rlength (cons r1 l))))==b. -Rewrite <- H1; Reflexivity. -Elim (IHl r1 H2 H3 H4); Intros g [H5 H6]. -Pose g' := [x:R]Cases (total_order_Rle r1 x) of - | (leftT _) => (g x) - | (rightT _) => (f a) end. -Assert H7 : ``r1<=b``. -Rewrite <- H4; Apply RList_P7; [Assumption | Left; Reflexivity]. -Assert H8 : (IsStepFun g' a b). -Unfold IsStepFun; Assert H8 := (pre g); Unfold IsStepFun in H8; Elim H8; Intros lg H9; Unfold is_subdivision in H9; Elim H9; Clear H9; Intros lg2 H9; Split with (cons a lg); Unfold is_subdivision; Split with (cons (f a) lg2); Unfold adapted_couple in H9; Decompose [and] H9; Clear H9; Unfold adapted_couple; Repeat Split. -Unfold ordered_Rlist; Intros; Simpl in H9; Induction i. -Simpl; Rewrite H12; Replace (Rmin r1 b) with r1. -Simpl in H0; Rewrite <- H0; Apply (H O); Simpl; Apply lt_O_Sn. -Unfold Rmin; Case (total_order_Rle r1 b); Intro; [Reflexivity | Elim n; Assumption]. -Apply (H10 i); Apply lt_S_n. -Replace (S (pred (Rlength lg))) with (Rlength lg). -Apply H9. -Apply S_pred with O; Apply neq_O_lt; Intro; Rewrite <- H14 in H9; Elim (lt_n_O ? H9). -Simpl; Assert H14 : ``a<=b``. -Rewrite <- H1; Simpl in H0; Rewrite <- H0; Apply RList_P7; [Assumption | Left; Reflexivity]. -Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Assert H14 : ``a<=b``. -Rewrite <- H1; Simpl in H0; Rewrite <- H0; Apply RList_P7; [Assumption | Left; Reflexivity]. -Replace (Rmax a b) with (Rmax r1 b). -Rewrite <- H11; Induction lg. -Simpl in H13; Discriminate. -Reflexivity. -Unfold Rmax; Case (total_order_Rle a b); Case (total_order_Rle r1 b); Intros; Reflexivity Orelse Elim n; Assumption. -Simpl; Rewrite H13; Reflexivity. -Intros; Simpl in H9; Induction i. -Unfold constant_D_eq open_interval; Simpl; Intros; Assert H16 : (Rmin r1 b)==r1. -Unfold Rmin; Case (total_order_Rle r1 b); Intro; [Reflexivity | Elim n; Assumption]. -Rewrite H16 in H12; Rewrite H12 in H14; Elim H14; Clear H14; Intros _ H14; Unfold g'; Case (total_order_Rle r1 x); Intro r3. -Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r3 H14)). -Reflexivity. -Change (constant_D_eq g' (open_interval (pos_Rl lg i) (pos_Rl lg (S i))) (pos_Rl lg2 i)); Clear Hreci; Assert H16 := (H15 i); Assert H17 : (lt i (pred (Rlength lg))). -Apply lt_S_n. -Replace (S (pred (Rlength lg))) with (Rlength lg). -Assumption. -Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H14 in H9; Elim (lt_n_O ? H9). -Assert H18 := (H16 H17); Unfold constant_D_eq open_interval in H18; Unfold constant_D_eq open_interval; Intros; Assert H19 := (H18 ? H14); Rewrite <- H19; Unfold g'; Case (total_order_Rle r1 x); Intro. -Reflexivity. -Elim n; Replace r1 with (Rmin r1 b). -Rewrite <- H12; Elim H14; Clear H14; Intros H14 _; Left; Apply Rle_lt_trans with (pos_Rl lg i); Try Assumption. -Apply RList_P5. -Assumption. -Elim (RList_P3 lg (pos_Rl lg i)); Intros; Apply H21; Exists i; Split. -Reflexivity. -Apply lt_trans with (pred (Rlength lg)); Try Assumption. -Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H22 in H17; Elim (lt_n_O ? H17). -Unfold Rmin; Case (total_order_Rle r1 b); Intro; [Reflexivity | Elim n0; Assumption]. -Exists (mkStepFun H8); Split. -Simpl; Unfold g'; Case (total_order_Rle r1 b); Intro. -Assumption. -Elim n; Assumption. -Intros; Simpl in H9; Induction i. -Unfold constant_D_eq co_interval; Simpl; Intros; Simpl in H0; Rewrite H0; Elim H10; Clear H10; Intros; Unfold g'; Case (total_order_Rle r1 x); Intro r3. -Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r3 H11)). -Reflexivity. -Clear Hreci; Change (constant_D_eq (mkStepFun H8) (co_interval (pos_Rl (cons r1 l) i) (pos_Rl (cons r1 l) (S i))) (f (pos_Rl (cons r1 l) i))); Assert H10 := (H6 i); Assert H11 : (lt i (pred (Rlength (cons r1 l)))). -Simpl; Apply lt_S_n; Assumption. -Assert H12 := (H10 H11); Unfold constant_D_eq co_interval in H12; Unfold constant_D_eq co_interval; Intros; Rewrite <- (H12 ? H13); Simpl; Unfold g'; Case (total_order_Rle r1 x); Intro. -Reflexivity. -Elim n; Elim H13; Clear H13; Intros; Apply Rle_trans with (pos_Rl (cons r1 l) i); Try Assumption; Change ``(pos_Rl (cons r1 l) O)<=(pos_Rl (cons r1 l) i)``; Elim (RList_P6 (cons r1 l)); Intros; Apply H15; [Assumption | Apply le_O_n | Simpl; Apply lt_trans with (Rlength l); [Apply lt_S_n; Assumption | Apply lt_n_Sn]]. -Qed. - -Lemma StepFun_P39 : (a,b:R;f:(StepFun a b)) (RiemannInt_SF f)==(Ropp (RiemannInt_SF (mkStepFun (StepFun_P6 (pre f))))). -Intros; Unfold RiemannInt_SF; Case (total_order_Rle a b); Case (total_order_Rle b a); Intros. -Assert H : (adapted_couple f a b (subdivision f) (subdivision_val f)); [Apply StepFun_P1 | Assert H0 : (adapted_couple (mkStepFun (StepFun_P6 (pre f))) b a (subdivision (mkStepFun (StepFun_P6 (pre f)))) (subdivision_val (mkStepFun (StepFun_P6 (pre f))))); [Apply StepFun_P1 | Assert H1 : a==b; [Apply Rle_antisym; Assumption | Rewrite (StepFun_P8 H H1); Assert H2 : b==a; [Symmetry; Apply H1 | Rewrite (StepFun_P8 H0 H2); Ring]]]]. -Rewrite Ropp_Ropp; EApply StepFun_P17; [Apply StepFun_P1 | Apply StepFun_P2; Pose H := (StepFun_P6 (pre f)); Unfold IsStepFun in H; Elim H; Intros; Unfold is_subdivision; Elim p; Intros; Apply p0]. -Apply eq_Ropp; EApply StepFun_P17; [Apply StepFun_P1 | Apply StepFun_P2; Pose H := (StepFun_P6 (pre f)); Unfold IsStepFun in H; Elim H; Intros; Unfold is_subdivision; Elim p; Intros; Apply p0]. -Assert H : ``aR;a,b,c:R;l1,l2,lf1,lf2:Rlist) ``a ``b (adapted_couple f a b l1 lf1) -> (adapted_couple f b c l2 lf2) -> (adapted_couple f a c (cons_Rlist l1 l2) (FF (cons_Rlist l1 l2) f)). -Intros f a b c l1 l2 lf1 lf2 H H0 H1 H2; Unfold adapted_couple in H1 H2; Unfold adapted_couple; Decompose [and] H1; Decompose [and] H2; Clear H1 H2; Repeat Split. -Apply RList_P25; Try Assumption. -Rewrite H10; Rewrite H4; Unfold Rmin Rmax; Case (total_order_Rle a b); Case (total_order_Rle b c); Intros; (Right; Reflexivity) Orelse (Elim n; Left; Assumption). -Rewrite RList_P22. -Rewrite H5; Unfold Rmin Rmax; Case (total_order_Rle a b); Case (total_order_Rle a c); Intros; [Reflexivity | Elim n; Apply Rle_trans with b; Left; Assumption | Elim n; Left; Assumption | Elim n0; Left; Assumption]. -Red; Intro; Rewrite H1 in H6; Discriminate. -Rewrite RList_P24. -Rewrite H9; Unfold Rmin Rmax; Case (total_order_Rle b c); Case (total_order_Rle a c); Intros; [Reflexivity | Elim n; Apply Rle_trans with b; Left; Assumption | Elim n; Left; Assumption | Elim n0; Left; Assumption]. -Red; Intro; Rewrite H1 in H11; Discriminate. -Apply StepFun_P20. -Rewrite RList_P23; Apply neq_O_lt; Red; Intro. -Assert H2 : (plus (Rlength l1) (Rlength l2))=O. -Symmetry; Apply H1. -Elim (plus_is_O ? ? H2); Intros; Rewrite H12 in H6; Discriminate. -Unfold constant_D_eq open_interval; Intros; Elim (le_or_lt (S (S i)) (Rlength l1)); Intro. -Assert H14 : (pos_Rl (cons_Rlist l1 l2) i) == (pos_Rl l1 i). -Apply RList_P26; Apply lt_S_n; Apply le_lt_n_Sm; Apply le_S_n; Apply le_trans with (Rlength l1); [Assumption | Apply le_n_Sn]. -Assert H15 : (pos_Rl (cons_Rlist l1 l2) (S i))==(pos_Rl l1 (S i)). -Apply RList_P26; Apply lt_S_n; Apply le_lt_n_Sm; Assumption. -Rewrite H14 in H2; Rewrite H15 in H2; Assert H16 : (le (2) (Rlength l1)). -Apply le_trans with (S (S i)); [Repeat Apply le_n_S; Apply le_O_n | Assumption]. -Elim (RList_P20 ? H16); Intros r1 [r2 [r3 H17]]; Rewrite H17; Change (f x)==(pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i); Rewrite RList_P12. -Induction i. -Simpl; Assert H18 := (H8 O); Unfold constant_D_eq open_interval in H18; Assert H19 : (lt O (pred (Rlength l1))). -Rewrite H17; Simpl; Apply lt_O_Sn. -Assert H20 := (H18 H19); Repeat Rewrite H20. -Reflexivity. -Assert H21 : ``r1<=r2``. -Rewrite H17 in H3; Apply (H3 O). -Simpl; Apply lt_O_Sn. -Elim H21; Intro. -Split. -Rewrite H17; Simpl; Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Assumption | DiscrR]]. -Rewrite H17; Simpl; Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite (Rplus_sym r1); Rewrite double; Apply Rlt_compatibility; Assumption | DiscrR]]. -Elim H2; Intros; Rewrite H17 in H23; Rewrite H17 in H24; Simpl in H24; Simpl in H23; Rewrite H22 in H23; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H23 H24)). -Assumption. -Clear Hreci; Rewrite RList_P13. -Rewrite H17 in H14; Rewrite H17 in H15; Change (pos_Rl (cons_Rlist (cons r2 r3) l2) i)== (pos_Rl (cons r1 (cons r2 r3)) (S i)) in H14; Rewrite H14; Change (pos_Rl (cons_Rlist (cons r2 r3) l2) (S i))==(pos_Rl (cons r1 (cons r2 r3)) (S (S i))) in H15; Rewrite H15; Assert H18 := (H8 (S i)); Unfold constant_D_eq open_interval in H18; Assert H19 : (lt (S i) (pred (Rlength l1))). -Apply lt_pred; Apply lt_S_n; Apply le_lt_n_Sm; Assumption. -Assert H20 := (H18 H19); Repeat Rewrite H20. -Reflexivity. -Rewrite <- H17; Assert H21 : ``(pos_Rl l1 (S i))<=(pos_Rl l1 (S (S i)))``. -Apply (H3 (S i)); Apply lt_pred; Apply lt_S_n; Apply le_lt_n_Sm; Assumption. -Elim H21; Intro. -Split. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Assumption | DiscrR]]. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite (Rplus_sym (pos_Rl l1 (S i))); Rewrite double; Apply Rlt_compatibility; Assumption | DiscrR]]. -Elim H2; Intros; Rewrite H22 in H23; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H23 H24)). -Assumption. -Simpl; Rewrite H17 in H1; Simpl in H1; Apply lt_S_n; Assumption. -Rewrite RList_P14; Rewrite H17 in H1; Simpl in H1; Apply H1. -Inversion H12. -Assert H16 : (pos_Rl (cons_Rlist l1 l2) (S i))==b. -Rewrite RList_P29. -Rewrite H15; Rewrite <- minus_n_n; Rewrite H10; Unfold Rmin; Case (total_order_Rle b c); Intro; [Reflexivity | Elim n; Left; Assumption]. -Rewrite H15; Apply le_n. -Induction l1. -Simpl in H15; Discriminate. -Clear Hrecl1; Simpl in H1; Simpl; Apply lt_n_S; Assumption. -Assert H17 : (pos_Rl (cons_Rlist l1 l2) i)==b. -Rewrite RList_P26. -Replace i with (pred (Rlength l1)); [Rewrite H4; Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Left; Assumption] | Rewrite H15; Reflexivity]. -Rewrite H15; Apply lt_n_Sn. -Rewrite H16 in H2; Rewrite H17 in H2; Elim H2; Intros; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H14 H18)). -Assert H16 : (pos_Rl (cons_Rlist l1 l2) i) == (pos_Rl l2 (minus i (Rlength l1))). -Apply RList_P29. -Apply le_S_n; Assumption. -Apply lt_le_trans with (pred (Rlength (cons_Rlist l1 l2))); [Assumption | Apply le_pred_n]. -Assert H17 : (pos_Rl (cons_Rlist l1 l2) (S i))==(pos_Rl l2 (S (minus i (Rlength l1)))). -Replace (S (minus i (Rlength l1))) with (minus (S i) (Rlength l1)). -Apply RList_P29. -Apply le_S_n; Apply le_trans with (S i); [Assumption | Apply le_n_Sn]. -Induction l1. -Simpl in H6; Discriminate. -Clear Hrecl1; Simpl in H1; Simpl; Apply lt_n_S; Assumption. -Symmetry; Apply minus_Sn_m; Apply le_S_n; Assumption. -Assert H18 : (le (2) (Rlength l1)). -Clear f c l2 lf2 H0 H3 H8 H7 H10 H9 H11 H13 i H1 x H2 H12 m H14 H15 H16 H17; Induction l1. -Discriminate. -Clear Hrecl1; Induction l1. -Simpl in H5; Simpl in H4; Assert H0 : ``(Rmin a b)<(Rmax a b)``. -Unfold Rmin Rmax; Case (total_order_Rle a b); Intro; [Assumption | Elim n; Left; Assumption]. -Rewrite <- H5 in H0; Rewrite <- H4 in H0; Elim (Rlt_antirefl ? H0). -Clear Hrecl1; Simpl; Repeat Apply le_n_S; Apply le_O_n. -Elim (RList_P20 ? H18); Intros r1 [r2 [r3 H19]]; Rewrite H19; Change (f x)==(pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i); Rewrite RList_P12. -Induction i. -Assert H20 := (le_S_n ? ? H15); Assert H21 := (le_trans ? ? ? H18 H20); Elim (le_Sn_O ? H21). -Clear Hreci; Rewrite RList_P13. -Rewrite H19 in H16; Rewrite H19 in H17; Change (pos_Rl (cons_Rlist (cons r2 r3) l2) i)== (pos_Rl l2 (minus (S i) (Rlength (cons r1 (cons r2 r3))))) in H16; Rewrite H16; Change (pos_Rl (cons_Rlist (cons r2 r3) l2) (S i))== (pos_Rl l2 (S (minus (S i) (Rlength (cons r1 (cons r2 r3)))))) in H17; Rewrite H17; Assert H20 := (H13 (minus (S i) (Rlength l1))); Unfold constant_D_eq open_interval in H20; Assert H21 : (lt (minus (S i) (Rlength l1)) (pred (Rlength l2))). -Apply lt_pred; Rewrite minus_Sn_m. -Apply simpl_lt_plus_l with (Rlength l1); Rewrite <- le_plus_minus. -Rewrite H19 in H1; Simpl in H1; Rewrite H19; Simpl; Rewrite RList_P23 in H1; Apply lt_n_S; Assumption. -Apply le_trans with (S i); [Apply le_S_n; Assumption | Apply le_n_Sn]. -Apply le_S_n; Assumption. -Assert H22 := (H20 H21); Repeat Rewrite H22. -Reflexivity. -Rewrite <- H19; Assert H23 : ``(pos_Rl l2 (minus (S i) (Rlength l1)))<=(pos_Rl l2 (S (minus (S i) (Rlength l1))))``. -Apply H7; Apply lt_pred. -Rewrite minus_Sn_m. -Apply simpl_lt_plus_l with (Rlength l1); Rewrite <- le_plus_minus. -Rewrite H19 in H1; Simpl in H1; Rewrite H19; Simpl; Rewrite RList_P23 in H1; Apply lt_n_S; Assumption. -Apply le_trans with (S i); [Apply le_S_n; Assumption | Apply le_n_Sn]. -Apply le_S_n; Assumption. -Elim H23; Intro. -Split. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Assumption | DiscrR]]. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite (Rplus_sym (pos_Rl l2 (minus (S i) (Rlength l1)))); Rewrite double; Apply Rlt_compatibility; Assumption | DiscrR]]. -Rewrite <- H19 in H16; Rewrite <- H19 in H17; Elim H2; Intros; Rewrite H19 in H25; Rewrite H19 in H26; Simpl in H25; Simpl in H16; Rewrite H16 in H25; Simpl in H26; Simpl in H17; Rewrite H17 in H26; Simpl in H24; Rewrite H24 in H25; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H25 H26)). -Assert H23 : (pos_Rl (cons_Rlist l1 l2) (S i))==(pos_Rl l2 (minus (S i) (Rlength l1))). -Rewrite H19; Simpl; Simpl in H16; Apply H16. -Assert H24 : (pos_Rl (cons_Rlist l1 l2) (S (S i)))==(pos_Rl l2 (S (minus (S i) (Rlength l1)))). -Rewrite H19; Simpl; Simpl in H17; Apply H17. -Rewrite <- H23; Rewrite <- H24; Assumption. -Simpl; Rewrite H19 in H1; Simpl in H1; Apply lt_S_n; Assumption. -Rewrite RList_P14; Rewrite H19 in H1; Simpl in H1; Simpl; Apply H1. -Qed. - -Lemma StepFun_P41 : (f:R->R;a,b,c:R) ``a<=b``->``b<=c``->(IsStepFun f a b) -> (IsStepFun f b c) -> (IsStepFun f a c). -Unfold IsStepFun; Unfold is_subdivision; Intros; Elim X; Clear X; Intros l1 [lf1 H1]; Elim X0; Clear X0; Intros l2 [lf2 H2]; Case (total_order_T a b); Intro. -Elim s; Intro. -Case (total_order_T b c); Intro. -Elim s0; Intro. -Split with (cons_Rlist l1 l2); Split with (FF (cons_Rlist l1 l2) f); Apply StepFun_P40 with b lf1 lf2; Assumption. -Split with l1; Split with lf1; Rewrite b0 in H1; Assumption. -Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H0 r)). -Split with l2; Split with lf2; Rewrite <- b0 in H2; Assumption. -Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H r)). -Qed. - -Lemma StepFun_P42 : (l1,l2:Rlist;f:R->R) (pos_Rl l1 (pred (Rlength l1)))==(pos_Rl l2 O) -> ``(Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)) == (Int_SF (FF l1 f) l1) + (Int_SF (FF l2 f) l2)``. -Intros l1 l2 f; NewInduction l1 as [|r l1 IHl1]; Intros H; [ Simpl; Ring | NewDestruct l1; [Simpl in H; Simpl; NewDestruct l2; [Simpl; Ring | Simpl; Simpl in H; Rewrite H; Ring] | Simpl; Rewrite Rplus_assoc; Apply Rplus_plus_r; Apply IHl1; Rewrite <- H; Reflexivity]]. -Qed. - -Lemma StepFun_P43 : (f:R->R;a,b,c:R;pr1:(IsStepFun f a b);pr2:(IsStepFun f b c);pr3:(IsStepFun f a c)) ``(RiemannInt_SF (mkStepFun pr1))+(RiemannInt_SF (mkStepFun pr2))==(RiemannInt_SF (mkStepFun pr3))``. -Intros f; Intros; Assert H1 : (SigT ? [l:Rlist](sigTT ? [l0:Rlist](adapted_couple f a b l l0))). -Apply pr1. -Assert H2 : (SigT ? [l:Rlist](sigTT ? [l0:Rlist](adapted_couple f b c l l0))). -Apply pr2. -Assert H3 : (SigT ? [l:Rlist](sigTT ? [l0:Rlist](adapted_couple f a c l l0))). -Apply pr3. -Elim H1; Clear H1; Intros l1 [lf1 H1]; Elim H2; Clear H2; Intros l2 [lf2 H2]; Elim H3; Clear H3; Intros l3 [lf3 H3]. -Replace (RiemannInt_SF (mkStepFun pr1)) with (Cases (total_order_Rle a b) of (leftT _) => (Int_SF lf1 l1) | (rightT _) => ``-(Int_SF lf1 l1)`` end). -Replace (RiemannInt_SF (mkStepFun pr2)) with (Cases (total_order_Rle b c) of (leftT _) => (Int_SF lf2 l2) | (rightT _) => ``-(Int_SF lf2 l2)`` end). -Replace (RiemannInt_SF (mkStepFun pr3)) with (Cases (total_order_Rle a c) of (leftT _) => (Int_SF lf3 l3) | (rightT _) => ``-(Int_SF lf3 l3)`` end). -Case (total_order_Rle a b); Case (total_order_Rle b c); Case (total_order_Rle a c); Intros. -Elim r1; Intro. -Elim r0; Intro. -Replace (Int_SF lf3 l3) with (Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)). -Replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). -Replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). -Symmetry; Apply StepFun_P42. -Unfold adapted_couple in H1 H2; Decompose [and] H1; Decompose [and] H2; Clear H1 H2; Rewrite H11; Rewrite H5; Unfold Rmax Rmin; Case (total_order_Rle a b); Case (total_order_Rle b c); Intros; Reflexivity Orelse Elim n; Assumption. -EApply StepFun_P17; [Apply StepFun_P21; Unfold is_subdivision; Split with lf2; Apply H2; Assumption | Assumption]. -EApply StepFun_P17; [Apply StepFun_P21; Unfold is_subdivision; Split with lf1; Apply H1 | Assumption]. -EApply StepFun_P17; [Apply (StepFun_P40 H H0 H1 H2) | Apply H3]. -Replace (Int_SF lf2 l2) with R0. -Rewrite Rplus_Or; EApply StepFun_P17; [Apply H1 | Rewrite <- H0 in H3; Apply H3]. -Symmetry; EApply StepFun_P8; [Apply H2 | Assumption]. -Replace (Int_SF lf1 l1) with R0. -Rewrite Rplus_Ol; EApply StepFun_P17; [Apply H2 | Rewrite H in H3; Apply H3]. -Symmetry; EApply StepFun_P8; [Apply H1 | Assumption]. -Elim n; Apply Rle_trans with b; Assumption. -Apply r_Rplus_plus with (Int_SF lf2 l2); Replace ``(Int_SF lf2 l2)+((Int_SF lf1 l1)+ -(Int_SF lf2 l2))`` with (Int_SF lf1 l1); [Idtac | Ring]. -Assert H : ``cR;a,b,c:R) (IsStepFun f a b) -> ``a<=c<=b`` -> (IsStepFun f a c). -Intros f; Intros; Assert H0 : ``a<=b``. -Elim H; Intros; Apply Rle_trans with c; Assumption. -Elim H; Clear H; Intros; Unfold IsStepFun in X; Unfold is_subdivision in X; Elim X; Clear X; Intros l1 [lf1 H2]; Cut (l1,lf1:Rlist;a,b,c:R;f:R->R) (adapted_couple f a b l1 lf1) -> ``a<=c<=b`` -> (SigT ? [l:Rlist](sigTT ? [l0:Rlist](adapted_couple f a c l l0))). -Intros; Unfold IsStepFun; Unfold is_subdivision; EApply X. -Apply H2. -Split; Assumption. -Clear f a b c H0 H H1 H2 l1 lf1; Induction l1. -Intros; Unfold adapted_couple in H; Decompose [and] H; Clear H; Simpl in H4; Discriminate. -Induction r0. -Intros; Assert H1 : ``a==b``. -Unfold adapted_couple in H; Decompose [and] H; Clear H; Simpl in H3; Simpl in H2; Assert H7 : ``a<=b``. -Elim H0; Intros; Apply Rle_trans with c; Assumption. -Replace a with (Rmin a b). -Pattern 2 b; Replace b with (Rmax a b). -Rewrite <- H2; Rewrite H3; Reflexivity. -Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Split with (cons r nil); Split with lf1; Assert H2 : ``c==b``. -Rewrite H1 in H0; Elim H0; Intros; Apply Rle_antisym; Assumption. -Rewrite H2; Assumption. -Intros; Clear X; Induction lf1. -Unfold adapted_couple in H; Decompose [and] H; Clear H; Simpl in H4; Discriminate. -Clear Hreclf1; Assert H1 : (sumboolT ``c<=r1`` ``r1R;a,b,c:R) (IsStepFun f a b) -> ``a<=c<=b`` -> (IsStepFun f c b). -Intros f; Intros; Assert H0 : ``a<=b``. -Elim H; Intros; Apply Rle_trans with c; Assumption. -Elim H; Clear H; Intros; Unfold IsStepFun in X; Unfold is_subdivision in X; Elim X; Clear X; Intros l1 [lf1 H2]; Cut (l1,lf1:Rlist;a,b,c:R;f:R->R) (adapted_couple f a b l1 lf1) -> ``a<=c<=b`` -> (SigT ? [l:Rlist](sigTT ? [l0:Rlist](adapted_couple f c b l l0))). -Intros; Unfold IsStepFun; Unfold is_subdivision; EApply X; [Apply H2 | Split; Assumption]. -Clear f a b c H0 H H1 H2 l1 lf1; Induction l1. -Intros; Unfold adapted_couple in H; Decompose [and] H; Clear H; Simpl in H4; Discriminate. -Induction r0. -Intros; Assert H1 : ``a==b``. -Unfold adapted_couple in H; Decompose [and] H; Clear H; Simpl in H3; Simpl in H2; Assert H7 : ``a<=b``. -Elim H0; Intros; Apply Rle_trans with c; Assumption. -Replace a with (Rmin a b). -Pattern 2 b; Replace b with (Rmax a b). -Rewrite <- H2; Rewrite H3; Reflexivity. -Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. -Split with (cons r nil); Split with lf1; Assert H2 : ``c==b``. -Rewrite H1 in H0; Elim H0; Intros; Apply Rle_antisym; Assumption. -Rewrite <- H2 in H1; Rewrite <- H1; Assumption. -Intros; Clear X; Induction lf1. -Unfold adapted_couple in H; Decompose [and] H; Clear H; Simpl in H4; Discriminate. -Clear Hreclf1; Assert H1 : (sumboolT ``c<=r1`` ``r1R;a,b,c:R) (IsStepFun f a b) -> (IsStepFun f b c) -> (IsStepFun f a c). -Intros f; Intros; Case (total_order_Rle a b); Case (total_order_Rle b c); Intros. -Apply StepFun_P41 with b; Assumption. -Case (total_order_Rle a c); Intro. -Apply StepFun_P44 with b; Try Assumption. -Split; [Assumption | Auto with real]. -Apply StepFun_P6; Apply StepFun_P44 with b. -Apply StepFun_P6; Assumption. -Split; Auto with real. -Case (total_order_Rle a c); Intro. -Apply StepFun_P45 with b; Try Assumption. -Split; Auto with real. -Apply StepFun_P6; Apply StepFun_P45 with b. -Apply StepFun_P6; Assumption. -Split; [Assumption | Auto with real]. -Apply StepFun_P6; Apply StepFun_P41 with b; Auto with real Orelse Apply StepFun_P6; Assumption. -Qed. -- cgit v1.2.3