diff options
Diffstat (limited to 'theories/Reals/RiemannInt_SF.v')
| -rw-r--r-- | theories/Reals/RiemannInt_SF.v | 350 |
1 files changed, 146 insertions, 204 deletions
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 8eb49bf3..1484ab2a 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -40,26 +40,25 @@ Proof. assert (H2 : exists x : R, E x). elim H; intros; exists (INR x); unfold E; exists x; split; [ assumption | reflexivity ]. - assert (H3 := completeness E H1 H2); elim H3; intros; unfold is_lub in p; - elim p; clear p; intros; unfold is_upper_bound in H4, H5; + destruct (completeness E H1 H2) as (x,(H4,H5)); unfold is_upper_bound in H4, H5; assert (H6 : 0 <= x). - elim H2; intros; unfold E in H6; elim H6; intros; elim H7; intros; + destruct H2 as (x0,H6). remember H6 as H7. destruct H7 as (x1,(H8,H9)). apply Rle_trans with x0; [ rewrite <- H9; change (INR 0 <= 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 Rplus_le_reg_l with 1; + apply H5; intros x0 H9. assert (H10 := H4 _ H9); unfold E in H9; elim H9; intros x1 (H12,<-). + apply Rplus_le_reg_l with 1; 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)%Z). 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; + destruct (IZN _ H14) as (x2,H15). + rewrite H15, <- INR_IZR_INZ; apply le_INR; apply lt_le_S. + apply INR_lt; apply Rle_lt_trans with x; [ assumption | rewrite INR_IZR_INZ; rewrite <- H15; assumption ]. assert (H10 : x = IZR (up x) - 1). apply Rle_antisym; @@ -70,32 +69,32 @@ Proof. [ assumption | ring ] ]. assert (H11 : (0 <= up x)%Z). 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). + assert (H12 := IZN_var H11); elim H12; clear H12; intros x0 H8; assert (H13 : E x). elim (classic (E x)); intro; try assumption. cut (forall y:R, E y -> y <= x - 1). - intro; assert (H14 := H5 _ H13); cut (x - 1 < x). - intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H15)). + intro H13; assert (H14 := H5 _ H13); cut (x - 1 < x). + intro H15; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H15)). apply Rminus_lt; replace (x - 1 - x) with (-1); [ idtac | ring ]; rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; apply Rlt_0_1. - intros; assert (H14 := H4 _ H13); elim H14; intro; unfold E in H13; elim H13; - intros; elim H16; intros; apply Rplus_le_reg_l with 1. + intros y H13; assert (H14 := H4 _ H13); elim H14; intro H15; unfold E in H13; elim H13; + intros x1 H16; elim H16; intros H17 H18; apply Rplus_le_reg_l with 1. replace (1 + (x - 1)) with x; [ idtac | ring ]; rewrite <- H18; replace (1 + INR x1) with (INR (S x1)); [ idtac | rewrite S_INR; ring ]. cut (x = INR (pred x0)). - intro; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18; + intro H19; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18; rewrite <- H19; assumption. - rewrite H10; rewrite p; rewrite <- INR_IZR_INZ; replace 1 with (INR 1); + rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; replace 1 with (INR 1); [ idtac | reflexivity ]; rewrite <- minus_INR. replace (x0 - 1)%nat with (pred x0); [ reflexivity | case x0; [ reflexivity | intro; simpl; apply minus_n_O ] ]. - induction x0 as [| x0 Hrecx0]; - [ rewrite p in H7; rewrite <- INR_IZR_INZ in H7; simpl in H7; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H7)) - | apply le_n_S; apply le_O_n ]. - rewrite H15 in H13; elim H12; assumption. + induction x0 as [|x0 Hrecx0]. + rewrite H8 in H3. rewrite <- INR_IZR_INZ in H3; simpl in H3. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H3)). + apply le_n_S; apply le_O_n. + rewrite H15 in H13; elim H12; assumption. split with (pred x0); unfold E in H13; elim H13; intros; elim H12; intros; - rewrite H10 in H15; rewrite p in H15; rewrite <- INR_IZR_INZ in H15; + rewrite H10 in H15; rewrite H8 in H15; rewrite <- INR_IZR_INZ in H15; assert (H16 : INR x0 = INR x1 + 1). rewrite H15; ring. rewrite <- S_INR in H16; assert (H17 := INR_eq _ _ H16); rewrite H17; @@ -144,7 +143,7 @@ Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f). Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := match projT2 (pre f) with - | existT a b => a + | existT _ a b => a end. Fixpoint Int_SF (l k:Rlist) : R := @@ -173,8 +172,8 @@ Lemma StepFun_P1 : forall (a b:R) (f:StepFun a b), adapted_couple f a b (subdivision f) (subdivision_val f). Proof. - intros a b f; unfold subdivision_val; case (projT2 (pre f)); intros; - apply a0. + intros a b f; unfold subdivision_val; case (projT2 (pre f)) as (x,H); + apply H. Qed. Lemma StepFun_P2 : @@ -201,19 +200,17 @@ Proof. 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 (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - simpl; unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + simpl; unfold Rmin; decide (Rle_dec a b) with H; reflexivity. + simpl; unfold Rmax; decide (Rle_dec a b) with H; reflexivity. unfold constant_D_eq, open_interval; intros; simpl in H0; inversion H0; [ reflexivity | elim (le_Sn_O _ H3) ]. Qed. Lemma StepFun_P4 : forall a b c:R, IsStepFun (fct_cte c) a b. Proof. - intros; unfold IsStepFun; case (Rle_dec a b); intro. + intros; unfold IsStepFun; destruct (Rle_dec a b) as [Hle|Hnle]. apply existT with (cons a (cons b nil)); unfold is_subdivision; - apply existT with (cons c nil); apply (StepFun_P3 c r). + apply existT with (cons c nil); apply (StepFun_P3 c Hle). apply existT with (cons b (cons a nil)); unfold is_subdivision; apply existT with (cons c nil); apply StepFun_P2; apply StepFun_P3; auto with real. @@ -244,17 +241,15 @@ Lemma StepFun_P7 : Proof. unfold adapted_couple; intros; decompose [and] H0; clear H0; assert (H5 : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with H; reflexivity. 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 (Rle_dec r2 b); intro; - [ reflexivity | elim n; assumption ]. - unfold Rmax; case (Rle_dec r2 b); intro; - [ rewrite H5 in H2; rewrite <- H2; reflexivity | elim n; assumption ]. + rewrite H5 in H2; unfold Rmin; decide (Rle_dec r2 b) with H7; reflexivity. + unfold Rmax; decide (Rle_dec r2 b) with H7. + rewrite H5 in H2; rewrite <- H2; reflexivity. simpl in H4; simpl; apply INR_eq; apply Rplus_eq_reg_l with 1; do 2 rewrite (Rplus_comm 1); do 2 rewrite <- S_INR; rewrite H4; reflexivity. @@ -340,33 +335,28 @@ Proof. 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 (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with H0; reflexivity. elim H6; clear H6; intros l' [lf' H6]; case (Req_dec 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 (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - simpl; unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + simpl; unfold Rmin; decide (Rle_dec a b) with H0; reflexivity. + simpl; unfold Rmax; decide (Rle_dec a b) with H0; reflexivity. 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 0%nat). simpl; apply lt_O_Sn. unfold open_interval; simpl; rewrite H7; simpl in H13; - rewrite H13; unfold Rmin; case (Rle_dec a b); - intro; [ assumption | elim n; assumption ]. + rewrite H13; unfold Rmin; decide (Rle_dec a b) with H0; 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 (Rle_dec t2 b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec t2 b) with H5; reflexivity. unfold adapted_couple in H6; elim H6; clear H6; intros; elim (RList_P20 _ (StepFun_P9 H6 H7)); intros s1 [s2 [s3 H9]]; induction lf' as [| r2 lf' Hreclf']. @@ -391,18 +381,16 @@ Proof. apply (H16 (S i)); simpl; assumption. simpl; simpl in H14; rewrite H14; reflexivity. simpl; simpl in H18; rewrite H18; unfold Rmax; - case (Rle_dec a b); case (Rle_dec t2 b); intros; reflexivity || elim n; - assumption. + decide (Rle_dec a b) with H0; decide (Rle_dec t2 b) with H5; reflexivity. simpl; simpl in H20; apply H20. intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. - simpl; simpl in H6; case (total_order_T x t2); intro. - elim s; intro. + simpl; simpl in H6; destruct (total_order_T x t2) as [[Hlt|Heq]|Hgt]. apply (H17 0%nat); [ simpl; apply lt_O_Sn | unfold open_interval; simpl; elim H6; intros; split; assumption ]. - rewrite b0; assumption. + rewrite Heq; assumption. rewrite H10; apply (H22 0%nat); [ simpl; apply lt_O_Sn | unfold open_interval; simpl; replace s1 with t2; @@ -440,8 +428,7 @@ Proof. assumption. simpl; simpl in H19; apply H19. rewrite H9; simpl; simpl in H13; rewrite H13; unfold Rmax; - case (Rle_dec t2 b); case (Rle_dec a b); intros; reflexivity || elim n; - assumption. + decide (Rle_dec t2 b) with H5; decide (Rle_dec a b) with H0; reflexivity. rewrite H9; simpl; simpl in H15; rewrite H15; reflexivity. intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. @@ -483,8 +470,7 @@ Proof. assumption. simpl; simpl in H18; apply H18. rewrite H9; simpl; simpl in H12; rewrite H12; unfold Rmax; - case (Rle_dec t2 b); case (Rle_dec a b); intros; reflexivity || elim n; - assumption. + decide (Rle_dec t2 b) with H5; decide (Rle_dec a b) with H0; reflexivity. rewrite H9; simpl; simpl in H14; rewrite H14; reflexivity. intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. @@ -511,8 +497,7 @@ Proof. 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 (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ] ]. + | unfold Rmax; decide (Rle_dec a b) with H0; reflexivity ]. Qed. Lemma StepFun_P11 : @@ -528,7 +513,7 @@ Proof. simpl in H10; simpl in H5; rewrite H10; rewrite H5; reflexivity. assert (H14 := H3 0%nat (lt_O_Sn _)); simpl in H14; elim H14; intro. assert (H15 := H7 0%nat (lt_O_Sn _)); simpl in H15; elim H15; intro. - rewrite <- H12 in H1; case (Rle_dec r1 s2); intro; try assumption. + rewrite <- H12 in H1; destruct (Rle_dec r1 s2) as [Hle|Hnle]; try assumption. assert (H16 : s2 < r1); auto with real. induction s3 as [| r0 s3 Hrecs3]. simpl in H9; rewrite H9 in H16; cut (r1 <= Rmax a b). @@ -662,12 +647,11 @@ Lemma StepFun_P13 : 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. Proof. - intros; case (total_order_T a b); intro. - elim s; intro. - eapply StepFun_P11; [ apply a0 | apply H0 | apply H1 ]. + intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. + eapply StepFun_P11; [ apply Hlt | apply H0 | apply H1 ]. elim H; assumption. eapply StepFun_P11; - [ apply r0 | apply StepFun_P2; apply H0 | apply StepFun_P12; apply H1 ]. + [ apply Hgt | apply StepFun_P2; apply H0 | apply StepFun_P12; apply H1 ]. Qed. Lemma StepFun_P14 : @@ -689,11 +673,9 @@ Proof. case (Req_dec a b); intro. rewrite (StepFun_P8 H2 H4); rewrite (StepFun_P8 H H4); reflexivity. assert (Hyp_min : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with H1; reflexivity. assert (Hyp_max : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with H1; reflexivity. elim (RList_P20 _ (StepFun_P9 H H4)); intros s1 [s2 [s3 H5]]; rewrite H5 in H; rewrite H5; induction lf1 as [| r3 lf1 Hreclf1]. unfold adapted_couple in H2; decompose [and] H2; @@ -883,8 +865,8 @@ Lemma StepFun_P15 : adapted_couple f a b l1 lf1 -> adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2. Proof. - intros; case (Rle_dec a b); intro; - [ apply (StepFun_P14 r H H0) + intros; destruct (Rle_dec a b) as [Hle|Hnle]; + [ apply (StepFun_P14 Hle H H0) | assert (H1 : b <= a); [ auto with real | eapply StepFun_P14; @@ -897,8 +879,8 @@ Lemma StepFun_P16 : exists l' : Rlist, (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). Proof. - intros; case (Rle_dec a b); intro; - [ apply (StepFun_P10 r H) + intros; destruct (Rle_dec a b) as [Hle|Hnle]; + [ apply (StepFun_P10 Hle H) | assert (H1 : b <= a); [ auto with real | assert (H2 := StepFun_P10 H1 (StepFun_P2 H)); elim H2; @@ -961,9 +943,8 @@ Lemma StepFun_P21 : forall (a b:R) (f:R -> R) (l:Rlist), is_subdivision f a b l -> adapted_couple f a b l (FF l f). Proof. - 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. + intros * (x & H & H1 & H0 & H2 & H4). + 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; @@ -1003,11 +984,9 @@ Lemma StepFun_P22 : Proof. 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 (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity. assert (Hyp_max : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity. apply existT 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; @@ -1221,13 +1200,13 @@ Proof. [ apply lt_n_S; assumption | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21) ]. - elim (Rle_dec (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro. + elim (Rle_dec (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro a0. assert (H23 : (S x0 <= x0)%nat). apply H20; unfold I; split; assumption. elim (le_Sn_n _ H23). assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lf (S x0)). auto with real. - clear b0; apply RList_P17; try assumption. + clear a0; apply RList_P17; try assumption. apply RList_P2; assumption. elim (RList_P9 lf lg (pos_Rl lf (S x0))); intros; apply H25; left; elim (RList_P3 lf (pos_Rl lf (S x0))); intros; apply H27; @@ -1255,11 +1234,9 @@ Lemma StepFun_P24 : Proof. 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 (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity. assert (Hyp_max : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity. apply existT 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; @@ -1471,12 +1448,12 @@ Proof. apply lt_n_S; assumption. symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21). - elim (Rle_dec (pos_Rl lg (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro. + elim (Rle_dec (pos_Rl lg (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro a0. assert (H23 : (S x0 <= x0)%nat); [ apply H20; unfold I; split; assumption | elim (le_Sn_n _ H23) ]. assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lg (S x0)). auto with real. - clear b0; apply RList_P17; try assumption; + clear a0; apply RList_P17; try assumption; [ apply RList_P2; assumption | elim (RList_P9 lf lg (pos_Rl lg (S x0))); intros; apply H25; right; elim (RList_P3 lg (pos_Rl lg (S x0))); intros; @@ -1652,7 +1629,7 @@ Lemma StepFun_P34 : a <= b -> Rabs (RiemannInt_SF f) <= RiemannInt_SF (mkStepFun (StepFun_P32 f)). Proof. - intros; unfold RiemannInt_SF; case (Rle_dec a b); intro. + intros; unfold RiemannInt_SF; decide (Rle_dec a b) with H. replace (Int_SF (subdivision_val (mkStepFun (StepFun_P32 f))) (subdivision (mkStepFun (StepFun_P32 f)))) with @@ -1663,7 +1640,6 @@ Proof. apply StepFun_P17 with (fun x:R => Rabs (f x)) a b; [ apply StepFun_P31; apply StepFun_P1 | apply (StepFun_P1 (mkStepFun (StepFun_P32 f))) ]. - elim n; assumption. Qed. Lemma StepFun_P35 : @@ -1741,24 +1717,21 @@ Lemma StepFun_P36 : (forall x:R, a < x < b -> f x <= g x) -> RiemannInt_SF f <= RiemannInt_SF g. Proof. - intros; unfold RiemannInt_SF; case (Rle_dec a b); intro. + intros; unfold RiemannInt_SF; decide (Rle_dec a b) with H. 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 (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ] + [ unfold Rmin; decide (Rle_dec a b) with H; reflexivity | assert (H7 : Rmax a b = b); - [ unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ] + [ unfold Rmax; decide (Rle_dec a b) with H; reflexivity | 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 : @@ -1819,8 +1792,7 @@ Proof. induction i as [| i Hreci]. simpl; rewrite H12; replace (Rmin r1 b) with r1. simpl in H0; rewrite <- H0; apply (H 0%nat); simpl; apply lt_O_Sn. - unfold Rmin; case (Rle_dec r1 b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. apply (H10 i); apply lt_S_n. replace (S (pred (Rlength lg))) with (Rlength lg). apply H9. @@ -1829,8 +1801,7 @@ Proof. simpl; assert (H14 : a <= b). rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7; [ assumption | left; reflexivity ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with H14; reflexivity. assert (H14 : a <= b). rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7; [ assumption | left; reflexivity ]. @@ -1838,14 +1809,13 @@ Proof. rewrite <- H11; induction lg as [| r0 lg Hreclg]. simpl in H13; discriminate. reflexivity. - unfold Rmax; case (Rle_dec a b); case (Rle_dec r1 b); intros; - reflexivity || elim n; assumption. + unfold Rmax; decide (Rle_dec a b) with H14; decide (Rle_dec r1 b) with H7; + reflexivity. simpl; rewrite H13; reflexivity. intros; simpl in H9; induction i as [| i Hreci]. unfold constant_D_eq, open_interval; simpl; intros; assert (H16 : Rmin r1 b = r1). - unfold Rmin; case (Rle_dec r1 b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. rewrite H16 in H12; rewrite H12 in H14; elim H14; clear H14; intros _ H14; unfold g'; case (Rle_dec r1 x); intro r3. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H14)). @@ -1862,9 +1832,9 @@ Proof. 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 (Rle_dec r1 x); intro. + case (Rle_dec r1 x) as [|[]]. reflexivity. - elim n; replace r1 with (Rmin r1 b). + 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. @@ -1874,12 +1844,9 @@ Proof. 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 (Rle_dec r1 b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. exists (mkStepFun H8); split. - simpl; unfold g'; case (Rle_dec r1 b); intro. - assumption. - elim n; assumption. + simpl; unfold g'; decide (Rle_dec r1 b) with H7; assumption. intros; simpl in H9; induction i as [| i Hreci]. unfold constant_D_eq, co_interval; simpl; intros; simpl in H0; rewrite H0; elim H10; clear H10; intros; unfold g'; @@ -1896,9 +1863,9 @@ Proof. 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 (Rle_dec r1 x); intro. + case (Rle_dec r1 x) as [|[]]. reflexivity. - elim n; elim H13; clear H13; intros; + elim H13; clear H13; intros; apply Rle_trans with (pos_Rl (cons r1 l) i); try assumption; change (pos_Rl (cons r1 l) 0 <= pos_Rl (cons r1 l) i); elim (RList_P6 (cons r1 l)); intros; apply H15; @@ -1954,24 +1921,22 @@ Proof. 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 (Rle_dec a b); - case (Rle_dec b c); intros; - (right; reflexivity) || (elim n; left; assumption). + rewrite H10; rewrite H4; unfold Rmin, Rmax; case (Rle_dec a b) as [|[]]; + case (Rle_dec b c) as [|[]]; + (right; reflexivity) || (left; assumption). rewrite RList_P22. - rewrite H5; unfold Rmin, Rmax; case (Rle_dec a b); case (Rle_dec a c); - intros; + rewrite H5; unfold Rmin, Rmax; case (Rle_dec a c) as [|[]]; case (Rle_dec a b) as [|[]]; [ reflexivity - | elim n; apply Rle_trans with b; left; assumption - | elim n; left; assumption - | elim n0; left; assumption ]. + | left; assumption + | apply Rle_trans with b; left; assumption + | left; assumption ]. red; intro; rewrite H1 in H6; discriminate. rewrite RList_P24. - rewrite H9; unfold Rmin, Rmax; case (Rle_dec b c); case (Rle_dec a c); - intros; + rewrite H9; unfold Rmin, Rmax; case (Rle_dec a c) as [|[]]; case (Rle_dec b c) as [|[]]; [ reflexivity - | elim n; apply Rle_trans with b; left; assumption - | elim n; left; assumption - | elim n0; left; assumption ]. + | left; assumption + | apply Rle_trans with b; left; assumption + | left; assumption ]. red; intro; rewrite H1 in H11; discriminate. apply StepFun_P20. rewrite RList_P23; apply neq_O_lt; red; intro. @@ -2061,7 +2026,7 @@ Proof. 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 (Rle_dec b c); intro; [ reflexivity | elim n; left; assumption ]. + case (Rle_dec b c) as [|[]]; [ reflexivity | left; assumption ]. rewrite H15; apply le_n. induction l1 as [| r l1 Hrecl1]. simpl in H15; discriminate. @@ -2069,8 +2034,8 @@ Proof. assert (H17 : pos_Rl (cons_Rlist l1 l2) i = b). rewrite RList_P26. replace i with (pred (Rlength l1)); - [ rewrite H4; unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; left; assumption ] + [ rewrite H4; unfold Rmax; case (Rle_dec a b) as [|[]]; + [ reflexivity | left; assumption ] | rewrite H15; reflexivity ]. rewrite H15; apply lt_n_Sn. rewrite H16 in H2; rewrite H17 in H2; elim H2; intros; @@ -2095,8 +2060,8 @@ Proof. discriminate. clear Hrecl1; induction l1 as [| r0 l1 Hrecl1]. simpl in H5; simpl in H4; assert (H0 : Rmin a b < Rmax a b). - unfold Rmin, Rmax; case (Rle_dec a b); intro; - [ assumption | elim n; left; assumption ]. + unfold Rmin, Rmax; case (Rle_dec a b) as [|[]]; + [ assumption | left; assumption ]. rewrite <- H5 in H0; rewrite <- H4 in H0; elim (Rlt_irrefl _ H0). clear Hrecl1; simpl; repeat apply le_n_S; apply le_O_n. elim (RList_P20 _ H18); intros r1 [r2 [r3 H19]]; rewrite H19; @@ -2222,9 +2187,9 @@ Proof. | left _ => Int_SF lf3 l3 | right _ => - Int_SF lf3 l3 end. - case (Rle_dec a b); case (Rle_dec b c); case (Rle_dec a c); intros. - elim r1; intro. - elim r0; intro. + case (Rle_dec a b) as [Hle|Hnle]; case (Rle_dec b c) as [Hle'|Hnle']; case (Rle_dec a c) as [Hle''|Hnle'']. + elim Hle; intro. + elim Hle'; 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). @@ -2232,8 +2197,7 @@ Proof. 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 (Rle_dec a b); case (Rle_dec b c); intros; reflexivity || elim n; - assumption. + decide (Rle_dec a b) with Hle; decide (Rle_dec b c) with Hle'; reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2; assumption @@ -2250,13 +2214,13 @@ Proof. rewrite Rplus_0_l; 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. + elim Hnle''; apply Rle_trans with b; assumption. apply Rplus_eq_reg_l 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 : c < b). auto with real. - elim r; intro. + elim Hle''; intro. rewrite Rplus_comm; replace (Int_SF lf1 l1) with (Int_SF (FF (cons_Rlist l3 l2) f) (cons_Rlist l3 l2)). @@ -2264,12 +2228,9 @@ Proof. replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). apply StepFun_P42. unfold adapted_couple in H2, H3; decompose [and] H2; decompose [and] H3; - clear H3 H2; rewrite H10; rewrite H6; unfold Rmax, Rmin; - case (Rle_dec a c); case (Rle_dec b c); intros; - [ elim n; assumption - | reflexivity - | elim n0; assumption - | elim n1; assumption ]. + clear H3 H2; rewrite H10; rewrite H6; unfold Rmax, Rmin. + decide (Rle_dec a c) with Hle''; decide (Rle_dec b c) with Hnle'; + reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. @@ -2284,7 +2245,7 @@ Proof. symmetry ; eapply StepFun_P8; [ apply H3 | assumption ]. replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1). ring. - elim r; intro. + elim Hle; intro. replace (Int_SF lf2 l2) with (Int_SF (FF (cons_Rlist l3 l1) f) (cons_Rlist l3 l1)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). @@ -2292,11 +2253,7 @@ Proof. symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H3; decompose [and] H1; decompose [and] H3; clear H3 H1; rewrite H9; rewrite H5; unfold Rmax, Rmin; - case (Rle_dec a c); case (Rle_dec a b); intros; - [ elim n; assumption - | elim n1; assumption - | reflexivity - | elim n1; assumption ]. + decide (Rle_dec a c) with Hnle''; decide (Rle_dec a b) with Hle; reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. @@ -2316,7 +2273,7 @@ Proof. auto with real. replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1). ring. - rewrite Rplus_comm; elim r; intro. + rewrite Rplus_comm; elim Hle''; intro. replace (Int_SF lf2 l2) with (Int_SF (FF (cons_Rlist l1 l3) f) (cons_Rlist l1 l3)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). @@ -2324,11 +2281,8 @@ Proof. symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H3; decompose [and] H1; decompose [and] H3; clear H3 H1; rewrite H11; rewrite H5; unfold Rmax, Rmin; - case (Rle_dec a c); case (Rle_dec a b); intros; - [ elim n; assumption - | reflexivity - | elim n0; assumption - | elim n1; assumption ]. + decide (Rle_dec a c) with Hle''; decide (Rle_dec a b) with Hnle; + reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. @@ -2346,7 +2300,7 @@ Proof. auto with real. replace (Int_SF lf1 l1) with (Int_SF lf2 l2 + Int_SF lf3 l3). ring. - elim r; intro. + elim Hle'; intro. replace (Int_SF lf1 l1) with (Int_SF (FF (cons_Rlist l2 l3) f) (cons_Rlist l2 l3)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). @@ -2354,11 +2308,8 @@ Proof. symmetry ; apply StepFun_P42. unfold adapted_couple in H2, H3; decompose [and] H2; decompose [and] H3; clear H3 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; - case (Rle_dec a c); case (Rle_dec b c); intros; - [ elim n; assumption - | elim n1; assumption - | reflexivity - | elim n1; assumption ]. + decide (Rle_dec a c) with Hnle''; decide (Rle_dec b c) with Hle'; + reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. @@ -2371,8 +2322,8 @@ Proof. replace (Int_SF lf2 l2) with 0. rewrite Rplus_0_l; eapply StepFun_P17; [ apply H3 | rewrite H0 in H1; apply H1 ]. - symmetry ; eapply StepFun_P8; [ apply H2 | assumption ]. - elim n; apply Rle_trans with a; try assumption. + symmetry; eapply StepFun_P8; [ apply H2 | assumption ]. + elim Hnle'; apply Rle_trans with a; try assumption. auto with real. assert (H : c < b). auto with real. @@ -2387,11 +2338,8 @@ Proof. symmetry ; apply StepFun_P42. unfold adapted_couple in H2, H1; decompose [and] H2; decompose [and] H1; clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; - case (Rle_dec a b); case (Rle_dec b c); intros; - [ elim n1; assumption - | elim n1; assumption - | elim n0; assumption - | reflexivity ]. + decide (Rle_dec a b) with Hnle; decide (Rle_dec b c) with Hnle'; + reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. @@ -2463,10 +2411,8 @@ Proof. replace a with (Rmin a b). pattern b at 2; replace b with (Rmax a b). rewrite <- H2; rewrite H3; reflexivity. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with H7; reflexivity. + unfold Rmin; decide (Rle_dec a b) with H7; reflexivity. 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. @@ -2475,20 +2421,18 @@ Proof. discriminate. clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}). case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ]. - elim H1; intro. + elim H1; intro a0. split with (cons r (cons c nil)); split with (cons r3 nil); unfold adapted_couple in H; decompose [and] H; clear H; assert (H6 : r = a). - simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b); intro; + simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b) as [|[]]; [ reflexivity - | elim n; elim H0; intros; apply Rle_trans with c; assumption ]. + | elim H0; intros; apply Rle_trans with c; assumption ]. elim H0; clear H0; intros; unfold adapted_couple; repeat split. rewrite H6; unfold ordered_Rlist; intros; simpl in H8; inversion H8; [ simpl; assumption | elim (le_Sn_O _ H10) ]. - simpl; unfold Rmin; case (Rle_dec a c); intro; - [ assumption | elim n; assumption ]. - simpl; unfold Rmax; case (Rle_dec a c); intro; - [ reflexivity | elim n; assumption ]. + simpl; unfold Rmin; decide (Rle_dec a c) with H; assumption. + simpl; unfold Rmax; decide (Rle_dec a c) with H; reflexivity. unfold constant_D_eq, open_interval; intros; simpl in H8; inversion H8. simpl; assert (H10 := H7 0%nat); @@ -2508,8 +2452,8 @@ Proof. assert (H14 : a <= b). elim H0; intros; apply Rle_trans with c; assumption. assert (H16 : r = a). - simpl in H7; rewrite H7; unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + simpl in H7; rewrite H7; unfold Rmin; decide (Rle_dec a b) with H14; + reflexivity. induction l1' as [| r4 l1' Hrecl1']. simpl in H13; discriminate. clear Hrecl1'; unfold adapted_couple; repeat split. @@ -2517,18 +2461,18 @@ Proof. simpl; replace r4 with r1. apply (H5 0%nat). simpl; apply lt_O_Sn. - simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c); intro; - [ reflexivity | elim n; left; assumption ]. + simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c) as [|[]]; + [ reflexivity | left; assumption ]. apply (H9 i); simpl; apply lt_S_n; assumption. - simpl; unfold Rmin; case (Rle_dec a c); intro; - [ assumption | elim n; elim H0; intros; assumption ]. + simpl; unfold Rmin; case (Rle_dec a c) as [|[]]; + [ assumption | elim H0; intros; assumption ]. replace (Rmax a c) with (Rmax r1 c). rewrite <- H11; reflexivity. - unfold Rmax; case (Rle_dec r1 c); case (Rle_dec a c); intros; - [ reflexivity - | elim n; elim H0; intros; assumption - | elim n; left; assumption - | elim n0; left; assumption ]. + unfold Rmax; case (Rle_dec a c) as [|[]]; case (Rle_dec r1 c) as [|[]]; + [ reflexivity + | left; assumption + | elim H0; intros; assumption + | left; assumption ]. simpl; simpl in H13; rewrite H13; reflexivity. intros; simpl in H; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. @@ -2539,8 +2483,8 @@ Proof. elim H4; clear H4; intros; split; try assumption; replace r1 with r4. assumption. - simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c); intro; - [ reflexivity | elim n; left; assumption ]. + simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c) as [|[]]; + [ reflexivity | left; assumption ]. clear Hreci; simpl; apply H15. simpl; apply lt_S_n; assumption. unfold open_interval; apply H4. @@ -2578,10 +2522,8 @@ Proof. replace a with (Rmin a b). pattern b at 2; replace b with (Rmax a b). rewrite <- H2; rewrite H3; reflexivity. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with H7; reflexivity. + unfold Rmin; decide (Rle_dec a b) with H7; reflexivity. 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. @@ -2590,22 +2532,22 @@ Proof. discriminate. clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}). case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ]. - elim H1; intro. + elim H1; intro a0. split with (cons c (cons r1 r2)); split with (cons r3 lf1); unfold adapted_couple in H; decompose [and] H; clear H; unfold adapted_couple; repeat split. unfold ordered_Rlist; intros; simpl in H; induction i as [| i Hreci]. simpl; assumption. clear Hreci; apply (H2 (S i)); simpl; assumption. - simpl; unfold Rmin; case (Rle_dec c b); intro; - [ reflexivity | elim n; elim H0; intros; assumption ]. + simpl; unfold Rmin; case (Rle_dec c b) as [|[]]; + [ reflexivity | elim H0; intros; assumption ]. replace (Rmax c b) with (Rmax a b). rewrite <- H3; reflexivity. - unfold Rmax; case (Rle_dec a b); case (Rle_dec c b); intros; + unfold Rmax; case (Rle_dec c b) as [|[]]; case (Rle_dec a b) as [|[]]; [ reflexivity - | elim n; elim H0; intros; assumption - | elim n; elim H0; intros; apply Rle_trans with c; assumption - | elim n0; elim H0; intros; apply Rle_trans with c; assumption ]. + | elim H0; intros; apply Rle_trans with c; assumption + | elim H0; intros; assumption + | elim H0; intros; apply Rle_trans with c; assumption ]. simpl; simpl in H5; apply H5. intros; simpl in H; induction i as [| i Hreci]. unfold constant_D_eq, open_interval; intros; simpl; @@ -2615,9 +2557,9 @@ Proof. intros; split; try assumption; apply Rle_lt_trans with c; try assumption; replace r with a. elim H0; intros; assumption. - simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b); intros; + simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b) as [|[]]; [ reflexivity - | elim n; elim H0; intros; apply Rle_trans with c; assumption ]. + | elim H0; intros; apply Rle_trans with c; assumption ]. clear Hreci; apply (H7 (S i)); simpl; assumption. cut (adapted_couple f r1 b (cons r1 r2) lf1). cut (r1 <= c <= b). |