diff options
Diffstat (limited to 'theories/Reals/Ranalysis5.v')
| -rw-r--r-- | theories/Reals/Ranalysis5.v | 87 |
1 files changed, 36 insertions, 51 deletions
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index d172139f..afb78e1c 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Rbase. @@ -15,6 +17,7 @@ Require Import RiemannInt. Require Import SeqProp. Require Import Max. Require Import Omega. +Require Import Lra. Local Open Scope R_scope. (** * Preliminaries lemmas *) @@ -26,46 +29,34 @@ Lemma f_incr_implies_g_incr_interv : forall f g:R->R, forall lb ub, (forall x , f lb <= x -> x <= f ub -> lb <= g x <= ub) -> (forall x y, f lb <= x -> x < y -> y <= f ub -> g x < g y). Proof. -intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub. - assert (x_encad : f lb <= x <= f ub). - split ; [assumption | apply Rle_trans with (r2:=y) ; [apply Rlt_le|] ; assumption]. - assert (y_encad : f lb <= y <= f ub). - split ; [apply Rle_trans with (r2:=x) ; [|apply Rlt_le] ; assumption | assumption]. - assert (Temp1 : lb <= lb) by intuition ; assert (Temp2 : ub <= ub) by intuition. - assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)). - assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)). - clear Temp1 Temp2. - case (Rlt_dec (g x) (g y)). - intuition. + intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub. + assert (x_encad : f lb <= x <= f ub) by lra. + assert (y_encad : f lb <= y <= f ub) by lra. + assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)). + assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)). + case (Rlt_dec (g x) (g y)); [ easy |]. intros Hfalse. - assert (Temp := Rnot_lt_le _ _ Hfalse). - assert (Hcontradiction : y <= x). - replace y with (id y) by intuition ; replace x with (id x) by intuition ; - rewrite <- f_eq_g. rewrite <- f_eq_g. - assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y). + assert (Temp := Rnot_lt_le _ _ Hfalse). + enough (y <= x) by lra. + replace y with (id y) by easy. + replace x with (id x) by easy. + rewrite <- f_eq_g by easy. + rewrite <- f_eq_g by easy. + assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y). { intros m n lb_le_m m_le_n n_lt_ub. case (m_le_n). - intros ; apply Rlt_le ; apply f_incr ; [| | apply Rlt_le] ; assumption. - intros Hyp ; rewrite Hyp ; apply Req_le ; reflexivity. - apply f_incr2. - intuition. intuition. - Focus 3. intuition. - Focus 2. intuition. - Focus 2. intuition. Focus 2. intuition. - assert (Temp2 : g x <> ub). - intro Hf. - assert (Htemp : (comp f g) x = f ub). - unfold comp ; rewrite Hf ; reflexivity. - rewrite f_eq_g in Htemp ; unfold id in Htemp. - assert (Htemp2 : x < f ub). - apply Rlt_le_trans with (r2:=y) ; intuition. - clear -Htemp Htemp2. fourier. - intuition. intuition. - clear -Temp2 gx_encad. - case (proj2 gx_encad). - intuition. - intro Hfalse ; apply False_ind ; apply Temp2 ; assumption. - apply False_ind. clear - Hcontradiction x_lt_y. fourier. + - intros; apply Rlt_le, f_incr, Rlt_le; assumption. + - intros Hyp; rewrite Hyp; apply Req_le; reflexivity. + } + apply f_incr2; intuition. + enough (g x <> ub) by lra. + intro Hf. + assert (Htemp : (comp f g) x = f ub). { + unfold comp; rewrite Hf; reflexivity. + } + rewrite f_eq_g in Htemp by easy. + unfold id in Htemp. + fourier. Qed. Lemma derivable_pt_id_interv : forall (lb ub x:R), @@ -245,12 +236,8 @@ Lemma IVT_interv_prelim0 : forall (x y:R) (P:R->bool) (N:nat), x <= Dichotomy_ub x y P N <= y /\ x <= Dichotomy_lb x y P N <= y. Proof. assert (Sublemma : forall x y lb ub, lb <= x <= ub /\ lb <= y <= ub -> lb <= (x+y) / 2 <= ub). - intros x y lb ub Hyp. - split. - replace lb with ((lb + lb) * /2) by field. - unfold Rdiv ; apply Rmult_le_compat_r ; intuition. - replace ub with ((ub + ub) * /2) by field. - unfold Rdiv ; apply Rmult_le_compat_r ; intuition. + intros x y lb ub Hyp. + lra. intros x y P N x_lt_y. induction N. simpl ; intuition. @@ -1027,9 +1014,7 @@ Qed. Lemma ub_lt_2_pos : forall x ub lb, lb < x -> x < ub -> 0 < (ub-lb)/2. Proof. intros x ub lb lb_lt_x x_lt_ub. - assert (T : 0 < ub - lb). - fourier. - unfold Rdiv ; apply Rlt_mult_inv_pos ; intuition. +lra. Qed. Definition mkposreal_lb_ub (x lb ub:R) (lb_lt_x:lb<x) (x_lt_ub:x<ub) : posreal. @@ -1102,7 +1087,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn rewrite <- Rmult_1_r ; replace 1 with (derive_pt id c (pr2 c P)) by reg. replace (- (fn N (x + h) - fn N x)) with (fn N x - fn N (x + h)) by field. assumption. - solve[apply Rlt_not_eq ; intuition]. + now apply Rlt_not_eq, IZR_lt. rewrite <- Hc'; clear Hc Hc'. replace (derive_pt (fn N) c (pr1 c P)) with (fn' N c). replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by field. |