From 99be46eb50213d1f35dfc4d30f35760ad5e75621 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 1 Aug 2014 14:39:51 +0200 Subject: More proofs independent of the names generated by induction/elim over a dependent elimination principle for Prop arguments. --- theories/Reals/MVT.v | 47 +++++++++++++++++++++--------------------- theories/Reals/RiemannInt_SF.v | 5 ++--- 2 files changed, 26 insertions(+), 26 deletions(-) (limited to 'theories/Reals') diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index 4b8d9af48..e3c5298d7 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -151,14 +151,14 @@ Proof. cut (forall c:R, a <= c <= b -> continuity_pt id c); [ intro | intros; apply derivable_continuous_pt; apply derivable_id ]. assert (H2 := MVT f id a b X X0 H H0 H1). - elim H2; intros c H3; elim H3; intros. + destruct H2 as (c & P & H4). exists c; split. - cut (derive_pt id c (X0 c x) = derive_pt id c (derivable_pt_id c)); - [ intro | apply pr_nu ]. + cut (derive_pt id c (X0 c P) = derive_pt id c (derivable_pt_id c)); + [ intro H5 | apply pr_nu ]. rewrite H5 in H4; rewrite (derive_pt_id c) in H4; rewrite Rmult_1_r in H4; - rewrite <- H4; replace (derive_pt f c (X c x)) with (derive_pt f c (pr c)); + rewrite <- H4; replace (derive_pt f c (X c P)) with (derive_pt f c (pr c)); [ idtac | apply pr_nu ]; apply Rmult_comm. - apply x. + apply P. Qed. Theorem MVT_cor2 : @@ -173,14 +173,14 @@ Proof. intro; cut (forall c:R, a <= c <= b -> derivable_pt id c). intro X1; cut (forall c:R, a < c < b -> derivable_pt id c). intro X2; cut (forall c:R, a <= c <= b -> continuity_pt id c). - intro; elim (MVT f id a b X0 X2 H H1 H2); intros; elim H3; clear H3; intros; - exists x; split. - cut (derive_pt id x (X2 x x0) = 1). - cut (derive_pt f x (X0 x x0) = f' x). + intro; elim (MVT f id a b X0 X2 H H1 H2); intros x (P,H3). + exists x; split. + cut (derive_pt id x (X2 x P) = 1). + cut (derive_pt f x (X0 x P) = f' x). intros; rewrite H4 in H3; rewrite H5 in H3; unfold id in H3; rewrite Rmult_1_r in H3; rewrite Rmult_comm; symmetry ; assumption. - apply derive_pt_eq_0; apply H0; elim x0; intros; split; left; assumption. + apply derive_pt_eq_0; apply H0; elim P; intros; split; left; assumption. apply derive_pt_eq_0; apply derivable_pt_lim_id. assumption. intros; apply derivable_continuous_pt; apply X1; assumption. @@ -217,12 +217,12 @@ Proof. assert (H3 := MVT f id a b pr H2 H0 H); assert (H4 : forall x:R, a <= x <= b -> continuity_pt id x). intros; apply derivable_continuous; apply derivable_id. - elim (H3 H4); intros; elim H5; intros; exists x; exists x0; rewrite H1 in H6; - unfold id in H6; unfold Rminus in H6; rewrite Rplus_opp_r in H6; - rewrite Rmult_0_l in H6; apply Rmult_eq_reg_l with (b - a); - [ rewrite Rmult_0_r; apply H6 - | apply Rminus_eq_contra; red; intro; rewrite H7 in H0; - elim (Rlt_irrefl _ H0) ]. + destruct (H3 H4) as (c & P & H6). exists c; exists P; rewrite H1 in H6. + unfold id in H6; unfold Rminus in H6; rewrite Rplus_opp_r in H6. + rewrite Rmult_0_l in H6; apply Rmult_eq_reg_l with (b - a); + [ rewrite Rmult_0_r; apply H6 + | apply Rminus_eq_contra; red; intro H7; rewrite H7 in H0; + elim (Rlt_irrefl _ H0) ]. Qed. (**********) @@ -655,14 +655,15 @@ Proof. elim H1; intros; apply Rle_trans with x; assumption. elim H1; clear H1; intros; elim H1; clear H1; intro. assert (H7 := MVT f id a x H4 H2 H1 H5 H3). - elim H7; intros; elim H8; intros; assert (H10 : a < x0 < b). - elim x1; intros; split. - assumption. - apply Rlt_le_trans with x; assumption. - assert (H11 : derive_pt f x0 (H4 x0 x1) = 0). - replace (derive_pt f x0 (H4 x0 x1)) with (derive_pt f x0 (pr x0 H10)); + destruct H7 as (c & P & H9). + assert (H10 : a < c < b). + split. + apply P. + apply Rlt_le_trans with x; [apply P|assumption]. + assert (H11 : derive_pt f c (H4 c P) = 0). + replace (derive_pt f c (H4 c P)) with (derive_pt f c (pr c H10)); [ apply H0 | apply pr_nu ]. - assert (H12 : derive_pt id x0 (H2 x0 x1) = 1). + assert (H12 : derive_pt id c (H2 c P) = 1). apply derive_pt_eq_0; apply derivable_pt_lim_id. rewrite H11 in H9; rewrite H12 in H9; rewrite Rmult_0_r in H9; rewrite Rmult_1_r in H9; apply Rminus_diag_uniq; symmetry ; diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index ef5d37bff..f98b1a143 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -943,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; -- cgit v1.2.3