diff options
Diffstat (limited to 'contrib/fourier')
| -rw-r--r-- | contrib/fourier/Fourier.v | 7 | ||||
| -rw-r--r-- | contrib/fourier/Fourier_util.v | 406 |
2 files changed, 198 insertions, 215 deletions
diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v index b02688de63..d550927599 100644 --- a/contrib/fourier/Fourier.v +++ b/contrib/fourier/Fourier.v @@ -20,9 +20,6 @@ Require Export Fourier_util. Require Export Field. Require Export DiscrR. -Tactic Definition Fourier := - Abstract (FourierZ;Field;DiscrR). - -Tactic Definition FourierEq := - Apply Rge_ge_eq ; Fourier. +Ltac fourier := abstract (fourierz; field; discrR). +Ltac fourier_eq := apply Rge_antisym; fourier. diff --git a/contrib/fourier/Fourier_util.v b/contrib/fourier/Fourier_util.v index 0f36eda8cb..dcc45b66e4 100644 --- a/contrib/fourier/Fourier_util.v +++ b/contrib/fourier/Fourier_util.v @@ -13,229 +13,215 @@ Comments "Lemmas used by the tactic Fourier". Open Scope R_scope. -Lemma Rfourier_lt: - (x1, y1, a : R) (Rlt x1 y1) -> (Rlt R0 a) -> (Rlt (Rmult a x1) (Rmult a y1)). -Intros; Apply Rlt_monotony; Assumption. -Qed. - -Lemma Rfourier_le: - (x1, y1, a : R) (Rle x1 y1) -> (Rlt R0 a) -> (Rle (Rmult a x1) (Rmult a y1)). -Red. -Intros. -Case H; Auto with real. -Qed. - -Lemma Rfourier_lt_lt: - (x1, y1, x2, y2, a : R) - (Rlt x1 y1) -> - (Rlt x2 y2) -> - (Rlt R0 a) -> (Rlt (Rplus x1 (Rmult a x2)) (Rplus y1 (Rmult a y2))). -Intros x1 y1 x2 y2 a H H0 H1; Try Assumption. -Apply Rplus_lt. -Try Exact H. -Apply Rfourier_lt. -Try Exact H0. -Try Exact H1. -Qed. - -Lemma Rfourier_lt_le: - (x1, y1, x2, y2, a : R) - (Rlt x1 y1) -> - (Rle x2 y2) -> - (Rlt R0 a) -> (Rlt (Rplus x1 (Rmult a x2)) (Rplus y1 (Rmult a y2))). -Intros x1 y1 x2 y2 a H H0 H1; Try Assumption. -Case H0; Intros. -Apply Rplus_lt. -Try Exact H. -Apply Rfourier_lt; Auto with real. -Rewrite H2. -Rewrite (Rplus_sym y1 (Rmult a y2)). -Rewrite (Rplus_sym x1 (Rmult a y2)). -Apply Rlt_compatibility. -Try Exact H. -Qed. - -Lemma Rfourier_le_lt: - (x1, y1, x2, y2, a : R) - (Rle x1 y1) -> - (Rlt x2 y2) -> - (Rlt R0 a) -> (Rlt (Rplus x1 (Rmult a x2)) (Rplus y1 (Rmult a y2))). -Intros x1 y1 x2 y2 a H H0 H1; Try Assumption. -Case H; Intros. -Apply Rfourier_lt_le; Auto with real. -Rewrite H2. -Apply Rlt_compatibility. -Apply Rfourier_lt; Auto with real. -Qed. - -Lemma Rfourier_le_le: - (x1, y1, x2, y2, a : R) - (Rle x1 y1) -> - (Rle x2 y2) -> - (Rlt R0 a) -> (Rle (Rplus x1 (Rmult a x2)) (Rplus y1 (Rmult a y2))). -Intros x1 y1 x2 y2 a H H0 H1; Try Assumption. -Case H0; Intros. -Red. -Left; Try Assumption. -Apply Rfourier_le_lt; Auto with real. -Rewrite H2. -Case H; Intros. -Red. -Left; Try Assumption. -Rewrite (Rplus_sym x1 (Rmult a y2)). -Rewrite (Rplus_sym y1 (Rmult a y2)). -Apply Rlt_compatibility. -Try Exact H3. -Rewrite H3. -Red. -Right; Try Assumption. -Auto with real. -Qed. - -Lemma Rlt_zero_pos_plus1: (x : R) (Rlt R0 x) -> (Rlt R0 (Rplus R1 x)). -Intros x H; Try Assumption. -Rewrite Rplus_sym. -Apply Rlt_r_plus_R1. -Red; Auto with real. -Qed. - -Lemma Rlt_mult_inv_pos: - (x, y : R) (Rlt R0 x) -> (Rlt R0 y) -> (Rlt R0 (Rmult x (Rinv y))). -Intros x y H H0; Try Assumption. -Replace R0 with (Rmult x R0). -Apply Rlt_monotony; Auto with real. -Ring. -Qed. - -Lemma Rlt_zero_1: (Rlt R0 R1). -Exact Rlt_R0_R1. -Qed. - -Lemma Rle_zero_pos_plus1: (x : R) (Rle R0 x) -> (Rle R0 (Rplus R1 x)). -Intros x H; Try Assumption. -Case H; Intros. -Red. -Left; Try Assumption. -Apply Rlt_zero_pos_plus1; Auto with real. -Rewrite <- H0. -Replace (Rplus R1 R0) with R1. -Red; Left. -Exact Rlt_zero_1. -Ring. -Qed. - -Lemma Rle_mult_inv_pos: - (x, y : R) (Rle R0 x) -> (Rlt R0 y) -> (Rle R0 (Rmult x (Rinv y))). -Intros x y H H0; Try Assumption. -Case H; Intros. -Red; Left. -Apply Rlt_mult_inv_pos; Auto with real. -Rewrite <- H1. -Red; Right; Ring. -Qed. - -Lemma Rle_zero_1: (Rle R0 R1). -Red; Left. -Exact Rlt_zero_1. -Qed. - -Lemma Rle_not_lt: - (n, d : R) (Rle R0 (Rmult n (Rinv d))) -> ~ (Rlt R0 (Rmult (Ropp n) (Rinv d))). -Intros n d H; Red; Intros H0; Try Exact H0. -Generalize (Rle_not R0 (Rmult n (Rinv d))). -Intros H1; Elim H1; Try Assumption. -Replace (Rmult n (Rinv d)) with (Ropp (Ropp (Rmult n (Rinv d)))). -Replace R0 with (Ropp (Ropp R0)). -Replace (Ropp (Rmult n (Rinv d))) with (Rmult (Ropp n) (Rinv d)). -Replace (Ropp R0) with R0. -Red. -Try Exact H0. -Apply Rgt_Ropp. -Replace (Ropp (Rmult n (Rinv d))) with (Rmult (Ropp n) (Rinv d)). -Replace (Ropp R0) with R0. -Red. -Try Exact H0. -Ring. -Ring. -Ring. -Ring. -Ring. -Ring. -Qed. - -Lemma Rnot_lt0: (x : R) ~ (Rlt R0 (Rmult R0 x)). -Intros x; Try Assumption. -Replace (Rmult R0 x) with R0. -Apply Rlt_antirefl. -Ring. -Qed. - -Lemma Rlt_not_le: - (n, d : R) (Rlt R0 (Rmult n (Rinv d))) -> ~ (Rle R0 (Rmult (Ropp n) (Rinv d))). -Intros n d H; Try Assumption. -Apply Rle_not. -Replace R0 with (Ropp R0). -Replace (Rmult (Ropp n) (Rinv d)) with (Ropp (Rmult n (Rinv d))). -Apply Rlt_Ropp. -Try Exact H. -Ring. -Ring. +Lemma Rfourier_lt : forall x1 y1 a:R, x1 < y1 -> 0 < a -> a * x1 < a * y1. +intros; apply Rmult_lt_compat_l; assumption. +Qed. + +Lemma Rfourier_le : forall x1 y1 a:R, x1 <= y1 -> 0 < a -> a * x1 <= a * y1. +red in |- *. +intros. +case H; auto with real. +Qed. + +Lemma Rfourier_lt_lt : + forall x1 y1 x2 y2 a:R, + x1 < y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. +intros x1 y1 x2 y2 a H H0 H1; try assumption. +apply Rplus_lt_compat. +try exact H. +apply Rfourier_lt. +try exact H0. +try exact H1. +Qed. + +Lemma Rfourier_lt_le : + forall x1 y1 x2 y2 a:R, + x1 < y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. +intros x1 y1 x2 y2 a H H0 H1; try assumption. +case H0; intros. +apply Rplus_lt_compat. +try exact H. +apply Rfourier_lt; auto with real. +rewrite H2. +rewrite (Rplus_comm y1 (a * y2)). +rewrite (Rplus_comm x1 (a * y2)). +apply Rplus_lt_compat_l. +try exact H. +Qed. + +Lemma Rfourier_le_lt : + forall x1 y1 x2 y2 a:R, + x1 <= y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. +intros x1 y1 x2 y2 a H H0 H1; try assumption. +case H; intros. +apply Rfourier_lt_le; auto with real. +rewrite H2. +apply Rplus_lt_compat_l. +apply Rfourier_lt; auto with real. +Qed. + +Lemma Rfourier_le_le : + forall x1 y1 x2 y2 a:R, + x1 <= y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 <= y1 + a * y2. +intros x1 y1 x2 y2 a H H0 H1; try assumption. +case H0; intros. +red in |- *. +left; try assumption. +apply Rfourier_le_lt; auto with real. +rewrite H2. +case H; intros. +red in |- *. +left; try assumption. +rewrite (Rplus_comm x1 (a * y2)). +rewrite (Rplus_comm y1 (a * y2)). +apply Rplus_lt_compat_l. +try exact H3. +rewrite H3. +red in |- *. +right; try assumption. +auto with real. +Qed. + +Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x. +intros x H; try assumption. +rewrite Rplus_comm. +apply Rle_lt_0_plus_1. +red in |- *; auto with real. +Qed. + +Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. +intros x y H H0; try assumption. +replace 0 with (x * 0). +apply Rmult_lt_compat_l; auto with real. +ring. +Qed. + +Lemma Rlt_zero_1 : 0 < 1. +exact Rlt_0_1. +Qed. + +Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x. +intros x H; try assumption. +case H; intros. +red in |- *. +left; try assumption. +apply Rlt_zero_pos_plus1; auto with real. +rewrite <- H0. +replace (1 + 0) with 1. +red in |- *; left. +exact Rlt_zero_1. +ring. +Qed. + +Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. +intros x y H H0; try assumption. +case H; intros. +red in |- *; left. +apply Rlt_mult_inv_pos; auto with real. +rewrite <- H1. +red in |- *; right; ring. +Qed. + +Lemma Rle_zero_1 : 0 <= 1. +red in |- *; left. +exact Rlt_zero_1. +Qed. + +Lemma Rle_not_lt : forall n d:R, 0 <= n * / d -> ~ 0 < - n * / d. +intros n d H; red in |- *; intros H0; try exact H0. +generalize (Rgt_not_le 0 (n * / d)). +intros H1; elim H1; try assumption. +replace (n * / d) with (- - (n * / d)). +replace 0 with (- -0). +replace (- (n * / d)) with (- n * / d). +replace (-0) with 0. +red in |- *. +try exact H0. +apply Ropp_gt_lt_contravar. +replace (- (n * / d)) with (- n * / d). +replace (-0) with 0. +red in |- *. +try exact H0. +ring. +ring. +ring. +ring. +ring. +ring. +Qed. + +Lemma Rnot_lt0 : forall x:R, ~ 0 < 0 * x. +intros x; try assumption. +replace (0 * x) with 0. +apply Rlt_irrefl. +ring. +Qed. + +Lemma Rlt_not_le : forall n d:R, 0 < n * / d -> ~ 0 <= - n * / d. +intros n d H; try assumption. +apply Rgt_not_le. +replace 0 with (-0). +replace (- n * / d) with (- (n * / d)). +apply Ropp_lt_gt_contravar. +try exact H. +ring. +ring. +Qed. + +Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y. +unfold not in |- *; intros. +apply H. +apply Rplus_lt_reg_r with x. +replace (x + 0) with x. +replace (x + (y - x)) with y. +try exact H0. +ring. +ring. Qed. -Lemma Rnot_lt_lt: (x, y : R) ~ (Rlt R0 (Rminus y x)) -> ~ (Rlt x y). -Unfold not; Intros. -Apply H. -Apply Rlt_anti_compatibility with x. -Replace (Rplus x R0) with x. -Replace (Rplus x (Rminus y x)) with y. -Try Exact H0. -Ring. -Ring. +Lemma Rnot_le_le : forall x y:R, ~ 0 <= y - x -> ~ x <= y. +unfold not in |- *; intros. +apply H. +case H0; intros. +left. +apply Rplus_lt_reg_r with x. +replace (x + 0) with x. +replace (x + (y - x)) with y. +try exact H1. +ring. +ring. +right. +rewrite H1; ring. Qed. -Lemma Rnot_le_le: (x, y : R) ~ (Rle R0 (Rminus y x)) -> ~ (Rle x y). -Unfold not; Intros. -Apply H. -Case H0; Intros. -Left. -Apply Rlt_anti_compatibility with x. -Replace (Rplus x R0) with x. -Replace (Rplus x (Rminus y x)) with y. -Try Exact H1. -Ring. -Ring. -Right. -Rewrite H1; Ring. +Lemma Rfourier_gt_to_lt : forall x y:R, y > x -> x < y. +unfold Rgt in |- *; intros; assumption. Qed. -Lemma Rfourier_gt_to_lt: (x, y : R) (Rgt y x) -> (Rlt x y). -Unfold Rgt; Intros; Assumption. -Qed. - -Lemma Rfourier_ge_to_le: (x, y : R) (Rge y x) -> (Rle x y). -Intros x y; Exact (Rge_le y x). -Qed. - -Lemma Rfourier_eqLR_to_le: (x, y : R) x == y -> (Rle x y). -Exact eq_Rle. +Lemma Rfourier_ge_to_le : forall x y:R, y >= x -> x <= y. +intros x y; exact (Rge_le y x). +Qed. + +Lemma Rfourier_eqLR_to_le : forall x y:R, x = y -> x <= y. +exact Req_le. Qed. -Lemma Rfourier_eqRL_to_le: (x, y : R) y == x -> (Rle x y). -Exact eq_Rle_sym. +Lemma Rfourier_eqRL_to_le : forall x y:R, y = x -> x <= y. +exact Req_le_sym. Qed. -Lemma Rfourier_not_ge_lt: (x, y : R) ((Rge x y) -> False) -> (Rlt x y). -Exact not_Rge. +Lemma Rfourier_not_ge_lt : forall x y:R, (x >= y -> False) -> x < y. +exact Rnot_ge_lt. Qed. -Lemma Rfourier_not_gt_le: (x, y : R) ((Rgt x y) -> False) -> (Rle x y). -Exact Rgt_not_le. +Lemma Rfourier_not_gt_le : forall x y:R, (x > y -> False) -> x <= y. +exact Rnot_gt_le. Qed. -Lemma Rfourier_not_le_gt: (x, y : R) ((Rle x y) -> False) -> (Rgt x y). -Exact not_Rle. +Lemma Rfourier_not_le_gt : forall x y:R, (x <= y -> False) -> x > y. +exact Rnot_le_lt. Qed. -Lemma Rfourier_not_lt_ge: (x, y : R) ((Rlt x y) -> False) -> (Rge x y). -Exact Rlt_not_ge. -Qed. +Lemma Rfourier_not_lt_ge : forall x y:R, (x < y -> False) -> x >= y. +exact Rnot_lt_ge. +Qed.
\ No newline at end of file |